Bump mathlib

LeanCamCombi.lean

@@ -20,8 +20,6 @@ import LeanCamCombi.KruskalKatona
 import LeanCamCombi.LittlewoodOfford
 import LeanCamCombi.Mathlib.Algebra.BigOperators.Ring
 import LeanCamCombi.Mathlib.Algebra.Order.BigOperators.LocallyFinite
-import LeanCamCombi.Mathlib.Algebra.Order.Ring.Canonical
-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
@@ -37,7 +35,6 @@ import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Finite
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Maps
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Multipartite
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
-import LeanCamCombi.Mathlib.Data.Finset.Card
 import LeanCamCombi.Mathlib.Data.Finset.Pointwise
 import LeanCamCombi.Mathlib.Data.Finset.PosDiffs
 import LeanCamCombi.Mathlib.Data.List.Basic
@@ -53,7 +50,6 @@ import LeanCamCombi.Mathlib.Order.Hom.Lattice
 import LeanCamCombi.Mathlib.Order.Interval.Finset.Basic
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
 import LeanCamCombi.Mathlib.Order.Sublattice
-import LeanCamCombi.Mathlib.Order.SupClosed
 import LeanCamCombi.Mathlib.Probability.Independence.Basic
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 import LeanCamCombi.Mathlib.RingTheory.Int.Basic

LeanCamCombi/ErdosGinzburgZiv.lean

@@ -5,9 +5,7 @@ Authors: Yaël Dillies
 -/
 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.Defs
 import LeanCamCombi.Mathlib.FieldTheory.Finite.Basic
 import LeanCamCombi.Mathlib.RingTheory.Int.Basic
 

LeanCamCombi/Kneser/KneserRuzsa.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mantas Bakšys, Yaël Dillies
 -/
 import Mathlib.Combinatorics.Additive.ETransform
-import LeanCamCombi.Mathlib.Data.Finset.Card
 import LeanCamCombi.Kneser.MulStab
 
 /-!

LeanCamCombi/Mathlib/Combinatorics/Schnirelmann.lean

@@ -1,5 +1,4 @@
 import Mathlib.Combinatorics.Schnirelmann
-import LeanCamCombi.Mathlib.Algebra.Order.Sub.Canonical
 
 open Finset
 open scoped Classical Pointwise

LeanCamCombi/Mathlib/Data/List/DropRight.lean

@@ -1,6 +1,6 @@
 import Mathlib.Data.List.DropRight
 import LeanCamCombi.Mathlib.Data.List.Basic
-import LeanCamCombi.Mathlib.Algebra.Order.Sub.Canonical
+import LeanCamCombi.Mathlib.Data.Nat.Defs
 
 namespace List
 variable {α : Type*} {l l' l₀ l₁ l₂ : List α} {a b : α} {m n : ℕ}
@@ -35,7 +35,7 @@ alias ⟨IsSuffix.eq_rtake, _⟩ := suffix_iff_eq_rtake
 @[simp] lemma rdrop_min : l.rdrop (min n l.length) = l.rdrop n := sorry
 
 lemma take_prefix_take (h : m ≤ n) : l.take m <+: l.take n := by
-  rw [prefix_iff_eq_take, length_take, take_take, min_right_comm, min_eq_left h, take_min]
+  rw [prefix_iff_eq_take, length_take, take_take, Nat.min_right_comm, min_eq_left h, take_min]
 
 lemma drop_suffix_drop (h : m ≤ n) : l.drop n <:+ l.drop m := sorry
 

LeanCamCombi/Mathlib/Data/Nat/Defs.lean

@@ -1,13 +1,17 @@
 import Mathlib.Data.Nat.Defs
 
 namespace Nat
-variable {a b : ℕ}
-
-lemma eq_of_dvd_of_lt_two_mul (ha : a ≠ 0) (hdvd : b ∣ a) (hlt : a < 2 * b) : a = b := by
-  obtain ⟨_ | _ | c, rfl⟩ := hdvd
-  · simp at ha
-  · exact Nat.mul_one _
-  · rw [Nat.mul_comm] at hlt
-    cases Nat.not_le_of_lt hlt (Nat.mul_le_mul_right _ (by omega))
+
+protected lemma min_left_comm (a b c : ℕ) : min a (min b c) = min b (min a c) := by
+  rw [← Nat.min_assoc, ← Nat.min_assoc, b.min_comm]
+
+protected lemma max_left_comm (a b c : ℕ) : max a (max b c) = max b (max a c) := by
+  rw [← Nat.max_assoc, ← Nat.max_assoc, b.max_comm]
+
+protected lemma min_right_comm (a b c : ℕ) : min (min a b) c = min (min a c) b := by
+  rw [Nat.min_assoc, Nat.min_assoc, b.min_comm]
+
+protected lemma max_right_comm (a b c : ℕ) : max (max a b) c = max (max a c) b := by
+  rw [Nat.max_assoc, Nat.max_assoc, b.max_comm]
 
 end Nat

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "15d42e1a92a80d0db5ca1c12123866ba392b9d76",
+   "rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474",
+   "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "dff3a0ef1acdb1f34dd05dbaa41e620d22c6a3cf",
+   "rev": "895010aa7d965a703e0061d0acc9920664411a70",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -67,7 +67,7 @@
   {"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
-   "rev": "d812b96744f9b60879cbfa9c436de2b95003db2a",
+   "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -94,7 +94,7 @@
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "rev": "b61771aaa8f15bce5e3a38aebeb6dda487f4f29c",
+   "rev": "50b0f4db1f3e384a94f589ed36d24e509904d205",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",