chore: adaptations for nightly-2025-12-13 (#142)

Author: kim-em

Archive/Imo/Imo2015Q6.lean

@@ -85,7 +85,7 @@ lemma pool_subset_Icc : ∀ {t}, pool a t ⊆ Icc 0 2014
   | t + 1 => by
     intro x hx
     simp_rw [pool, mem_map, Equiv.coe_toEmbedding, Equiv.subRight_apply] at hx
-    obtain ⟨y, my, ey⟩ := hx
+    obtain ⟨y, my, rfl⟩ := hx
     suffices y ∈ Icc 1 2015 by rw [mem_Icc] at this ⊢; lia
     rw [mem_insert, mem_erase] at my; rcases my with h | ⟨h₁, h₂⟩
     · exact h ▸ ha.1 t

Mathlib/Algebra/GroupWithZero/Torsion.lean

@@ -27,7 +27,7 @@ theorem IsMulTorsionFree.mk' (ih : ∀ x ≠ 0, ∀ y ≠ 0, ∀ n ≠ 0, (x ^ n
   refine ⟨fun n hn x y hxy ↦ ?_⟩
   by_cases h : x ≠ 0 ∧ y ≠ 0
   · exact ih x h.1 y h.2 n hn hxy
-  grind [pow_eq_zero, zero_pow]
+  grind [eq_zero_of_pow_eq_zero, zero_pow]
 
 variable [UniqueFactorizationMonoid M] [NormalizationMonoid M] [IsMulTorsionFree Mˣ]
 

Mathlib/Algebra/Polynomial/Coeff.lean

@@ -225,7 +225,18 @@ end Fewnomials
 theorem coeff_mul_X_pow (p : R[X]) (n d : ℕ) :
     coeff (p * Polynomial.X ^ n) (d + n) = coeff p d := by
   rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
-  all_goals grind [mem_antidiagonal, mul_zero]
+  #adaptation_note
+  /--
+  It may be possible to change this back to
+  `all_goals grind [mem_antidiagonal, mul_zero]`
+  on nightly-2025-12-14 (or ideally without needing the `mul_zero`),
+  but if not just remove this note.
+  The proof by `grind` is a hack, doing arithmetic reasoning (i.e. `mul_zero`) by e-matching.
+  -/
+  · rintro ⟨i, j⟩ h1 h2
+    rw [coeff_X_pow, if_neg, mul_zero]
+    grind [mem_antidiagonal]
+  · grind [mem_antidiagonal]
 
 @[simp]
 theorem coeff_X_pow_mul (p : R[X]) (n d : ℕ) :

Mathlib/Algebra/Polynomial/RuleOfSigns.lean

@@ -313,7 +313,15 @@ theorem succ_signVariations_le_X_sub_C_mul (hη : 0 < η) (hP : P ≠ 0) :
   · --P is zero degree, therefore a constant.
     have hcQ : 0 < coeff P 0 := by grind [leadingCoeff]
     have hxcQ : coeff ((X - C η) * P) 1 = coeff P 0 := by
-      grind [coeff_X_sub_C_mul, mul_zero, coeff_eq_zero_of_natDegree_lt]
+      #adaptation_note
+      /--
+      It may be possible to change this back to
+      `grind [coeff_X_sub_C_mul, mul_zero, coeff_eq_zero_of_natDegree_lt]`
+      on nightly-2025-12-14 (or ideally without needing the `mul_zero`),
+      but if not just remove this note.
+      The proof by `grind` is a hack, doing arithmetic reasoning (i.e. `mul_zero`) by e-matching.
+      -/
+      simp_all [coeff_X_sub_C_mul, coeff_eq_zero_of_natDegree_lt]
     dsimp [signVariations, coeffList]
     rw [withBotSucc_degree_eq_natDegree_add_one hP, withBotSucc_degree_eq_natDegree_add_one h_mul]
     simp [h_deg_mul, hxcQ, hη, hcQ, hd, List.range_succ]

Mathlib/AlgebraicTopology/SimplicialSet/Path.lean

@@ -104,7 +104,7 @@ def mk₂ {n : ℕ} {X : Truncated.{u} (n + 1)} (p q : X.Path 1)
 
 /-- For `j + l ≤ m`, a path of length `m` restricts to a path of length `l`, namely
 the subpath spanned by the vertices `j ≤ i ≤ j + l` and edges `j ≤ i < j + l`. -/
-def interval (f : Path X m) (j l : ℕ) (h : j + l ≤ m := by lia) : Path X l where
+def interval (f : Path X m) (j l : ℕ) (h : j + l ≤ m := by omega) : Path X l where
   vertex i := f.vertex ⟨j + i, by lia⟩
   arrow i := f.arrow ⟨j + i, by lia⟩
   arrow_src i := f.arrow_src ⟨j + i, by lia⟩

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

@@ -259,6 +259,7 @@ lemma cfcₙHom_eq_cfcₙ_extend {a : A} (g : R → R) (ha : p a) (f : C(σₙ R
   have hg0 : (Function.extend Subtype.val f g) 0 = 0 := by
     rw [← quasispectrum.coe_zero (R := R) a, Subtype.val_injective.extend_apply]
     exact map_zero f
+  generalize Function.extend Subtype.val f g = f' at *
   rw [cfcₙ_apply ..]
   congr!
 

Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean

@@ -60,18 +60,18 @@ variable {J : Type w}
 inductive WalkingParallelFamily (J : Type w) : Type w
   | zero : WalkingParallelFamily J
   | one : WalkingParallelFamily J
+deriving Inhabited
 
 open WalkingParallelFamily
 
+-- We do not use `deriving DecidableEq` here
+-- because it generates an instance with unnecessary hypotheses.
 instance : DecidableEq (WalkingParallelFamily J)
   | zero, zero => isTrue rfl
-  | zero, one => isFalse fun t => WalkingParallelFamily.noConfusion t
-  | one, zero => isFalse fun t => WalkingParallelFamily.noConfusion t
+  | zero, one => isFalse fun t => by grind
+  | one, zero => isFalse fun t => by grind
   | one, one => isTrue rfl
 
-instance : Inhabited (WalkingParallelFamily J) :=
-  ⟨zero⟩
-
 -- Don't generate unnecessary `sizeOf_spec` lemma which the `simpNF` linter will complain about.
 set_option genSizeOfSpec false in
 /-- The type family of morphisms for the diagram indexing a wide (co)equalizer. -/

Mathlib/CategoryTheory/Shift/CommShiftTwo.lean

@@ -66,7 +66,7 @@ noncomputable def CommShift₂Setup.int [Preadditive D] [HasShift D ℤ]
   assoc _ _ _ := by
     dsimp
     rw [← zpow_add, ← zpow_add]
-    cutsat
+    lia
   commShift _ _ := ⟨by cat_disch⟩
   ε p q := (-1) ^ (p * q)
 

Mathlib/Combinatorics/Quiver/Path.lean

@@ -270,7 +270,7 @@ def decidableEqBddPathsOfDecidableEq (n : ℕ) (h₁ : DecidableEq V)
     | _, _, .nil, .nil => isTrue rfl
     | _, _, .nil, .cons _ _
     | _, _, .cons _ _, .nil =>
-      isFalse fun h => Quiver.Path.noConfusion rfl (heq_of_eq (Subtype.mk.inj h))
+      isFalse fun h => Quiver.Path.noConfusion rfl .rfl .rfl .rfl (heq_of_eq (Subtype.mk.inj h))
     | _, _, .cons (b := v') p' α, .cons (b := v'') q' β =>
       match v', v'', h₁ v' v'' with
       | _, _, isTrue (Eq.refl _) =>

Mathlib/Control/Lawful.lean

@@ -21,24 +21,6 @@ section
 
 variable {σ : Type u} {m : Type u → Type v} {α β : Type u}
 
-/--
-`StateT` doesn't require a constructor, but it appears confusing to declare the
-following theorem as a simp theorem.
-```lean
-@[simp]
-theorem run_fun (f : σ → m (α × σ)) (st : σ) : StateT.run (fun s => f s) st = f st :=
-  rfl
-```
-If we declare this theorem as a simp theorem, `StateT.run f st` is simplified to `f st` by eta
-reduction. This breaks the structure of `StateT`.
-So, we declare a constructor-like definition `StateT.mk` and a simp theorem for it.
--/
-protected def mk (f : σ → m (α × σ)) : StateT σ m α := f
-
-@[simp]
-theorem run_mk (f : σ → m (α × σ)) (st : σ) : StateT.run (StateT.mk f) st = f st :=
-  rfl
-
 /-- A copy of `LawfulFunctor.map_const` for `StateT` that holds even if `m` is not lawful. -/
 protected lemma map_const [Monad m] :
     (Functor.mapConst : α → StateT σ m β → StateT σ m α) = Functor.map ∘ Function.const β :=
@@ -62,38 +44,4 @@ theorem run_monadLift {n} [Monad m] [MonadLiftT n m] (x : n α) :
     (monadLift x : ExceptT ε m α).run = Except.ok <$> (monadLift x : m α) :=
   rfl
 
-@[simp]
-theorem run_monadMap {n} [MonadFunctorT n m] (f : ∀ {α}, n α → n α) :
-    (monadMap (@f) x : ExceptT ε m α).run = monadMap (@f) x.run :=
-  rfl
-
 end ExceptT
-
-namespace ReaderT
-
-section
-
-variable {m : Type u → Type v}
-variable {α σ : Type u}
-
-/--
-`ReaderT` doesn't require a constructor, but it appears confusing to declare the
-following theorem as a simp theorem.
-```lean
-@[simp]
-theorem run_fun (f : σ → m α) (r : σ) : ReaderT.run (fun r' => f r') r = f r :=
-  rfl
-```
-If we declare this theorem as a simp theorem, `ReaderT.run f st` is simplified to `f st` by eta
-reduction. This breaks the structure of `ReaderT`.
-So, we declare a constructor-like definition `ReaderT.mk` and a simp theorem for it.
--/
-protected def mk (f : σ → m α) : ReaderT σ m α := f
-
-@[simp]
-theorem run_mk (f : σ → m α) (r : σ) : ReaderT.run (ReaderT.mk f) r = f r :=
-  rfl
-
-end
-
-end ReaderT