Trigger CI for leanprover-community/batteries#1071

Archive/Imo/Imo1964Q1.lean

@@ -5,25 +5,17 @@ Authors: Kevin Buzzard
 -/
 import Mathlib.Tactic.IntervalCases
 import Mathlib.Data.Nat.ModEq
-import Mathlib.Tactic.Ring
 
 /-!
 # IMO 1964 Q1
 
 (a) Find all positive integers $n$ for which $2^n-1$ is divisible by $7$.
-
 (b) Prove that there is no positive integer $n$ for which $2^n+1$ is divisible by $7$.
 
-We define a predicate for the solutions in (a), and prove that it is the set of positive
-integers which are a multiple of 3.
--/
-
-
-/-!
-## Intermediate lemmas
+For (a), we find that the order of $2$ mod $7$ is $3$. Therefore for (b), it suffices to check
+$n = 0, 1, 2$.
 -/
 
-
 open Nat
 
 namespace Imo1964Q1
@@ -33,17 +25,13 @@ theorem two_pow_mod_seven (n : ℕ) : 2 ^ n ≡ 2 ^ (n % 3) [MOD 7] :=
   calc 2 ^ n = 2 ^ (3 * (n / 3) + t) := by rw [Nat.div_add_mod]
     _ = (2 ^ 3) ^ (n / 3) * 2 ^ t := by rw [pow_add, pow_mul]
     _ ≡ 1 ^ (n / 3) * 2 ^ t [MOD 7] := by gcongr; decide
-    _ = 2 ^ t := by ring
-
-/-!
-## The question
--/
+    _ = 2 ^ t := by rw [one_pow, one_mul]
 
+end Imo1964Q1
 
-def ProblemPredicate (n : ℕ) : Prop :=
-  7 ∣ 2 ^ n - 1
+open Imo1964Q1
 
-theorem imo1964_q1a (n : ℕ) (_ : 0 < n) : ProblemPredicate n ↔ 3 ∣ n := by
+theorem imo1964_q1a (n : ℕ) (_ : 0 < n) : 7 ∣ 2 ^ n - 1 ↔ 3 ∣ n := by
   let t := n % 3
   have : t < 3 := Nat.mod_lt _ (by decide)
   calc 7 ∣ 2 ^ n - 1 ↔ 2 ^ n ≡ 1 [MOD 7] := by
@@ -53,15 +41,11 @@ theorem imo1964_q1a (n : ℕ) (_ : 0 < n) : ProblemPredicate n ↔ 3 ∣ n := by
     _ ↔ t = 0 := by interval_cases t <;> decide
     _ ↔ 3 ∣ n := by rw [dvd_iff_mod_eq_zero]
 
-end Imo1964Q1
-
-open Imo1964Q1
-
 theorem imo1964_q1b (n : ℕ) : ¬7 ∣ 2 ^ n + 1 := by
   intro h
   let t := n % 3
   have : t < 3 := Nat.mod_lt _ (by decide)
   have H : 2 ^ t + 1 ≡ 0 [MOD 7] := calc
-    2 ^ t + 1 ≡ 2 ^ n + 1 [MOD 7 ] := by gcongr ?_ + 1; exact (two_pow_mod_seven n).symm
+    2 ^ t + 1 ≡ 2 ^ n + 1 [MOD 7] := by gcongr ?_ + 1; exact (two_pow_mod_seven n).symm
       _ ≡ 0 [MOD 7] := h.modEq_zero_nat
   interval_cases t <;> contradiction

Mathlib.lean

@@ -554,6 +554,7 @@ import Mathlib.Algebra.Module.Presentation.Differentials
 import Mathlib.Algebra.Module.Presentation.DirectSum
 import Mathlib.Algebra.Module.Presentation.Finite
 import Mathlib.Algebra.Module.Presentation.Free
+import Mathlib.Algebra.Module.Presentation.RestrictScalars
 import Mathlib.Algebra.Module.Presentation.Tautological
 import Mathlib.Algebra.Module.Prod
 import Mathlib.Algebra.Module.Projective
@@ -2526,6 +2527,7 @@ import Mathlib.Data.Int.Cast.Basic
 import Mathlib.Data.Int.Cast.Defs
 import Mathlib.Data.Int.Cast.Field
 import Mathlib.Data.Int.Cast.Lemmas
+import Mathlib.Data.Int.Cast.Pi
 import Mathlib.Data.Int.Cast.Prod
 import Mathlib.Data.Int.CharZero
 import Mathlib.Data.Int.ConditionallyCompleteOrder
