Bump mathlib

LeanCamCombi/Kneser/Kneser.lean

@@ -49,7 +49,7 @@ lemma mulStab_mul_ssubset_mulStab (hs₁ : (s ∩ a • C.mulStab).Nonempty)
     have hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) := mul_mem_mul hx hy
     apply subset_trans (mulStab_subset_div_right hxymem)
     have : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (x * y) • C.mulStab := by
-      apply subset_trans (mul_subset_mul (inter_subset_right s _) (inter_subset_right t _))
+      apply subset_trans (mul_subset_mul inter_subset_right inter_subset_right)
       rw [smul_mul_smul]
       rw [← hac, ← had, smul_mul_smul, smul_assoc]
       apply smul_finset_subset_smul_finset
@@ -67,7 +67,7 @@ lemma mulStab_mul_ssubset_mulStab (hs₁ : (s ∩ a • C.mulStab).Nonempty)
       mul_assoc, ← mul_assoc, mul_assoc _ a b, inv_mul_self (a * b), one_mul, ← smul_eq_mul,
       smul_assoc, smul_mulStab hc, smul_mulStab hd]
   have hsub : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * b) • C.mulStab := by
-    apply subset_trans (mul_subset_mul (inter_subset_right s _) (inter_subset_right t _))
+    apply subset_trans (mul_subset_mul inter_subset_right inter_subset_right)
     simp only [smul_mul_smul, mulStab_mul_mulStab, subset_refl]
   have hxy : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) := mul_mem_mul hx hy
   rw [this] at hsub
@@ -79,7 +79,7 @@ lemma mulStab_mul_ssubset_mulStab (hs₁ : (s ∩ a • C.mulStab).Nonempty)
   push_neg
   refine' ⟨a * c * (b * d), by convert hxy, _⟩
   rw [smul_eq_mul, mul_comm, ← smul_eq_mul, hwz]
-  exact not_mem_mono (mul_subset_mul (inter_subset_left s _) (inter_subset_left t _)) hzst
+  exact not_mem_mono (mul_subset_mul inter_subset_left inter_subset_left) hzst
 
 @[to_additive]
 lemma mulStab_union (hs₁ : (s ∩ a • C.mulStab).Nonempty) (ht₁ : (t ∩ b • C.mulStab).Nonempty)
