Merge master into nightly-testing

Author: mathlib-nightly-testing[bot]

.github/actions/get-mathlib-ci/action.yml

@@ -10,7 +10,7 @@ inputs:
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
     # This is also updated automatically by .github/workflows/update_dependencies.yml
-    default: 8c3d31d2beba80d86de30b6ccd373d2c3a76b26e
+    default: ca86f6900d53e503e28ec1cfa2bff2f505474553
   path:
     description: Checkout destination path.
     required: false

Archive/Imo/Imo2002Q3.lean

@@ -12,7 +12,7 @@ import Mathlib.RingTheory.Polynomial.Content
 Find all pairs of positive integers $m,n ≥ 3$ for which there exist infinitely many
 positive integers $a$ such that $(a^m+a-1) / (a^n+a^2-1)$ is itself an integer.
 
-# Solution
+## Solution
 
 It suffices to find $(m,n)$ pairs for which $a^n+a^2-1 ∣ a^m+a-1$, where both sides are viewed as
 polynomials in $a$. This automatically gives $n ≤ m$, so we have

Archive/Imo/Imo2010Q5.lean

@@ -25,7 +25,7 @@ Determine if there exists a finite sequence of operations of the allowed types,
 that the five boxes $B_1, B_2, B_3, B_4, B_5$ become empty, while box $B_6$ contains exactly
 $2010^{2010^{2010}}$ coins.
 
-# Solution
+## Solution
 
 We follow the solution from https://web.evanchen.cc/exams/IMO-2010-notes.pdf.
 

Mathlib.lean

@@ -694,9 +694,11 @@ public import Mathlib.Algebra.Jordan.Basic
 public import Mathlib.Algebra.Lie.Abelian
 public import Mathlib.Algebra.Lie.AdjointAction.Basic
 public import Mathlib.Algebra.Lie.AdjointAction.Derivation
+public import Mathlib.Algebra.Lie.AdjointAction.JordanChevalley
 public import Mathlib.Algebra.Lie.BaseChange
 public import Mathlib.Algebra.Lie.Basic
 public import Mathlib.Algebra.Lie.Basis
+public import Mathlib.Algebra.Lie.CartanCriterion
 public import Mathlib.Algebra.Lie.CartanExists
 public import Mathlib.Algebra.Lie.CartanMatrix
 public import Mathlib.Algebra.Lie.CartanSubalgebra
@@ -1568,6 +1570,7 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.Subdivision
 public import Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
 public import Mathlib.AlgebraicTopology.SingularHomology.Basic
 public import Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance
+public import Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat
 public import Mathlib.AlgebraicTopology.SingularSet
 public import Mathlib.AlgebraicTopology.TopologicalSimplex
 public import Mathlib.Analysis.AbsoluteValue.Equivalence
@@ -3514,9 +3517,10 @@ public import Mathlib.Combinatorics.SimpleGraph.Bipartite
 public import Mathlib.Combinatorics.SimpleGraph.Cayley
 public import Mathlib.Combinatorics.SimpleGraph.Circulant
 public import Mathlib.Combinatorics.SimpleGraph.Clique
+public import Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
+public import Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
 public import Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
 public import Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
-public import Mathlib.Combinatorics.SimpleGraph.ConcreteColorings
 public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
 public import Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
 public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
@@ -3528,7 +3532,6 @@ public import Mathlib.Combinatorics.SimpleGraph.DegreeSum
 public import Mathlib.Combinatorics.SimpleGraph.DeleteEdges
 public import Mathlib.Combinatorics.SimpleGraph.Density
 public import Mathlib.Combinatorics.SimpleGraph.Diam
-public import Mathlib.Combinatorics.SimpleGraph.EdgeLabeling
 public import Mathlib.Combinatorics.SimpleGraph.Ends.Defs
 public import Mathlib.Combinatorics.SimpleGraph.Ends.Properties
 public import Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
@@ -3595,11 +3598,13 @@ public import Mathlib.Computability.Language
 public import Mathlib.Computability.MyhillNerode
 public import Mathlib.Computability.NFA
 public import Mathlib.Computability.Partrec
+public import Mathlib.Computability.PartrecBasis
 public import Mathlib.Computability.PartrecCode
 public import Mathlib.Computability.PostTuringMachine
 public import Mathlib.Computability.Primrec
 public import Mathlib.Computability.Primrec.Basic
 public import Mathlib.Computability.Primrec.List
+public import Mathlib.Computability.RE
 public import Mathlib.Computability.RecursiveIn
 public import Mathlib.Computability.Reduce
 public import Mathlib.Computability.RegularExpressions
@@ -7084,8 +7089,8 @@ public import Mathlib.Tactic.Linarith.Parsing
 public import Mathlib.Tactic.Linarith.Preprocessing
 public import Mathlib.Tactic.Linarith.Verification
 public import Mathlib.Tactic.LinearCombination
-public import Mathlib.Tactic.LinearCombination'
 public import Mathlib.Tactic.LinearCombination.Lemmas
