Trigger CI for leanprover/lean4#4595

.github/workflows/lean4checker.yml

@@ -69,7 +69,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout v4.8.0
+          git checkout v4.9.0
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .

Archive/Imo/Imo1986Q5.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Data.Real.NNReal
+import Mathlib.Data.NNReal.Basic
 
 /-!
 # IMO 1986 Q5

Archive/Imo/Imo2008Q4.lean

@@ -5,7 +5,7 @@ Authors: Manuel Candales
 -/
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Real.Sqrt
-import Mathlib.Data.Real.NNReal
+import Mathlib.Data.NNReal.Basic
 import Mathlib.Tactic.LinearCombination
 
 #align_import imo.imo2008_q4 from "leanprover-community/mathlib"@"308826471968962c6b59c7ff82a22757386603e3"

Mathlib.lean

@@ -269,6 +269,7 @@ import Mathlib.Algebra.Group.WithOne.Basic
 import Mathlib.Algebra.Group.WithOne.Defs
 import Mathlib.Algebra.GroupPower.IterateHom
 import Mathlib.Algebra.GroupWithZero.Basic
+import Mathlib.Algebra.GroupWithZero.Center
 import Mathlib.Algebra.GroupWithZero.Commute
 import Mathlib.Algebra.GroupWithZero.Conj
 import Mathlib.Algebra.GroupWithZero.Defs
@@ -299,6 +300,7 @@ import Mathlib.Algebra.Homology.ConcreteCategory
 import Mathlib.Algebra.Homology.DerivedCategory.Basic
 import Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
 import Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
+import Mathlib.Algebra.Homology.DerivedCategory.ShortExact
 import Mathlib.Algebra.Homology.DifferentialObject
 import Mathlib.Algebra.Homology.Embedding.Basic
 import Mathlib.Algebra.Homology.Embedding.Extend
@@ -420,6 +422,7 @@ import Mathlib.Algebra.Module.GradedModule
 import Mathlib.Algebra.Module.Hom
 import Mathlib.Algebra.Module.Injective
 import Mathlib.Algebra.Module.LinearMap.Basic
+import Mathlib.Algebra.Module.LinearMap.Defs
 import Mathlib.Algebra.Module.LinearMap.End
 import Mathlib.Algebra.Module.LinearMap.Polynomial
 import Mathlib.Algebra.Module.LinearMap.Prod
@@ -1382,6 +1385,7 @@ import Mathlib.CategoryTheory.GlueData
 import Mathlib.CategoryTheory.GradedObject
 import Mathlib.CategoryTheory.GradedObject.Associator
 import Mathlib.CategoryTheory.GradedObject.Bifunctor
+import Mathlib.CategoryTheory.GradedObject.Monoidal
 import Mathlib.CategoryTheory.GradedObject.Single
 import Mathlib.CategoryTheory.GradedObject.Trifunctor
 import Mathlib.CategoryTheory.GradedObject.Unitor
@@ -1653,6 +1657,7 @@ import Mathlib.CategoryTheory.Sites.Coherent.Comparison
 import Mathlib.CategoryTheory.Sites.Coherent.Equivalence
 import Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
 import Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology
+import Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
 import Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent
 import Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular
 import Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
@@ -1701,6 +1706,7 @@ import Mathlib.CategoryTheory.Sites.Types
 import Mathlib.CategoryTheory.Sites.Whiskering
 import Mathlib.CategoryTheory.Skeletal
 import Mathlib.CategoryTheory.SmallObject.Construction
+import Mathlib.CategoryTheory.SmallObject.Iteration
 import Mathlib.CategoryTheory.Subobject.Basic
 import Mathlib.CategoryTheory.Subobject.Comma
 import Mathlib.CategoryTheory.Subobject.FactorThru
@@ -2150,6 +2156,8 @@ import Mathlib.Data.Multiset.Sym
 import Mathlib.Data.NNRat.BigOperators
 import Mathlib.Data.NNRat.Defs
 import Mathlib.Data.NNRat.Lemmas
+import Mathlib.Data.NNReal.Basic
+import Mathlib.Data.NNReal.Star
 import Mathlib.Data.Nat.Bits
 import Mathlib.Data.Nat.Bitwise
 import Mathlib.Data.Nat.Cast.Basic
