Bump mathlib

LeanCamCombi.lean

@@ -16,18 +16,19 @@ import LeanCamCombi.Kneser.MulStab
 import LeanCamCombi.KruskalKatona
 import LeanCamCombi.LittlewoodOfford
 import LeanCamCombi.Mathlib.Algebra.BigOperators.LocallyFinite
-import LeanCamCombi.Mathlib.Analysis.Convex.Combination
+import LeanCamCombi.Mathlib.Algebra.BigOperators.Ring
+import LeanCamCombi.Mathlib.Algebra.Order.Sub.Canonical
 import LeanCamCombi.Mathlib.Analysis.Convex.Exposed
 import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
 import LeanCamCombi.Mathlib.Analysis.Convex.Independence
 import LeanCamCombi.Mathlib.Analysis.Convex.SimplicialComplex.Basic
 import LeanCamCombi.Mathlib.Combinatorics.Colex
-import LeanCamCombi.Mathlib.Combinatorics.SetFamily.AhlswedeZhang
 import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shatter
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Containment
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Degree
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
+import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Maps
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Multipartite
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
 import LeanCamCombi.Mathlib.Data.Finset.Card

LeanCamCombi/Incidence.lean

@@ -218,16 +218,8 @@ instance instNonAssocSemiring [Preorder α] [LocallyFiniteOrder α] [DecidableEq
   mul := (· * ·)
   zero := 0
   one := 1
-  one_mul := fun f ↦ by
-    ext a b
-    simp_rw [mul_apply, one_apply, sum_boole_mul]
-    exact ite_eq_left_iff.2 (not_imp_comm.1 fun h ↦ left_mem_Icc.2 <| le_of_ne_zero <| Ne.symm h)
-  mul_one := fun f ↦ by
-    ext a b
-    simp_rw [mul_apply, one_apply, eq_comm, sum_mul_boole]
-    convert
-      (ite_eq_left_iff.2 <|
-          not_imp_comm.1 fun h ↦ right_mem_Icc.2 <| le_of_ne_zero <| Ne.symm h).symm
+  one_mul := fun f ↦ by ext; simp [*]
+  mul_one := fun f ↦ by ext; simp [*]
 
 instance instSemiring [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] [Semiring 𝕜] :
     Semiring (IncidenceAlgebra 𝕜 α) where

LeanCamCombi/Kneser/Kneser.lean

@@ -202,7 +202,7 @@ lemma disjoint_mul_sub_card_le {a : α} (b : α) {s t C : Finset α} (has : a 
       · apply smul_finset_subset_smul (mem_union_left t has) (mem_sdiff.mp hx).1
       have hx' := (mem_sdiff.mp hx).2
       contrapose! hx'
-      obtain ⟨y, d, hyst, hd, hxyd⟩ := mem_mul.mp hx'
+      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
       have hyC : y ∈ a • C.mulStab := by
@@ -255,7 +255,7 @@ lemma inter_mul_sub_card_le {a : α} {s t C : Finset α} (has : a ∈ s)
       have hx' := (mem_sdiff.mp hx).2
       contrapose! hx'
       rw [← inter_distrib_right]
-      obtain ⟨y, d, hyst, hd, hxyd⟩ := mem_mul.mp hx'
+      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
       have hyC : y ∈ a • C.mulStab := by
@@ -380,7 +380,7 @@ theorem mul_kneser :
     rw [mul_subset_left_iff (hs.mul ht), hstab, ← coe_subset, coe_one]
     exact hCstab.not_subset_singleton
   simp_rw [mul_subset_iff_left, Classical.not_forall, mem_mul] at this
-  obtain ⟨_, ⟨a, b, ha, hb, rfl⟩, hab⟩ := this
+  obtain ⟨_, ⟨a, ha, b, hb, rfl⟩, hab⟩ := this
   set s₁ := s ∩ a • H with hs₁
   set s₂ := s ∩ b • H with hs₂
   set t₁ := t ∩ b • H with ht₁

LeanCamCombi/Kneser/KneserRuzsa.lean

@@ -58,15 +58,15 @@ lemma le_card_union_add_card_mulStab_union :
       mulStab (image QuotientGroup.mk t) = 1 := by
       ext x
       constructor
-      · simp only [Nonempty.image_iff, mem_one, and_imp, ← QuotientGroup.mk_one]
+      · simp only [image_nonempty, mem_one, and_imp, ← QuotientGroup.mk_one]
         intro hx
         rw [← mulStab_quotient_commute_subgroup N s, ← mulStab_quotient_commute_subgroup N t] at hx
         simp only [mem_inter, mem_image] at hx
         obtain ⟨⟨y, hy, hyx⟩, ⟨z, hz, hzx⟩⟩ := hx
         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, mem_inf, mem_stabilizer_iff] at hyx hzx ⊢
+        simp only [mul_one, inv_mem_iff, Subgroup.mem_inf, mem_stabilizer_iff] at hyx hzx ⊢
         constructor
         · convert hyx.1 using 1
           rw [mul_comm, mul_smul]
@@ -79,7 +79,7 @@ lemma le_card_union_add_card_mulStab_union :
         all_goals { aesop }
       · aesop
     specialize this (α := α ⧸ N) (s := s.image (↑)) (t := t.image (↑))
-    simp only [Nonempty.image_iff, mulStab_nonempty, mul_nonempty, and_imp,
+    simp only [image_nonempty, mulStab_nonempty, mul_nonempty, and_imp,
       forall_true_left, hs, ht, h1] at this
     calc
     min (card s + card Hs) (card t + card Ht) =

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'' _ _⟩
 
 @[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'' _ _⟩
   rw [mem_mulStab ⟨a, ha⟩] at hb
   rw [← hb]
   exact smul_mem_smul_finset ha
@@ -157,7 +157,7 @@ variable [CommGroup α] [DecidableEq α] {s t : Finset α} {a : α}
 
 @[to_additive]
 lemma mulStab_subset_div_left (ha : a ∈ s) : s.mulStab ⊆ {a} / s := by
-  refine fun b hb ↦ mem_div.2 ⟨_, _, mem_singleton_self _, ?_, div_div_cancel _ _⟩
+  refine fun b hb ↦ mem_div.2 ⟨_, mem_singleton_self _, _, ?_, div_div_cancel _ _⟩
   rw [mem_mulStab ⟨a, ha⟩] at hb
   rwa [← hb, ← inv_smul_mem_iff, smul_eq_mul, inv_mul_eq_div] at ha
 
@@ -357,7 +357,7 @@ lemma mulStab_quotient_commute_subgroup (s : Subgroup α) (t : Finset α)
   · simp
   have hti : (image (QuotientGroup.mk (s := s)) t).Nonempty := by aesop
   ext x;
-  simp only [mem_image, Nonempty.image_iff, mem_mulStab hti]
+  simp only [mem_image, image_nonempty, mem_mulStab hti]
   constructor
   · rintro ⟨a, hax⟩
     rw [← hax.2]

LeanCamCombi/KruskalKatona.lean

@@ -412,7 +412,7 @@ lemma EKR {𝒜 : Finset (Finset (Fin n))} {r : ℕ} (h𝒜 : (𝒜 : Set (Finse
   have h𝒜bar : (𝒜ᶜˢ : Set (Finset (Fin n))).Sized (n - r) := by simpa using h₂.compls
   have : n - 2 * r ≤ n - r := by
     rw [tsub_le_tsub_iff_left ‹r ≤ n›]
-    exact Nat.le_mul_of_pos_left zero_lt_two
+    exact Nat.le_mul_of_pos_left _ zero_lt_two
   -- We can use the Lovasz form of Kruskal-Katona to get |∂^[n-2k] 𝒜ᶜˢ| ≥ (n-1) choose r
   have kk :=
     lovasz_form ‹n - 2 * r ≤ n - r› ((tsub_le_tsub_iff_left ‹1 ≤ n›).2 h1r) tsub_le_self h𝒜bar z.le

LeanCamCombi/Mathlib/Algebra/BigOperators/Ring.lean

@@ -0,0 +1,16 @@
+import Mathlib.Algebra.BigOperators.Ring
+
+open scoped BigOperators
+
+namespace Finset
+variable {ι α : Type*}
+
+section NonAssocSemiring
+variable [NonAssocSemiring α] [DecidableEq ι]
+
+-- TODO: Replace `sum_boole_mul`
+lemma sum_boole_mul' (s : Finset ι) (f : ι → α) (i : ι) :
+    ∑ j in s, ite (i = j) 1 0 * f j = ite (i ∈ s) (f i) 0 := by simp
+
+end NonAssocSemiring
+end Finset

LeanCamCombi/Mathlib/Algebra/Order/Sub/Canonical.lean

@@ -0,0 +1,3 @@
+import Mathlib.Algebra.Order.Sub.Canonical
+
+attribute [simp] tsub_lt_self_iff

LeanCamCombi/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean

@@ -1,5 +1,4 @@
 import Mathlib.Analysis.Convex.SimplicialComplex.Basic
-import LeanCamCombi.Mathlib.Analysis.Convex.Combination
 import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 
 open Finset Geometry