Shorten List.pairwise statements

src/Std/Data/DHashMap/Internal/List/Associative.lean

@@ -175,7 +175,7 @@ theorem getValueCast?_cons_self [BEq α] [LawfulBEq α] {l : List ((a : α) × 
 theorem getValueCast?_of_mem [BEq α] [LawfulBEq α]
     {l : List ((a : α) × β a)}
     {k : α} (k' : α ) (v : β k) (k_beq : k == k') (mem : ⟨k, v⟩ ∈ l)
-    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) l) :
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
     getValueCast? k' l = some (cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v) := by
   induction l with
   | nil => simp at mem
@@ -928,7 +928,7 @@ theorem DistinctKeys.nil [BEq α] : DistinctKeys ([] : List ((a : α) × β a))
   ⟨by simp⟩
 
 theorem DistinctKeys.def [BEq α] {l : List ((a : α) × β a)} :
-    DistinctKeys l ↔ List.Pairwise (fun a b => (a.1 == b.1) = false) l :=
+    DistinctKeys l ↔ l.Pairwise (fun a b => (a.1 == b.1) = false) :=
   ⟨fun h => by simpa [keys_eq_map, List.pairwise_map] using h.distinct,
   fun h => ⟨by simpa [keys_eq_map, List.pairwise_map] using h⟩⟩
 
@@ -2218,7 +2218,7 @@ theorem getKeyD_insertList_of_mem [BEq α] [EquivBEq α]
 theorem perm_insertList [BEq α] [ReflBEq α] [PartialEquivBEq α]
     {l toInsert : List ((a : α) × β a)}
     (distinct_l : DistinctKeys l)
-    (distinct_toInsert : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert)
+    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
     (distinct_both : ∀ (a : α), ¬ (containsKey a l ∧ containsKey a toInsert)) :
     Perm (insertList l toInsert) (l ++ toInsert) := by
   rw [← DistinctKeys.def] at distinct_toInsert
@@ -2263,7 +2263,7 @@ theorem perm_insertList [BEq α] [ReflBEq α] [PartialEquivBEq α]
 theorem length_insertList [BEq α] [EquivBEq α]
     {l toInsert : List ((a : α) × β a)}
     (distinct_l : DistinctKeys l)
-    (distinct_toInsert : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert)
+    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
     (distinct_both : ∀ (a : α), ¬ (containsKey a l ∧ (toInsert.map Sigma.fst).contains a)) :
     (insertList l toInsert).length = l.length + toInsert.length := by
   rw [← DistinctKeys.def] at distinct_toInsert
@@ -2350,7 +2350,7 @@ theorem getValue?_insertList_of_contains_eq_false [BEq α] [PartialEquivBEq α]
 theorem getValue?_insertList_of_mem [BEq α] [PartialEquivBEq α]
     {l toInsert : List ((_ : α) × β )}
     {k k' : α} (k_beq : k == k') {v : β}
-    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert)
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : ⟨k, v⟩ ∈ toInsert) :
     getValue? k' (insertList l toInsert) = v := by
   induction toInsert generalizing l with
@@ -2394,7 +2394,7 @@ theorem getValue!_insertList_of_contains_eq_false [BEq α] [PartialEquivBEq α]
 
 theorem getValue!_insertList_of_mem [BEq α] [PartialEquivBEq α] [Inhabited β]
     {l toInsert : List ((_ : α) × β)} {k k' : α} {v: β} (k_beq : k == k')
-    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert):
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ toInsert):
     getValue! k' (insertList l toInsert) = v := by
   simp only [getValue!_eq_getValue?]
   rw [getValue?_insertList_of_mem (mem:= mem)]
@@ -2412,7 +2412,7 @@ theorem getValueD_insertList_of_contains_eq_false [BEq α] [PartialEquivBEq α]
 
 theorem getValueD_insertList_of_mem [BEq α] [PartialEquivBEq α]
     {l toInsert : List ((_ : α) × β)} {k k' : α} {v fallback: β} (k_beq : k == k')