+public import Mathlib.Tactic.LinearCombinationPrime
 public import Mathlib.Tactic.Linter
 public import Mathlib.Tactic.Linter.CommandRanges
 public import Mathlib.Tactic.Linter.CommandStart
@@ -7857,6 +7862,7 @@ public import Mathlib.Topology.Sheaves.Skyscraper
 public import Mathlib.Topology.Sheaves.Stalks
 public import Mathlib.Topology.ShrinkingLemma
 public import Mathlib.Topology.Sion
+public import Mathlib.Topology.SmallInductiveDimension
 public import Mathlib.Topology.Sober
 public import Mathlib.Topology.Specialization
 public import Mathlib.Topology.Spectral.Basic

Mathlib/Algebra/Algebra/Basic.lean

@@ -138,7 +138,9 @@ end SubsemiringAlgebra
 def algebraMapSubmonoid (S : Type*) [Semiring S] [Algebra R S] (M : Submonoid R) : Submonoid S :=
   M.map (algebraMap R S)
 
-theorem mem_algebraMapSubmonoid_of_mem {S : Type*} [Semiring S] [Algebra R S] {M : Submonoid R}
+variable {S : Type*} [Semiring S] [Algebra R S]
+
+theorem mem_algebraMapSubmonoid_of_mem {M : Submonoid R}
     (x : M) : algebraMap R S x ∈ algebraMapSubmonoid S M :=
   Set.mem_image_of_mem (algebraMap R S) x.2
 
@@ -147,10 +149,15 @@ lemma algebraMapSubmonoid_self (M : Submonoid R) : Algebra.algebraMapSubmonoid R
   Submonoid.map_id M
 
 @[simp]
-lemma algebraMapSubmonoid_powers {S : Type*} [Semiring S] [Algebra R S] (r : R) :
+lemma algebraMapSubmonoid_powers (r : R) :
     Algebra.algebraMapSubmonoid S (.powers r) = Submonoid.powers (algebraMap R S r) := by
   simp [Algebra.algebraMapSubmonoid]
 
+lemma algebraMapSubmonoid_isUnit_le :
+    algebraMapSubmonoid S (IsUnit.submonoid R) ≤ IsUnit.submonoid S := by
+  rintro x ⟨y, hy, rfl⟩
+  exact hy.map _
+
 end Semiring
 
 section CommSemiring

Mathlib/Algebra/Category/AlgCat/Limits.lean

@@ -67,7 +67,6 @@ instance limitAlgebra :
     Algebra R (Types.Small.limitCone (F ⋙ forget (AlgCat.{w} R))).pt :=
   inferInstanceAs <| Algebra R (Shrink (sectionsSubalgebra F))
 
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
 set_option backward.isDefEq.respectTransparency false in
 /-- `limit.π (F ⋙ forget (AlgCat R)) j` as an `AlgHom`. -/
 def limitπAlgHom (j) :

Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean

@@ -199,7 +199,6 @@ def kerHomogeneousCochainsZeroEquiv
   continuous_invFun := continuous_induced_rng.mpr
     (continuous_induced_rng.mpr ((ContinuousLinearMap.const R G).cont.comp continuous_subtype_val))
 
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
 set_option backward.isDefEq.respectTransparency false in
 open ShortComplex HomologyData in
 /-- `H⁰_cont(G, X) ≅ Xᴳ`. -/

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -509,26 +509,10 @@ def smulNatTrans : R →+* End (forget₂ (ModuleCat R) AddCommGrpCat) where
   toFun r :=
     { app := fun M => M.smul r
       naturality := fun _ _ _ => smul_naturality _ r }
