Merge master into nightly-testing

Author: mathlib-nightly-testing[bot]

Mathlib.lean

@@ -1339,6 +1339,7 @@ public import Mathlib.AlgebraicGeometry.Fiber
 public import Mathlib.AlgebraicGeometry.FunctionField
 public import Mathlib.AlgebraicGeometry.GammaSpecAdjunction
 public import Mathlib.AlgebraicGeometry.Geometrically.Basic
+public import Mathlib.AlgebraicGeometry.Geometrically.Connected
 public import Mathlib.AlgebraicGeometry.Geometrically.Integral
 public import Mathlib.AlgebraicGeometry.Geometrically.Irreducible
 public import Mathlib.AlgebraicGeometry.Geometrically.Reduced
@@ -1510,6 +1511,7 @@ public import Mathlib.AlgebraicTopology.SimplicialObject.II
 public import Mathlib.AlgebraicTopology.SimplicialObject.Op
 public import Mathlib.AlgebraicTopology.SimplicialObject.Split
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
+public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
@@ -1528,6 +1530,7 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
 public import Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
 public import Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
 public import Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
+public import Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
 public import Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance
 public import Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
 public import Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
@@ -1559,9 +1562,10 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
 public import Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
 public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
 public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation
+public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexOp
 public import Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
 public import Mathlib.AlgebraicTopology.SingularHomology.Basic
-public import Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat
+public import Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance
 public import Mathlib.AlgebraicTopology.SingularSet
 public import Mathlib.AlgebraicTopology.TopologicalSimplex
 public import Mathlib.Analysis.AbsoluteValue.Equivalence
@@ -6503,6 +6507,7 @@ public import Mathlib.RingTheory.LocalProperties.Semilocal
 public import Mathlib.RingTheory.LocalProperties.Submodule
 public import Mathlib.RingTheory.LocalRing.Basic
 public import Mathlib.RingTheory.LocalRing.Defs
+public import Mathlib.RingTheory.LocalRing.Length
 public import Mathlib.RingTheory.LocalRing.LocalSubring
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs

Mathlib/Algebra/Category/Grp/CartesianMonoidal.lean

@@ -119,11 +119,6 @@ noncomputable def cartesianMonoidalCategory : CartesianMonoidalCategory AddCommG
   .ofChosenFiniteProducts ⟨_, (isZero_of_subsingleton (AddCommGrpCat.of PUnit.{u + 1})).isTerminal⟩
     fun G H ↦ binaryProductLimitCone G H
 
--- This is deprecated, but still used as a `local instance` in
--- Mathlib.Algebra.Category.Grp.LeftExactFunctor
-@[instance_reducible, deprecated (since := "2025-10-10")]
-alias cartesianMonoidalCategoryAddCommGrp := cartesianMonoidalCategory
-
 attribute [local instance] cartesianMonoidalCategory
 
 noncomputable instance : BraidedCategory AddCommGrpCat.{u} := .ofCartesianMonoidalCategory

Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean

@@ -45,8 +45,7 @@ namespace leftExactFunctorForgetEquivalence
 
 attribute [local instance] hasFiniteProducts_of_hasFiniteBiproducts
 
--- This was deprecated on 2025-10-10 but is still used as a local instance here!
-attribute [local instance] AddCommGrpCat.cartesianMonoidalCategoryAddCommGrp
+attribute [local instance] AddCommGrpCat.cartesianMonoidalCategory
 
 set_option backward.privateInPublic true in
 private noncomputable local instance : CartesianMonoidalCategory C := .ofHasFiniteProducts

Mathlib/Algebra/Group/Action/Defs.lean

@@ -619,10 +619,10 @@ but here you can use the even stronger class `MulSemiringAction`, which captures
 how the action plays with both multiplication and addition. -/
 @[ext]
 class MulDistribMulAction (M N : Type*) [Monoid M] [Monoid N] extends MulAction M N where
-  /-- Distributivity of `•` across `*` -/
-  smul_mul : ∀ (r : M) (x y : N), r • (x * y) = r • x * r • y
   /-- Multiplying `1` by a scalar gives `1` -/
   smul_one : ∀ r : M, r • (1 : N) = 1
+  /-- Distributivity of `•` across `*` -/
+  smul_mul : ∀ (r : M) (x y : N), r • (x * y) = r • x * r • y
 
 export MulDistribMulAction (smul_one)
 

Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

@@ -511,7 +511,7 @@ left-cancellative multiplication.
 @[to_additive
 /-- See `card_le_card_add_left` for a more convenient but less general version for types with a
 left-cancellative addition. -/]
-lemma card_le_card_mul_left_of_injective (has : a ∈ s) (ha : Function.Injective (a * ·)) :
+lemma card_le_card_mul_left_of_injective (has : a ∈ s) (ha : IsLeftRegular a) :
     #t ≤ #(s * t) :=
   card_le_card_image₂_left _ has ha
 
@@ -522,7 +522,7 @@ right-cancellative multiplication.
 @[to_additive
 /-- See `card_le_card_add_right` for a more convenient but less general version for types with a
 right-cancellative addition. -/]
-lemma card_le_card_mul_right_of_injective (hat : a ∈ t) (ha : Function.Injective (· * a)) :
+lemma card_le_card_mul_right_of_injective (hat : a ∈ t) (ha : IsRightRegular a) :
     #s ≤ #(s * t) :=
   card_le_card_image₂_right _ hat ha
 