@@ -93,7 +93,7 @@ lemma mulStab_union (hs₁ : (s ∩ a • C.mulStab).Nonempty) (ht₁ : (t ∩ b
     ((subset_inter (mulStab_mul_ssubset_mulStab hs₁ ht₁ hab).subset Subset.rfl).trans
           inter_mulStab_subset_mulStab_union).antisymm'
       fun x hx => _
-  replace hx := (mem_mulStab $ (hs₁.mul ht₁).mono $ subset_union_right _ _).mp hx
+  replace hx := (mem_mulStab $ (hs₁.mul ht₁).mono subset_union_right).mp hx
   rw [smul_finset_union] at hx
   suffices hxC : x ∈ C.mulStab by
     rw [(mem_mulStab hCne).mp hxC] at hx
@@ -119,16 +119,16 @@ lemma mulStab_union (hs₁ : (s ∩ a • C.mulStab).Nonempty) (ht₁ : (t ∩ b
     rw [mul_mulStab] at hxyC
     exact hyne.not_disjoint (hC.mono_left $ le_iff_subset.2 hxyC)
   have hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) :=
-    hxyC.left_le_of_le_sup_left (hxyCsubC.trans $ (subset_union_left _ _).trans hx.subset')
+    hxyC.left_le_of_le_sup_left (hxyCsubC.trans $ subset_union_left.trans hx.subset')
   suffices s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab by
     have := (card_le_card hxysub).not_lt ((card_lt_card this).trans_eq ?_)
     cases this
     simp_rw [card_smul_finset]
   apply ssubset_of_subset_not_subset
-  · refine' (mul_subset_mul (inter_subset_right _ _) (inter_subset_right _ _)).trans _
+  · refine' (mul_subset_mul inter_subset_right inter_subset_right).trans _
     simp only [smul_mul_smul, mulStab_mul_mulStab, subset_refl]
   · contrapose! hab
-    exact hab.trans (mul_subset_mul (inter_subset_left _ _) (inter_subset_left _ _))
+    exact hab.trans (mul_subset_mul inter_subset_left inter_subset_left)
 
 @[to_additive]
 lemma mul_aux1
@@ -184,12 +184,12 @@ lemma disjoint_mul_sub_card_le {a : α} (b : α) {s t C : Finset α} (has : a 
             (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)).card := by
       rw [card_sdiff
           (subset_trans (mul_subset_mul_left hst)
-            (subset_trans (mul_subset_mul_right (inter_subset_right s _)) _)),
+            (subset_trans (mul_subset_mul_right inter_subset_right) _)),
         card_smul_finset, Int.ofNat_sub]
       · apply le_trans (card_le_card (mul_subset_mul_left hst))
         apply
           le_trans (card_le_card inter_mul_subset)
-            (le_of_le_of_eq (card_le_card (inter_subset_right _ _)) _)
+            (le_of_le_of_eq (card_le_card inter_subset_right) _)
         rw [smul_mul_assoc, mulStab_mul_mulStab, card_smul_finset]
       · simp only [smul_mul_assoc, mulStab_mul_mulStab, Subset.rfl]
     _ ≤ ((s ∪ t) * C.mulStab).card -
@@ -241,7 +241,7 @@ lemma inter_mul_sub_card_le {a : α} {s t C : Finset α} (has : a ∈ s)
       all_goals
         apply subset_trans (mul_subset_mul_left hst)
         rw [← union_inter_distrib_right]
-        refine' subset_trans (mul_subset_mul_right (inter_subset_right _ _)) _
+        refine' subset_trans (mul_subset_mul_right inter_subset_right) _
         simp only [smul_mul_assoc, mulStab_mul_mulStab, Subset.rfl]
     _ ≤
         ((s ∪ t) * C.mulStab).card -
@@ -352,13 +352,13 @@ theorem mul_kneser :
   simp only [mul_smul_comm, smul_mul_assoc, mulStab_smul, card_smul_finset] at *
   have hst : (s ∩ t).Nonempty := ⟨_, mem_inter.2 ⟨ha, hc⟩⟩
   have hsts : s ∩ t ⊂ s :=
-    ⟨inter_subset_left _ _, not_subset.2 ⟨_, hb, fun h => hbac $ inter_subset_right _ _ h⟩⟩
+    ⟨inter_subset_left, not_subset.2 ⟨_, hb, fun h => hbac $ inter_subset_right h⟩⟩
   clear! a b
   set convergent : Set (Finset α) :=
     {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card}
   have convergent_nonempty : convergent.Nonempty := by
     refine' ⟨s ∩ t * (s ∪ t), inter_mul_union_subset, (add_le_add_right (card_le_card $
-      subset_mul_left _ $ one_mem_mulStab.2 $ hst.mul $ hs.mono $ subset_union_left _ _) _).trans $
+      subset_mul_left _ $ one_mem_mulStab.2 $ hst.mul $ hs.mono subset_union_left) _).trans $
         ih (s ∩ t) (s ∪ t) _⟩
     exact add_lt_add_of_le_of_lt (card_le_card inter_mul_union_subset) (card_lt_card hsts)
   let C := argminOn (fun C : Finset α => C.mulStab.card) IsWellFounded.wf _ convergent_nonempty
@@ -385,10 +385,10 @@ theorem mul_kneser :
   set s₂ := s ∩ b • H with hs₂
   set t₁ := t ∩ b • H with ht₁
   set t₂ := t ∩ a • H with ht₂
