merge bump/nightly-2026-04-16

Author: kim-em

Mathlib.lean

@@ -1514,6 +1514,7 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
+public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
 public import Mathlib.AlgebraicTopology.SimplicialSet.Basic
 public import Mathlib.AlgebraicTopology.SimplicialSet.Boundary
 public import Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
@@ -6978,6 +6979,7 @@ public import Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
 public import Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
 public import Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
 public import Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
+public import Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
 public import Mathlib.Tactic.ComputeDegree
 public import Mathlib.Tactic.CongrExclamation
 public import Mathlib.Tactic.CongrM
@@ -7431,6 +7433,7 @@ public import Mathlib.Topology.Bornology.Real
 public import Mathlib.Topology.CWComplex.Abstract.Basic
 public import Mathlib.Topology.CWComplex.Classical.Basic
 public import Mathlib.Topology.CWComplex.Classical.Finite
+public import Mathlib.Topology.CWComplex.Classical.Graph
 public import Mathlib.Topology.CWComplex.Classical.Subcomplex
 public import Mathlib.Topology.Category.Born
 public import Mathlib.Topology.Category.CompHaus.Basic

Mathlib/Algebra/Category/ModuleCat/Stalk.lean

@@ -64,7 +64,7 @@ to avoid needing even more. (The maxHeartbeats limit was also bumped up a little
 the meaning of maxHeartbeats changed -- level metavariables started allocating some more memory in
 general.) -/
 set_option backward.isDefEq.respectTransparency false in
-set_option maxHeartbeats 720000 in --
+set_option maxHeartbeats 700000 in --
 set_option synthInstance.maxHeartbeats 40000 in
 /-- (Implementation). The module structure on `AddCommGrpCat.FilteredColimits.colimit`. -/
 noncomputable abbrev filteredColimitsModule : Module (RingCat.FilteredColimits.colimit R)

Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean

@@ -87,6 +87,21 @@ lemma δ_eq_iff (i : Fin (d + 2)) :
   ⟨fun h ↦ (hxy.existsUnique_δ_cast_simplex hd).unique h (hxy.δ_index hd),
     by rintro rfl; apply δ_index⟩
 
+include hxy in
+lemma le : x ≤ y := by
+  have := hxy.δ_index rfl
+  simp only [cast_simplex_rfl] at this
+  rw [S.le_def, ← y.subcomplex_cast hxy.dim_eq, Subfunctor.ofSection_le_iff,
+    ← this]
+  exact ⟨(SimplexCategory.δ _).op, rfl⟩
+
+include hxy in
+lemma unique (f : ⦋d⦌ ⟶ ⦋d + 1⦌) [Mono f]
+    (hf : X.map f.op (y.cast (by rw [hxy.dim_eq, hd])).simplex = (x.cast hd).simplex) :
+    f = SimplexCategory.δ (hxy.index hd) :=
+  (hxy.cast hd).2.unique ⟨by dsimp; infer_instance, hf⟩
+    ⟨by dsimp; infer_instance, hxy.δ_index hd⟩
+
 end
 
 include hxy in

Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean

@@ -134,6 +134,14 @@ lemma ne (x : P.I) (y : P.II) :
   have : x ∈ P.I ∩ P.II := ⟨hx, hy⟩
   simp [P.inter] at this
 
+lemma le [P.IsProper] (x : P.II) :
+    x.1 ≤ (P.p x).1 :=
+  (P.isUniquelyCodimOneFace x).le
+
+lemma lt [P.IsProper] (x : P.II) :
+    x.1 < (P.p x).1 :=
+  lt_of_le_of_ne' (P.le x) (P.ne _ _)
+
 variable {Y : SSet.{u}} {B : Y.Subcomplex} (e : Y ≅ X) (hA : A.preimage e.hom = B)
 
 /-- Given an isomorphism `Y ≅ X` of simplicial sets, a pairing `P` of a subcomplex