Merge branch 'nightly-testing' of https://github.com/leanprover-community/mathlib4-nightly-testing into nightly-testing

Author: kim-em

Mathlib.lean

@@ -899,6 +899,7 @@ public import Mathlib.Algebra.Order.Antidiag.Pi
 public import Mathlib.Algebra.Order.Antidiag.Prod
 public import Mathlib.Algebra.Order.Archimedean.Basic
 public import Mathlib.Algebra.Order.Archimedean.Class
+public import Mathlib.Algebra.Order.Archimedean.Defs
 public import Mathlib.Algebra.Order.Archimedean.Hom
 public import Mathlib.Algebra.Order.Archimedean.IndicatorCard
 public import Mathlib.Algebra.Order.Archimedean.Submonoid
@@ -1493,6 +1494,7 @@ public import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiM
 public import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
 public import Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
 public import Mathlib.AlgebraicTopology.SimplexCategory.Rev
+public import Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
 public import Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
 public import Mathlib.AlgebraicTopology.SimplexCategory.Truncated
 public import Mathlib.AlgebraicTopology.SimplicialCategory.Basic
@@ -1536,8 +1538,10 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
 public import Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
 public import Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
 public import Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
+public import Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
 public import Mathlib.AlgebraicTopology.SimplicialSet.Op
 public import Mathlib.AlgebraicTopology.SimplicialSet.Path
+public import Mathlib.AlgebraicTopology.SimplicialSet.PiZero
 public import Mathlib.AlgebraicTopology.SimplicialSet.Presentable
 public import Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
 public import Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
@@ -6229,6 +6233,7 @@ public import Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
 public import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
 public import Mathlib.RingTheory.AlgebraicIndependent.Transcendental
 public import Mathlib.RingTheory.Artinian.Algebra
+public import Mathlib.RingTheory.Artinian.Defs
 public import Mathlib.RingTheory.Artinian.Instances
 public import Mathlib.RingTheory.Artinian.Module
 public import Mathlib.RingTheory.Artinian.Ring
@@ -6243,6 +6248,7 @@ public import Mathlib.RingTheory.Binomial
 public import Mathlib.RingTheory.ChainOfDivisors
 public import Mathlib.RingTheory.ClassGroup
 public import Mathlib.RingTheory.Coalgebra.Basic
+public import Mathlib.RingTheory.Coalgebra.CoassocSimps
 public import Mathlib.RingTheory.Coalgebra.Convolution
 public import Mathlib.RingTheory.Coalgebra.Equiv
 public import Mathlib.RingTheory.Coalgebra.GroupLike

Mathlib/Algebra/Algebra/Equiv.lean