-    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert):
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ toInsert):
     getValueD k' (insertList l toInsert) fallback= v := by
   simp only [getValueD_eq_getValue?]
   rw [getValue?_insertList_of_mem (mem:= mem)]
@@ -2627,7 +2627,7 @@ theorem getKeyD_insertListConst_of_mem [BEq α] [EquivBEq α]
 theorem length_insertListConst [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)}
     (distinct_l : DistinctKeys l)
-    (distinct_toInsert : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert)
+    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
     (distinct_both : ∀ (a : α), ¬ (containsKey a l ∧ (toInsert.map Prod.fst).contains a)) :
     (insertListConst l toInsert).length = l.length + toInsert.length := by
   rw [insertListConst_eq_insertList]
@@ -2677,7 +2677,7 @@ theorem getValue?_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq
 theorem getValue?_insertListConst_of_mem [BEq α] [PartialEquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)}
     {k k' : α} (k_beq : k == k') {v : β}
-    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert)
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : ⟨k, v⟩ ∈ toInsert) :
     getValue? k' (insertListConst l toInsert) = v := by
   rw [insertListConst_eq_insertList]
@@ -2698,7 +2698,7 @@ theorem getValue!_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq
 
 theorem getValue!_insertListConst_of_mem [BEq α] [PartialEquivBEq α] [Inhabited β]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v: β} (k_beq : k == k')
-    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert):
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ toInsert):
     getValue! k' (insertListConst l toInsert) = v := by
   rw [insertListConst_eq_insertList, getValue!_insertList_of_mem (k_beq:=k_beq)]
   · apply pairwise_list_conversion_insertListConst distinct
@@ -2716,7 +2716,7 @@ theorem getValueD_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq
 
 theorem getValueD_insertListConst_of_mem [BEq α] [PartialEquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v fallback: β} (k_beq : k == k')
-    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert):
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ toInsert):
     getValueD k' (insertListConst l toInsert) fallback= v := by
   rw [insertListConst_eq_insertList, getValueD_insertList_of_mem (k_beq:= k_beq)]
   · apply pairwise_list_conversion_insertListConst distinct
@@ -3034,7 +3034,7 @@ theorem getKeyD_insertListIfNewUnit_of_mem_of_contains [BEq α] [EquivBEq α]
 theorem length_insertListIfNewUnit [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
     (distinct_l : DistinctKeys l)
-    (distinct_toInsert : List.Pairwise (fun a b => (a == b) = false) toInsert)
+    (distinct_toInsert : toInsert.Pairwise (fun a b => (a == b) = false))
     (distinct_both : ∀ (a : α), ¬ (containsKey a l ∧ toInsert.contains a)) :
     (insertListIfNewUnit l toInsert).length = l.length + toInsert.length := by
   induction toInsert generalizing l with

src/Std/Data/DHashMap/Internal/RawLemmas.lean

@@ -1009,7 +1009,7 @@ theorem get?_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHas
 
 theorem get?_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List ((_ : α) × β)} {k k' : α} (k_beq : k == k') {v : β} (mem : ⟨k, v⟩ ∈ l)
-    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) :
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false )) :
     Const.get? (m.insertMany l).1 k' = v := by
   simp_to_model using getValue?_insertList_of_mem
 
@@ -1022,7 +1022,7 @@ theorem get_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHash
 
 theorem get_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List ((_ : α) × β)} {k k' : α} (k_beq : k == k') {v : β} (mem : ⟨k, v⟩ ∈ l)
-    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) {h'}:
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false )) {h'}:
     Const.get (m.insertMany l).1 k' h' = v := by
   simp_to_model using getValue_insertList_of_mem
 
@@ -1034,7 +1034,7 @@ theorem get!_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHas
 
 theorem get!_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF)
     {l : List ((_ : α) × β)} {k k' : α} (k_beq : k == k') {v : β} (mem: ⟨k, v⟩ ∈ l)
