diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean b/Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean
index a8ad46dc1d626..1cad63a0ce349 100644
--- a/Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean
+++ b/Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean
@@ -104,7 +104,9 @@ noncomputable def mappingConeHomOfDegreewiseSplitXIso (p q : ℤ) (hpq : p + 1 =
       mappingCone.inl_v_snd_v_assoc, mappingCone.inr_f_snd_v_assoc, zero_sub, sub_neg_eq_add, ← h]
     abel
 
-set_option backward.isDefEq.lazyWhnfCore false in -- See https://github.com/leanprover-community/mathlib4/issues/12534
+-- See https://github.com/leanprover-community/mathlib4/issues/12534
+-- Removing this adds about 7% to the instruction count in this file.
+set_option backward.isDefEq.lazyWhnfCore false in
 /-- The canonical isomorphism `mappingCone (homOfDegreewiseSplit S σ) ≅ S.X₂⟦(1 : ℤ)⟧`. -/
 @[simps!]
 noncomputable def mappingConeHomOfDegreewiseSplitIso :
diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean b/Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean
index 190ca3c42f6fe..9984135144e10 100644
--- a/Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean
+++ b/Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean
@@ -29,7 +29,9 @@ open HomologicalComplex
 
 attribute [local simp] XIsoOfEq_hom_naturality smul_smul
 
-set_option backward.isDefEq.lazyWhnfCore false in -- See https://github.com/leanprover-community/mathlib4/issues/12534
+-- See https://github.com/leanprover-community/mathlib4/issues/12534
+-- Removing this adds about 10% to the instruction count in this file.
+set_option backward.isDefEq.lazyWhnfCore false in
 /-- The natural isomorphism `(K⟦n⟧).sc' i j k ≅ K.sc' i' j' k'` when `n + i = i'`,
 `n + j = j'` and `n + k = k'`. -/
 @[simps!]
diff --git a/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean b/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
index 4001156b0e699..798ea261934d2 100644
--- a/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
+++ b/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
@@ -225,15 +225,10 @@ theorem OrderIso.mulRight₀'_symm {a : α} (ha : a ≠ 0) :
   ext
   rfl
 
-#adaptation_note /-- 2024-04-23
-After https://github.com/leanprover/lean4/pull/3965,
-we need to either write `@inv_zero (G₀ := α) (_)` in `neg_top`,
-or use `set_option backward.isDefEq.lazyProjDelta false`.
-See https://github.com/leanprover-community/mathlib4/issues/12535 -/
 instance : LinearOrderedAddCommGroupWithTop (Additive αᵒᵈ) :=
   { Additive.subNegMonoid, instLinearOrderedAddCommMonoidWithTopAdditiveOrderDual,
     Additive.instNontrivial with
-    neg_top := set_option backward.isDefEq.lazyProjDelta false in @inv_zero _ (_)
+    neg_top := inv_zero (G₀ := α)
     add_neg_cancel := fun a ha ↦ mul_inv_cancel₀ (G₀ := α) (id ha : Additive.toMul a ≠ 0) }
 
 lemma pow_lt_pow_succ (ha : 1 < a) : a ^ n < a ^ n.succ := by