Bump mathlib

LeanCamCombi.lean

@@ -15,10 +15,7 @@ import LeanCamCombi.Kneser.Mathlib
 import LeanCamCombi.Kneser.MulStab
 import LeanCamCombi.KruskalKatona
 import LeanCamCombi.LittlewoodOfford
-import LeanCamCombi.Mathlib.Algebra.BigOperators.Basic
 import LeanCamCombi.Mathlib.Algebra.BigOperators.LocallyFinite
-import LeanCamCombi.Mathlib.Algebra.Order.Ring.Canonical
-import LeanCamCombi.Mathlib.Algebra.Order.Ring.Defs
 import LeanCamCombi.Mathlib.Analysis.Convex.Combination
 import LeanCamCombi.Mathlib.Analysis.Convex.Exposed
 import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
@@ -33,19 +30,16 @@ import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Degree
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Multipartite
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
-import LeanCamCombi.Mathlib.Data.Finset.Basic
 import LeanCamCombi.Mathlib.Data.Finset.Card
 import LeanCamCombi.Mathlib.Data.Finset.Lattice
 import LeanCamCombi.Mathlib.Data.Finset.Pointwise
 import LeanCamCombi.Mathlib.Data.Finset.PosDiffs
-import LeanCamCombi.Mathlib.Data.Fintype.Basic
 import LeanCamCombi.Mathlib.Data.List.Basic
 import LeanCamCombi.Mathlib.Data.Nat.Factors
 import LeanCamCombi.Mathlib.Data.Set.Finite
 import LeanCamCombi.Mathlib.Data.Set.Image
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup
-import LeanCamCombi.Mathlib.MeasureTheory.Measure.Typeclasses
 import LeanCamCombi.Mathlib.Order.Category.BoolAlg
 import LeanCamCombi.Mathlib.Order.ConditionallyCompleteLattice.Basic
 import LeanCamCombi.Mathlib.Order.Hom.Lattice

LeanCamCombi/BernoulliSeq.lean

@@ -3,9 +3,7 @@ Copyright (c) 2022 Yaël Dillies, Kexing Ying. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Kexing Ying
 -/
-import Mathlib.Algebra.BigOperators.Basic
 import Mathlib.Probability.IdentDistrib
-import LeanCamCombi.Mathlib.MeasureTheory.Measure.Typeclasses
 import LeanCamCombi.Mathlib.Probability.Independence.Basic
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 

LeanCamCombi/Incidence.lean