@@ -2925,6 +2927,9 @@ import Mathlib.Data.ZMod.Units
 import Mathlib.Deprecated.AlgebraClasses
 import Mathlib.Deprecated.Aliases
 import Mathlib.Deprecated.ByteArray
+import Mathlib.Deprecated.Cardinal.Continuum
+import Mathlib.Deprecated.Cardinal.Finite
+import Mathlib.Deprecated.Cardinal.PartENat
 import Mathlib.Deprecated.Combinator
 import Mathlib.Deprecated.Equiv
 import Mathlib.Deprecated.Group
@@ -4426,6 +4431,7 @@ import Mathlib.RingTheory.MaximalSpectrum
 import Mathlib.RingTheory.Multiplicity
 import Mathlib.RingTheory.MvPolynomial
 import Mathlib.RingTheory.MvPolynomial.Basic
+import Mathlib.RingTheory.MvPolynomial.EulerIdentity
 import Mathlib.RingTheory.MvPolynomial.FreeCommRing
 import Mathlib.RingTheory.MvPolynomial.Homogeneous
 import Mathlib.RingTheory.MvPolynomial.Ideal
@@ -4618,7 +4624,6 @@ import Mathlib.SetTheory.Cardinal.ENat
 import Mathlib.SetTheory.Cardinal.Finite
 import Mathlib.SetTheory.Cardinal.Finsupp
 import Mathlib.SetTheory.Cardinal.Free
-import Mathlib.SetTheory.Cardinal.PartENat
 import Mathlib.SetTheory.Cardinal.SchroederBernstein
 import Mathlib.SetTheory.Cardinal.Subfield
 import Mathlib.SetTheory.Cardinal.ToNat
@@ -5350,6 +5355,7 @@ import Mathlib.Topology.UniformSpace.CompactConvergence
 import Mathlib.Topology.UniformSpace.CompareReals
 import Mathlib.Topology.UniformSpace.CompleteSeparated
 import Mathlib.Topology.UniformSpace.Completion
+import Mathlib.Topology.UniformSpace.Dini
 import Mathlib.Topology.UniformSpace.Equicontinuity
 import Mathlib.Topology.UniformSpace.Equiv
 import Mathlib.Topology.UniformSpace.HeineCantor

Mathlib/Algebra/BigOperators/Group/List.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best
 -/
 import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.Group.Int
+import Mathlib.Data.List.Lemmas
 import Mathlib.Data.List.Dedup
 import Mathlib.Data.List.Flatten
 import Mathlib.Data.List.Pairwise
@@ -661,22 +662,10 @@ lemma mem_mem_ranges_iff_lt_sum (l : List ℕ) {n : ℕ} :
     (∃ s ∈ l.ranges, n ∈ s) ↔ n < l.sum := by
   rw [← mem_range, ← ranges_flatten, mem_flatten]
 
-@[simp]
-theorem length_flatMap (l : List α) (f : α → List β) :
-    length (List.flatMap l f) = sum (map (length ∘ f) l) := by
-  rw [List.flatMap, length_flatten, map_map]
-
 @[deprecated (since := "2024-10-16")] alias length_bind := length_flatMap
 
-lemma countP_flatMap (p : β → Bool) (l : List α) (f : α → List β) :
-    countP p (l.flatMap f) = sum (map (countP p ∘ f) l) := by
-  rw [List.flatMap, countP_flatten, map_map]
-
 @[deprecated (since := "2024-10-16")] alias countP_bind := countP_flatMap
 
-lemma count_flatMap [BEq β] (l : List α) (f : α → List β) (x : β) :
-    count x (l.flatMap f) = sum (map (count x ∘ f) l) := countP_flatMap _ _ _
-
 @[deprecated (since := "2024-10-16")] alias count_bind := count_flatMap
 
 /-- In a flatten, taking the first elements up to an index which is the sum of the lengths of the

Mathlib/Algebra/Category/AlgebraCat/Basic.lean

@@ -153,7 +153,7 @@ instance hasForgetToRing : HasForget₂ (AlgebraCat.{v} R) RingCat.{v} where
 instance hasForgetToModule : HasForget₂ (AlgebraCat.{v} R) (ModuleCat.{v} R) where
   forget₂ :=
     { obj := fun M => ModuleCat.of R M
-      map := fun f => ModuleCat.asHom f.hom.toLinearMap }
+      map := fun f => ModuleCat.ofHom f.hom.toLinearMap }
 
 @[simp]
 lemma forget₂_module_obj (X : AlgebraCat.{v} R) :
