Bump mathlib

LeanCamCombi.lean

@@ -1,5 +1,6 @@
 import LeanCamCombi.Archive.CauchyDavenportFromKneser
 import LeanCamCombi.BernoulliSeq
+import LeanCamCombi.ConvexContinuous
 import LeanCamCombi.DiscreteDeriv
 import LeanCamCombi.ErdosGinzburgZiv
 import LeanCamCombi.ErdosRenyi.Basic
@@ -42,12 +43,11 @@ import LeanCamCombi.Mathlib.Data.Finset.PosDiffs
 import LeanCamCombi.Mathlib.Data.List.Basic
 import LeanCamCombi.Mathlib.Data.List.DropRight
 import LeanCamCombi.Mathlib.Data.Multiset.Basic
+import LeanCamCombi.Mathlib.Data.Nat.Defs
 import LeanCamCombi.Mathlib.Data.Nat.Factors
-import LeanCamCombi.Mathlib.Data.Nat.Order.Lemmas
 import LeanCamCombi.Mathlib.Data.Set.Finite
 import LeanCamCombi.Mathlib.Data.Set.Image
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
-import LeanCamCombi.Mathlib.Data.Subtype
 import LeanCamCombi.Mathlib.FieldTheory.Finite.Basic
 import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup
 import LeanCamCombi.Mathlib.Order.Category.BoolAlg

LeanCamCombi/BernoulliSeq.lean