@@ -2286,14 +2294,14 @@ import Mathlib.Data.Real.EReal
 import Mathlib.Data.Real.GoldenRatio
 import Mathlib.Data.Real.Hyperreal
 import Mathlib.Data.Real.Irrational
-import Mathlib.Data.Real.NNReal
 import Mathlib.Data.Real.Pi.Bounds
 import Mathlib.Data.Real.Pi.Leibniz
 import Mathlib.Data.Real.Pi.Wallis
 import Mathlib.Data.Real.Pointwise
 import Mathlib.Data.Real.Sign
 import Mathlib.Data.Real.Sqrt
 import Mathlib.Data.Real.Star
+import Mathlib.Data.Real.StarOrdered
 import Mathlib.Data.Rel
 import Mathlib.Data.SProd
 import Mathlib.Data.Semiquot
@@ -2511,6 +2519,7 @@ import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
 import Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
 import Mathlib.Geometry.Manifold.Metrizable
 import Mathlib.Geometry.Manifold.PartitionOfUnity
+import Mathlib.Geometry.Manifold.PoincareConjecture
 import Mathlib.Geometry.Manifold.Sheaf.Basic
 import Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
 import Mathlib.Geometry.Manifold.Sheaf.Smooth
@@ -3720,6 +3729,7 @@ import Mathlib.RingTheory.PowerSeries.Inverse
 import Mathlib.RingTheory.PowerSeries.Order
 import Mathlib.RingTheory.PowerSeries.Trunc
 import Mathlib.RingTheory.PowerSeries.WellKnown
+import Mathlib.RingTheory.Presentation
 import Mathlib.RingTheory.Prime
 import Mathlib.RingTheory.PrincipalIdealDomain
 import Mathlib.RingTheory.QuotSMulTop
@@ -3851,7 +3861,7 @@ import Mathlib.Tactic.Coe
 import Mathlib.Tactic.Common
 import Mathlib.Tactic.ComputeDegree
 import Mathlib.Tactic.Congr!
-import Mathlib.Tactic.Congrm
+import Mathlib.Tactic.CongrM
 import Mathlib.Tactic.Constructor
 import Mathlib.Tactic.Continuity
 import Mathlib.Tactic.Continuity.Init
@@ -3866,7 +3876,7 @@ import Mathlib.Tactic.DeriveToExpr
 import Mathlib.Tactic.DeriveTraversable
 import Mathlib.Tactic.Eqns
 import Mathlib.Tactic.Eval
-import Mathlib.Tactic.Existsi
+import Mathlib.Tactic.ExistsI
 import Mathlib.Tactic.Explode
 import Mathlib.Tactic.Explode.Datatypes
 import Mathlib.Tactic.Explode.Pretty
@@ -4030,9 +4040,9 @@ import Mathlib.Tactic.Variable
 import Mathlib.Tactic.WLOG
 import Mathlib.Tactic.Widget.Calc
 import Mathlib.Tactic.Widget.CommDiag
-import Mathlib.Tactic.Widget.Congrm
+import Mathlib.Tactic.Widget.CongrM
 import Mathlib.Tactic.Widget.Conv
-import Mathlib.Tactic.Widget.Gcongr
+import Mathlib.Tactic.Widget.GCongr
 import Mathlib.Tactic.Widget.SelectInsertParamsClass
 import Mathlib.Tactic.Widget.SelectPanelUtils
 import Mathlib.Tactic.Zify

Mathlib/Algebra/Algebra/Defs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
 import Mathlib.Algebra.BigOperators.Group.Finset
-import Mathlib.Algebra.Module.LinearMap.Basic
+import Mathlib.Algebra.Module.LinearMap.Defs
 import Mathlib.Data.Rat.Cast.Defs
 
 #align_import algebra.algebra.basic from "leanprover-community/mathlib"@"36b8aa61ea7c05727161f96a0532897bd72aedab"

Mathlib/Algebra/Group/Center.lean

