[#14600] feat: warn on inexact deprecations

batteries/Batteries/Data/Array/Lemmas.lean

@@ -12,7 +12,7 @@ public import Batteries.Data.List.Lemmas
 
 namespace Array
 
-@[deprecated forIn_toList (since := "2025-07-01")]
+@[deprecated forIn_toList +typeChanged (since := "2025-07-01")]
 theorem forIn_eq_forIn_toList [Monad m]
     (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
     forIn as b f = forIn as.toList b f := by

batteries/Batteries/Data/List/Basic.lean

@@ -620,7 +620,7 @@ where
 ```
 Chain R a [b, c, d] ↔ R a b ∧ R b c ∧ R c d
 ``` -/
-@[deprecated IsChain (since := "2025-09-19")]
+@[deprecated IsChain +typeChanged (since := "2025-09-19")]
 def Chain : (α → α → Prop) → α → List α → Prop := (IsChain · <| · :: ·)
 
 set_option linter.deprecated false in

batteries/Batteries/Data/List/Lemmas.lean

@@ -36,7 +36,7 @@ attribute [grind =] zipIdx_nil zipIdx_cons
 
 /-! ### toArray-/
 
-@[deprecated List.getElem_toArray (since := "2025-09-11")]
+@[deprecated List.getElem_toArray +typeChanged (since := "2025-09-11")]
 theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) :
     (Array.mk xs)[i] = xs[i] := List.getElem_toArray h
 
@@ -113,7 +113,7 @@ theorem erase_eq_self_iff_forall_bne [BEq α] (a : α) (xs : List α) :
 
 /-! ### findIdx? -/
 
-@[deprecated findIdx_eq_getD_findIdx? (since := "2025-11-06")]
+@[deprecated findIdx_eq_getD_findIdx? +typeChanged (since := "2025-11-06")]
 theorem findIdx_eq_findIdx? (p : α → Bool) (l : List α) :
     l.findIdx p = (match l.findIdx? p with | some i => i | none => l.length) := by
   rw [findIdx_eq_getD_findIdx?]
@@ -386,14 +386,14 @@ theorem isChain_of_isChain_cons (p : IsChain R (b :: l)) : IsChain R l := by gri
 
 alias IsChain.of_cons := isChain_of_isChain_cons
 
-@[deprecated IsChain.of_cons (since := "2026-02-10")]
+@[deprecated IsChain.of_cons +typeChanged (since := "2026-02-10")]
 theorem isChain_cons_of_isChain_cons_cons : IsChain R (a :: b :: l) →
     IsChain R (b :: l) := IsChain.of_cons
 
 @[deprecated (since := "2025-09-19")]
 alias chain_of_chain_cons := isChain_cons_of_isChain_cons_cons
 
-@[deprecated IsChain.of_cons (since := "2026-02-10")]
+@[deprecated IsChain.of_cons +typeChanged (since := "2026-02-10")]
 theorem isChain_of_isChain_cons_cons : IsChain R (a :: b :: l) →
     IsChain R l := IsChain.of_cons ∘ IsChain.of_cons
 
@@ -445,15 +445,15 @@ theorem isChain_range' (s : Nat) : ∀ n step : Nat,
   | 1, _ => .singleton _
   | n + 2, step => (isChain_range' (s + step) (n + 1) step).cons_cons rfl
 
-@[deprecated isChain_range' (since := "2025-09-19")]
+@[deprecated isChain_range' +typeChanged (since := "2025-09-19")]
 theorem chain_succ_range' (s n step : Nat) :
     IsChain (fun a b => b = a + step) (s :: range' (s + step) n step) := isChain_range'  _ (n + 1) _
 
 theorem isChain_lt_range' (s n : Nat) (h : 0 < step) :
     IsChain (· < ·) (range' s n step) :=
   (isChain_range' s n step).imp fun | _, _, rfl => Nat.lt_add_of_pos_right h
 
-@[deprecated isChain_lt_range' (since := "2025-09-19")]
+@[deprecated isChain_lt_range' +typeChanged (since := "2025-09-19")]
 theorem chain_lt_range' (s n : Nat) (h : 0 < step) :
     IsChain (· < ·) (s :: range' (s + step) n step) := isChain_lt_range' _ (n + 1) h
 

batteries/Batteries/Data/String/Matcher.lean

@@ -121,7 +121,7 @@ abbrev findAllSubstr (s : String) (pattern : Substring.Raw) : Array Substring.Ra
 abbrev findSubstr? (s : String) (pattern : Substring.Raw) : Option Substring.Raw :=
   s.toRawSubstring.findSubstr? pattern
 
-@[deprecated String.contains (since := "2026-02-25"), inherit_doc Substring.Raw.containsSubstr]
+@[deprecated String.contains +typeChanged (since := "2026-02-25"), inherit_doc Substring.Raw.containsSubstr]
 abbrev containsSubstr (s : String) (pattern : Substring.Raw) : Bool :=
   s.toRawSubstring.containsSubstr pattern
 

batteries/Batteries/Logic.lean

@@ -85,14 +85,14 @@ theorem eqRec_heq_self {α : Sort _} {a : α} {motive : (a' : α) → a = a' →
     (x : motive a rfl) {a' : α} (e : a = a') : @Eq.rec α a motive x a' e ≍ x := by
   subst e; rfl
 
-@[deprecated eqRec_heq_iff (since := "12-07-2026")]
+@[deprecated eqRec_heq_iff +typeChanged (since := "12-07-2026")]
 theorem eqRec_heq_iff_heq {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _}
     {x : motive a rfl} {a' : α} {e : a = a'} {β : Sort _} {y : β} :
     @Eq.rec α a motive x a' e ≍ y ↔ x ≍ y := by
   subst e; rfl
 
 
-@[deprecated heq_eqRec_iff (since := "12-07-2026")]
+@[deprecated heq_eqRec_iff +typeChanged (since := "12-07-2026")]
 theorem heq_eqRec_iff_heq {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _}
     {x : motive a rfl} {a' : α} {e : a = a'} {β : Sort _} {y : β} :
     y ≍ @Eq.rec α a motive x a' e ↔ y ≍ x := by

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-07-29
+leanprover/lean4-pr-releases:pr-release-14600-453dceb

mathlib4/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -1219,7 +1219,7 @@ variable (R) in
 semiring.
 
 See note [reducible non-instances]. -/
-@[deprecated isMulCommutative_adjoin (since := "2026-03-11")]
+@[deprecated isMulCommutative_adjoin +typeChanged (since := "2026-03-11")]
 abbrev adjoinNonUnitalCommSemiringOfComm {s : Set A} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :
     NonUnitalCommSemiring (adjoin R s) :=
   have := isMulCommutative_adjoin R hcomm
@@ -1234,7 +1234,7 @@ open scoped IsMulCommutative in
 ring.
 
 See note [reducible non-instances]. -/
-@[deprecated isMulCommutative_adjoin (since := "2026-03-11")]
+@[deprecated isMulCommutative_adjoin +typeChanged (since := "2026-03-11")]
 abbrev adjoinNonUnitalCommRingOfComm (R : Type*) {A : Type*} [CommRing R] [NonUnitalRing A]
     [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A}
     (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) : NonUnitalCommRing (adjoin R s) :=

mathlib4/Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

@@ -769,7 +769,7 @@ open scoped IsMulCommutative in
 semiring.
 
 See note [reducible non-instances]. -/
-@[deprecated isMulCommutative_adjoin (since := "2026-03-11")]
+@[deprecated isMulCommutative_adjoin +typeChanged (since := "2026-03-11")]
 abbrev adjoinCommSemiringOfComm {s : Set A} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :
     CommSemiring (adjoin R s) :=
   have := isMulCommutative_adjoin R hcomm
@@ -849,7 +849,7 @@ variable (R)
 open scoped IsMulCommutative in
 /-- If all elements of `s : Set A` commute pairwise, then `adjoin R s` is a commutative
 ring. -/
-@[deprecated isMulCommutative_adjoin (since := "2026-03-11")]
+@[deprecated isMulCommutative_adjoin +typeChanged (since := "2026-03-11")]
 abbrev adjoinCommRingOfComm {s : Set A} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :
     CommRing (adjoin R s) :=
   have := isMulCommutative_adjoin R hcomm

mathlib4/Mathlib/Algebra/Category/AlgCat/Basic.lean

@@ -149,7 +149,7 @@ instance : Inhabited (AlgCat R) :=
 
 lemma forget_obj {A : AlgCat.{v} R} : (forget (AlgCat.{v} R)).obj A = A := rfl
 
-@[deprecated ConcreteCategory.forget_map_eq_ofHom (since := "2026-03-03")]
+@[deprecated ConcreteCategory.forget_map_eq_ofHom +typeChanged (since := "2026-03-03")]
 lemma forget_map {A B : AlgCat.{v} R} (f : A ⟶ B) :
     (forget (AlgCat.{v} R)).map f = (f : _ → _) :=
   rfl

mathlib4/Mathlib/Algebra/Category/CommAlgCat/Basic.lean

@@ -120,7 +120,7 @@ instance : Inhabited (CommAlgCat R) := ⟨of R R⟩
 
 lemma forget_obj (A : CommAlgCat.{v} R) : (forget (CommAlgCat.{v} R)).obj A = A := rfl
 
-@[deprecated ConcreteCategory.forget_map_eq_ofHom (since := "2026-03-06")]
+@[deprecated ConcreteCategory.forget_map_eq_ofHom +typeChanged (since := "2026-03-06")]
 lemma forget_map (f : A ⟶ B) : (forget (CommAlgCat.{v} R)).map f = (f : _ → _) := rfl
 
 instance : CommRing ((forget (CommAlgCat R)).obj A) := inferInstanceAs <| CommRing A

mathlib4/Mathlib/Algebra/Category/CommBialgCat.lean

@@ -121,7 +121,7 @@ instance : Inhabited (CommBialgCat R) := ⟨of R R⟩
 lemma forget_obj (A : CommBialgCat.{v} R) : (forget (CommBialgCat.{v} R)).obj A = A :=
   rfl
 
-@[deprecated ConcreteCategory.forget_map_eq_ofHom (since := "2026-03-06")]
+@[deprecated ConcreteCategory.forget_map_eq_ofHom +typeChanged (since := "2026-03-06")]
 lemma forget_map (f : A ⟶ B) : (forget (CommBialgCat.{v} R)).map f = (f : _ → _) := rfl
 
 instance : CommRing ((forget (CommBialgCat R)).obj A) := inferInstanceAs <| CommRing A

mathlib4/Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -218,7 +218,7 @@ end
 definitional equality issues. -/
 lemma forget_obj {M : ModuleCat.{v} R} : (forget (ModuleCat.{v} R)).obj M = M := rfl
 
-@[deprecated ConcreteCategory.forget_map_eq_ofHom (since := "2026-03-02")]
+@[deprecated ConcreteCategory.forget_map_eq_ofHom +typeChanged (since := "2026-03-02")]
 lemma forget_map {M N : ModuleCat.{v} R} (f : M ⟶ N) :
     (forget (ModuleCat.{v} R)).map f = (f : _ → _) :=
   rfl

mathlib4/Mathlib/Algebra/Category/ModuleCat/Semi.lean

@@ -195,7 +195,7 @@ definitional equality issues. -/
 lemma forget_obj {M : SemimoduleCat.{v} R} : ((forget (SemimoduleCat.{v} R)).obj M : Type _) = M :=
   rfl
 
-@[deprecated ConcreteCategory.forget_map_eq_ofHom (since := "2026-02-25")]
+@[deprecated ConcreteCategory.forget_map_eq_ofHom +typeChanged (since := "2026-02-25")]
 lemma forget_map {M N : SemimoduleCat.{v} R} (f : M ⟶ N) :
     (forget (SemimoduleCat.{v} R)).map f = (f : _ → _) :=
   rfl

mathlib4/Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean

@@ -55,7 +55,7 @@ class Presentation.IsFinite {M : SheafOfModules.{u} R} (p : M.Presentation) : Pr
 attribute [instance] Presentation.IsFinite.isFiniteType_generators
   Presentation.IsFinite.isFiniteType_relations
 
-@[deprecated Presentation.IsFinite.isFiniteType_relations (since := "2026-04-14")]
+@[deprecated Presentation.IsFinite.isFiniteType_relations +typeChanged (since := "2026-04-14")]
 lemma Presentation.IsFinite.finite_relations {M : SheafOfModules.{u} R} (p : M.Presentation)
     [p.IsFinite] : Finite p.relations.I := GeneratingSections.IsFiniteType.finite
 

mathlib4/Mathlib/Algebra/FreeMonoid/Basic.lean

@@ -114,13 +114,13 @@ theorem toList_one : toList (1 : FreeMonoid α) = [] := rfl
 @[to_additive (attr := simp)]
 theorem ofList_nil : ofList ([] : List α) = 1 := rfl
 
-@[to_additive (attr := deprecated toList_one (since := "2026-03-26"))]
+@[to_additive (attr := deprecated toList_one +typeChanged (since := "2026-03-26"))]
 theorem toList_nil : toList ([] : FreeMonoid α) = [] := rfl
 
 @[to_additive (attr := simp)]
 theorem toList_mul (xs ys : FreeMonoid α) : toList (xs * ys) = toList xs ++ toList ys := rfl
 
-@[to_additive (attr := deprecated toList_mul (since := "2026-03-26"))]
+@[to_additive (attr := deprecated toList_mul +typeChanged (since := "2026-03-26"))]
 theorem toList_cons (x : α) (xs : FreeMonoid α) : toList (x :: xs) = x :: toList xs := rfl
 
 @[to_additive (attr := simp)]

mathlib4/Mathlib/Algebra/Group/Finsupp.lean

@@ -92,7 +92,7 @@ noncomputable def uniqueAddEquiv (i : ι) [Subsingleton ι] : (ι →₀ M) ≃+
 
 /-- If `M` is the trivial monoid, then the monoid of finitely supported functions `ι →₀ M` is
 is isomorphic to `M`. -/
-@[simps!, deprecated uniqueAddEquiv (since := "2026-05-06")]
+@[simps!, deprecated uniqueAddEquiv +typeChanged (since := "2026-05-06")]
 noncomputable def _root_.AddEquiv.finsuppUnique {ι : Type*} [Unique ι] : (ι →₀ M) ≃+ M where
   toEquiv := .finsuppUnique
   map_add' _ _ := rfl
@@ -177,7 +177,7 @@ lemma support_single_add_single_subset [DecidableEq ι] {f₁ f₂ : ι} {g₁ g
   exact subset_trans Finsupp.support_single_subset (by simp)
 
 set_option backward.isDefEq.respectTransparency false in
-@[deprecated uniqueAddEquiv_symm_apply (since := "2026-05-06")]
+@[deprecated uniqueAddEquiv_symm_apply +typeChanged (since := "2026-05-06")]
 lemma _root_.AddEquiv.finsuppUnique_symm {M : Type*} [AddZeroClass M] (d : M) :
     AddEquiv.finsuppUnique.symm d = single () d := by ext; simp [AddEquiv.finsuppUnique]
 

mathlib4/Mathlib/Algebra/Group/Subgroup/Defs.lean

@@ -399,8 +399,10 @@ theorem toSubmonoid_le {p q : Subgroup G} : p.toSubmonoid ≤ q.toSubmonoid ↔
 @[to_additive]
 lemma coe_nonempty (s : Subgroup G) : (s : Set G).Nonempty := ⟨1, one_mem _⟩
 
-attribute [deprecated OneMemClass.coe_nonempty (since := "2026-04-20")] Subgroup.coe_nonempty
-attribute [deprecated ZeroMemClass.coe_nonempty (since := "2026-04-20")] AddSubgroup.coe_nonempty
+attribute [deprecated OneMemClass.coe_nonempty
+  +typeChanged (since := "2026-04-20")] Subgroup.coe_nonempty
+attribute [deprecated ZeroMemClass.coe_nonempty
+  +typeChanged (since := "2026-04-20")] AddSubgroup.coe_nonempty
 
 end Subgroup
 
@@ -714,11 +716,11 @@ theorem le_normalizer : H ≤ normalizer H := fun x xH n => by
 
 end Normalizer
 
-@[to_additive (attr := deprecated inferInstance (since := "2026-04-09"))]
+@[to_additive (attr := deprecated inferInstance +typeChanged (since := "2026-04-09"))]
 theorem commGroup_isMulCommutative {G : Type*} [CommGroup G] (H : Subgroup G) :
     IsMulCommutative H := inferInstance
 
-@[to_additive (attr := deprecated setLike_mul_comm (since := "2026-03-09"))]
+@[to_additive (attr := deprecated setLike_mul_comm +typeChanged (since := "2026-03-09"))]
 lemma mul_comm_of_mem_isMulCommutative [IsMulCommutative H] {a b : G} (ha : a ∈ H) (hb : b ∈ H) :
     a * b = b * a :=
   setLike_mul_comm ha hb

mathlib4/Mathlib/Algebra/GroupWithZero/Action/Defs.lean

@@ -381,7 +381,7 @@ protected abbrev Function.Surjective.distribMulAction [AddMonoid B] [SMul M B] (
 variable (A)
 
 /-- Each element of the monoid defines an additive monoid homomorphism. -/
-@[simps!, deprecated DistribSMul.toAddMonoidHom (since := "2026-01-07")]
+@[simps!, deprecated DistribSMul.toAddMonoidHom +typeChanged (since := "2026-01-07")]
 def DistribMulAction.toAddMonoidHom (x : M) : A →+ A :=
   DistribSMul.toAddMonoidHom A x
 

mathlib4/Mathlib/Algebra/GroupWithZero/Associated.lean

@@ -538,7 +538,7 @@ instance : IsBotOneClass (Associates M) where
 instance instOrderBot : OrderBot (Associates M) where
   bot_le _ := one_le
 
-@[deprecated _root_.one_le (since := "2026-05-07")]
+@[deprecated _root_.one_le +typeChanged (since := "2026-05-07")]
 protected theorem one_le {a : Associates M} : 1 ≤ a :=
   one_le
 

mathlib4/Mathlib/Algebra/Module/Hom.lean

@@ -115,7 +115,7 @@ namespace AddMonoidHom
 /-- Scalar multiplication on the left as an additive monoid homomorphism.
 
 See also the linear map version of this `Module.End.smulLeft`. -/
-@[simps! -fullyApplied, deprecated DistribSMul.toAddMonoidHom (since := "2026-01-07")]
+@[simps! -fullyApplied, deprecated DistribSMul.toAddMonoidHom +typeChanged (since := "2026-01-07")]
 protected def smulLeft [AddMonoid A] [DistribSMul M A] (c : M) : A →+ A :=
   DistribSMul.toAddMonoidHom _ c
 

mathlib4/Mathlib/Algebra/MonoidAlgebra/Defs.lean

@@ -356,7 +356,7 @@ lemma single_zero (m : M) : (single m 0 : R[M]) = 0 := by simp [single]
 lemma single_add (m : M) (r₁ r₂ : R) : single m (r₁ + r₂) = single m r₁ + single m r₂ := by
   ext; simp
 
-@[to_additive (attr := deprecated coeff_add (since := "2026-06-18"))]
+@[to_additive (attr := deprecated coeff_add +typeChanged (since := "2026-06-18"))]
 lemma coe_add (f g : R[M]) : ⇑(f + g).coeff = f.coeff + g.coeff := rfl
 
 @[to_additive (attr := simp)]
@@ -410,7 +410,7 @@ lemma addHom_ext' {N : Type*} [AddZeroClass N] ⦃f g : R[M] →+ N⦄
     (hfg : ∀ m, f.comp (singleAddHom m) = g.comp (singleAddHom m)) : f = g :=
   addMonoidHom_ext <| by simpa [DFunLike.ext_iff] using hfg
 
-@[to_additive (attr := deprecated Finsupp.sum_single_index (since := "2026-06-18"))]
+@[to_additive (attr := deprecated Finsupp.sum_single_index +typeChanged (since := "2026-06-18"))]
 lemma sum_single_index [AddCommMonoid N] {m : M} {r : R} {h : M → R → N} (h_zero : h m 0 = 0) :
     (single m r).coeff.sum h = h m r := by
   simp [h_zero]
@@ -421,7 +421,7 @@ lemma sum_coeff_single (f : R[M]) : f.coeff.sum single = f := by ext; simp
 @[to_additive (attr := deprecated sum_coeff_single (since := "2026-06-18"))]
 alias sum_single := sum_coeff_single
 
-@[to_additive (attr := deprecated Finsupp.single_apply (since := "2026-06-18"))]
+@[to_additive (attr := deprecated Finsupp.single_apply +typeChanged (since := "2026-06-18"))]
 theorem coeff_single_apply {a a' : M} {b : R} [Decidable (a = a')] :
     (single a b).coeff a' = if a = a' then b else 0 :=
   Finsupp.single_apply
@@ -596,14 +596,14 @@ lemma coeff_single_mul_of_forall_mul_ne (r : R) (x : R[M]) (h : ∀ d, m * d ≠
     (single m r * x).coeff m' = 0 := by classical simp [coeff_mul, h]
 
 set_option backward.isDefEq.respectTransparency false in
-@[to_additive (attr := deprecated coeff_mul_single_of_forall_mul_ne (since := "2026-06-18"))
-  (dont_translate := R)]
+@[to_additive (attr := deprecated coeff_mul_single_of_forall_mul_ne
+  +typeChanged (since := "2026-06-18")) (dont_translate := R)]
 lemma mul_single_apply_of_not_exists_mul (r : R) {g g' : M} (x : R[M])
     (h : ¬∃ d, g' = d * g) : (x * single g r).coeff g' = 0 :=
   coeff_mul_single_of_forall_mul_ne _ _ <| by simpa [eq_comm] using h
 
-@[to_additive (attr := deprecated coeff_single_mul_of_forall_mul_ne (since := "2026-06-18"))
-  (dont_translate := R)]
+@[to_additive (attr := deprecated coeff_single_mul_of_forall_mul_ne
+  +typeChanged (since := "2026-06-18")) (dont_translate := R)]
 lemma single_mul_apply_of_not_exists_mul (r : R) {g g' : M} (x : R[M])
     (h : ¬∃ d, g' = g * d) : (single g r * x).coeff g' = 0 :=
   coeff_single_mul_of_forall_mul_ne _ _ <| by simpa [eq_comm] using h
@@ -930,7 +930,7 @@ lemma intCast_def [MulOneClass M] (z : ℤ) : (z : R[M]) = single 1 (z : R) := r
 @[to_additive (dont_translate := R)]
 instance ring [Monoid M] : Ring R[M] where
 
-@[deprecated coeff_neg (since := "2026-06-18")]
+@[deprecated coeff_neg +typeChanged (since := "2026-06-18")]
 lemma neg_apply (m : M) (x : R[M]) : (-x).coeff m = -x.coeff m := rfl
 
 end Ring

mathlib4/Mathlib/Algebra/MvPolynomial/Basic.lean

@@ -597,8 +597,9 @@ theorem eq_monomial_of_support_subset_singleton {φ : MvPolynomial σ R} {d₀ :
   classical
   ext d
   rcases eq_or_ne d d₀ with rfl | hd
-  · rw [coeff_monomial, if_pos rfl]
-  · rw [notMem_support_iff.mp fun hmem ↦ hd (h d hmem), coeff_monomial, if_neg fun e ↦ hd e.symm]
+  · rw [coeff_monomial, ite_eq_left rfl]
+  · rw [notMem_support_iff.mp fun hmem ↦ hd (h d hmem), coeff_monomial,
+      ite_eq_right fun e ↦ hd e.symm]
 
 @[simp]
 theorem coeff_C [DecidableEq σ] (m) (a) :

mathlib4/Mathlib/Algebra/MvPolynomial/CommRing.lean

@@ -87,7 +87,7 @@ theorem notMem_support_sub_monomial_sub_monomial (d d' : σ →₀ ℕ) (c : R)
     d ∉ (p - (monomial d c - monomial d' c)).support := by
   classical
   rw [notMem_support_iff, coeff_sub, coeff_sub, coeff_monomial, coeff_monomial,
-    if_pos rfl, if_neg hdd'.symm, sub_zero, hc, sub_self]
+    ite_eq_left rfl, ite_eq_right hdd'.symm, sub_zero, hc, sub_self]
 
 /-- Subtracting `monomial d c - monomial d' c` from `p`, where `c = coeff d p` and `d ≠ d'`,
 leaves the support inside `p.support.erase d ∪ {d'}`. -/