@@ -69,9 +69,6 @@ def toAlgEquiv {F R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Alg
     [Algebra R B] [EquivLike F A B] [AlgEquivClass F R A B] (f : F) : A ≃ₐ[R] B :=
   { (f : A ≃ B), (f : A ≃+* B) with commutes' := commutes f }
 
-instance (F R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
-    [EquivLike F A B] [AlgEquivClass F R A B] : CoeTC F (A ≃ₐ[R] B) :=
-  ⟨toAlgEquiv⟩
 end AlgEquivClass
 
 namespace AlgEquiv
@@ -137,7 +134,7 @@ theorem toEquiv_eq_coe : e.toEquiv = e :=
 
 @[simp]
 protected theorem coe_coe {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) :
-    ⇑(f : A₁ ≃ₐ[R] A₂) = f :=
+    ⇑(AlgEquivClass.toAlgEquiv f) = f :=
   rfl
 
 theorem coe_fun_injective : @Function.Injective (A₁ ≃ₐ[R] A₂) (A₁ → A₂) fun e => (e : A₁ → A₂) :=
@@ -255,13 +252,13 @@ theorem invFun_eq_symm {e : A₁ ≃ₐ[R] A₂} : e.invFun = e.symm :=
 @[simp]
 theorem coe_apply_coe_coe_symm_apply {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂]
     (f : F) (x : A₂) :
-    f ((f : A₁ ≃ₐ[R] A₂).symm x) = x :=
+    f ((AlgEquivClass.toAlgEquiv f).symm x) = x :=
   EquivLike.right_inv f x
 
 @[simp]
 theorem coe_coe_symm_apply_coe_apply {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂]
     (f : F) (x : A₁) :
-    (f : A₁ ≃ₐ[R] A₂).symm (f x) = x :=
+    (AlgEquivClass.toAlgEquiv f).symm (f x) = x :=
   EquivLike.left_inv f x
 
 /-- `simp` normal form of `invFun_eq_symm` -/

Mathlib/Algebra/Algebra/Spectrum/Basic.lean

@@ -424,7 +424,7 @@ theorem AlgEquiv.spectrum_eq {F R A B : Type*} [CommSemiring R] [Ring A] [Ring B
     spectrum R (f a) = spectrum R a :=
   Set.Subset.antisymm (AlgHom.spectrum_apply_subset _ _) <| by
     simpa only [AlgEquiv.coe_algHom, AlgEquiv.coe_coe_symm_apply_coe_apply] using
-      AlgHom.spectrum_apply_subset (f : A ≃ₐ[R] B).symm (f a)
+      AlgHom.spectrum_apply_subset (AlgEquivClass.toAlgEquiv f : A ≃ₐ[R] B).symm (f a)
 
 section ConjugateUnits
 

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -78,12 +78,12 @@ theorem prod_Icc_succ_top {a b : ℕ} (hab : a ≤ b + 1) (f : ℕ → M) :
 @[to_additive]
 theorem prod_range_mul_prod_Ico (f : ℕ → M) {m n : ℕ} (h : m ≤ n) :
     ((∏ k ∈ range m, f k) * ∏ k ∈ Ico m n, f k) = ∏ k ∈ range n, f k :=
-  Nat.Ico_zero_eq_range ▸ Nat.Ico_zero_eq_range ▸ prod_Ico_consecutive f m.zero_le h
+  Nat.Ico_zero_eq_range m ▸ Nat.Ico_zero_eq_range n ▸ prod_Ico_consecutive f m.zero_le h
 
 @[to_additive]
 theorem prod_range_eq_mul_Ico (f : ℕ → M) {n : ℕ} (hn : 0 < n) :
     ∏ x ∈ Finset.range n, f x = f 0 * ∏ x ∈ Ico 1 n, f x :=
-  Finset.range_eq_Ico ▸ Finset.prod_eq_prod_Ico_succ_bot hn f
+  Finset.range_eq_Ico n ▸ Finset.prod_eq_prod_Ico_succ_bot hn f
 
 @[to_additive]
 theorem prod_Ico_eq_mul_inv {δ : Type*} [CommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) :

Mathlib/Algebra/BigOperators/Module.lean

@@ -59,7 +59,8 @@ theorem sum_range_by_parts :
       f (n - 1) • G n - ∑ i ∈ range (n - 1), (f (i + 1) - f i) • G (i + 1) := by
   by_cases hn : n = 0
   · simp [hn]
-  · rw [range_eq_Ico, sum_Ico_by_parts f g (Nat.pos_of_ne_zero hn), sum_range_zero, smul_zero,
-      sub_zero, range_eq_Ico]
+  · simp only [range_eq_Ico]
+    rw [sum_Ico_by_parts f g (Nat.pos_of_ne_zero hn), sum_range_zero, smul_zero, sub_zero]
+    simp only [← range_eq_Ico]
 
 end Finset

Mathlib/Algebra/Exact.lean

@@ -92,7 +92,7 @@ lemma iff_rangeFactorization [One P] (hg : 1 ∈ Set.range g) :
     MulExact f g ↔ MulExact ((↑) : Set.range f → N) (Set.rangeFactorization g) := by
   letI : One (Set.range g) := ⟨⟨1, hg⟩⟩
   have : ((1 : Set.range g) : P) = 1 := rfl
-  simp [MulExact, Set.rangeFactorization, Subtype.ext_iff, this]
+  simp [MulExact, Subtype.ext_iff, this]
 
 /-- If two maps `f : M → N` and `g : N → P` are exact, then the induced maps
 `Set.range f → N → Set.range g` are exact.
@@ -430,8 +430,7 @@ def Exact.splitInjectiveEquiv
     · intro x y e
       simp only [prod_apply, Pi.prod, Prod.mk.injEq] at e
       obtain ⟨z, hz⟩ := (h (x - y)).mp (by simpa [sub_eq_zero] using e.2)
-      suffices z = 0 by rw [← sub_eq_zero, ← hz, this, map_zero]
-      rw [← h₁ z, hz, map_sub, e.1, sub_self]
+      rw [← sub_eq_zero, ← hz, ← h₁ z, hz, map_sub, e.1, sub_self, map_zero]
     · rintro ⟨x, y⟩
       obtain ⟨y, rfl⟩ := hg y
       refine ⟨f x + y - f (l.1 y), by ext <;> simp [h₁, h₂]⟩

Mathlib/Algebra/Module/Torsion/Basic.lean

@@ -534,9 +534,8 @@ namespace Module
 variable [Ring R] [AddCommGroup M] [Module R M]
 variable {I : Ideal R} {r : R}
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- can't be an instance because `hM` can't be inferred -/
+@[implicit_reducible]
 def IsTorsionBySet.hasSMul (hM : IsTorsionBySet R M I) : SMul (R ⧸ I) M where
   smul b := QuotientAddGroup.lift I.toAddSubgroup (smulAddHom R M)
     (by rwa [isTorsionBySet_iff_subset_annihilator] at hM) b
@@ -557,17 +556,16 @@ theorem IsTorsionBy.mk_smul [(Ideal.span {r}).IsTwoSided] (hM : IsTorsionBy R M
     Ideal.Quotient.mk (Ideal.span {r}) b • x = b • x :=
   rfl
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- An `(R ⧸ I)`-module is an `R`-module which `IsTorsionBySet R M I`. -/
+@[implicit_reducible]
 def IsTorsionBySet.module [I.IsTwoSided] (hM : IsTorsionBySet R M I) : Module (R ⧸ I) M :=
-  letI := hM.hasSMul; I.mkQ_surjective.moduleLeft _ (IsTorsionBySet.mk_smul hM)
+  letI := hM.hasSMul; fast_instance% I.mkQ_surjective.moduleLeft _ (IsTorsionBySet.mk_smul hM)
 
 instance IsTorsionBySet.isScalarTower [I.IsTwoSided] (hM : IsTorsionBySet R M I)
     {S : Type*} [SMul S R] [SMul S M] [IsScalarTower S R M] [IsScalarTower S R R] :
-    @IsScalarTower S (R ⧸ I) M _ (IsTorsionBySet.module hM).toSMul _ :=
+    @IsScalarTower S (R ⧸ I) M _ hM.hasSMul _ :=
   -- Porting note: still needed to be fed the Module R / I M instance
-  @IsScalarTower.mk S (R ⧸ I) M _ (IsTorsionBySet.module hM).toSMul _
+  @IsScalarTower.mk S (R ⧸ I) M _ hM.hasSMul _
     (fun b d x => Quotient.inductionOn' d fun c => (smul_assoc b c x :))
 
 /-- If an `R`-module `M` is annihilated by a two-sided ideal `I`, then the identity is a semilinear
@@ -580,20 +578,19 @@ def IsTorsionBySet.semilinearMap [I.IsTwoSided] (hM : IsTorsionBySet R M I) :
     map_smul' := fun _ _ ↦ rfl }
 
 theorem IsTorsionBySet.isSemisimpleModule_iff [I.IsTwoSided]
-    (hM : Module.IsTorsionBySet R M I) : let _ := hM.module
+    (hM : Module.IsTorsionBySet R M I) : letI := hM.module
     IsSemisimpleModule (R ⧸ I) M ↔ IsSemisimpleModule R M :=
-  let _ := hM.module
+  letI := hM.module
   (hM.semilinearMap.isSemisimpleModule_iff_of_bijective Function.bijective_id).symm
 
 /-- An `(R ⧸ Ideal.span {r})`-module is an `R`-module for which `IsTorsionBy R M r`. -/
 abbrev IsTorsionBy.module [h : (Ideal.span {r}).IsTwoSided] (hM : IsTorsionBy R M r) :
     Module (R ⧸ Ideal.span {r}) M := by
   rw [Ideal.span] at h; exact ((isTorsionBySet_span_singleton_iff r).mpr hM).module
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- Any module is also a module over the quotient of the ring by the annihilator.
 Not an instance because it causes synthesis failures / timeouts. -/
+@[implicit_reducible]
 def quotientAnnihilator : Module (R ⧸ Module.annihilator R M) M :=
   (isTorsionBySet_annihilator R M).module
 
@@ -989,9 +986,8 @@ lemma torsionBy.mod_self_nsmul' (s : ℕ) {x : A} (h : x ∈ A[n]) :
     s • x = (s % n) • x :=
   nsmul_eq_mod_nsmul s (torsionBy.nsmul_iff.mp h)
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- For a natural number `n`, the `n`-torsion subgroup of `A` is a `ZMod n` module. -/
+@[implicit_reducible]
 def torsionBy.zmodModule : Module (ZMod n) A[n] :=
   AddCommGroup.zmodModule torsionBy.nsmul
 

Mathlib/Algebra/Order/Archimedean/Basic.lean

@@ -5,28 +5,27 @@ Authors: Mario Carneiro
 -/
 module
 
+public import Mathlib.Algebra.Field.Defs
+public import Mathlib.Algebra.Order.Archimedean.Defs
 public import Mathlib.Algebra.Order.Floor.Semiring
-public import Mathlib.Algebra.Order.Monoid.Units
-public import Mathlib.Algebra.Order.Ring.Pow
-public import Mathlib.Data.Int.LeastGreatest
+public import Mathlib.Order.Directed
 public import Mathlib.Data.Rat.Floor
+
 import Mathlib.Algebra.Order.Group.Basic
+import Mathlib.Algebra.Order.Monoid.Units
+import Mathlib.Algebra.Order.Ring.Pow
+import Mathlib.Data.Int.LeastGreatest
 
 /-!
-# Archimedean groups and fields.
+# Archimedean groups and fields
 
-This file defines the archimedean property for ordered groups and proves several results connected
-to this notion. Being archimedean means that for all elements `x` and `y>0` there exists a natural
-number `n` such that `x ≤ n • y`.
+This file proves several results connected to the notion of Archimedean groups. Being Archimedean
+means that for all elements `x` and `y > 0` there exists a natural number `n` such that `x ≤ n • y`.
 
 ## Main definitions
 
-* `Archimedean` is a typeclass for an ordered additive commutative monoid to have the archimedean
-  property.
-* `MulArchimedean` is a typeclass for an ordered commutative monoid to have the "mul-archimedean
-  property" where for `x` and `y > 1`, there exists a natural number `n` such that `x ≤ y ^ n`.
-* `Archimedean.floorRing` defines a floor function on an archimedean linearly ordered ring making
-  it into a `floorRing`.
+* `Archimedean.floorRing` defines a floor function on an archimedean linearly ordered ring making it
+  into a `floorRing`.
 
 ## Main statements
 
@@ -41,25 +40,6 @@ open Int Set
 
 variable {G M R K : Type*}
 
-/-- An ordered additive commutative monoid is called `Archimedean` if for any two elements `x`, `y`
-such that `0 < y`, there exists a natural number `n` such that `x ≤ n • y`. -/
-class Archimedean (M) [AddCommMonoid M] [PartialOrder M] : Prop where
-  /-- For any two elements `x`, `y` such that `0 < y`, there exists a natural number `n`
-  such that `x ≤ n • y`. -/
-  arch : ∀ (x : M) {y : M}, 0 < y → ∃ n : ℕ, x ≤ n • y
-
-section MulArchimedean
-
-/-- An ordered commutative monoid is called `MulArchimedean` if for any two elements `x`, `y`
-such that `1 < y`, there exists a natural number `n` such that `x ≤ y ^ n`. -/
-@[to_additive Archimedean]
-class MulArchimedean (M) [CommMonoid M] [PartialOrder M] : Prop where
-  /-- For any two elements `x`, `y` such that `1 < y`, there exists a natural number `n`
-  such that `x ≤ y ^ n`. -/
-  arch : ∀ (x : M) {y : M}, 1 < y → ∃ n : ℕ, x ≤ y ^ n
-
-end MulArchimedean
-
 @[to_additive]
 lemma MulArchimedean.comap [CommMonoid G] [LinearOrder G] [CommMonoid M] [PartialOrder M]
     [MulArchimedean M] (f : G →* M) (hf : StrictMono f) :
@@ -85,13 +65,7 @@ instance Multiplicative.instMulArchimedean [AddCommGroup G] [PartialOrder G] [Ar
     MulArchimedean (Multiplicative G) :=
   ⟨fun x _ hy ↦ Archimedean.arch x.toAdd hy⟩
 
-@[to_additive]
-theorem exists_lt_pow [CommMonoid M] [PartialOrder M] [MulArchimedean M] [MulLeftStrictMono M]
-    {a : M} (ha : 1 < a) (b : M) : ∃ n : ℕ, b < a ^ n :=
-  let ⟨k, hk⟩ := MulArchimedean.arch b ha
-  ⟨k + 1, hk.trans_lt <| pow_lt_pow_right' ha k.lt_succ_self⟩
-
-section LinearOrderedCommGroup
+section IsOrderedMonoid
 
 variable [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G]
 
@@ -152,21 +126,12 @@ theorem existsUnique_sub_zpow_mem_Ioc {a : G} (ha : 1 < a) (b c : G) :
     simpa only [Equiv.neg_apply, zpow_neg, div_inv_eq_mul] using
       existsUnique_add_zpow_mem_Ioc ha b c
 
-@[to_additive]
-theorem exists_pow_lt {a : G} (ha : a < 1) (b : G) : ∃ n : ℕ, a ^ n < b :=
-  (exists_lt_pow (one_lt_inv'.mpr ha) b⁻¹).imp <| by simp
-
-end LinearOrderedCommGroup
+end IsOrderedMonoid
 
 section OrderedSemiring
 
 variable [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R]
 
-theorem exists_nat_ge (x : R) :
-    ∃ n : ℕ, x ≤ n := by
-  nontriviality R
-  exact (Archimedean.arch x one_pos).imp fun n h => by rwa [← nsmul_one]
-
 instance (priority := 100) : IsDirectedOrder R :=
   ⟨fun x y ↦
     let ⟨m, hm⟩ := exists_nat_ge x; let ⟨n, hn⟩ := exists_nat_ge y
@@ -178,9 +143,6 @@ end OrderedSemiring
 section StrictOrderedSemiring
 variable [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {y : R}
 
-lemma exists_nat_gt (x : R) : ∃ n : ℕ, x < n :=
-  (exists_lt_nsmul zero_lt_one x).imp fun n hn ↦ by rwa [← nsmul_one]
-
 theorem add_one_pow_unbounded_of_pos (x : R) (hy : 0 < y) : ∃ n : ℕ, x < (y + 1) ^ n :=
   have : 0 ≤ 1 + y := add_nonneg zero_le_one hy.le
   (Archimedean.arch x hy).imp fun n h ↦
@@ -204,11 +166,6 @@ section OrderedRing
 
 variable [Ring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R]
 
-theorem exists_int_ge (x : R) : ∃ n : ℤ, x ≤ n := let ⟨n, h⟩ := exists_nat_ge x; ⟨n, mod_cast h⟩
-
-theorem exists_int_le (x : R) : ∃ n : ℤ, n ≤ x :=
-  let ⟨n, h⟩ := exists_int_ge (-x); ⟨-n, by simpa [neg_le] using h⟩
-
 instance (priority := 100) : IsCodirectedOrder R where
   directed a b :=
     let ⟨m, hm⟩ := exists_int_le a; let ⟨n, hn⟩ := exists_int_le b
@@ -220,14 +177,6 @@ end OrderedRing
 section StrictOrderedRing
 variable [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R]
 
-theorem exists_int_gt (x : R) : ∃ n : ℤ, x < n :=
-  let ⟨n, h⟩ := exists_nat_gt x
-  ⟨n, by rwa [Int.cast_natCast]⟩
-
-theorem exists_int_lt (x : R) : ∃ n : ℤ, (n : R) < x :=
-  let ⟨n, h⟩ := exists_int_gt (-x)
-  ⟨-n, by rw [Int.cast_neg]; exact neg_lt.1 h⟩
-
 /-- See `exists_floor'` for a more general version which only assumes the element is bounded by
 two integers. -/
 theorem exists_floor (x : R) : ∃ fl : ℤ, ∀ z : ℤ, z ≤ fl ↔ (z : R) ≤ x := by