refactor(data/set/pairwise): use {{..}} arguments (#17230)

Author: urkud

archive/100-theorems-list/82_cubing_a_cube.lean

@@ -158,7 +158,7 @@ begin
     { rw [←add_le_add_iff_right (1 : ℝ)], convert b_add_w_le_one h, rw hi, rw zero_add },
     apply zero_le_b h, apply lt_of_lt_of_le (side_subset h $ (cs i').b_mem_side j).2,
     simp [hi, zero_le_b h] },
-  exact h.pairwise_disjoint i' i hi' ⟨hp, h2p⟩
+  exact h.pairwise_disjoint hi' ⟨hp, h2p⟩
 end
 
 /-- The top of a cube (which is the bottom of the cube shifted up by its width) must be covered by
@@ -176,7 +176,7 @@ begin
   rw [← h.2, mem_Union] at this, rcases this with ⟨i', hi'⟩,
   rw [mem_Union], use i', refine ⟨_, λ j, hi' j.succ⟩,
   have : i ≠ i', { rintro rfl, apply not_le_of_lt (hi' 0).2, rw [hp0], refl },
-  have := h.1 i i' this, rw [on_fun, to_set_disjoint, exists_fin_succ] at this,
+  have := h.1 this, rw [on_fun, to_set_disjoint, exists_fin_succ] at this,
   rcases this with h0|⟨j, hj⟩,
   rw [hp0], symmetry, apply eq_of_Ico_disjoint h0 (by simp [hw]) _,
   convert hi' 0, rw [hp0], refl,