-  have hs₁s : s₁ ⊆ s := inter_subset_left _ _
-  have hs₂s : s₂ ⊆ s := inter_subset_left _ _
-  have ht₁t : t₁ ⊆ t := inter_subset_left _ _
-  have ht₂t : t₂ ⊆ t := inter_subset_left _ _
+  have hs₁s : s₁ ⊆ s := inter_subset_left
+  have hs₂s : s₂ ⊆ s := inter_subset_left
+  have ht₁t : t₁ ⊆ t := inter_subset_left
+  have ht₂t : t₂ ⊆ t := inter_subset_left
   have has₁ : a ∈ s₁ := mem_inter.mpr ⟨ha, mem_smul_finset.2 ⟨1, one_mem_mulStab.2 hC, mul_one _⟩⟩
   have hbt₁ : b ∈ t₁ := mem_inter.mpr ⟨hb, mem_smul_finset.2 ⟨1, one_mem_mulStab.2 hC, mul_one _⟩⟩
   have hs₁ne : s₁.Nonempty := ⟨_, has₁⟩
@@ -401,10 +401,10 @@ theorem mul_kneser :
   have hC₂st : C₂ ⊆ s * t := union_subset hCst (mul_subset_mul hs₂s ht₂t)
   have hstabH₁ : s₁ * t₁ ⊆ (a * b) • H := by
     rw [hH, ← mulStab_mul_mulStab C, ← smul_mul_smul]
-    apply mul_subset_mul (inter_subset_right _ _) (inter_subset_right _ _)
+    apply mul_subset_mul inter_subset_right inter_subset_right
   have hstabH₂ : s₂ * t₂ ⊆ (a * b) • H := by
     rw [hH, ← mulStab_mul_mulStab C, ← smul_mul_smul, mul_comm s₂ t₂]
-    apply mul_subset_mul (inter_subset_right _ _) (inter_subset_right _ _)
+    apply mul_subset_mul inter_subset_right inter_subset_right
   have hCst₁ := disjoint_of_subset_right hstabH₁ (disjoint_smul_mulStab hCst hab)
   have hCst₂ := disjoint_of_subset_right hstabH₂ (disjoint_smul_mulStab hCst hab)
   have hst₁ : (s₁ * t₁).card + s₁.card < (s * t).card + s.card :=
@@ -461,8 +461,8 @@ theorem mul_kneser :
     conv_lhs => rw [← card_union_of_disjoint hST, ← card_union_of_disjoint hSTst, ← mul_one (s ∪ t)]
     refine' card_le_card
       (union_subset (union_subset _ _) $ mul_subset_mul_left $ one_subset.2 hC.one_mem_mulStab)
-    · exact hSst.trans ((sdiff_subset _ _).trans $ smul_finset_subset_smul $ mem_union_left _ ha)
-    · exact hTst.trans ((sdiff_subset _ _).trans $ smul_finset_subset_smul $ mem_union_right _ hb)
+    · exact hSst.trans (sdiff_subset.trans $ smul_finset_subset_smul $ mem_union_left _ ha)
+    · exact hTst.trans (sdiff_subset.trans $ smul_finset_subset_smul $ mem_union_right _ hb)
   have hH₁ne : H₁.Nonempty := (hs₁ne.mul ht₁ne).mulStab
   have hH₂ne : H₂.Nonempty := (hs₂ne.mul ht₂ne).mulStab
   -- Now we prove inequality (2)

LeanCamCombi/Kneser/KneserRuzsa.lean

@@ -238,11 +238,11 @@ lemma le_card_mul_add_card_mulStab_mul (hs : s.Nonempty) (ht : t.Nonempty) :
   rw [← mul_smul]
   refine'
     smul_finset_subset_iff.2