-  map_one' := NatTrans.ext (by
-    #adaptation_note /-- Prior to https://github.com/leanprover/lean4/pull/12244
-    this was just `cat_disch`. -/
-    simp +instances only [forget₂_obj, map_one, End.one_def]
-    cat_disch)
-  map_zero' := NatTrans.ext (by
-    #adaptation_note /-- Prior to https://github.com/leanprover/lean4/pull/12244
-    this was just `cat_disch`. -/
-    simp +instances only [forget₂_obj, map_zero]
-    cat_disch)
-  map_mul' _ _ := NatTrans.ext (by
-    #adaptation_note /-- Prior to https://github.com/leanprover/lean4/pull/12244
-    this was just `cat_disch`. -/
-    simp +instances only [forget₂_obj, map_mul, End.mul_def]
-    cat_disch)
-  map_add' _ _ := NatTrans.ext (by
-    #adaptation_note /-- Prior to https://github.com/leanprover/lean4/pull/12244
-    this was just `cat_disch`. -/
-    simp +instances only [forget₂_obj, map_add]
-    cat_disch)
+  map_one' := by cat_disch
+  map_zero' := by cat_disch
+  map_mul' _ _ := by cat_disch
+  map_add' _ _ := by cat_disch
 
 /-- Given `A : AddCommGrpCat` and a ring morphism `R →+* End A`, this is a type synonym
 for `A`, on which we shall define a structure of `R`-module. -/

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -823,7 +823,6 @@ def unit : 𝟭 (ModuleCat R) ⟶ extendScalars f ⋙ restrictScalars.{max v u
   app _ := Unit.map.{u₁, u₂, v} f
 
 set_option backward.isDefEq.respectTransparency false in
-set_option backward.proofsInPublic true in
 /-- For any `S`-module Y, there is a natural `R`-linear map from `S ⨂ Y` to `Y` by
 `s ⊗ y ↦ s • y` -/
 @[simps! hom_apply]
@@ -832,7 +831,7 @@ def Counit.map {Y : ModuleCat S} : (restrictScalars f ⋙ extendScalars f).obj Y
   { toFun :=
       letI m1 : Module R S := Module.compHom S f
       letI m2 : Module R Y := Module.compHom Y f
-      TensorProduct.lift
+      TensorProduct.lift (σ₁₂ := .id R)
       { toFun := fun s : S =>
         { toFun := fun y : Y => s • y,
           map_add' := smul_add _

Mathlib/Algebra/Category/ModuleCat/Kernels.lean

@@ -37,8 +37,7 @@ def kernelCone : KernelFork f :=
 def kernelIsLimit : IsLimit (kernelCone f) :=
   Fork.IsLimit.mk _
     (fun s => ofHom <|
-    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation on LinearMap.ker
-      LinearMap.codRestrict (LinearMap.ker f.hom) (Fork.ι s).hom fun c =>
+      LinearMap.codRestrict f.hom.ker (Fork.ι s).hom fun c =>
         LinearMap.mem_ker.2 <| by simp [← ConcreteCategory.comp_apply])
     (fun _ => hom_ext <| LinearMap.subtype_comp_codRestrict _ _ _) fun s m h =>
       hom_ext <| LinearMap.ext fun x => Subtype.ext_iff.2 (by simp [← h]; rfl)
@@ -64,11 +63,9 @@ def cokernelIsColimit : IsColimit (cokernelCocone f) :=
     (fun s => ofHom <| (LinearMap.range f.hom).liftQ (Cofork.π s).hom <|
       LinearMap.range_le_ker_iff.2 <| ModuleCat.hom_ext_iff.mp <| CokernelCofork.condition s)
     (fun s => hom_ext <| (LinearMap.range f.hom).liftQ_mkQ (Cofork.π s).hom _) fun s m h => by
-    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation
-    haveI : Epi (ofHom (LinearMap.range f.hom).mkQ) :=
+    haveI : Epi (ofHom f.hom.range.mkQ) :=
       (epi_iff_range_eq_top _).mpr (Submodule.range_mkQ _)
-    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation
-    apply (cancel_epi (ofHom (LinearMap.range f.hom).mkQ)).1
+    apply (cancel_epi (ofHom f.hom.range.mkQ)).1
     exact h
 
 /-- Construct an `IsColimit` structure of cokernels given `Function.Exact`. -/
@@ -105,29 +102,24 @@ variable {G H : ModuleCat.{v} R} (f : G ⟶ H)
 agrees with the usual module-theoretical kernel.
 -/
 noncomputable def kernelIsoKer {G H : ModuleCat.{v} R} (f : G ⟶ H) :
-    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation
-    kernel f ≅ ModuleCat.of R (LinearMap.ker f.hom) :=
+    kernel f ≅ ModuleCat.of R f.hom.ker :=
   limit.isoLimitCone ⟨_, kernelIsLimit f⟩
 
 -- We now show this isomorphism commutes with the inclusion of the kernel into the source.
 @[simp, elementwise]
-    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation
-theorem kernelIsoKer_inv_kernel_ι : (kernelIsoKer f).inv ≫ kernel.ι f =
-    ofHom (LinearMap.ker f.hom).subtype :=
+theorem kernelIsoKer_inv_kernel_ι : (kernelIsoKer f).inv ≫ kernel.ι f = ofHom f.hom.ker.subtype :=
   limit.isoLimitCone_inv_π _ _
 
 @[simp, elementwise]
 theorem kernelIsoKer_hom_ker_subtype :
-    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation
-    (kernelIsoKer f).hom ≫ ofHom (LinearMap.ker f.hom).subtype = kernel.ι f :=
+    (kernelIsoKer f).hom ≫ ofHom f.hom.ker.subtype = kernel.ι f :=
   IsLimit.conePointUniqueUpToIso_inv_comp _ (limit.isLimit _) WalkingParallelPair.zero
 
 /-- The categorical cokernel of a morphism in `ModuleCat`
 agrees with the usual module-theoretical quotient.
 -/
 noncomputable def cokernelIsoRangeQuotient {G H : ModuleCat.{v} R} (f : G ⟶ H) :
-    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation
-    cokernel f ≅ ModuleCat.of R (H ⧸ LinearMap.range f.hom) :=
+    cokernel f ≅ ModuleCat.of R (H ⧸ f.hom.range) :=
   colimit.isoColimitCocone ⟨_, cokernelIsColimit f⟩
 
 -- We now show this isomorphism commutes with the projection of target to the cokernel.