chore: bump toolchain to v4.13.0-rc1 (#17377)

This merges the already reviewed `bump/v4.13.0` branch. Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
leanprover-community · Oct 3, 2024 · f641187 · f641187
1 parent 3ca1060
commit f641187
Show file tree

Hide file tree

Showing 232 changed files with 809 additions and 761 deletions.
diff --git a/Archive/Examples/IfNormalization/WithoutAesop.lean b/Archive/Examples/IfNormalization/WithoutAesop.lean
@@ -92,8 +92,8 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
               · simp_all
         · have := ht₃ v
           have := he₃ v
-          simp_all? says simp_all only [normalized, Bool.and_eq_true, Bool.not_eq_true',
-              AList.lookup_insert_eq_none, ne_eq, AList.lookup_insert]
+          simp_all? says simp_all only [normalized, Bool.and_eq_true, Bool.not_eq_eq_eq_not,
+              Bool.not_true, AList.lookup_insert_eq_none, ne_eq, AList.lookup_insert]
           obtain ⟨⟨⟨tn, tc⟩, tr⟩, td⟩ := ht₂
           split <;> rename_i h'
           · subst h'
@@ -103,9 +103,9 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
           have := he₃ w
           by_cases h : w = v
           · subst h; simp_all
-          · simp_all? says simp_all only [normalized, Bool.and_eq_true, Bool.not_eq_true',
-              AList.lookup_insert_eq_none, ne_eq, not_false_eq_true, AList.lookup_insert_ne,
-              implies_true]
+          · simp_all? says simp_all only [normalized, Bool.and_eq_true, Bool.not_eq_eq_eq_not,
+              Bool.not_true, AList.lookup_insert_eq_none, ne_eq, not_false_eq_true,
+              AList.lookup_insert_ne, implies_true]
             obtain ⟨⟨⟨en, ec⟩, er⟩, ed⟩ := he₂
             split at b <;> rename_i h'
             · subst h'; simp_all

diff --git a/Cache/IO.lean b/Cache/IO.lean
@@ -338,7 +338,7 @@ def packCache (hashMap : HashMap) (overwrite verbose unpackedOnly : Bool)
 /-- Gets the set of all cached files -/
 def getLocalCacheSet : IO <| Lean.RBTree String compare := do
   let paths ← getFilesWithExtension CACHEDIR "ltar"
-  return .fromList (paths.data.map (·.withoutParent CACHEDIR |>.toString)) _
+  return .fromList (paths.toList.map (·.withoutParent CACHEDIR |>.toString)) _
 
 def isPathFromMathlib (path : FilePath) : Bool :=
   match path.components with

diff --git a/Cache/Requests.lean b/Cache/Requests.lean
@@ -184,7 +184,7 @@ def UPLOAD_URL : String :=
 /-- Formats the config file for `curl`, containing the list of files to be uploaded -/
 def mkPutConfigContent (fileNames : Array String) (token : String) : IO String := do
   let token := if useFROCache then "" else s!"?{token}" -- the FRO cache doesn't pass the token here
-  let l ← fileNames.data.mapM fun fileName : String => do
+  let l ← fileNames.toList.mapM fun fileName : String => do
     pure s!"-T {(IO.CACHEDIR / fileName).toString}\nurl = {mkFileURL UPLOAD_URL fileName}{token}"
   return "\n".intercalate l
 

diff --git a/Mathlib/Algebra/AddTorsor.lean b/Mathlib/Algebra/AddTorsor.lean
@@ -248,7 +248,6 @@ instance instAddTorsor : AddTorsor (G × G') (P × P') where
   zero_vadd _ := Prod.ext (zero_vadd _ _) (zero_vadd _ _)
   add_vadd _ _ _ := Prod.ext (add_vadd _ _ _) (add_vadd _ _ _)
   vsub p₁ p₂ := (p₁.1 -ᵥ p₂.1, p₁.2 -ᵥ p₂.2)
-  nonempty := Prod.instNonempty
   vsub_vadd' _ _ := Prod.ext (vsub_vadd _ _) (vsub_vadd _ _)
   vadd_vsub' _ _ := Prod.ext (vadd_vsub _ _) (vadd_vsub _ _)
 

diff --git a/Mathlib/Algebra/BigOperators/Group/List.lean b/Mathlib/Algebra/BigOperators/Group/List.lean
@@ -125,7 +125,7 @@ theorem prod_replicate (n : ℕ) (a : M) : (replicate n a).prod = a ^ n := by
 
 @[to_additive sum_eq_card_nsmul]
 theorem prod_eq_pow_card (l : List M) (m : M) (h : ∀ x ∈ l, x = m) : l.prod = m ^ l.length := by
-  rw [← prod_replicate, ← List.eq_replicate.mpr ⟨rfl, h⟩]
+  rw [← prod_replicate, ← List.eq_replicate_iff.mpr ⟨rfl, h⟩]
 
 @[to_additive]
 theorem prod_hom_rel (l : List ι) {r : M → N → Prop} {f : ι → M} {g : ι → N} (h₁ : r 1 1)
@@ -639,20 +639,15 @@ lemma ranges_join (l : List ℕ) : l.ranges.join = range l.sum := by simp [range
 lemma mem_mem_ranges_iff_lt_sum (l : List ℕ) {n : ℕ} :
     (∃ s ∈ l.ranges, n ∈ s) ↔ n < l.sum := by simp [mem_mem_ranges_iff_lt_natSum]
 
-lemma countP_join (p : α → Bool) : ∀ L : List (List α), countP p L.join = (L.map (countP p)).sum
-  | [] => rfl
-  | a :: l => by rw [join, countP_append, map_cons, sum_cons, countP_join _ l]
-
-lemma count_join [BEq α] (L : List (List α)) (a : α) : L.join.count a = (L.map (count a)).sum :=
-  countP_join _ _
-
 @[simp]
 theorem length_bind (l : List α) (f : α → List β) :
     length (List.bind l f) = sum (map (length ∘ f) l) := by
   rw [List.bind, length_join, map_map, Nat.sum_eq_listSum]
 
 lemma countP_bind (p : β → Bool) (l : List α) (f : α → List β) :
-    countP p (l.bind f) = sum (map (countP p ∘ f) l) := by rw [List.bind, countP_join, map_map]
+    countP p (l.bind f) = sum (map (countP p ∘ f) l) := by
+  rw [List.bind, countP_join, map_map]
+  simp
 
 lemma count_bind [BEq β] (l : List α) (f : α → List β) (x : β) :
     count x (l.bind f) = sum (map (count x ∘ f) l) := countP_bind _ _ _

diff --git a/Mathlib/Algebra/CharZero/Defs.lean b/Mathlib/Algebra/CharZero/Defs.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Data.Int.Cast.Defs
-import Mathlib.Algebra.NeZero
 import Mathlib.Logic.Function.Basic
 
 /-!

diff --git a/Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean b/Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
@@ -166,9 +166,6 @@ theorem succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq :
         gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) =
           convs'Aux (squashSeq s (m + 1)) (m + 2)
         by simpa only [convs'Aux, s_head_eq]
-      have : convs'Aux s.tail (m + 2) = convs'Aux (squashSeq s.tail m) (m + 1) := by
-        refine IH gp_succ_n ?_
-        simpa [Stream'.Seq.get?_tail] using s_succ_nth_eq
       have : (squashSeq s (m + 1)).head = some gp_head :=
         (squashSeq_nth_of_lt m.succ_pos).trans s_head_eq
       simp_all [convs'Aux, squashSeq_succ_n_tail_eq_squashSeq_tail_n]

diff --git a/Mathlib/Algebra/Field/Defs.lean b/Mathlib/Algebra/Field/Defs.lean
@@ -45,8 +45,8 @@ field, division ring, skew field, skew-field, skewfield
 
 assert_not_imported Mathlib.Tactic.Common
 
--- `NeZero` should not be needed in the basic algebraic hierarchy.
-assert_not_exists NeZero
+-- `NeZero` theory should not be needed in the basic algebraic hierarchy
+assert_not_imported Mathlib.Algebra.NeZero
 
 assert_not_exists MonoidHom
 

diff --git a/Mathlib/Algebra/Free.lean b/Mathlib/Algebra/Free.lean
@@ -6,7 +6,6 @@ Authors: Kenny Lau
 import Mathlib.Algebra.Group.Equiv.Basic
 import Mathlib.Control.Applicative
 import Mathlib.Control.Traversable.Basic
-import Mathlib.Data.List.Basic
 import Mathlib.Logic.Equiv.Defs
 import Mathlib.Tactic.AdaptationNote
 

diff --git a/Mathlib/Algebra/Group/Hom/Basic.lean b/Mathlib/Algebra/Group/Hom/Basic.lean
@@ -14,7 +14,7 @@ import Mathlib.Algebra.Group.Hom.Defs
 
 -- `NeZero` cannot be additivised, hence its theory should be developed outside of the
 -- `Algebra.Group` folder.
-assert_not_exists NeZero
+assert_not_imported Mathlib.Algebra.NeZero
 
 variable {α β M N P : Type*}
 

diff --git a/Mathlib/Algebra/Group/Hom/Defs.lean b/Mathlib/Algebra/Group/Hom/Defs.lean
@@ -143,8 +143,9 @@ homomorphisms.
 
 You should also extend this typeclass when you extend `AddMonoidHom`.
 -/
-class AddMonoidHomClass (F M N : Type*) [AddZeroClass M] [AddZeroClass N] [FunLike F M N]
-  extends AddHomClass F M N, ZeroHomClass F M N : Prop
+class AddMonoidHomClass (F : Type*) (M N : outParam Type*)
+    [AddZeroClass M] [AddZeroClass N] [FunLike F M N]
+    extends AddHomClass F M N, ZeroHomClass F M N : Prop
 
 -- Instances and lemmas are defined below through `@[to_additive]`.
 end add_zero

diff --git a/Mathlib/Algebra/Group/Subgroup/Basic.lean b/Mathlib/Algebra/Group/Subgroup/Basic.lean
@@ -94,27 +94,27 @@ variable {A : Type*} [AddGroup A]
 section SubgroupClass
 
 /-- `InvMemClass S G` states `S` is a type of subsets `s ⊆ G` closed under inverses. -/
-class InvMemClass (S G : Type*) [Inv G] [SetLike S G] : Prop where
+class InvMemClass (S : Type*) (G : outParam Type*) [Inv G] [SetLike S G] : Prop where
   /-- `s` is closed under inverses -/
   inv_mem : ∀ {s : S} {x}, x ∈ s → x⁻¹ ∈ s
 
 export InvMemClass (inv_mem)
 
 /-- `NegMemClass S G` states `S` is a type of subsets `s ⊆ G` closed under negation. -/
-class NegMemClass (S G : Type*) [Neg G] [SetLike S G] : Prop where
+class NegMemClass (S : Type*) (G : outParam Type*) [Neg G] [SetLike S G] : Prop where
   /-- `s` is closed under negation -/
   neg_mem : ∀ {s : S} {x}, x ∈ s → -x ∈ s
 
 export NegMemClass (neg_mem)
 
 /-- `SubgroupClass S G` states `S` is a type of subsets `s ⊆ G` that are subgroups of `G`. -/
-class SubgroupClass (S G : Type*) [DivInvMonoid G] [SetLike S G] extends SubmonoidClass S G,
-  InvMemClass S G : Prop
+class SubgroupClass (S : Type*) (G : outParam Type*) [DivInvMonoid G] [SetLike S G]
+    extends SubmonoidClass S G, InvMemClass S G : Prop
 
 /-- `AddSubgroupClass S G` states `S` is a type of subsets `s ⊆ G` that are
 additive subgroups of `G`. -/
-class AddSubgroupClass (S G : Type*) [SubNegMonoid G] [SetLike S G] extends AddSubmonoidClass S G,
-  NegMemClass S G : Prop
+class AddSubgroupClass (S : Type*) (G : outParam Type*) [SubNegMonoid G] [SetLike S G]
+    extends AddSubmonoidClass S G, NegMemClass S G : Prop
 
 attribute [to_additive] InvMemClass SubgroupClass
 

diff --git a/Mathlib/Algebra/Group/Subgroup/Finite.lean b/Mathlib/Algebra/Group/Subgroup/Finite.lean
@@ -165,9 +165,11 @@ theorem pi_mem_of_mulSingle_mem_aux [DecidableEq η] (I : Finset η) {H : Subgro
     x ∈ H := by
   induction I using Finset.induction_on generalizing x with
   | empty =>
-    convert one_mem H
-    ext i
-    exact h1 i (Finset.not_mem_empty i)
+    have : x = 1 := by
+      ext i
+      exact h1 i (Finset.not_mem_empty i)
+    rw [this]
+    exact one_mem H
   | insert hnmem ih =>
     rename_i i I
     have : x = Function.update x i 1 * Pi.mulSingle i (x i) := by

diff --git a/Mathlib/Algebra/Group/Submonoid/Operations.lean b/Mathlib/Algebra/Group/Submonoid/Operations.lean
@@ -591,7 +591,7 @@ theorem closure_closure_coe_preimage {s : Set M} : closure (((↑) : closure s
     Subtype.recOn x fun x hx _ => by
       refine closure_induction'
         (p := fun y hy ↦ (⟨y, hy⟩ : closure s) ∈ closure (((↑) : closure s → M) ⁻¹' s))
-          (fun g hg => subset_closure hg) ?_ (fun g₁ g₂ hg₁ hg₂ => ?_) hx
+          _ (fun g hg => subset_closure hg) ?_ (fun g₁ g₂ hg₁ hg₂ => ?_) hx
       · exact Submonoid.one_mem _
       · exact Submonoid.mul_mem _
 

diff --git a/Mathlib/Algebra/Group/Subsemigroup/Operations.lean b/Mathlib/Algebra/Group/Subsemigroup/Operations.lean
@@ -501,7 +501,7 @@ theorem closure_closure_coe_preimage {s : Set M} :
   eq_top_iff.2 fun x =>
     Subtype.recOn x fun _ hx' _ => closure_induction'
       (p := fun y hy ↦ (⟨y, hy⟩ : closure s) ∈ closure (((↑) : closure s → M) ⁻¹' s))
-        (fun _ hg => subset_closure hg) (fun _ _ _ _ => Subsemigroup.mul_mem _) hx'
+        _ (fun _ hg => subset_closure hg) (fun _ _ _ _ => Subsemigroup.mul_mem _) hx'
 
 /-- Given `Subsemigroup`s `s`, `t` of semigroups `M`, `N` respectively, `s × t` as a subsemigroup
 of `M × N`. -/

diff --git a/Mathlib/Algebra/Group/ZeroOne.lean b/Mathlib/Algebra/Group/ZeroOne.lean
@@ -6,17 +6,10 @@ Authors: Gabriel Ebner, Mario Carneiro
 import Mathlib.Tactic.ToAdditive
 
 /-!
-## Classes for `Zero` and `One`
--/
-
-class Zero.{u} (α : Type u) where
-  zero : α
+## Typeclass `One`
 
-instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
-instance (priority := 200) Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
-  zero := 0
+`Zero` has already been defined in Lean.
+-/
 
 universe u
 

diff --git a/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean b/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
@@ -304,7 +304,7 @@ theorem mk_mem_nonZeroDivisors_associates : Associates.mk a ∈ (Associates M₀
 /-- The non-zero divisors of associates of a monoid with zero `M₀` are isomorphic to the associates
 of the non-zero divisors of `M₀` under the map `⟨⟦a⟧, _⟩ ↦ ⟦⟨a, _⟩⟧`. -/
 def associatesNonZeroDivisorsEquiv : (Associates M₀)⁰ ≃* Associates M₀⁰ where
-  toEquiv := .subtypeQuotientEquivQuotientSubtype (s₂ := Associated.setoid _)
+  toEquiv := .subtypeQuotientEquivQuotientSubtype _ (s₂ := Associated.setoid _)
     (· ∈ nonZeroDivisors _)
     (by simp [mem_nonZeroDivisors_iff, Quotient.forall, Associates.mk_mul_mk])
     (by simp [Associated.setoid])

diff --git a/Mathlib/Algebra/Homology/HomologicalBicomplex.lean b/Mathlib/Algebra/Homology/HomologicalBicomplex.lean
@@ -205,7 +205,7 @@ def XXIsoOfEq {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : I₂} (h₂ :
 
 @[simp]
 lemma XXIsoOfEq_rfl (i₁ : I₁) (i₂ : I₂) :
-    K.XXIsoOfEq (rfl : i₁ = i₁) (rfl : i₂ = i₂) = Iso.refl _ := rfl
+    K.XXIsoOfEq _ _ _ (rfl : i₁ = i₁) (rfl : i₂ = i₂) = Iso.refl _ := rfl
 
 
 end HomologicalComplex₂
diff --git a/Mathlib/Algebra/Homology/TotalComplex.lean b/Mathlib/Algebra/Homology/TotalComplex.lean
@@ -260,15 +260,15 @@ noncomputable def ιTotal (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂)
 @[reassoc (attr := simp)]
 lemma XXIsoOfEq_hom_ιTotal {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : I₂} (h₂ : x₂ = y₂)
     (i₁₂ : I₁₂) (h : ComplexShape.π c₁ c₂ c₁₂ (y₁, y₂) = i₁₂) :
-    (K.XXIsoOfEq h₁ h₂).hom ≫ K.ιTotal c₁₂ y₁ y₂ i₁₂ h =
+    (K.XXIsoOfEq _ _ _ h₁ h₂).hom ≫ K.ιTotal c₁₂ y₁ y₂ i₁₂ h =
       K.ιTotal c₁₂ x₁ x₂ i₁₂ (by rw [h₁, h₂, h]) := by
   subst h₁ h₂
   simp
 
 @[reassoc (attr := simp)]
 lemma XXIsoOfEq_inv_ιTotal {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : I₂} (h₂ : x₂ = y₂)
     (i₁₂ : I₁₂) (h : ComplexShape.π c₁ c₂ c₁₂ (x₁, x₂) = i₁₂) :
-    (K.XXIsoOfEq h₁ h₂).inv ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h =
+    (K.XXIsoOfEq _ _ _ h₁ h₂).inv ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h =
       K.ιTotal c₁₂ y₁ y₂ i₁₂ (by rw [← h, h₁, h₂]) := by
   subst h₁ h₂
   simp

diff --git a/Mathlib/Algebra/Homology/TotalComplexShift.lean b/Mathlib/Algebra/Homology/TotalComplexShift.lean
@@ -129,7 +129,7 @@ noncomputable def totalShift₁XIso (n n' : ℤ) (h : n + x = n') :
     (((shiftFunctor₁ C x).obj K).total (up ℤ)).X n ≅ (K.total (up ℤ)).X n' where
   hom := totalDesc _ (fun p q hpq => K.ιTotal (up ℤ) (p + x) q n' (by dsimp at hpq ⊢; omega))
   inv := totalDesc _ (fun p q hpq =>
-    (K.XXIsoOfEq (Int.sub_add_cancel p x) rfl).inv ≫
+    (K.XXIsoOfEq _ _ _ (Int.sub_add_cancel p x) rfl).inv ≫
       ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (p - x) q n
         (by dsimp at hpq ⊢; omega))
   hom_inv_id := by
@@ -235,7 +235,7 @@ noncomputable def totalShift₂XIso (n n' : ℤ) (h : n + y = n') :
   hom := totalDesc _ (fun p q hpq => (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n'
     (by dsimp at hpq ⊢; omega))
   inv := totalDesc _ (fun p q hpq => (p * y).negOnePow •
-    (K.XXIsoOfEq rfl (Int.sub_add_cancel q y)).inv ≫
+    (K.XXIsoOfEq _ _ _ rfl (Int.sub_add_cancel q y)).inv ≫
       ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p (q - y) n (by dsimp at hpq ⊢; omega))
   hom_inv_id := by
     ext p q h

diff --git a/Mathlib/Algebra/Module/Submodule/Lattice.lean b/Mathlib/Algebra/Module/Submodule/Lattice.lean
@@ -291,7 +291,7 @@ theorem toAddSubmonoid_sSup (s : Set (Submodule R M)) :
     { toAddSubmonoid := sSup (toAddSubmonoid '' s)
       smul_mem' := fun t {m} h ↦ by
         simp_rw [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, sSup_eq_iSup'] at h ⊢
-        refine AddSubmonoid.iSup_induction'
+        refine AddSubmonoid.iSup_induction' _
           (C := fun x _ ↦ t • x ∈ ⨆ p : toAddSubmonoid '' s, (p : AddSubmonoid M)) ?_ ?_
           (fun x y _ _ ↦ ?_) h
         · rintro ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ x (hx : x ∈ p)

diff --git a/Mathlib/Algebra/NeZero.lean b/Mathlib/Algebra/NeZero.lean
@@ -10,32 +10,12 @@ import Mathlib.Order.Defs
 /-!
 # `NeZero` typeclass
 
-We create a typeclass `NeZero n` which carries around the fact that `(n : R) ≠ 0`.
+We give basic facts about the `NeZero n` typeclass.
 
-## Main declarations
-
-* `NeZero`: `n ≠ 0` as a typeclass.
 -/
 
 variable {R : Type*} [Zero R]
 
-/-- A type-class version of `n ≠ 0`. -/
-class NeZero (n : R) : Prop where
-  /-- The proposition that `n` is not zero. -/
-  out : n ≠ 0
-
-theorem NeZero.ne (n : R) [h : NeZero n] : n ≠ 0 :=
-  h.out
-
-theorem NeZero.ne' (n : R) [h : NeZero n] : 0 ≠ n :=
-  h.out.symm
-
-theorem neZero_iff {n : R} : NeZero n ↔ n ≠ 0 :=
-  ⟨fun h ↦ h.out, NeZero.mk⟩
-
-@[simp] lemma neZero_zero_iff_false {α : Type*} [Zero α] : NeZero (0 : α) ↔ False :=
-  ⟨fun h ↦ h.ne rfl, fun h ↦ h.elim⟩
-
 theorem not_neZero {n : R} : ¬NeZero n ↔ n = 0 := by simp [neZero_iff]
 
 theorem eq_zero_or_neZero (a : R) : a = 0 ∨ NeZero a :=
@@ -77,10 +57,6 @@ namespace NeZero
 
 variable {M : Type*} {x : M}
 
-instance succ {n : ℕ} : NeZero (n + 1) := ⟨n.succ_ne_zero⟩
-
 theorem of_pos [Preorder M] [Zero M] (h : 0 < x) : NeZero x := ⟨ne_of_gt h⟩
 
 end NeZero
-
-lemma Nat.pos_of_neZero (n : ℕ) [NeZero n] : 0 < n := Nat.pos_of_ne_zero (NeZero.ne _)
diff --git a/Mathlib/Algebra/Order/BigOperators/Group/List.lean b/Mathlib/Algebra/Order/BigOperators/Group/List.lean
@@ -164,7 +164,7 @@ variable [CanonicallyOrderedCommMonoid M] {l : List M}
 
 @[to_additive] lemma prod_eq_one_iff : l.prod = 1 ↔ ∀ x ∈ l, x = (1 : M) :=
   ⟨all_one_of_le_one_le_of_prod_eq_one fun _ _ => one_le _, fun h => by
-    rw [List.eq_replicate.2 ⟨_, h⟩, prod_replicate, one_pow]
+    rw [List.eq_replicate_iff.2 ⟨_, h⟩, prod_replicate, one_pow]
     · exact (length l)
     · rfl⟩