-      (inter_eq_left.1 $ eq_of_subset_of_card_le (inter_subset_left _ _) _)
+      (inter_eq_left.1 $ eq_of_subset_of_card_le inter_subset_left _)
   rw [← ht']
   refine'
     Nat.find_min' _
-      ⟨_, _, mem_inter.2 ⟨hbt' _, _⟩, (hs' _).trans $ subset_union_left _ _,
+      ⟨_, _, mem_inter.2 ⟨hbt' _, _⟩, (hs' _).trans subset_union_left,
         (mulDysonETransform.subset _ (s' b, t' b)).trans $ hst' _,
         (mulDysonETransform.card _ _).trans $ hstcard _, rfl⟩
   rwa [mem_inv_smul_finset_iff, smul_eq_mul, inv_mul_cancel_right]

LeanCamCombi/Kneser/Mathlib.lean

@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mantas Bakšys, Yaël Dillies
 -/
 import Mathlib.Algebra.CharP.Basic
-import Mathlib.Algebra.Group.Subgroup.Basic
-import Mathlib.Data.Finset.Pointwise
+import Mathlib.GroupTheory.Coset
 
 /-!
 # For mathlib

LeanCamCombi/Kneser/MulStab.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mantas Bakšys, Yaël Dillies
 -/
 import Mathlib.Algebra.Pointwise.Stabilizer
+import Mathlib.GroupTheory.GroupAction.Quotient
 import LeanCamCombi.Kneser.Mathlib
 import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup
 
@@ -146,7 +147,7 @@ lemma inter_mulStab_subset_mulStab_union : s.mulStab ∩ t.mulStab ⊆ (s ∪ t)
   obtain rfl | ht := t.eq_empty_or_nonempty
   · simp
   intro x hx