@@ -233,22 +233,11 @@ instance instSemiring [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] [Se
     Semiring (IncidenceAlgebra 𝕜 α) where
   __ := instNonAssocSemiring
   mul := (· * ·)
-  mul_assoc := fun f g h ↦ by
+  mul_assoc f g h := by
     ext a b
-    simp only [mul_apply, sum_mul, mul_sum]
-    rw [sum_sigma', sum_sigma']
-    apply sum_bij fun x _ ↦ Sigma.mk x.snd x.fst
-    · rintro c hc
-      simp only [mem_sigma, mem_Icc] at hc
-      simp only [mem_sigma, mem_Icc]
-      exact ⟨⟨hc.2.1, hc.2.2.trans hc.1.2⟩, hc.2.2, hc.1.2⟩
-    · rintro c _
-      simp only [mul_assoc]
-    · rintro ⟨c₁, c₂⟩ ⟨d₁, d₂⟩ hc hd ⟨⟩
-      rfl
-    · rintro c hc
-      simp only [exists_prop, Sigma.exists, mem_sigma, heq_iff_eq, Sigma.mk.inj_iff, mem_Icc] at *
-      exact ⟨c.2, c.1, ⟨⟨hc.1.1.trans hc.2.1, hc.2.2⟩, hc.1.1, hc.2.1⟩, c.eta.symm⟩
+    simp only [mul_apply, sum_mul, mul_sum, sum_sigma']
+    apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;>
+      aesop (add simp mul_assoc) (add unsafe le_trans)
   one := 1
   zero := 0
 
@@ -277,23 +266,11 @@ end Smul
 instance instIsScalarTower [Preorder α] [LocallyFiniteOrder α] [AddCommMonoid 𝕜] [Monoid 𝕜]
     [Semiring 𝕝] [AddCommMonoid 𝕞] [SMul 𝕜 𝕝] [Module 𝕝 𝕞] [DistribMulAction 𝕜 𝕞]
     [IsScalarTower 𝕜 𝕝 𝕞] :
-    IsScalarTower (IncidenceAlgebra 𝕜 α) (IncidenceAlgebra 𝕝 α) (IncidenceAlgebra 𝕞 α) :=
-  ⟨fun f g h ↦ by
+    IsScalarTower (IncidenceAlgebra 𝕜 α) (IncidenceAlgebra 𝕝 α) (IncidenceAlgebra 𝕞 α) where
+  smul_assoc f g h := by
     ext a b
-    simp only [smul_apply, sum_smul, smul_sum]
-    rw [sum_sigma', sum_sigma']
-    apply sum_bij fun x _ ↦ Sigma.mk x.snd x.fst
-    · rintro c hc
-      simp only [mem_sigma, mem_Icc] at hc
-      simp only [mem_sigma, mem_Icc]
-      exact ⟨⟨hc.2.1, hc.2.2.trans hc.1.2⟩, hc.2.2, hc.1.2⟩
-    · rintro c _
-      simp only [smul_assoc]
-    · rintro ⟨c₁, c₂⟩ ⟨d₁, d₂⟩ hc hd ⟨⟩
-      rfl
-    · rintro c hc
-      simp only [exists_prop, Sigma.exists, mem_sigma, heq_iff_eq, Sigma.mk.inj_iff, mem_Icc] at *
-      exact ⟨c.2, c.1, ⟨⟨hc.1.1.trans hc.2.1, hc.2.2⟩, hc.1.1, hc.2.1⟩, c.eta.symm⟩⟩
+    simp only [smul_apply, sum_smul, smul_sum, sum_sigma']
+    apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;> aesop (add unsafe le_trans)
 
 instance [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] [Semiring 𝕜] [Semiring 𝕝]
     [Module 𝕜 𝕝] : Module (IncidenceAlgebra 𝕜 α) (IncidenceAlgebra 𝕝 α) where
@@ -307,13 +284,12 @@ instance [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] [Semiring 𝕜]
 
 instance smulWithZeroRight [Zero 𝕜] [Zero 𝕝] [SMulWithZero 𝕜 𝕝] [LE α] :
     SMulWithZero 𝕜 (IncidenceAlgebra 𝕝 α) :=
-  Function.Injective.smulWithZero ⟨((⇑) : IncidenceAlgebra 𝕝 α → α → α → 𝕝), coe_zero⟩
-    FunLike.coe_injective coe_smul'
+  FunLike.coe_injective.smulWithZero ⟨((⇑) : IncidenceAlgebra 𝕝 α → α → α → 𝕝), coe_zero⟩ coe_smul'
 
 instance moduleRight [Preorder α] [Semiring 𝕜] [AddCommMonoid 𝕝] [Module 𝕜 𝕝] :
     Module 𝕜 (IncidenceAlgebra 𝕝 α) :=
-  Function.Injective.module _ ⟨⟨((⇑) : IncidenceAlgebra 𝕝 α → α → α → 𝕝), coe_zero⟩, coe_add⟩
-    FunLike.coe_injective coe_smul'
+  FunLike.coe_injective.module _ ⟨⟨((⇑) : IncidenceAlgebra 𝕝 α → α → α → 𝕝), coe_zero⟩, coe_add⟩
+    coe_smul'
 
 instance algebraRight [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] [CommSemiring 𝕜]
     [CommSemiring 𝕝] [Algebra 𝕜 𝕝] : Algebra 𝕜 (IncidenceAlgebra 𝕝 α) where
@@ -619,20 +595,8 @@ lemma moebius_inversion_top (f g : α → 𝕜) (h : ∀ x, g x = ∑ y in Ici x
       erw [sum_sigma' (Ici x) fun y ↦ Ici y]
       erw [sum_sigma' (Ici x) fun z ↦ Icc x z]
       simp only [mul_boole, MulZeroClass.zero_mul, ite_mul, zeta_apply]
-      refine' sum_bij (fun X _ ↦ ⟨X.snd, X.fst⟩) _ _ _ _
-      · intro X hX
-        simp only [mem_Ici, mem_sigma, mem_Icc]
-        simp only [mem_Ici, mem_sigma, mem_Icc] at hX
-        exact ⟨hX.1.trans hX.2, hX⟩
-      · intro X hX
-        simp only at *
-      · intro X Y ha hb h
-        simpa [Sigma.ext_iff, and_comm] using h
-      · intro X hX
-        use ⟨X.snd, X.fst⟩
-        simp only [and_true_iff, mem_Ici, eq_self_iff_true, Sigma.eta, mem_sigma, mem_Icc,
-          exists_prop] at *
-        exact hX.2
+      apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;>
+        aesop (add simp mul_assoc) (add unsafe le_trans)
     _ = ∑ z in Ici x, (mu 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) x z * f z := by
       simp_rw [mul_apply, sum_mul]
     _ = ∑ y in Ici x, ∑ z in Ici y, (1 : IncidenceAlgebra 𝕜 α) x z * f z := by

LeanCamCombi/Kneser/Kneser.lean

@@ -121,7 +121,7 @@ lemma mulStab_union (hs₁ : (s ∩ a • C.mulStab).Nonempty) (ht₁ : (t ∩ b
   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')
   suffices s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab by
-    have := (card_le_of_subset hxysub).not_lt ((card_lt_card this).trans_eq ?_)
+    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
@@ -186,18 +186,18 @@ lemma disjoint_mul_sub_card_le {a : α} (b : α) {s t C : Finset α} (has : a 
           (subset_trans (mul_subset_mul_left hst)
             (subset_trans (mul_subset_mul_right (inter_subset_right s _)) _)),
         card_smul_finset, Int.ofNat_sub]
-      · apply le_trans (card_le_of_subset (mul_subset_mul_left hst))
+      · apply le_trans (card_le_card (mul_subset_mul_left hst))
         apply
-          le_trans (card_le_of_subset inter_mul_subset)
-            (le_of_le_of_eq (card_le_of_subset (inter_subset_right _ _)) _)
+          le_trans (card_le_card inter_mul_subset)
+            (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 -
           ((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab).card := by
-      rw [← Int.ofNat_sub (card_le_of_subset (mul_subset_mul_left hst)), ←
+      rw [← Int.ofNat_sub (card_le_card (mul_subset_mul_left hst)), ←
         card_sdiff (mul_subset_mul_left hst)]
       norm_cast
-      apply card_le_of_subset
+      apply card_le_card
       refine' fun x hx => mem_sdiff.mpr ⟨_, _⟩
       · apply smul_finset_subset_smul (mem_union_left t has) (mem_sdiff.mp hx).1
       have hx' := (mem_sdiff.mp hx).2
@@ -234,7 +234,7 @@ lemma inter_mul_sub_card_le {a : α} {s t C : Finset α} (has : a ∈ s)
         (a • C.mulStab \
             ((s ∩ a • C.mulStab ∪ t ∩ a • C.mulStab) *
               (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab)).card := by
-      rw [card_sdiff, Int.ofNat_sub (card_le_of_subset _), card_smul_finset]
+      rw [card_sdiff, Int.ofNat_sub (card_le_card _), card_smul_finset]
       · rw [union_mul, le_sub_iff_add_le]
         apply le_trans (add_le_add_left (Int.ofNat_le.mpr $ card_union_le _ _) _)
         norm_num
@@ -246,10 +246,10 @@ lemma inter_mul_sub_card_le {a : α} {s t C : Finset α} (has : a ∈ s)
     _ ≤
         ((s ∪ t) * C.mulStab).card -
           ((s ∪ t) * (s ∩ a • C.mulStab * (t ∩ a • C.mulStab)).mulStab).card := by
-      rw [← Int.ofNat_sub (card_le_of_subset (mul_subset_mul_left hst)), ←
+      rw [← Int.ofNat_sub (card_le_card (mul_subset_mul_left hst)), ←
         card_sdiff (mul_subset_mul_left hst)]
       norm_cast
-      apply card_le_of_subset
+      apply card_le_card
       refine' fun x hx => mem_sdiff.mpr ⟨_, _⟩
       · apply smul_finset_subset_smul (mem_union_left t has) (mem_sdiff.mp hx).1
       have hx' := (mem_sdiff.mp hx).2
@@ -274,7 +274,7 @@ private lemma card_mul_add_card_lt (hC : C.Nonempty) (hs : s' ⊆ s) (ht : t' 
       (by
         rw [← tsub_pos_iff_lt, ← card_sdiff (mul_subset_mul hs ht), card_pos]
         exact hC.mono (subset_sdiff.2 ⟨hCst, hCst'⟩)) $
-    card_le_of_subset hs
+    card_le_card hs
 
 /-! ### Kneser's theorem -/
 
@@ -357,10 +357,10 @@ theorem mul_kneser :
   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_of_subset $
+    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 $
         ih (s ∩ t) (s ∪ t) _⟩
-    exact add_lt_add_of_le_of_lt (card_le_of_subset inter_mul_union_subset) (card_lt_card hsts)
+    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
   set H := C.mulStab with hH
   obtain ⟨hCst, hCcard⟩ : C ∈ convergent := argminOn_mem _ _ _ _
@@ -374,7 +374,7 @@ theorem mul_kneser :
   -- `s.card + t.card - 1 = (s ∩ t).card + (s ∪ t).card - 1.card = ≤ C.card ≤ (s * t).card`
   obtain hCstab | hCstab := eq_singleton_or_nontrivial (one_mem_mulStab.2 hC)
   · simp only [hH, hCstab, card_singleton, card_mul_singleton, card_inter_add_card_union] at hCcard
-    exact hCcard.trans (add_le_add_right (card_le_of_subset hCst) _)
+    exact hCcard.trans (add_le_add_right (card_le_card hCst) _)
   exfalso
   have : ¬s * t * H ⊆ s * t := by
     rw [mul_subset_left_iff (hs.mul ht), hstab, ← coe_subset, coe_one]
@@ -459,7 +459,7 @@ theorem mul_kneser :
   have hSTcard : (S.card : ℤ) + T.card + (s ∪ t).card ≤ ((s ∪ t) * H).card := by
     norm_cast
     conv_lhs => rw [← card_disjoint_union hST, ← card_disjoint_union hSTst, ← mul_one (s ∪ t)]
-    refine' card_le_of_subset
+    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)
@@ -468,7 +468,7 @@ theorem mul_kneser :
   -- Now we prove inequality (2)
   have aux2₁ : (s₁.card : ℤ) + t₁.card + H₁.card ≤ H.card := by
     rw [← le_sub_iff_add_le']
-    refine' (Int.le_of_dvd ((sub_nonneg_of_le $ Nat.cast_le.2 $ card_le_of_subset $
+    refine' (Int.le_of_dvd ((sub_nonneg_of_le $ Nat.cast_le.2 $ card_le_card $
       mul_subset_mul_left hH₁H.subset).trans_lt aux1₁) $ dvd_sub
         (dvd_sub (card_mulStab_dvd_card_mulStab (hs₁ne.mul ht₁ne) hH₁H.subset).natCast
           (card_mulStab_dvd_card_mul_mulStab _ _).natCast) $
@@ -478,7 +478,7 @@ theorem mul_kneser :
       Nat.cast_le.2 $ card_le_card_mul_right _ hH₁ne) _
   have aux2₂ : (s₂.card : ℤ) + t₂.card + H₂.card ≤ H.card := by
     rw [← le_sub_iff_add_le']
-    refine' (Int.le_of_dvd ((sub_nonneg_of_le $ Nat.cast_le.2 $ card_le_of_subset $
+    refine' (Int.le_of_dvd ((sub_nonneg_of_le $ Nat.cast_le.2 $ card_le_card $
       mul_subset_mul_left hH₂H.subset).trans_lt aux1₂) $ dvd_sub
         (dvd_sub (card_mulStab_dvd_card_mulStab (hs₂ne.mul ht₂ne) hH₂H.subset).natCast
           (card_mulStab_dvd_card_mul_mulStab _ _).natCast) $
@@ -500,7 +500,7 @@ theorem mul_kneser :
     _ ≤ ((s ∪ t) * H).card + (s ∩ t).card - C.card := by
       suffices (C.card : ℤ) + (s₁ * t₁).card ≤ (s * t).card by linarith [this, hSTcard]
       · norm_cast
-        simp only [← card_disjoint_union hCst₁, card_le_of_subset hC₁st]
+        simp only [← card_disjoint_union hCst₁, card_le_card hC₁st]
     _ ≤ H.card := by
       simp only [sub_le_iff_le_add, ← Int.ofNat_add, Int.ofNat_le, add_comm _ C.card,
         add_comm _ (s ∩ t).card, hCcard]
@@ -516,7 +516,7 @@ theorem mul_kneser :
     _ ≤ ((s ∪ t) * H).card + (s ∩ t).card - C.card := by
       suffices (C.card : ℤ) + (s₂ * t₂).card ≤ (s * t).card by linarith [this, hSTcard]
       · norm_cast
-        simp only [← card_disjoint_union hCst₂, card_le_of_subset hC₂st]
+        simp only [← card_disjoint_union hCst₂, card_le_card hC₂st]
     _ ≤ H.card := by
       simp only [sub_le_iff_le_add, ← Int.ofNat_add, Int.ofNat_le, add_comm _ C.card,
         add_comm _ (s ∩ t).card, hCcard]