@@ -162,7 +162,7 @@ lemma forget₂_module_obj (X : AlgebraCat.{v} R) :
 
 @[simp]
 lemma forget₂_module_map {X Y : AlgebraCat.{v} R} (f : X ⟶ Y) :
-    (forget₂ (AlgebraCat.{v} R) (ModuleCat.{v} R)).map f = ModuleCat.asHom f.hom.toLinearMap :=
+    (forget₂ (AlgebraCat.{v} R) (ModuleCat.{v} R)).map f = ModuleCat.ofHom f.hom.toLinearMap :=
   rfl
 
 variable {R} in

Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean

@@ -38,8 +38,8 @@ variable {R : Type u} [CommRing R]
 /-- An `R`-coalgebra is a comonoid object in the category of `R`-modules. -/
 @[simps] def toComonObj (X : CoalgebraCat R) : Comon_ (ModuleCat R) where
   X := ModuleCat.of R X
-  counit := ModuleCat.asHom Coalgebra.counit
-  comul := ModuleCat.asHom Coalgebra.comul
+  counit := ModuleCat.ofHom Coalgebra.counit
+  comul := ModuleCat.ofHom Coalgebra.comul
   counit_comul := by simpa only [ModuleCat.of_coe] using Coalgebra.rTensor_counit_comp_comul
   comul_counit := by simpa only [ModuleCat.of_coe] using Coalgebra.lTensor_counit_comp_comul
   comul_assoc := by simp_rw [ModuleCat.of_coe]; exact Coalgebra.coassoc.symm
@@ -50,7 +50,7 @@ variable (R) in
 def toComon : CoalgebraCat R ⥤ Comon_ (ModuleCat R) where
   obj X := toComonObj X
   map f :=