-  rw [mem_mulStab (Finset.Nonempty.mono (subset_union_left s t) hs), smul_finset_union,
+  rw [mem_mulStab (hs.mono subset_union_left), smul_finset_union,
     (mem_mulStab hs).mp (mem_of_mem_inter_left hx),
     (mem_mulStab ht).mp (mem_of_mem_inter_right hx)]
 
@@ -269,7 +270,15 @@ lemma card_mulStab_dvd_card_mulStab (hs : s.Nonempty) (h : s.mulStab ⊆ t.mulSt
   rw [← coe_subset, coe_mulStab hs, coe_mulStab ht, SetLike.coe_subset_coe] at h
   letI : Fintype (stabilizer α s) := fintypeStabilizerOfMulStab hs
   letI : Fintype (stabilizer α t) := fintypeStabilizerOfMulStab ht
-  convert Subgroup.card_dvd_of_le h using 1 <;> exact ((card_map _).trans card_attach).symm
+  convert Subgroup.card_dvd_of_le h using 1
+  simp [-mem_stabilizer_iff]
+  change _ = (s.mulStab.attach.map
+    ⟨Subtype.map id fun _ ↦ (mem_mulStab hs).1, Subtype.map_injective _ injective_id⟩).card
+  simp
+  simp [-mem_stabilizer_iff]
+  change _ = (t.mulStab.attach.map
+    ⟨Subtype.map id fun _ ↦ (mem_mulStab ht).1, Subtype.map_injective _ injective_id⟩).card
+  simp
 
 /-- A version of Lagrange's theorem. -/
 @[to_additive "A version of Lagrange's theorem."]

LeanCamCombi/KruskalKatona.lean

@@ -107,7 +107,7 @@ lemma shadow_initSeg [Fintype α] (hs : s.Nonempty) :
   have hjk : j ≤ k := min'_le _ _ (mem_compl.2 ‹k ∉ t›)
   have : j ∉ t := mem_compl.1 (min'_mem _ _)
   have hcard : card s = card (insert j t) := by
-    rw [card_insert_of_not_mem ‹j ∉ t›, ←‹_ = card t›, card_erase_add_one (min'_mem _ _)]
+    rw [card_insert_of_not_mem ‹j ∉ t›, ← ‹_ = card t›, card_erase_add_one (min'_mem _ _)]
   refine' ⟨j, ‹_›, hcard, _⟩
   -- Cases on j < k or j = k
   obtain hjk | r₁ := hjk.lt_or_eq
@@ -125,7 +125,7 @@ lemma shadow_initSeg [Fintype α] (hs : s.Nonempty) :
     apply min'_le _ _ (mem_of_mem_erase ‹_›)
   · rw [r₁]; apply mem_insert_self
   · apply mem_insert_of_mem
-    rw [←r₁] at gt
+    rw [← r₁] at gt
     by_contra
     apply (min'_le tᶜ _ _).not_lt gt
     rwa [mem_compl]
@@ -134,14 +134,14 @@ lemma shadow_initSeg [Fintype α] (hs : s.Nonempty) :
 protected lemma IsInitSeg.shadow [Finite α] (h₁ : IsInitSeg 𝒜 r) : IsInitSeg (∂ 𝒜) (r - 1) := by
   cases nonempty_fintype α
   obtain rfl | hr := Nat.eq_zero_or_pos r
-  · have : 𝒜 ⊆ {∅} := fun s hs ↦ by rw [mem_singleton, ←Finset.card_eq_zero]; exact h₁.1 hs
+  · have : 𝒜 ⊆ {∅} := fun s hs ↦ by rw [mem_singleton, ← Finset.card_eq_zero]; exact h₁.1 hs
     have := shadow_monotone this
     simp only [subset_empty, le_eq_subset, shadow_singleton_empty] at this
     simp [this]
   obtain rfl | h𝒜 := 𝒜.eq_empty_or_nonempty
   · simp
   obtain ⟨s, rfl, rfl⟩ := h₁.exists_initSeg h𝒜
-  rw [shadow_initSeg (card_pos.1 hr), ←card_erase_of_mem (min'_mem _ _)]
+  rw [shadow_initSeg (card_pos.1 hr), ← card_erase_of_mem (min'_mem _ _)]
   exact isInitSeg_initSeg
 
 end Colex
@@ -180,19 +180,19 @@ lemma compression_improved (𝒜 : Finset (Finset α)) (h₁ : UsefulCompression
   obtain ⟨UVd, same_size, hU, hV, max_lt⟩ := h₁
   refine' card_shadow_compression_le _ _ fun x Hx ↦ ⟨min' V hV, min'_mem _ _, _⟩
   obtain hU' | hU' := eq_or_lt_of_le (succ_le_iff.2 hU.card_pos)
-  · rw [←hU'] at same_size
-    have : erase U x = ∅ := by rw [←Finset.card_eq_zero, card_erase_of_mem Hx, ←hU']
+  · rw [← hU'] at same_size
+    have : erase U x = ∅ := by rw [← Finset.card_eq_zero, card_erase_of_mem Hx, ← hU']
     have : erase V (min' V hV) = ∅ := by
-      rw [←Finset.card_eq_zero, card_erase_of_mem (min'_mem _ _), ←same_size]
+      rw [← Finset.card_eq_zero, card_erase_of_mem (min'_mem _ _), ← same_size]
     rw [‹erase U x = ∅›, ‹erase V (min' V hV) = ∅›]
     exact isCompressed_self _ _
   refine' h₂ ⟨UVd.mono (erase_subset _ _) (erase_subset _ _), _, _, _, _⟩ (card_erase_lt_of_mem Hx)
   · rw [card_erase_of_mem (min'_mem _ _), card_erase_of_mem Hx, same_size]
-  · rwa [←card_pos, card_erase_of_mem Hx, tsub_pos_iff_lt]
-  · rwa [←Finset.card_pos, card_erase_of_mem (min'_mem _ _), ←same_size, tsub_pos_iff_lt]
+  · rwa [← card_pos, card_erase_of_mem Hx, tsub_pos_iff_lt]
+  · rwa [← Finset.card_pos, card_erase_of_mem (min'_mem _ _), ← same_size, tsub_pos_iff_lt]
   · refine' (Finset.max'_subset _ $ erase_subset _ _).trans_lt (max_lt.trans_le $
       le_max' _ _ $ mem_erase.2 ⟨(min'_lt_max'_of_card _ _).ne', max'_mem _ _⟩)
-    rwa [←same_size]
+    rwa [← same_size]
 
 /-- If we're compressed by all useful compressions, then we're an initial segment. This is the other
 key Kruskal-Katona part. -/
@@ -206,15 +206,15 @@ lemma isInitSeg_of_compressed {ℬ : Finset (Finset α)} {r : ℕ} (h₁ : (ℬ
   have hU : (A \ B).Nonempty := sdiff_nonempty.2 fun h ↦ hAB $ eq_of_subset_of_card_le h hAB'.ge
   have hV : (B \ A).Nonempty :=
     sdiff_nonempty.2 fun h ↦ hAB.symm $ eq_of_subset_of_card_le h hAB'.le
-  have disj : Disjoint (B \ A) (A \ B) := disjoint_sdiff.mono_left (sdiff_subset _ _)
+  have disj : Disjoint (B \ A) (A \ B) := disjoint_sdiff.mono_left sdiff_subset
   have smaller : max' _ hV < max' _ hU := by
     obtain hlt | heq | hgt := lt_trichotomy (max' _ hU) (max' _ hV)
-    · rw [←compress_sdiff_sdiff A B] at hAB hBA
+    · rw [← compress_sdiff_sdiff A B] at hAB hBA
       cases hBA.not_lt $ toColex_compress_lt_toColex hlt hAB
     · exact (disjoint_right.1 disj (max'_mem _ hU) $ heq.symm ▸ max'_mem _ _).elim
     · assumption
   refine' hB _
-  rw [←(h₂ _ _ ⟨disj, card_sdiff_comm hAB'.symm, hV, hU, smaller⟩).eq]
+  rw [← (h₂ _ _ ⟨disj, card_sdiff_comm hAB'.symm, hV, hU, smaller⟩).eq]
   exact mem_compression.2 (Or.inr ⟨hB, A, hA, compress_sdiff_sdiff _ _⟩)
 
 attribute [-instance] Fintype.decidableForallFintype
@@ -246,11 +246,11 @@ lemma familyMeasure_compression_lt_familyMeasure {U V : Finset (Fin n)} {hU : U.
     rw [filter_image, z, image_empty, union_empty]
     rwa [z, union_empty] at uA
   rw [familyMeasure, familyMeasure, sum_union compress_disjoint]
-  conv_rhs => rw [←uA]
+  conv_rhs => rw [← uA]
   rw [sum_union (disjoint_filter_filter_neg _ _ _), add_lt_add_iff_left, filter_image,
     sum_image compress_injOn]
   refine' sum_lt_sum_of_nonempty ne₂ fun A hA ↦ _
-  simp_rw [←sum_image (Fin.val_injective.injOn _)]
+  simp_rw [← sum_image Fin.val_injective.injOn]
   rw [geomSum_lt_geomSum_iff_toColex_lt_toColex le_rfl,
     toColex_image_lt_toColex_image Fin.val_strictMono]
   exact toColex_compress_lt_toColex h $ q _ hA
@@ -359,7 +359,7 @@ lemma lovasz_form (hir : i ≤ r) (hrk : r ≤ k) (hkn : k ≤ n)
     simp_rw [mem_image]
     rintro _ ⟨a, ha, q⟩
     rw [mem_powersetCard] at hA
-    rw [←q, ←mem_range]
+    rw [← q, ← mem_range]
     have := hA.1 ha
     rwa [mem_attachFin] at this
   suffices ∂^[i] 𝒞 = powersetCard (r - i) range'k by
@@ -371,15 +371,15 @@ lemma lovasz_form (hir : i ≤ r) (hrk : r ≤ k) (hkn : k ≤ n)
     rw [mem_powersetCard] at Ah
     refine' ⟨BsubA.trans Ah.1, _⟩
     symm
-    rw [Nat.sub_eq_iff_eq_add hir, ←Ah.2, ←card_sdiff_i, ←card_union_of_disjoint disjoint_sdiff,
+    rw [Nat.sub_eq_iff_eq_add hir, ← Ah.2, ← card_sdiff_i, ← card_union_of_disjoint disjoint_sdiff,
       union_sdiff_of_subset BsubA]
   rintro ⟨hBk, hB⟩
   have := exists_intermediate_set i ?_ hBk
   obtain ⟨C, BsubC, hCrange, hcard⟩ := this
-  rw [hB, ←Nat.add_sub_assoc hir, Nat.add_sub_cancel_left] at hcard
+  rw [hB, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left] at hcard
   refine' ⟨C, _, BsubC, _⟩; rw [mem_powersetCard]; exact ⟨hCrange, hcard⟩
   · rw [card_sdiff BsubC, hcard, hB, Nat.sub_sub_self hir]
-  · rwa [hB, card_attachFin, card_range, ←Nat.add_sub_assoc hir, Nat.add_sub_cancel_left]
+  · rwa [hB, card_attachFin, card_range, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left]
 
 end KK
 
@@ -393,7 +393,7 @@ lemma EKR {𝒜 : Finset (Finset (Fin n))} {r : ℕ} (h𝒜 : (𝒜 : Set (Finse
   · convert Nat.zero_le _
     rw [Finset.card_eq_zero, eq_empty_iff_forall_not_mem]
     refine' fun A HA ↦ h𝒜 HA HA _
-    rw [disjoint_self_iff_empty, ←Finset.card_eq_zero, ←b]
+    rw [disjoint_self_iff_empty, ← Finset.card_eq_zero, ← b]
     exact h₂ HA
   refine' le_of_not_lt fun size ↦ _
   -- Consider 𝒜ᶜˢ = {sᶜ | s ∈ 𝒜}
@@ -418,7 +418,7 @@ lemma EKR {𝒜 : Finset (Finset (Fin n))} {r : ℕ} (h𝒜 : (𝒜 : Set (Finse
   have q : n - r - (n - 2 * r) = r := by
     rw [tsub_right_comm, Nat.sub_sub_self, two_mul]
     apply Nat.add_sub_cancel
-    rw [mul_comm, ←Nat.le_div_iff_mul_le' zero_lt_two]
+    rw [mul_comm, ← Nat.le_div_iff_mul_le' zero_lt_two]
     exact h₃
   rw [q] at kk
   -- But this gives a contradiction: `n choose r < |𝒜| + |∂^[n-2k] 𝒜ᶜˢ|`

LeanCamCombi/Mathlib/Analysis/Convex/Extreme.lean

@@ -68,7 +68,7 @@ variable [NormedLinearOrderedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace
 -- beurk
 lemma inter_frontier_self_inter_convexHull_extreme :
     IsExtreme 𝕜 (closure s) (closure s ∩ frontier (convexHull 𝕜 s)) := by
-  refine' ⟨inter_subset_left _ _, fun x₁ hx₁A x₂ hx₂A x hxs hx => ⟨⟨hx₁A, _⟩, hx₂A, _⟩⟩
+  refine' ⟨inter_subset_left, fun x₁ hx₁A x₂ hx₂A x hxs hx => ⟨⟨hx₁A, _⟩, hx₂A, _⟩⟩
   sorry
   sorry
 

LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Degree.lean

@@ -23,7 +23,7 @@ lemma degOn_univ (a : α) : G.degOn univ a = G.degree a := by rw [degOn, degree,
 lemma degOn_union (h : Disjoint s t) (a) : G.degOn (s ∪ t) a = G.degOn s a + G.degOn t a := by
   unfold degOn
   rw [← card_union_of_disjoint, ← union_inter_distrib_right]
-  exact h.mono (inter_subset_left _ _) (inter_subset_left _ _)
+  exact h.mono inter_subset_left inter_subset_left
 
 -- edges from t to s\t equals edges from s\t to t
 lemma sum_degOn_comm (s t : Finset α) : ∑ a in s, G.degOn t a = ∑ a in t, G.degOn s a := by