@@ -5,7 +5,6 @@ Authors: Eric Wieser, Jireh Loreaux
 -/
 import Mathlib.Algebra.Group.Commute.Units
 import Mathlib.Algebra.Group.Invertible.Basic
-import Mathlib.Algebra.GroupWithZero.Units.Basic
 import Mathlib.Data.Set.Basic
 import Mathlib.Logic.Basic
 
@@ -28,6 +27,9 @@ We provide `Submonoid.center`, `AddSubmonoid.center`, `Subgroup.center`, `AddSub
 
 -/
 
+assert_not_exists Finset
+assert_not_exists MonoidWithZero
+assert_not_exists Subsemigroup
 
 variable {M : Type*}
 
@@ -162,14 +164,6 @@ theorem one_mem_center [MulOneClass M] : (1 : M) ∈ Set.center M where
 #align set.one_mem_center Set.one_mem_center
 #align set.zero_mem_add_center Set.zero_mem_addCenter
 
-@[simp]
-theorem zero_mem_center [MulZeroClass M] : (0 : M) ∈ Set.center M where
-  comm _ := by rw [zero_mul, mul_zero]
-  left_assoc _ _ := by rw [zero_mul, zero_mul, zero_mul]
-  mid_assoc _ _ := by rw [mul_zero, zero_mul, mul_zero]
-  right_assoc _ _ := by rw [mul_zero, mul_zero, mul_zero]
-#align set.zero_mem_center Set.zero_mem_center
-
 variable {M}
 
 @[to_additive (attr := simp) neg_mem_addCenter]
@@ -189,20 +183,6 @@ theorem subset_center_units [Monoid M] : ((↑) : Mˣ → M) ⁻¹' center M ⊆
 #align set.subset_center_units Set.subset_center_units
 #align set.subset_add_center_add_units Set.subset_addCenter_add_units
 
-theorem center_units_subset [GroupWithZero M] : Set.center Mˣ ⊆ ((↑) : Mˣ → M) ⁻¹' center M :=
-  fun _ ha => by
-    rw [mem_preimage, _root_.Semigroup.mem_center_iff]
-    intro b
-    obtain rfl | hb := eq_or_ne b 0
-    · rw [zero_mul, mul_zero]
-    · exact Units.ext_iff.mp (ha.comm (Units.mk0 b hb)).symm
-#align set.center_units_subset Set.center_units_subset
-
-/-- In a group with zero, the center of the units is the preimage of the center. -/
-theorem center_units_eq [GroupWithZero M] : Set.center Mˣ = ((↑) : Mˣ → M) ⁻¹' center M :=
-  Subset.antisymm center_units_subset subset_center_units
-#align set.center_units_eq Set.center_units_eq
-
 @[simp]
 theorem units_inv_mem_center [Monoid M] {a : Mˣ} (ha : ↑a ∈ Set.center M) :
     ↑a⁻¹ ∈ Set.center M := by
@@ -215,11 +195,6 @@ theorem invOf_mem_center [Monoid M] {a : M} [Invertible a] (ha : a ∈ Set.cente
   rw [Semigroup.mem_center_iff] at *
   exact (Commute.invOf_right <| ha ·)
 
-@[deprecated inv_mem_center (since := "2024-06-17")]
-theorem inv_mem_center₀ [GroupWithZero M] {a : M} (ha : a ∈ Set.center M) : a⁻¹ ∈ Set.center M :=
-  inv_mem_center ha
-#align set.inv_mem_center₀ Set.inv_mem_centerₓ
-
 @[to_additive (attr := simp) sub_mem_addCenter]
 theorem div_mem_center [DivisionMonoid M]
     {a b : M} (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) :
@@ -229,15 +204,4 @@ theorem div_mem_center [DivisionMonoid M]
 #align set.div_mem_center Set.div_mem_centerₓ
 #align set.sub_mem_add_center Set.sub_mem_addCenterₓ
 
-@[deprecated div_mem_center (since := "2024-06-17")]
-theorem div_mem_center₀ [GroupWithZero M] {a b : M} (ha : a ∈ Set.center M)
-    (hb : b ∈ Set.center M) : a / b ∈ Set.center M :=
-  div_mem_center ha hb
-#align set.div_mem_center₀ Set.div_mem_centerₓ
-
 end Set
-
--- Guard against import creep
-assert_not_exists Finset
-assert_not_exists Ring
-assert_not_exists Subsemigroup

Mathlib/Algebra/Group/Centralizer.lean

@@ -60,11 +60,6 @@ theorem one_mem_centralizer [MulOneClass M] : (1 : M) ∈ centralizer S := by
 #align set.one_mem_centralizer Set.one_mem_centralizer
 #align set.zero_mem_add_centralizer Set.zero_mem_addCentralizer
 
-@[simp]
-theorem zero_mem_centralizer [MulZeroClass M] : (0 : M) ∈ centralizer S := by
-  simp [mem_centralizer_iff]
-#align set.zero_mem_centralizer Set.zero_mem_centralizer
-
 variable {S} {a b : M}
 
 @[to_additive (attr := simp) add_mem_addCentralizer]
@@ -80,16 +75,6 @@ theorem inv_mem_centralizer [Group M] (ha : a ∈ centralizer S) : a⁻¹ ∈ ce
 #align set.inv_mem_centralizer Set.inv_mem_centralizer
 #align set.neg_mem_add_centralizer Set.neg_mem_addCentralizer
 
-@[simp]
-theorem inv_mem_centralizer₀ [GroupWithZero M] (ha : a ∈ centralizer S) : a⁻¹ ∈ centralizer S :=
-  (eq_or_ne a 0).elim
-    (fun h => by
-      rw [h, inv_zero]
-      exact zero_mem_centralizer S)
-    fun ha0 c hc => by
-    rw [mul_inv_eq_iff_eq_mul₀ ha0, mul_assoc, eq_inv_mul_iff_mul_eq₀ ha0, ha c hc]
-#align set.inv_mem_centralizer₀ Set.inv_mem_centralizer₀
-
 @[to_additive (attr := simp) sub_mem_addCentralizer]
 theorem div_mem_centralizer [Group M] (ha : a ∈ centralizer S) (hb : b ∈ centralizer S) :
     a / b ∈ centralizer S := by
@@ -98,13 +83,6 @@ theorem div_mem_centralizer [Group M] (ha : a ∈ centralizer S) (hb : b ∈ cen
 #align set.div_mem_centralizer Set.div_mem_centralizer
 #align set.sub_mem_add_centralizer Set.sub_mem_addCentralizer
 
-@[simp]
-theorem div_mem_centralizer₀ [GroupWithZero M] (ha : a ∈ centralizer S) (hb : b ∈ centralizer S) :
-    a / b ∈ centralizer S := by
-  rw [div_eq_mul_inv]
-  exact mul_mem_centralizer ha (inv_mem_centralizer₀ hb)
-#align set.div_mem_centralizer₀ Set.div_mem_centralizer₀
-
 @[to_additive addCentralizer_subset]
 theorem centralizer_subset [Mul M] (h : S ⊆ T) : centralizer T ⊆ centralizer S := fun _ ht s hs =>
   ht s (h hs)

Mathlib/Algebra/Group/Fin.lean

@@ -106,8 +106,7 @@ lemma lt_sub_one_iff {k : Fin (n + 2)} : k < k - 1 ↔ k = 0 := by
   · simp only [zero_eta, zero_sub, lt_iff_val_lt_val, val_zero, coe_neg_one, zero_lt_succ]
   have : (n + 1 + (k + 1)) % (n + 2) = k % (n + 2) := by
     rw [Nat.add_comm, Nat.add_right_comm, Nat.add_assoc, Nat.add_assoc, add_mod_right]
-  simp [lt_iff_val_lt_val, ext_iff, Fin.coe_sub, succ_eq_add_one, this,
-    mod_eq_of_lt ((lt_succ_self _).trans hk)]
+  simp [lt_iff_val_lt_val, ext_iff, Fin.coe_sub, this, mod_eq_of_lt ((lt_succ_self _).trans hk)]
 #align fin.lt_sub_one_iff Fin.lt_sub_one_iff
 
 @[simp] lemma le_sub_one_iff {k : Fin (n + 1)} : k ≤ k - 1 ↔ k = 0 := by

Mathlib/Algebra/GroupWithZero/Center.lean

@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2021 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser, Jireh Loreaux
+-/
+import Mathlib.Algebra.Group.Centralizer
+import Mathlib.Algebra.GroupWithZero.Units.Basic
+
+#align_import group_theory.subsemigroup.center from "leanprover-community/mathlib"@"1ac8d4304efba9d03fa720d06516fac845aa5353"
+
+/-!
+# Center of a group with zero
+-/
+
+assert_not_exists Finset
+assert_not_exists Ring
+assert_not_exists Subsemigroup
+
+variable {M₀ G₀ : Type*}
+
+namespace Set
+section MulZeroClass
+variable [MulZeroClass M₀] {s : Set M₀}
+
+variable (M₀) in
+@[simp] theorem zero_mem_center : (0 : M₀) ∈ center M₀ where
+  comm _ := by rw [zero_mul, mul_zero]
+  left_assoc _ _ := by rw [zero_mul, zero_mul, zero_mul]
+  mid_assoc _ _ := by rw [mul_zero, zero_mul, mul_zero]
+  right_assoc _ _ := by rw [mul_zero, mul_zero, mul_zero]
+#align set.zero_mem_center Set.zero_mem_center
+
+variable (s) in
+@[simp] theorem zero_mem_centralizer : (0 : M₀) ∈ centralizer s := by simp [mem_centralizer_iff]
+#align set.zero_mem_centralizer Set.zero_mem_centralizer
+
+end MulZeroClass
+
+section GroupWithZero
+variable [GroupWithZero G₀] {s : Set G₀} {a b : G₀}
+
+theorem center_units_subset : Set.center G₀ˣ ⊆ ((↑) : G₀ˣ → G₀) ⁻¹' center G₀ :=
+  fun _ ha => by
+    rw [mem_preimage, _root_.Semigroup.mem_center_iff]
+    intro b
+    obtain rfl | hb := eq_or_ne b 0
+    · rw [zero_mul, mul_zero]
+    · exact Units.ext_iff.mp (ha.comm (Units.mk0 b hb)).symm
+#align set.center_units_subset Set.center_units_subset
+
+/-- In a group with zero, the center of the units is the preimage of the center. -/
+theorem center_units_eq : center G₀ˣ = ((↑) : G₀ˣ → G₀) ⁻¹' center G₀ :=
+  Subset.antisymm center_units_subset subset_center_units
+#align set.center_units_eq Set.center_units_eq
+
+@[simp] theorem inv_mem_centralizer₀ (ha : a ∈ centralizer s) : a⁻¹ ∈ centralizer s :=
+  (eq_or_ne a 0).elim
+    (fun h => by
+      rw [h, inv_zero]
+      exact zero_mem_centralizer s)
+    fun ha0 c hc => by
+    rw [mul_inv_eq_iff_eq_mul₀ ha0, mul_assoc, eq_inv_mul_iff_mul_eq₀ ha0, ha c hc]
+#align set.inv_mem_centralizer₀ Set.inv_mem_centralizer₀
+
+@[simp] theorem div_mem_centralizer₀ (ha : a ∈ centralizer s) (hb : b ∈ centralizer s) :
+    a / b ∈ centralizer s := by
+  rw [div_eq_mul_inv]
+  exact mul_mem_centralizer ha (inv_mem_centralizer₀ hb)
+#align set.div_mem_centralizer₀ Set.div_mem_centralizer₀
+
+@[deprecated inv_mem_center (since := "2024-06-17")]
+theorem inv_mem_center₀ (ha : a ∈ Set.center G₀) : a⁻¹ ∈ Set.center G₀ :=
+  inv_mem_center ha
+#align set.inv_mem_center₀ Set.inv_mem_centerₓ
+
+@[deprecated div_mem_center (since := "2024-06-17")]
+theorem div_mem_center₀ (ha : a ∈ Set.center G₀) (hb : b ∈ Set.center G₀) : a / b ∈ Set.center G₀ :=
+  div_mem_center ha hb
+#align set.div_mem_center₀ Set.div_mem_centerₓ
+
+end GroupWithZero
+end Set