-    { hom := ModuleCat.asHom f.1
+    { hom := ModuleCat.ofHom f.1
       hom_counit := f.1.counit_comp
       hom_comul := f.1.map_comp_comul.symm }
 

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -267,8 +267,8 @@ end FGModuleCat
 @[simp] theorem LinearMap.comp_id_fgModuleCat
     {R} [Ring R] {G : FGModuleCat.{u} R} {H : Type u} [AddCommGroup H] [Module R H]
     (f : G →ₗ[R] H) : f.comp (𝟙 G) = f :=
-  Category.id_comp (ModuleCat.asHom f)
+  Category.id_comp (ModuleCat.ofHom f)
 @[simp] theorem LinearMap.id_fgModuleCat_comp
     {R} [Ring R] {G : Type u} [AddCommGroup G] [Module R G] {H : FGModuleCat.{u} R}
     (f : G →ₗ[R] H) : LinearMap.comp (𝟙 H) f = f :=
-  Category.comp_id (ModuleCat.asHom f)
+  Category.comp_id (ModuleCat.ofHom f)

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -209,21 +209,21 @@ variable {X₁ X₂ : Type v}
 open ModuleCat
 
 /-- Reinterpreting a linear map in the category of `R`-modules. -/
-def ModuleCat.asHom [AddCommGroup X₁] [Module R X₁] [AddCommGroup X₂] [Module R X₂] :
+def ModuleCat.ofHom [AddCommGroup X₁] [Module R X₁] [AddCommGroup X₂] [Module R X₂] :
     (X₁ →ₗ[R] X₂) → (ModuleCat.of R X₁ ⟶ ModuleCat.of R X₂) :=
   id
 
-@[deprecated (since := "2024-10-06")] alias ModuleCat.ofHom := ModuleCat.asHom
+@[deprecated (since := "2024-12-03")] alias ModuleCat.asHom := ModuleCat.ofHom
 
 /-- Reinterpreting a linear map in the category of `R`-modules -/
-scoped[ModuleCat] notation "↟" f:1024 => ModuleCat.asHom f
+scoped[ModuleCat] notation "↟" f:1024 => ModuleCat.ofHom f
 
 @[simp 1100]
-theorem ModuleCat.asHom_apply {R : Type u} [Ring R] {X Y : Type v} [AddCommGroup X] [Module R X]
+theorem ModuleCat.ofHom_apply {R : Type u} [Ring R] {X Y : Type v} [AddCommGroup X] [Module R X]
     [AddCommGroup Y] [Module R Y] (f : X →ₗ[R] Y) (x : X) : (↟ f) x = f x :=
   rfl
 
-@[deprecated (since := "2024-10-06")] alias ModuleCat.ofHom_apply := ModuleCat.asHom_apply
+@[deprecated (since := "2024-10-06")] alias ModuleCat.asHom_apply := ModuleCat.ofHom_apply
 
 /-- Reinterpreting a linear map in the category of `R`-modules. -/
 def ModuleCat.asHomRight [AddCommGroup X₁] [Module R X₁] {X₂ : ModuleCat.{v} R} :
@@ -440,8 +440,8 @@ end ModuleCat
 @[simp] theorem LinearMap.comp_id_moduleCat
     {R} [Ring R] {G : ModuleCat.{u} R} {H : Type u} [AddCommGroup H] [Module R H] (f : G →ₗ[R] H) :
     f.comp (𝟙 G) = f :=
-  Category.id_comp (ModuleCat.asHom f)
+  Category.id_comp (ModuleCat.ofHom f)
 @[simp] theorem LinearMap.id_moduleCat_comp
     {R} [Ring R] {G : Type u} [AddCommGroup G] [Module R G] {H : ModuleCat.{u} R} (f : G →ₗ[R] H) :
     LinearMap.comp (𝟙 H) f = f :=
-  Category.comp_id (ModuleCat.asHom f)
+  Category.comp_id (ModuleCat.ofHom f)

Mathlib/Algebra/Category/ModuleCat/Biproducts.lean

@@ -144,8 +144,8 @@ of modules. -/
 noncomputable def lequivProdOfRightSplitExact {f : B →ₗ[R] M} (hj : Function.Injective j)
     (exac : LinearMap.range j = LinearMap.ker g) (h : g.comp f = LinearMap.id) : (A × B) ≃ₗ[R] M :=
   ((ShortComplex.Splitting.ofExactOfSection _
-    (ShortComplex.Exact.moduleCat_of_range_eq_ker (ModuleCat.asHom j)
-    (ModuleCat.asHom g) exac) (asHom f) h
+    (ShortComplex.Exact.moduleCat_of_range_eq_ker (ModuleCat.ofHom j)
+    (ModuleCat.ofHom g) exac) (ofHom f) h
     (by simpa only [ModuleCat.mono_iff_injective])).isoBinaryBiproduct ≪≫
     biprodIsoProd _ _ ).symm.toLinearEquiv
 
@@ -154,8 +154,8 @@ of modules. -/
 noncomputable def lequivProdOfLeftSplitExact {f : M →ₗ[R] A} (hg : Function.Surjective g)
     (exac : LinearMap.range j = LinearMap.ker g) (h : f.comp j = LinearMap.id) : (A × B) ≃ₗ[R] M :=
   ((ShortComplex.Splitting.ofExactOfRetraction _
-    (ShortComplex.Exact.moduleCat_of_range_eq_ker (ModuleCat.asHom j)
-    (ModuleCat.asHom g) exac) (ModuleCat.asHom f) h
+    (ShortComplex.Exact.moduleCat_of_range_eq_ker (ModuleCat.ofHom j)
+    (ModuleCat.ofHom g) exac) (ModuleCat.ofHom f) h
     (by simpa only [ModuleCat.epi_iff_surjective] using hg)).isoBinaryBiproduct ≪≫
     biprodIsoProd _ _).symm.toLinearEquiv
 

Mathlib/Algebra/Category/ModuleCat/Images.lean

@@ -97,12 +97,12 @@ noncomputable def imageIsoRange {G H : ModuleCat.{v} R} (f : G ⟶ H) :
 
 @[simp, reassoc, elementwise]
 theorem imageIsoRange_inv_image_ι {G H : ModuleCat.{v} R} (f : G ⟶ H) :
-    (imageIsoRange f).inv ≫ Limits.image.ι f = ModuleCat.asHom f.range.subtype :=
+    (imageIsoRange f).inv ≫ Limits.image.ι f = ModuleCat.ofHom f.range.subtype :=
   IsImage.isoExt_inv_m _ _
 
 @[simp, reassoc, elementwise]
 theorem imageIsoRange_hom_subtype {G H : ModuleCat.{v} R} (f : G ⟶ H) :
-    (imageIsoRange f).hom ≫ ModuleCat.asHom f.range.subtype = Limits.image.ι f := by
+    (imageIsoRange f).hom ≫ ModuleCat.ofHom f.range.subtype = Limits.image.ι f := by
   rw [← imageIsoRange_inv_image_ι f, Iso.hom_inv_id_assoc]
 
 end ModuleCat

Mathlib/Algebra/Category/ModuleCat/Injective.lean

@@ -27,8 +27,8 @@ theorem injective_module_of_injective_object
     [inj : CategoryTheory.Injective <| ModuleCat.of R M] :
     Module.Injective R M where
   out X Y _ _ _ _ f hf g := by
-    have : CategoryTheory.Mono (ModuleCat.asHom f) := (ModuleCat.mono_iff_injective _).mpr hf
-    obtain ⟨l, rfl⟩ := inj.factors (ModuleCat.asHom g) (ModuleCat.asHom f)
+    have : CategoryTheory.Mono (ModuleCat.ofHom f) := (ModuleCat.mono_iff_injective _).mpr hf
+    obtain ⟨l, rfl⟩ := inj.factors (ModuleCat.ofHom g) (ModuleCat.ofHom f)
     exact ⟨l, fun _ ↦ rfl⟩
 
 theorem injective_iff_injective_object :

Mathlib/Algebra/Category/ModuleCat/Kernels.lean

@@ -26,7 +26,7 @@ variable {M N : ModuleCat.{v} R} (f : M ⟶ N)
 /-- The kernel cone induced by the concrete kernel. -/
 def kernelCone : KernelFork f :=
   -- Porting note: previously proven by tidy
-  KernelFork.ofι (asHom f.ker.subtype) <| by ext x; cases x; assumption
+  KernelFork.ofι (ofHom f.ker.subtype) <| by ext x; cases x; assumption
 
 /-- The kernel of a linear map is a kernel in the categorical sense. -/
 def kernelIsLimit : IsLimit (kernelCone f) :=
@@ -44,7 +44,7 @@ def kernelIsLimit : IsLimit (kernelCone f) :=
 
 /-- The cokernel cocone induced by the projection onto the quotient. -/
 def cokernelCocone : CokernelCofork f :=
-  CokernelCofork.ofπ (asHom f.range.mkQ) <| LinearMap.range_mkQ_comp _
+  CokernelCofork.ofπ (ofHom f.range.mkQ) <| LinearMap.range_mkQ_comp _
 
 /-- The projection onto the quotient is a cokernel in the categorical sense. -/
 def cokernelIsColimit : IsColimit (cokernelCocone f) :=
@@ -53,10 +53,10 @@ def cokernelIsColimit : IsColimit (cokernelCocone f) :=
       f.range.liftQ (Cofork.π s) <| LinearMap.range_le_ker_iff.2 <| CokernelCofork.condition s)
     (fun s => f.range.liftQ_mkQ (Cofork.π s) _) fun s m h => by
     -- Porting note (https://github.com/leanprover-community/mathlib4/pull/11036): broken dot notation
-    haveI : Epi (asHom (LinearMap.range f).mkQ) :=
+    haveI : Epi (ofHom (LinearMap.range f).mkQ) :=
       (epi_iff_range_eq_top _).mpr (Submodule.range_mkQ _)
     -- Porting note (https://github.com/leanprover-community/mathlib4/pull/11036): broken dot notation
-    apply (cancel_epi (asHom (LinearMap.range f).mkQ)).1
+    apply (cancel_epi (ofHom (LinearMap.range f).mkQ)).1
     convert h
     -- Porting note: no longer necessary
     -- exact Submodule.liftQ_mkQ _ _ _

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -1315,8 +1315,8 @@ namespace Associates
 variable [CancelCommMonoidWithZero α] [GCDMonoid α]
 
 instance instGCDMonoid : GCDMonoid (Associates α) where
-  gcd := Quotient.map₂' gcd fun _ _ (ha : Associated _ _) _ _ (hb : Associated _ _) => ha.gcd hb
-  lcm := Quotient.map₂' lcm fun _ _ (ha : Associated _ _) _ _ (hb : Associated _ _) => ha.lcm hb
+  gcd := Quotient.map₂ gcd fun _ _ (ha : Associated _ _) _ _ (hb : Associated _ _) => ha.gcd hb
+  lcm := Quotient.map₂ lcm fun _ _ (ha : Associated _ _) _ _ (hb : Associated _ _) => ha.lcm hb
   gcd_dvd_left := by rintro ⟨a⟩ ⟨b⟩; exact mk_le_mk_of_dvd (gcd_dvd_left _ _)
   gcd_dvd_right := by rintro ⟨a⟩ ⟨b⟩; exact mk_le_mk_of_dvd (gcd_dvd_right _ _)
   dvd_gcd := by

Mathlib/Algebra/Group/Subgroup/Finite.lean

@@ -6,6 +6,7 @@ Authors: Kexing Ying
 import Mathlib.Algebra.Group.Subgroup.Basic
 import Mathlib.Algebra.Group.Submonoid.BigOperators
 import Mathlib.Data.Finite.Card
+import Mathlib.Data.Set.Finite.Range
 
 /-!
 # Subgroups

Mathlib/Algebra/Group/Subgroup/Pointwise.lean

@@ -202,6 +202,21 @@ theorem closure_mul_le (S T : Set G) : closure (S * T) ≤ closure S ⊔ closure
     (closure S ⊔ closure T).mul_mem (SetLike.le_def.mp le_sup_left <| subset_closure hs)
       (SetLike.le_def.mp le_sup_right <| subset_closure ht)
 
+@[to_additive]
+lemma closure_pow_le : ∀ {n}, n ≠ 0 → closure (s ^ n) ≤ closure s
+  | 1, _ => by simp
+  | n + 2, _ =>
+    calc
+      closure (s ^ (n + 2))
+      _ = closure (s ^ (n + 1) * s) := by rw [pow_succ]
+      _ ≤ closure (s ^ (n + 1)) ⊔ closure s := closure_mul_le ..
+      _ ≤ closure s ⊔ closure s := by gcongr ?_ ⊔ _; exact closure_pow_le n.succ_ne_zero
+      _ = closure s := sup_idem _
+
+@[to_additive]
+lemma closure_pow {n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) : closure (s ^ n) = closure s :=
+  (closure_pow_le hn).antisymm <| by gcongr; exact subset_pow hs hn
+
 @[to_additive]
 theorem sup_eq_closure_mul (H K : Subgroup G) : H ⊔ K = closure ((H : Set G) * (K : Set G)) :=
   le_antisymm

Mathlib/Algebra/Group/Submonoid/Pointwise.lean

@@ -96,6 +96,21 @@ theorem closure_mul_le (S T : Set M) : closure (S * T) ≤ closure S ⊔ closure
     (closure S ⊔ closure T).mul_mem (SetLike.le_def.mp le_sup_left <| subset_closure hs)
       (SetLike.le_def.mp le_sup_right <| subset_closure ht)
 
+@[to_additive]
+lemma closure_pow_le : ∀ {n}, n ≠ 0 → closure (s ^ n) ≤ closure s
+  | 1, _ => by simp
+  | n + 2, _ =>
+    calc
+      closure (s ^ (n + 2))
+      _ = closure (s ^ (n + 1) * s) := by rw [pow_succ]
+      _ ≤ closure (s ^ (n + 1)) ⊔ closure s := closure_mul_le ..
+      _ ≤ closure s ⊔ closure s := by gcongr ?_ ⊔ _; exact closure_pow_le n.succ_ne_zero
+      _ = closure s := sup_idem _
+
+@[to_additive]
+lemma closure_pow {n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) : closure (s ^ n) = closure s :=
+  (closure_pow_le hn).antisymm <| by gcongr; exact subset_pow hs hn
+
 @[to_additive]
 theorem sup_eq_closure_mul (H K : Submonoid M) : H ⊔ K = closure ((H : Set M) * (K : Set M)) :=
   le_antisymm

Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean

@@ -33,7 +33,7 @@ linear maps `f` and `g` and the vanishing of their composition. -/
 def moduleCatMk {X₁ X₂ X₃ : Type v} [AddCommGroup X₁] [AddCommGroup X₂] [AddCommGroup X₃]
     [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃)
     (hfg : g.comp f = 0) : ShortComplex (ModuleCat.{v} R) :=
-  ShortComplex.mk (ModuleCat.asHom f) (ModuleCat.asHom g) hfg
+  ShortComplex.mk (ModuleCat.ofHom f) (ModuleCat.ofHom g) hfg
 
 variable (S : ShortComplex (ModuleCat.{v} R))
 
@@ -138,7 +138,7 @@ def moduleCatLeftHomologyData : S.LeftHomologyData where
     erw [Submodule.Quotient.mk_eq_zero]
     rw [LinearMap.mem_range]
     apply exists_apply_eq_apply
-  hπ := ModuleCat.cokernelIsColimit (ModuleCat.asHom S.moduleCatToCycles)
+  hπ := ModuleCat.cokernelIsColimit (ModuleCat.ofHom S.moduleCatToCycles)
 
 @[simp]
 lemma moduleCatLeftHomologyData_f' :