-    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) :
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false )) :
     Const.get! (m.insertMany l).1 k' = v := by
   simp_to_model using getValue!_insertList_of_mem
 
@@ -1046,7 +1046,7 @@ theorem getD_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHas
 
 theorem getD_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List ((_ : α) × β)} {k k' : α} (k_beq : k == k') {v fallback: β} (mem: ⟨k, v⟩ ∈ l)
-    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) :
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false )) :
     Const.getD (m.insertMany l).1 k' fallback = v := by
   simp_to_model using getValueD_insertList_of_mem
 
@@ -1139,14 +1139,14 @@ theorem getKeyD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.
 
 theorem size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)}
-    {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) l} :
+    {distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)} :
     (∀ (a : α), ¬ (m.contains a ∧ (l.map Prod.fst).contains a)) →
     (insertMany m l).1.1.size = m.1.size + l.length := by
   simp_to_model using length_insertListConst
 
 theorem isEmpty_insertMany_list_eq_false_of_isEmpty_eq_false [EquivBEq α] [LawfulHashable α]
     (h : m.1.WF) {l : List (α × β)} :
-    (m.1.isEmpty = false) → (insertMany m l).1.1.isEmpty  = false := by
+    (m.1.isEmpty = false) → (insertMany m l).1.1.isEmpty = false := by
   simp_to_model using isEmpty_insertListConst_eq_false_of_isEmpty_eq_false
 
 theorem isEmpty_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
@@ -1162,7 +1162,7 @@ theorem get?_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable
 
 theorem get?_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} (mem: ⟨k, v⟩ ∈ l)
-    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) :
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false )) :
     get? (insertMany m l).1 k' = v := by
   simp_to_model using getValue?_insertListConst_of_mem
 
@@ -1175,7 +1175,7 @@ theorem get_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable 
 
 theorem get_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} (mem: ⟨k, v⟩ ∈ l)
-    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) {h'}:
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false )) {h'}:
     get (insertMany m l).1 k' h' = v := by
   simp_to_model using getValue_insertListConst_of_mem
 
@@ -1187,7 +1187,7 @@ theorem get!_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHas
 
 theorem get!_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF)
     {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} (mem: ⟨k, v⟩ ∈ l)
-    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) :
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false )) :
     get! (insertMany m l).1 k' = v := by
   simp_to_model using getValue!_insertListConst_of_mem
 
@@ -1199,7 +1199,7 @@ theorem getD_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHas
 
 theorem getD_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k k' : α} (k_beq : k == k') {v fallback: β} (mem: ⟨k, v⟩ ∈ l)
-    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) :
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false )) :
     getD (insertMany m l).1 k' fallback = v := by
   simp_to_model using getValueD_insertListConst_of_mem
 
@@ -1261,7 +1261,7 @@ theorem getKey_insertManyIfNewUnit_list_of_mem_of_contains_eq_false [EquivBEq α
     {k k' : α} (k_beq : k == k')
     (distinct : l.Pairwise (fun a b => (a == b) = false))
     (mem : k ∈ l) {h'} :
-    m.contains k  = false →
+    m.contains k = false →
     getKey (insertManyIfNewUnit m l).1 k' h' = k := by
   simp_to_model using getKey_insertListIfNewUnit_of_mem_of_contains_eq_false
 
@@ -1314,7 +1314,7 @@ theorem getKeyD_insertManyIfNewUnit_list_of_mem_of_contains [EquivBEq α] [Lawfu
 
 theorem size_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List α}
-    (distinct : List.Pairwise (fun a b => (a == b) = false) l):
+    (distinct : l.Pairwise (fun a b => (a == b) = false)):
     (∀ (a : α), ¬ (m.contains a ∧ l.contains a)) →
     (insertManyIfNewUnit m l).1.1.size = m.1.size + l.length := by
   simp_to_model using length_insertListIfNewUnit