Mathlib/Algebra/Group/Pointwise/Finset/Scalar.lean

@@ -172,7 +172,9 @@ lemma coe_smul_finset (a : α) (s : Finset β) : ↑(a • s) = a • (↑s : Se
 
 @[to_additive] lemma smul_mem_smul_finset : b ∈ s → a • b ∈ a • s := mem_image_of_mem _
 
-@[to_additive] lemma smul_finset_card_le : #(a • s) ≤ #s := card_image_le
+@[to_additive] lemma card_smul_finset_le : #(a • s) ≤ #s := card_image_le
+@[deprecated (since := "2026-04-16")] alias smul_finset_card_le := card_smul_finset_le
+@[deprecated (since := "2026-04-16")] alias vadd_finset_card_le := card_vadd_finset_le
 
 @[to_additive (attr := simp)]
 lemma smul_finset_empty (a : α) : a • (∅ : Finset β) = ∅ := rfl

Mathlib/Algebra/Group/Subgroup/Finite.lean

@@ -174,12 +174,6 @@ open Set
 
 variable {η : Type*} {f : η → Type*} [∀ i, Group (f i)]
 
-@[to_additive (attr := deprecated Submonoid.pi_mem_of_mulSingle_mem_aux (since := "2025-10-08"))]
-theorem pi_mem_of_mulSingle_mem_aux [DecidableEq η] (I : Finset η) {H : Subgroup (∀ i, f i)}
-    (x : ∀ i, f i) (h1 : ∀ i, i ∉ I → x i = 1) (h2 : ∀ i, i ∈ I → Pi.mulSingle i (x i) ∈ H) :
-    x ∈ H :=
-  Submonoid.pi_mem_of_mulSingle_mem_aux I x h1 h2
-
 @[to_additive]
 theorem pi_mem_of_mulSingle_mem [Finite η] [DecidableEq η] {H : Subgroup (∀ i, f i)} (x : ∀ i, f i)
     (h : ∀ i, Pi.mulSingle i (x i) ∈ H) : x ∈ H :=

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -250,8 +250,6 @@ instance (priority := 900) isReduced_of_noZeroDivisors [NoZeroDivisors M₀] :
 
 variable [IsReduced M₀]
 
-@[deprecated (since := "2025-10-14")] alias pow_eq_zero := eq_zero_of_pow_eq_zero
-
 @[simp] lemma pow_eq_zero_iff (hn : n ≠ 0) : a ^ n = 0 ↔ a = 0 :=
   ⟨eq_zero_of_pow_eq_zero, (·.symm ▸ zero_pow hn)⟩
 

Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean

@@ -689,6 +689,14 @@ namespace ChainComplex
 variable {C : Type*} [Category* C] [HasZeroMorphisms C]
   (K L : ChainComplex C ℕ) (φ : K ⟶ L) [K.HasHomology 0]
 
+instance isIso_iCycles₀ : IsIso (K.iCycles 0) :=
+  K.isIso_iCycles 0 0 (by simp) (by simp)
+
+/-- The canonical isomorphism `K.cycles 0 ≅ K.X 0` for a chain complex `K`
+indexed by `ℕ`. -/
+noncomputable abbrev cycles₀Iso : K.cycles 0 ≅ K.X 0 :=
+  K.iCyclesIso 0 0 (by simp) (by simp)
+
 instance isIso_homologyι₀ :
     IsIso (K.homologyι 0) :=
   K.isIso_homologyι 0 _ rfl (by simp)
@@ -715,6 +723,14 @@ namespace CochainComplex
 variable {C : Type*} [Category* C] [HasZeroMorphisms C]
   (K L : CochainComplex C ℕ) (φ : K ⟶ L) [K.HasHomology 0]
 
+instance isIso_pOpcycles₀ : IsIso (K.pOpcycles 0) :=
+  K.isIso_pOpcycles 0 0 (by simp) (by simp)
+
+/-- The canonical isomorphism `K.X 0 ≅ K.opcycles 0` for a cochain complex `K`
+indexed by `ℕ`. -/
+noncomputable abbrev opcycles₀Iso : K.X 0 ≅ K.opcycles 0 :=
+  K.pOpcyclesIso 0 0 (by simp) (by simp)
+
 instance isIso_homologyπ₀ :
     IsIso (K.homologyπ 0) :=
   K.isIso_homologyπ _ 0 rfl (by simp)

Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean

@@ -159,6 +159,14 @@ def ofIsColimitCokernelCofork (hg : S.g = 0) (c : CokernelCofork S.f) (hc : IsCo
     (hc : IsColimit c) : (ofIsColimitCokernelCofork S hg c hc).f' = S.f := by
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+lemma ofIsColimitCokernelCofork_liftK (hg : S.g = 0) (c : CokernelCofork S.f) (hc : IsColimit c)
+    {T : C} (φ : T ⟶ S.X₂) :
+    dsimp% (ofIsColimitCokernelCofork S hg c hc).liftK φ (by simp [hg]) = φ := by
+  rw [← cancel_mono (ofIsColimitCokernelCofork S hg c hc).i, liftK_i]
+  simp
+
 /-- When the second map `S.g` is zero, this is the left homology data on `S` given by
 the chosen `cokernel S.f` -/
 @[simps!]