@@ -395,9 +395,9 @@ begin
       intro j₂, by_cases hj₂ : j₂ = j,
       { simpa [side_tail, p', hj'.symm, hj₂] using hi''.2 j },
       { simpa [hj₂] using hi'.2 j₂ } },
-    apply not_disjoint_iff.mpr ⟨(cs i).b, (cs i).b_mem_to_set, this⟩ (h.1 i i' i_i') },
+    apply not_disjoint_iff.mpr ⟨(cs i).b, (cs i).b_mem_to_set, this⟩ (h.1 i_i') },
   have i_i'' : i ≠ i'', { intro h, induction h, simpa [hx'.2] using hi''.2 j' },
-  apply not.elim _ (h.1 i' i'' i'_i''),
+  apply not.elim _ (h.1 i'_i''),
   simp only [on_fun, to_set_disjoint, not_disjoint_iff, forall_fin_succ, not_exists, comp_app],
   refine ⟨⟨c.b 0, bottom_mem_side h2i', bottom_mem_side h2i''⟩, _⟩,
   intro j₂,

src/algebra/big_operators/finprod.lean

@@ -792,7 +792,7 @@ begin
   rw [← bUnion_univ, ← finset.coe_univ, ← finset.coe_bUnion,
     finprod_mem_coe_finset, finset.prod_bUnion],
   { simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype] },
-  { exact λ x _ y _ hxy, finset.disjoint_coe.1 (h x y hxy) }
+  { exact λ x _ y _ hxy, finset.disjoint_coe.1 (h hxy) }
 end
 
 /-- Given a family of sets `t : ι → set α`, a finite set `I` in the index type such that all sets

src/algebra/direct_sum/module.lean

@@ -315,7 +315,7 @@ the two submodules are complementary. Over a `ring R`, this is true as an iff, a
 `direct_sum.is_internal_iff_is_compl`. --/
 lemma is_internal.is_compl {A : ι → submodule R M} {i j : ι} (hij : i ≠ j)
   (h : (set.univ : set ι) = {i, j}) (hi : is_internal A) : is_compl (A i) (A j) :=
-⟨hi.submodule_independent.pairwise_disjoint _ _ hij, eq.le $ hi.submodule_supr_eq_top.symm.trans $
+⟨hi.submodule_independent.pairwise_disjoint hij, eq.le $ hi.submodule_supr_eq_top.symm.trans $
   by rw [←Sup_pair, supr, ←set.image_univ, h, set.image_insert_eq, set.image_singleton]⟩
 
 end semiring

src/algebra/group/pi.lean

@@ -320,7 +320,7 @@ lemma pi.mul_single_apply_commute [Π i, mul_one_class $ f i] (x : Π i, f i) (i
 begin
   obtain rfl | hij := decidable.eq_or_ne i j,
   { refl },
-  { exact pi.mul_single_commute _ _ hij _ _, },
+  { exact pi.mul_single_commute hij _ _, },
 end
 
 @[to_additive update_eq_sub_add_single]

src/data/finset/basic.lean

@@ -2902,11 +2902,7 @@ variables {s : finset α}
 
 lemma pairwise_subtype_iff_pairwise_finset' (r : β → β → Prop) (f : α → β) :
   pairwise (r on λ x : s, f x) ↔ (s : set α).pairwise (r on f) :=
-begin
-  refine ⟨λ h x hx y hy hxy, h ⟨x, hx⟩ ⟨y, hy⟩ (by simpa only [subtype.mk_eq_mk, ne.def]), _⟩,
-  rintros h ⟨x, hx⟩ ⟨y, hy⟩ hxy,
-  exact h hx hy (subtype.mk_eq_mk.not.mp hxy)
-end
+pairwise_subtype_iff_pairwise_set (s : set α) (r on f)
 
 lemma pairwise_subtype_iff_pairwise_finset (r : α → α → Prop) :
   pairwise (r on λ x : s, x) ↔ (s : set α).pairwise r :=

src/data/mv_polynomial/variables.lean

@@ -387,7 +387,7 @@ begin
     intros v hv v2 hv2,
     rw finset.mem_bUnion at hv2,
     rcases hv2 with ⟨i, his, hi⟩,
-    refine h a i _ _ hv _ hi,
+    refine h _ _ hv _ hi,
     rintro rfl,
     contradiction }
 end

src/data/polynomial/ring_division.lean

@@ -818,7 +818,7 @@ begin
   rw [prod_multiset_root_eq_finset_root, polynomial.map_prod],
   refine finset.prod_dvd_of_coprime (λ a _ b _ h, _) (λ a _, _),
   { simp_rw [polynomial.map_pow, polynomial.map_sub, map_C, map_X],
-    exact (pairwise_coprime_X_sub_C (is_fraction_ring.injective R $ fraction_ring R) _ _ h).pow },
+    exact (pairwise_coprime_X_sub_C (is_fraction_ring.injective R $ fraction_ring R) h).pow },
   { exact polynomial.map_dvd _ (pow_root_multiplicity_dvd p a) },
 end
 

src/data/set/pairwise.lean

@@ -32,12 +32,12 @@ section pairwise
 variables {f g : ι → α} {s t u : set α} {a b : α}
 
 /-- A relation `r` holds pairwise if `r i j` for all `i ≠ j`. -/
-def pairwise (r : α → α → Prop) := ∀ i j, i ≠ j → r i j
+def pairwise (r : α → α → Prop) := ∀ ⦃i j⦄, i ≠ j → r i j
 
 lemma pairwise.mono (hr : pairwise r) (h : ∀ ⦃i j⦄, r i j → p i j) : pairwise p :=
-λ i j hij, h $ hr i j hij
+λ i j hij, h $ hr hij
 
-protected lemma pairwise.eq (h : pairwise r) : ¬ r a b → a = b := not_imp_comm.1 $ h _ _
+protected lemma pairwise.eq (h : pairwise r) : ¬ r a b → a = b := not_imp_comm.1 $ @h _ _
 
 lemma pairwise_on_bool (hr : symmetric r) {a b : α} : pairwise (r on (λ c, cond c a b)) ↔ r a b :=
 by simpa [pairwise, function.on_fun] using @hr a b
@@ -47,15 +47,11 @@ lemma pairwise_disjoint_on_bool [semilattice_inf α] [order_bot α] {a b : α} :
 pairwise_on_bool disjoint.symm
 
 lemma symmetric.pairwise_on [linear_order ι] (hr : symmetric r) (f : ι → α) :
-  pairwise (r on f) ↔ ∀ m n, m < n → r (f m) (f n) :=
-⟨λ h m n hmn, h m n hmn.ne, λ h m n hmn, begin
-  obtain hmn' | hmn' := hmn.lt_or_lt,
-  { exact h _ _ hmn' },
-  { exact hr (h _ _ hmn') }
-end⟩
+  pairwise (r on f) ↔ ∀ ⦃m n⦄, m < n → r (f m) (f n) :=
+⟨λ h m n hmn, h hmn.ne, λ h m n hmn, hmn.lt_or_lt.elim (@h _ _) (λ h', hr (h h'))⟩
 
 lemma pairwise_disjoint_on [semilattice_inf α] [order_bot α] [linear_order ι] (f : ι → α) :
-  pairwise (disjoint on f) ↔ ∀ m n, m < n → disjoint (f m) (f n) :=
+  pairwise (disjoint on f) ↔ ∀ ⦃m n⦄, m < n → disjoint (f m) (f n) :=
 symmetric.pairwise_on disjoint.symm f
 
 lemma pairwise_disjoint.mono [semilattice_inf α] [order_bot α]
@@ -223,20 +219,13 @@ by { rw [sUnion_eq_Union, pairwise_Union (h.directed_coe), set_coe.forall], refl
 
 end set
 
-lemma pairwise.set_pairwise (h : pairwise r) (s : set α) : s.pairwise r := λ x hx y hy, h x y
+lemma pairwise.set_pairwise (h : pairwise r) (s : set α) : s.pairwise r := λ x hx y hy hxy, h hxy
 
 end pairwise
 
-lemma pairwise_subtype_iff_pairwise_set {α : Type*} (s : set α) (r : α → α → Prop) :
+lemma pairwise_subtype_iff_pairwise_set (s : set α) (r : α → α → Prop) :
   pairwise (λ (x : s) (y : s), r x y) ↔ s.pairwise r :=
-begin
-  split,
-  { assume h x hx y hy hxy,
-    exact h ⟨x, hx⟩ ⟨y, hy⟩ (by simpa only [subtype.mk_eq_mk, ne.def]) },
-  { rintros h ⟨x, hx⟩ ⟨y, hy⟩ hxy,
-    simp only [subtype.mk_eq_mk, ne.def] at hxy,
-    exact h hx hy hxy }
-end
+by simp only [pairwise, set.pairwise, set_coe.forall, ne.def, subtype.ext_iff, subtype.coe_mk]
 
 alias pairwise_subtype_iff_pairwise_set ↔ pairwise.set_of_subtype set.pairwise.subtype
 

src/field_theory/separable.lean

@@ -168,7 +168,7 @@ end
 
 lemma separable_prod {ι : Sort*} [fintype ι] {f : ι → R[X]}
   (h1 : pairwise (is_coprime on f)) (h2 : ∀ x, (f x).separable) : (∏ x, f x).separable :=
-separable_prod' (λ x hx y hy hxy, h1 x y hxy) (λ x hx, h2 x)
+separable_prod' (λ x hx y hy hxy, h1 hxy) (λ x hx, h2 x)
 
 lemma separable.inj_of_prod_X_sub_C [nontrivial R] {ι : Sort*} {f : ι → R} {s : finset ι}
   (hfs : (∏ i in s, (X - C (f i))).separable)

src/group_theory/free_product.lean

@@ -591,7 +591,7 @@ lemma lift_word_ping_pong {i j k} (w : neword H i j) (hk : j ≠ k) :
 begin
   rename [i → i', j → j', k → m, hk → hm],
   induction w with i x hne_one i j k l w₁ hne w₂  hIw₁ hIw₂ generalizing m; clear i' j',
-  { simpa using hpp _ _ hm _ hne_one, },
+  { simpa using hpp hm _ hne_one, },
   { calc lift f (neword.append w₁ hne w₂).prod • X m
         = lift f w₁.prod • lift f w₂.prod • X m : by simp [mul_action.mul_smul]
     ... ⊆ lift f w₁.prod • X k : set_smul_subset_set_smul_iff.mpr (hIw₂ hm)
@@ -607,7 +607,7 @@ begin
   have : X k ⊆ X i,
     by simpa [heq1] using lift_word_ping_pong f X hpp w hlast.symm,
   obtain ⟨x, hx⟩ := hXnonempty k,
-  exact hXdisj k i hhead ⟨hx, this hx⟩,
+  exact hXdisj hhead ⟨hx, this hx⟩,
 end
 
 include hnontriv
@@ -796,10 +796,10 @@ begin
   { intros i j hij,
     simp only [X'],
     apply disjoint.union_left; apply disjoint.union_right,
-    { exact hXdisj i j hij, },
+    { exact hXdisj hij, },
     { exact hXYdisj i j, },
     { exact (hXYdisj j i).symm, },
-    { exact hYdisj i j hij, }, },
+    { exact hYdisj hij, }, },
 
   show pairwise (λ i j, ∀ h : H i, h ≠ 1 → f i h • X' j ⊆ X' i),
   { rintros i j hij,
@@ -816,7 +816,7 @@ begin
     cases (lt_or_gt_of_ne hnne0).swap with hlt hgt,
     { have h1n : 1 ≤ n := hlt,
       calc a i ^ n • X' j ⊆ a i ^ n • (Y i)ᶜ : smul_set_mono
-            ((hXYdisj j i).union_left $ hYdisj j i hij.symm).subset_compl_right
+            ((hXYdisj j i).union_left $ hYdisj hij.symm).subset_compl_right
       ... ⊆ X i :
       begin
         refine int.le_induction _ _ _ h1n,
@@ -832,7 +832,7 @@ begin
       ... ⊆ X' i : set.subset_union_left _ _, },
     { have h1n : n ≤ -1, { apply int.le_of_lt_add_one, simpa using hgt, },
       calc a i ^ n • X' j ⊆ a i ^ n • (X i)ᶜ : smul_set_mono
-            ((hXdisj j i hij.symm).union_left (hXYdisj i j).symm).subset_compl_right
+            ((hXdisj hij.symm).union_left (hXYdisj i j).symm).subset_compl_right
       ... ⊆ Y i :
       begin
         refine int.le_induction_down _ _ _ h1n,