@@ -137,8 +137,8 @@ protected lemma union (h : IndepFun X Y μ) :
       add_tsub_assoc_of_le (mul_le_of_le_one_left' $ hX.le_one)]
     · exact (add_le_add_left (mul_le_of_le_one_right' $ hY.le_one) _).trans_eq
         (add_tsub_cancel_of_le hX.le_one)
-  · rwa [IndepFun_iff, MeasurableSpace.comap_compl measurable_compl, MeasurableSpace.comap_compl measurable_compl,
-      ←IndepFun_iff]
+  · rwa [IndepFun_iff, MeasurableSpace.comap_compl measurable_compl,
+      MeasurableSpace.comap_compl measurable_compl, ← IndepFun_iff]
 
 end IsBernoulliSeq
 end ProbabilityTheory

LeanCamCombi/DiscreteDeriv.lean

@@ -1,7 +1,7 @@
+import Mathlib.Algebra.Polynomial.AlgebraMap
 import Mathlib.Algebra.Polynomial.BigOperators
+import Mathlib.Algebra.Polynomial.Degree.Lemmas
 import Mathlib.Data.Finsupp.Notation
-import Mathlib.Data.Polynomial.AlgebraMap
-import Mathlib.Data.Polynomial.Degree.Lemmas
 
 open Finset
 open scoped BigOperators

LeanCamCombi/ErdosGinzburgZiv.lean

@@ -7,8 +7,7 @@ import Mathlib.Data.Multiset.Fintype
 import Mathlib.FieldTheory.ChevalleyWarning
 import LeanCamCombi.Mathlib.Algebra.Order.Ring.Canonical
 import LeanCamCombi.Mathlib.Data.Multiset.Basic
-import LeanCamCombi.Mathlib.Data.Nat.Order.Lemmas
-import LeanCamCombi.Mathlib.Data.Subtype
+import LeanCamCombi.Mathlib.Data.Nat.Defs
 import LeanCamCombi.Mathlib.FieldTheory.Finite.Basic
 import LeanCamCombi.Mathlib.RingTheory.Int.Basic
 
@@ -98,8 +97,8 @@ private lemma aux (hs : Multiset.card s = 2 * p - 1) :
     · rw [Finset.card_attach, card_toEnumFinset, hs]
       exact tsub_lt_self (mul_pos zero_lt_two (Fact.out : p.Prime).pos) zero_lt_one
   -- From `f₂ x = 0`, we get that `p` divides the sum of the `a ∈ s` such that `x a ≠ 0`.
-  · simpa only [f₂, map_sum, ZMod.pow_card_sub_one, Finset.sum_map_val, Finset.sum_filter, smul_eval,
-      map_pow, eval_X, mul_ite, mul_zero, mul_one] using x.2.2
+  · simpa only [f₂, map_sum, ZMod.pow_card_sub_one, Finset.sum_map_val, Finset.sum_filter,
+      smul_eval, map_pow, eval_X, mul_ite, mul_zero, mul_one] using x.2.2
 
 --TODO: Rename `Multiset.pairwise_nil` to `Multiset.pairwise_zero`
 

LeanCamCombi/Incidence.lean

@@ -552,7 +552,7 @@ lemma mu_toDual (a b : α) : mu 𝕜 (toDual a) (toDual b) = mu 𝕜 b a := by
   ext a b
   simp only [mul_boole, one_apply, mul_apply, coe_mk, zeta_apply]
   obtain rfl | h := eq_or_ne a b
-  · simp
+  · simp [mud]
   · rw [if_neg h]
     convert_to ∑ x in Icc (ofDual b) (ofDual a), mu 𝕜 x a = 0
     sorry
@@ -683,7 +683,8 @@ variable (𝕜) [Ring 𝕜] [PartialOrder α] [PartialOrder β] [LocallyFiniteOr
   [LocallyFiniteOrder β] [DecidableEq α] [DecidableEq β] [DecidableRel ((· ≤ ·) : α → α → Prop)]
   [DecidableRel ((· ≤ ·) : β → β → Prop)]
 
-/-- The Möbius function on a product order. Based on lemma 2.1.13 of Incidence Algebras by Spiegel and O'Donnell. -/
+/-- The Möbius function on a product order. Based on lemma 2.1.13 of Incidence Algebras by Spiegel
+and O'Donnell. -/
 @[simp]
 lemma mu_prod_mu : (mu 𝕜).prod (mu 𝕜) = (mu 𝕜 : IncidenceAlgebra 𝕜 (α × β)) := by
   refine left_inv_eq_right_inv ?_ zeta_mul_mu

LeanCamCombi/Kneser/Kneser.lean

@@ -240,7 +240,7 @@ lemma inter_mul_sub_card_le {a : α} {s t C : Finset α} (has : a ∈ s)
         norm_num
       all_goals
         apply subset_trans (mul_subset_mul_left hst)
-        rw [← inter_distrib_right]
+        rw [← union_inter_distrib_right]
         refine' subset_trans (mul_subset_mul_right (inter_subset_right _ _)) _
         simp only [smul_mul_assoc, mulStab_mul_mulStab, Subset.rfl]
     _ ≤
@@ -254,7 +254,7 @@ lemma inter_mul_sub_card_le {a : α} {s t C : Finset α} (has : a ∈ s)
       · apply smul_finset_subset_smul (mem_union_left t has) (mem_sdiff.mp hx).1
       have hx' := (mem_sdiff.mp hx).2
       contrapose! hx'
-      rw [← inter_distrib_right]
+      rw [← union_inter_distrib_right]
       obtain ⟨y, hyst, d, hd, hxyd⟩ := mem_mul.mp hx'
       obtain ⟨c, hc, hcx⟩ := mem_smul_finset.mp (mem_sdiff.mp hx).1
       rw [← hcx, ← eq_mul_inv_iff_mul_eq] at hxyd
@@ -345,7 +345,7 @@ theorem mul_kneser :
   rw [← inv_smul_eq_iff] at ht'
   subst ht'
   rename' t' => t
-  rw [mem_inv_smul_finset_iff, smul_eq_mul, div_mul_cancel'] at hc
+  rw [mem_inv_smul_finset_iff, smul_eq_mul, div_mul_cancel] at hc
   rw [div_mul_comm, mem_inv_smul_finset_iff, smul_eq_mul, ← mul_assoc, div_mul_div_cancel',
     div_self', one_mul] at hbac
   rw [smul_finset_nonempty] at ht
@@ -419,13 +419,13 @@ theorem mul_kneser :
   obtain ht₂ | ht₂ne := t₂.eq_empty_or_nonempty
   · have aux₁_contr :=
       disjoint_mul_sub_card_le b (hs₁s has₁) (disjoint_iff_inter_eq_empty.2 ht₂) hH₁H.subset
-    linarith [aux1₁, aux₁_contr, Int.coe_nat_nonneg (t₁ * (s₁ * t₁).mulStab).card]
+    linarith [aux1₁, aux₁_contr, Int.natCast_nonneg (t₁ * (s₁ * t₁).mulStab).card]
   obtain hs₂ | hs₂ne := s₂.eq_empty_or_nonempty
   · have aux1₁_contr :=
       disjoint_mul_sub_card_le a (ht₁t hbt₁) (disjoint_iff_inter_eq_empty.2 hs₂)
         (by rw [mul_comm]; exact hH₁H.subset)
     simp only [union_comm t s, mul_comm t₁ s₁] at aux1₁_contr
-    linarith [aux1₁, aux1₁_contr, Int.coe_nat_nonneg (s₁ * (s₁ * t₁).mulStab).card]
+    linarith [aux1₁, aux1₁_contr, Int.natCast_nonneg (s₁ * (s₁ * t₁).mulStab).card]
   have hC₂stab : C₂.mulStab = H₂ := mulStab_union hs₂ne ht₂ne (by rwa [mul_comm]) hCst₂
   have hH₂H : H₂ ⊂ H := mulStab_mul_ssubset_mulStab hs₂ne ht₂ne (by rwa [mul_comm])
   have aux1₂ :=
@@ -444,17 +444,17 @@ theorem mul_kneser :
           habH).mono
       sdiff_le sdiff_le
   have hSst : S ⊆ a • H \ (s ∪ t) := by
-    simp only [hS, hs₁, ht₂, ← inter_distrib_right, sdiff_inter_self_right, Subset.rfl]
+    simp only [hS, hs₁, ht₂, ← union_inter_distrib_right, sdiff_inter_self_right, Subset.rfl]
   have hTst : T ⊆ b • H \ (s ∪ t) := by
-    simp only [hT, hs₂, ht₁, ← inter_distrib_right, sdiff_inter_self_right, Subset.rfl]
+    simp only [hT, hs₂, ht₁, ← union_inter_distrib_right, sdiff_inter_self_right, Subset.rfl]
   have hSTst : Disjoint (S ∪ T) (s ∪ t) := (subset_sdiff.1 hSst).2.sup_left (subset_sdiff.1 hTst).2
   have hstconv : s * t ∉ convergent := by
     apply hCmin (s * t)
     rw [hstab]
     refine (hC.mulStab_nontrivial.mp hCstab).symm.ssubset_of_subset ?_
     simp only [one_subset, one_mem_mulStab, hC]
-  simp only [Set.mem_setOf_eq, Subset.rfl, true_and_iff, not_le, hstab, mul_one, card_one]
-    at hstconv
+  simp only [Set.mem_setOf_eq, Subset.rfl, true_and_iff, not_le, hstab, mul_one, card_one,
+    convergent] at hstconv
   zify at hstconv
   have hSTcard : (S.card : ℤ) + T.card + (s ∪ t).card ≤ ((s ∪ t) * H).card := by
     norm_cast

LeanCamCombi/Kneser/KneserRuzsa.lean

@@ -38,7 +38,8 @@ namespace Finset
 -- Lemma 3.3 in Ruzsa's notes
 @[to_additive]
 lemma le_card_union_add_card_mulStab_union :
-    min (s.card + s.mulStab.card) (t.card + t.mulStab.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card := by
+    min (s.card + s.mulStab.card) (t.card + t.mulStab.card) ≤
+      (s ∪ t).card + (s ∪ t).mulStab.card := by
   obtain rfl | hs := s.eq_empty_or_nonempty
   · simp [-zero_le']
   -- TODO: `to_additive` chokes on `zero_le'`
@@ -65,7 +66,7 @@ lemma le_card_union_add_card_mulStab_union :
         obtain ⟨w, hwx⟩ := Quotient.exists_rep x
         have : ⟦w⟧ = QuotientGroup.mk (s := N) w := by exact rfl
         rw [← hwx, this, QuotientGroup.eq] at hyx hzx ⊢
-        simp only [mul_one, inv_mem_iff, Subgroup.mem_inf, mem_stabilizer_iff] at hyx hzx ⊢
+        simp only [mul_one, inv_mem_iff, Subgroup.mem_inf, mem_stabilizer_iff, N] at hyx hzx ⊢
         constructor
         · convert hyx.1 using 1
           rw [mul_comm, mul_smul]
@@ -76,7 +77,7 @@ lemma le_card_union_add_card_mulStab_union :
           congr
           simp only [← inv_smul_eq_iff, inv_inv, ← (mem_mulStab ht), hz]
         all_goals { aesop }
-      · aesop
+      · simp (config := { contextual := true }) [*]
     specialize this (α := α ⧸ N) (s := s.image (↑)) (t := t.image (↑))
     simp only [image_nonempty, mulStab_nonempty, mul_nonempty, and_imp,
       forall_true_left, hs, ht, h1] at this
@@ -100,89 +101,90 @@ lemma le_card_union_add_card_mulStab_union :
       (card (image (QuotientGroup.mk (s := N)) t) +
       card (mulStab (image (QuotientGroup.mk (s := N)) t))) := by
         rw [mulStab_quotient_commute_subgroup N t, mulStab_quotient_commute_subgroup N s]
-        all_goals { aesop }
+        all_goals simp [*]
     _ ≤ Nat.card N * (card (image (QuotientGroup.mk (s := N)) s ∪
       image (QuotientGroup.mk (s := N)) t) +
       card (mulStab (image (QuotientGroup.mk (s := N)) s ∪
       image (QuotientGroup.mk (s := N)) t))) := Nat.mul_le_mul_left _ this
-    _ ≤ card (s ∪ t) + card (mulStab (s ∪ t)) := by
+    _ ≤ card (s ∪ t) + card (s ∪ t).mulStab := by
       rw [mul_add, ← image_union, subgroup_mul_card_eq_mul_of_mul_stab_subset N (s ∪ t),
           ← mulStab_quotient_commute_subgroup N (s ∪ t),
-          subgroup_mul_card_eq_mul_of_mul_stab_subset N (mulStab (s ∪ t))]
+          subgroup_mul_card_eq_mul_of_mul_stab_subset N (s ∪ t).mulStab]
       all_goals
       { simp only [hNmulstab, mulStab_idem]; norm_cast; exact inter_mulStab_subset_mulStab_union }
-  obtain hst | hst := (subset_union_left s t).eq_or_ssubset
-  · simp [hst.symm]
-  obtain hts | hts := (subset_union_right s t).eq_or_ssubset
-  · simp [hts.symm]
-  have : H.card = Hs.card * Ht.card := by
-    refine' card_mul_iff.2 fun a ha b hb hab => _
-    replace hab : a.2 * b.2⁻¹ = a.1⁻¹ * b.1 := by
-      rw [mul_inv_eq_iff_eq_mul, mul_assoc, ← inv_mul_eq_iff_eq_mul, inv_inv]
-      exact hab
-    have : a.1⁻¹ * b.1 ∈ Hs ∩ Ht := by
-      simp only [mem_inter]
-      constructor
-      · rw [mem_mulStab hs, mul_smul, inv_smul_eq_iff,
-          (mem_mulStab hs).mp (show b.1 ∈ mulStab s by aesop),
-          (mem_mulStab hs).mp (show a.1 ∈ mulStab s by aesop)]
-      · rw [← hab, mem_mulStab ht, mul_comm, mul_smul, inv_smul_eq_iff,
-          (mem_mulStab ht).mp (show b.2 ∈ mulStab t by aesop),
-          (mem_mulStab ht).mp (show a.2 ∈ mulStab t by aesop)]
-    simp only [h1, mem_one] at this
-    ext
-    · rw [← inv_mul_eq_one, this]
-    · rw [← mul_inv_eq_one, hab, this]
+  -- obtain hst | hst := (subset_union_left s t).eq_or_ssubset
+  -- · simp [hst.symm]
+  -- obtain hts | hts := (subset_union_right s t).eq_or_ssubset
+  -- · simp [hts.symm]
+  -- have : H.card = Hs.card * Ht.card := by
+  --   refine' card_mul_iff.2 fun a ha b hb hab => _
+  --   replace hab : a.2 * b.2⁻¹ = a.1⁻¹ * b.1 := by
+  --     rw [mul_inv_eq_iff_eq_mul, mul_assoc, ← inv_mul_eq_iff_eq_mul, inv_inv]
+  --     exact hab
+  --   have : a.1⁻¹ * b.1 ∈ Hs ∩ Ht := by
+  --     simp only [mem_inter]
+  --     constructor
+  --     · rw [mem_mulStab hs, mul_smul, inv_smul_eq_iff,
+  --         (mem_mulStab hs).mp hb.1,
+  --         (mem_mulStab hs).mp ha.1]
+  --     · rw [← hab, mem_mulStab ht, mul_comm, mul_smul, inv_smul_eq_iff,
+  --         (mem_mulStab ht).mp hb.2,
+  --         (mem_mulStab ht).mp ha.2]
+  --   simp only [h1, mem_one] at this
+  --   ext
+  --   · rw [← inv_mul_eq_one, this]
+  --   · rw [← mul_inv_eq_one, hab, this]
   -- mistake in proof sketch, need to interchange `Hs` and `Ht`
-  suffices h2 : Hs.card - (mulStab (s ∪ t)).card ≤ (s \ t).card ∨
-                Ht.card - (mulStab (s ∪ t)).card ≤ (t \ s).card by
-    simp only [min_le_iff]
-    cases' h2 with h2 h2
-    · left
-      sorry
-    · right
-      sorry
-  have Hst : (mulStab (s ∪ t)).Nonempty := ht.inr.mulStab
-  set k : α → ℕ := fun a =>
-    card ((a • H).image (QuotientGroup.mk (s := stabilizer α s)) ∩ s.image QuotientGroup.mk)
-  set l : α → ℕ := fun a =>
-   card ((a • H).image (QuotientGroup.mk (s := stabilizer α t)) ∩ t.image QuotientGroup.mk)
-  have hkt : ∀ a, k a ≤ Ht.card := sorry
-  have hls : ∀ a, l a ≤ Hs.card := sorry
-  have hk : ∀ a, (s \ t ∩ a • H).card = k a * (Hs.card - l a) := by sorry
-  have hl : ∀ a, (t \ s ∩ a • H).card = l a * (Ht.card - k a) := by sorry
-  by_cases hkl :
-    (∀ a, k a = 0 ∨ k a = Ht.card ∨ l a = 0 ∨ l a = Hs.card) ∧
-      ((∀ a, k a = 0 → l a = 0) ∨ ∀ a, l a = 0 → k a = 0)
-  · obtain ⟨hkl, hkl' | hkl'⟩ := hkl
-    · refine' Or.inl ((tsub_eq_zero_of_le $ card_mono _).trans_le $ zero_le _)
-      sorry
-    · refine' Or.inr ((tsub_eq_zero_of_le $ card_mono _).trans_le $ zero_le _)
-      sorry
-  -- the remaining sketch is flawed since `H` is defined to be `Hbar` in Ruzsa's notes and
-  -- `mulStab (s ∪ t) = H` in the notes
-  suffices hHst : (Hs.card - 1) * (Ht.card - 1) ≤ (s \ t).card * (t \ s).card by
-    by_contra!
-    exact hHst.not_lt $ CanonicallyOrderedCommSemiring.mul_lt_mul_of_lt_of_lt (this.1.trans_le $
-      tsub_le_tsub_left (one_le_card.2 Hst) _) $ this.2.trans_le $
-      tsub_le_tsub_left (one_le_card.2 Hst) _
-  simp (config := {zeta := false}) only
-    [not_and_or, not_or, Classical.not_forall, not_ne_iff, not_imp] at hkl
-  obtain ⟨a, hka, hka', hla, hla'⟩ | ⟨⟨a, hka, hla⟩, b, hlb, hkb⟩ := hkl
-  · refine le_trans ?_ (mul_le_mul' (card_mono $ inter_subset_left _ $ a • H) $
-      card_mono $ inter_subset_left _ $ a • H)
-    rw [hk, hl, mul_comm (k a), mul_mul_mul_comm, mul_comm (k a)]
-    refine le_trans ?_
-      (mul_le_mul' (Nat.add_sub_one_le_mul (tsub_pos_of_lt $ (hls _).lt_of_ne hla').ne' hla) $
-        Nat.add_sub_one_le_mul (tsub_pos_of_lt $ (hkt _).lt_of_ne hka').ne' hka)
-    rw [tsub_add_cancel_of_le (hkt _), tsub_add_cancel_of_le (hls _)]
-  refine'
-    mul_le_mul' (tsub_le_self.trans $ le_trans _ $ card_mono $ inter_subset_left _ $ b • H)
-      (tsub_le_self.trans $ le_trans _ $ card_mono $ inter_subset_left _ $ a • H)
-  · rw [hk, hlb, tsub_zero]
-    exact le_mul_of_one_le_left' (pos_iff_ne_zero.2 hkb)
-  · rw [hl, hka, tsub_zero]
-    exact le_mul_of_one_le_left' (pos_iff_ne_zero.2 hla)
+  -- suffices h2 : Hs.card - (s ∪ t).mulStab.card ≤ (s \ t).card ∨
+  --               Ht.card - (s ∪ t).mulStab.card ≤ (t \ s).card by
+  --   simp only [min_le_iff]
+  --   cases' h2 with h2 h2
+  --   · left
+  --     sorry
+  --   · right
+  --     sorry
+  -- have Hst : (s ∪ t).mulStab.Nonempty := ht.inr.mulStab
+  -- set k : α → ℕ := fun a =>
+  --   card ((a • H).image (QuotientGroup.mk (s := stabilizer α s)) ∩ s.image QuotientGroup.mk)
+  sorry
+  -- set l : α → ℕ := fun a =>
+  --   card ((a • H).image (QuotientGroup.mk (s := stabilizer α t)) ∩ t.image QuotientGroup.mk)
+  -- have hkt : ∀ a, k a ≤ Ht.card := sorry
+  -- have hls : ∀ a, l a ≤ Hs.card := sorry
+  -- have hk : ∀ a, (s \ t ∩ a • H).card = k a * (Hs.card - l a) := by sorry
+  -- have hl : ∀ a, (t \ s ∩ a • H).card = l a * (Ht.card - k a) := by sorry
+  -- by_cases hkl :
+  --   (∀ a, k a = 0 ∨ k a = Ht.card ∨ l a = 0 ∨ l a = Hs.card) ∧
+  --     ((∀ a, k a = 0 → l a = 0) ∨ ∀ a, l a = 0 → k a = 0)
+  -- · obtain ⟨hkl, hkl' | hkl'⟩ := hkl
+  --   · refine' Or.inl ((tsub_eq_zero_of_le $ card_mono _).trans_le $ zero_le _)
+  --     sorry
+  --   · refine' Or.inr ((tsub_eq_zero_of_le $ card_mono _).trans_le $ zero_le _)
+  --     sorry
+  -- -- the remaining sketch is flawed since `H` is defined to be `Hbar` in Ruzsa's notes and
+  -- -- `mulStab (s ∪ t) = H` in the notes
+  -- suffices hHst : (Hs.card - 1) * (Ht.card - 1) ≤ (s \ t).card * (t \ s).card by
+  --   by_contra!
+  --   exact hHst.not_lt $ CanonicallyOrderedCommSemiring.mul_lt_mul_of_lt_of_lt (this.1.trans_le $
+  --     tsub_le_tsub_left (one_le_card.2 Hst) _) $ this.2.trans_le $
+  --     tsub_le_tsub_left (one_le_card.2 Hst) _
+  -- simp (config := {zeta := false}) only
+  --   [not_and_or, not_or, Classical.not_forall, not_ne_iff, not_imp] at hkl
+  -- obtain ⟨a, hka, hka', hla, hla'⟩ | ⟨⟨a, hka, hla⟩, b, hlb, hkb⟩ := hkl
+  -- · refine le_trans ?_ (mul_le_mul' (card_mono $ inter_subset_left _ $ a • H) $
+  --     card_mono $ inter_subset_left _ $ a • H)
+  --   rw [hk, hl, mul_comm (k a), mul_mul_mul_comm, mul_comm (k a)]
+  --   refine le_trans ?_
+  --     (mul_le_mul' (Nat.add_sub_one_le_mul (tsub_pos_of_lt $ (hls _).lt_of_ne hla').ne' hla) $
+  --       Nat.add_sub_one_le_mul (tsub_pos_of_lt $ (hkt _).lt_of_ne hka').ne' hka)
+  --   rw [tsub_add_cancel_of_le (hkt _), tsub_add_cancel_of_le (hls _)]
+  -- refine'
+  --   mul_le_mul' (tsub_le_self.trans $ le_trans _ $ card_mono $ inter_subset_left _ $ b • H)
+  --     (tsub_le_self.trans $ le_trans _ $ card_mono $ inter_subset_left _ $ a • H)
+  -- · rw [hk, hlb, tsub_zero]
+  --   exact le_mul_of_one_le_left' (pos_iff_ne_zero.2 hkb)
+  -- · rw [hl, hka, tsub_zero]
+  --   exact le_mul_of_one_le_left' (pos_iff_ne_zero.2 hla)
 
 -- Lemma 3.4 in Ruzsa's notes
 @[to_additive]
@@ -247,8 +249,8 @@ lemma le_card_mul_add_card_mulStab_mul (hs : s.Nonempty) (ht : t.Nonempty) :
 
 /-- **Kneser's multiplication lemma**: A lower bound on the size of `s * t` in terms of its
 stabilizer. -/
-@[to_additive
-      "**Kneser's addition lemma**: A lower bound on the size of `s + t` in terms of its\nstabilizer."]
+@[to_additive "**Kneser's addition lemma**: A lower bound on the size of `s + t` in terms of its
+stabilizer."]
 lemma mul_kneser' (s t : Finset α) :
     (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤
       (s * t).card + (s * t).mulStab.card := by
@@ -263,10 +265,10 @@ lemma mul_kneser' (s t : Finset α) :
       _
   rw [mul_mulStab_mul_mul_mul_mulStab_mul]
 
-/-- The strict version of **Kneser's multiplication lemma**. If the LHS of `finset.mul_kneser`
+/-- The strict version of **Kneser's multiplication theorem**. If the LHS of `Finset.mul_kneser`
 does not equal the RHS, then it is in fact much smaller. -/
-@[to_additive
-      "The strict version of **Kneser's addition lemma**. If the LHS of\n`finset.add_kneser` does not equal the RHS, then it is in fact much smaller."]
+@[to_additive "The strict version of **Kneser's addition theorem**. If the LHS of
+`Finset.add_kneser` does not equal the RHS, then it is in fact much smaller."]
 lemma mul_strict_kneser'
     (h :
       (s * (s * t).mulStab).card + (t * (s * t).mulStab).card <

LeanCamCombi/Kneser/MulStab.lean

@@ -38,14 +38,14 @@ def mulStab (s : Finset α) : Finset α := (s / s).filter fun a ↦ a • s = s
 lemma mem_mulStab (hs : s.Nonempty) : a ∈ s.mulStab ↔ a • s = s := by
   rw [mulStab, mem_filter, mem_div, and_iff_right_of_imp]
   obtain ⟨b, hb⟩ := hs
-  exact fun h ↦ ⟨_, by rw [← h]; exact smul_mem_smul_finset hb, _, hb, mul_div_cancel'' _ _⟩
+  exact fun h ↦ ⟨_, by rw [← h]; exact smul_mem_smul_finset hb, _, hb, mul_div_cancel_right _ _⟩
 
 @[to_additive]
 lemma mulStab_subset_div : s.mulStab ⊆ s / s := filter_subset _ _
 
 @[to_additive]
 lemma mulStab_subset_div_right (ha : a ∈ s) : s.mulStab ⊆ s / {a} := by
-  refine fun b hb ↦ mem_div.2 ⟨_, ?_, _, mem_singleton_self _, mul_div_cancel'' _ _⟩
+  refine fun b hb ↦ mem_div.2 ⟨_, ?_, _, mem_singleton_self _, mul_div_cancel_right _ _⟩
   rw [mem_mulStab ⟨a, ha⟩] at hb
   rw [← hb]
   exact smul_mem_smul_finset ha