diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean
index 9821f88ef7ee2e..00db86006680b2 100644
--- a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean
+++ b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean
@@ -96,7 +96,6 @@ lemma le : x ≤ y := by
     ← this]
   exact ⟨(SimplexCategory.δ _).op, rfl⟩
 
-set_option backward.defeqAttrib.useBackward true in
 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) :
@@ -116,7 +115,6 @@ lemma op : (S.opEquiv.symm x).IsUniquelyCodimOneFace (S.opEquiv.symm y) := by
   obtain ⟨i, rfl⟩ := i.rev_surjective
   simpa [← hxy.δ_eq_iff rfl] using hi
 
-set_option backward.defeqAttrib.useBackward true in
 include hxy in
 lemma of_iso {Y : SSet.{u}} (e : X ≅ Y) :
     (S.mk (e.hom.app _ x.simplex)).IsUniquelyCodimOneFace (S.mk (e.hom.app _ y.simplex)) := by
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Op.lean b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Op.lean
index d1ba23806c652e..1354d413a4c0e7 100644
--- a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Op.lean
+++ b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Op.lean
@@ -26,7 +26,7 @@ variable {X : SSet.{u}} {A : X.Subcomplex} (P : A.Pairing)
 
 /-- If `P` is a pairing for a subcomplex `A` of a simplicial set `X`,
 this is the corresponding pairing of `A.op`. -/
-@[simps I II]
+@[implicit_reducible, simps I II]
 def op : A.op.Pairing where
   I := Subcomplex.N.opEquiv ⁻¹' P.I
   II := Subcomplex.N.opEquiv ⁻¹' P.II
@@ -35,18 +35,15 @@ def op : A.op.Pairing where
   p := (N.opEquiv.subtypeEquiv (by simp)).trans
     (P.p.trans (N.opEquiv.symm.subtypeEquiv (by simp)))
 
-set_option backward.defeqAttrib.useBackward true in
 @[simp]
 lemma op_p (x : P.II) :
     dsimp% P.op.p ⟨Subcomplex.N.opEquiv.symm x.1, x.2⟩ =
       ⟨Subcomplex.N.opEquiv.symm (P.p x), by simp⟩ := rfl
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 lemma op_ancestralRel_iff (x y : P.II) :
     P.op.AncestralRel ⟨Subcomplex.N.opEquiv.symm x.1, x.2⟩
       ⟨Subcomplex.N.opEquiv.symm y.1, y.2⟩ ↔ P.AncestralRel x y :=
-  and_congr (not_congr (by aesop)) (by simp)
+  and_congr (not_congr (by simp [Subtype.ext_iff])) (by simp)
 
 instance [P.IsProper] : P.op.IsProper where
   isUniquelyCodimOneFace x := (P.isUniquelyCodimOneFace ⟨_, x.2⟩).op
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean
index e0ec27cc094f6d..7422e4948b29ec 100644
--- a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean
+++ b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean
@@ -146,7 +146,7 @@ variable {Y : SSet.{u}} {B : Y.Subcomplex} (e : Y ≅ X) (hA : A.preimage e.hom
 
 /-- Given an isomorphism `Y ≅ X` of simplicial sets, a pairing `P` of a subcomplex
 `A` of `X`, this is a pairing for a subcomplex `B` of `Y` if `A.preimage e.hom = B`. -/
-@[simps I II]
+@[implicit_reducible, simps I II]
 def ofIso : B.Pairing where
   I := Subcomplex.N.orderIsoOfIso e hA ⁻¹' P.I
   II := Subcomplex.N.orderIsoOfIso e hA ⁻¹' P.II
@@ -165,7 +165,6 @@ unif_hint {X : SSet.{u}} {A : X.Subcomplex} (P : A.Pairing)
     {Y : SSet.{u}} {B : Y.Subcomplex} (e : Y ≅ X) (hA : A.preimage e.hom = B) where
   ⊢ (P.ofIso e hA).II ≟ (N.orderIsoOfIso e hA) ⁻¹' P.II
 
-set_option backward.defeqAttrib.useBackward true in
 @[simp]
 lemma ofIso_p (x : P.II) :
     dsimp% (P.ofIso e hA).p ⟨(Subcomplex.N.orderIsoOfIso e hA).symm x, by simp⟩ =
@@ -175,8 +174,6 @@ lemma ofIso_p (x : P.II) :
   change e'.symm (P.p ⟨e' (e'.symm x), _⟩) = e'.symm (P.p x)
   simp
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 lemma ofIso_ancestralRel_iff (x y : P.II) :
     (P.ofIso e hA).AncestralRel
       ⟨(Subcomplex.N.orderIsoOfIso e hA).symm x, by simp⟩
@@ -184,7 +181,6 @@ lemma ofIso_ancestralRel_iff (x y : P.II) :
     P.AncestralRel x y :=
   and_congr (not_congr (by aesop)) (by simp)
 
-set_option backward.defeqAttrib.useBackward true in
 instance [P.IsProper] : (P.ofIso e hA).IsProper where
   isUniquelyCodimOneFace := by
     rintro ⟨x, hx⟩
@@ -202,8 +198,6 @@ instance [P.IsRegular] : (P.ofIso e hA).IsRegular where
     refine hP.false ⟨fun n ↦ ⟨_, (f n).2⟩, fun n ↦ ?_⟩
     simpa [← P.ofIso_ancestralRel_iff e hA] using hf n
 
-set_option backward.isDefEq.respectTransparency false in
-@[simp]
 lemma ofIso_index (x : P.II) {d : ℕ} (hd : x.1.dim = d) [P.IsProper] :
     ((P.ofIso e hA).isUniquelyCodimOneFace ⟨(N.orderIsoOfIso e hA).symm x, by simp⟩).index hd =
       (isUniquelyCodimOneFace P x).index hd := by
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/PairingCore.lean b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/PairingCore.lean
index f0b398fa36a5c2..34e85a707a447b 100644
--- a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/PairingCore.lean
+++ b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/PairingCore.lean
@@ -62,6 +62,7 @@ variable {A}
 
 /-- The `PairingCore` structure induced by a pairing. The opposite construction
 is `PairingCore.pairing`. -/
+@[implicit_reducible]
 noncomputable def Pairing.pairingCore (P : A.Pairing) [P.IsProper] :
     A.PairingCore where
   ι := P.II
@@ -102,12 +103,12 @@ namespace PairingCore
 variable (h : A.PairingCore)
 
 /-- The type (I) simplices of `h : A.PairingCore`, as a family indexed by `h.ι`. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def type₁ (s : h.ι) : A.N :=
   Subcomplex.N.mk (h.simplex s) (h.nonDegenerate₁ s) (h.notMem₁ s)
 
 /-- The type (II) simplices of `h : A.PairingCore`, as a family indexed by `h.ι`. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def type₂ (s : h.ι) : A.N :=
   Subcomplex.N.mk (X.δ (h.index s) (h.simplex s)) (h.nonDegenerate₂ s)
     (h.notMem₂ s)
@@ -128,21 +129,21 @@ lemma surjective (x : A.N) :
   · exact ⟨s, Or.inr (by rwa [N.ext_iff, SSet.N.ext_iff])⟩
 
 /-- The type (I) simplices of `h : A.PairingCore`, as a subset of `A.N`. -/
-def I : Set A.N := Set.range h.type₁
+abbrev I : Set A.N := Set.range h.type₁
 
 /-- The type (II) simplices of `h : A.PairingCore`, as a subset of `A.N`. -/
-def II : Set A.N := Set.range h.type₂
+abbrev II : Set A.N := Set.range h.type₂
 
 /-- The bijection `h.ι ≃ h.I` when `h : A.PairingCore`. -/
-@[simps! apply_coe]
+@[implicit_reducible, simps! apply_coe]
 noncomputable def equivI : h.ι ≃ h.I := Equiv.ofInjective _ h.injective_type₁
 
 /-- The bijection `h.ι ≃ h.II` when `h : A.PairingCore`. -/
-@[simps! apply_coe]
+@[implicit_reducible, simps! apply_coe]
 noncomputable def equivII : h.ι ≃ h.II := Equiv.ofInjective _ h.injective_type₂
 
 /-- The pairing induced by `h : A.PairingCore`. -/
-@[simps I II]
+@[implicit_reducible, simps I II]
 noncomputable def pairing : A.Pairing where
   I := h.I
   II := h.II
@@ -169,10 +170,9 @@ lemma pairing_p_symm_equivI (x : h.ι) :
     DFunLike.coe (F := h.I ≃ h.II) h.pairing.p.symm (h.equivI x) = h.equivII x := by
   simp [pairing]
 
-set_option backward.defeqAttrib.useBackward true in
 lemma type₁_pairing (x : h.ι) :
     h.type₁ x = h.pairing.p (h.equivII x) := by
-  simp +instances
+  simp
 
 /-- The condition that `h : A.PairingCore` is proper, i.e. for each `s : h.ι`,
 the type (II) simplex `h.type₂ s` is uniquely a `1`-codimensional
@@ -192,8 +192,6 @@ instance [X.Nonsingular] : h.IsProper where
         (fun _ _ hi hj ↦ Nonsingular.δ_injective _
           (h.nonDegenerate₁ s) _ _ (hi.trans hj.symm)))
 
-set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 instance [h.IsProper] : h.pairing.IsProper where
   isUniquelyCodimOneFace x := by
     obtain ⟨s, rfl⟩ := h.equivII.surjective x
@@ -202,16 +200,14 @@ instance [h.IsProper] : h.pairing.IsProper where
 lemma isProper_pairing_iff :
     h.pairing.IsProper ↔ h.IsProper := by
   refine ⟨fun _ ↦ ⟨fun s ↦ ?_⟩, fun _ ↦ inferInstance⟩
-  simpa [type₁_pairing] using h.pairing.isUniquelyCodimOneFace (h.equivII s)
+  simpa using h.pairing.isUniquelyCodimOneFace (h.equivII s)
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma isUniquelyCodimOneFace_index [h.IsProper] (s : h.ι) :
     (h.isUniquelyCodimOneFace s).index rfl = h.index s := by
   symm
   simp [← (h.isUniquelyCodimOneFace s).δ_eq_iff]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma isUniquelyCodimOneFace_index_coe
     [h.IsProper] (s : h.ι) {d : ℕ} (hd : h.dim s = d) :
     ((h.isUniquelyCodimOneFace s).index hd).val = (h.index s).val := by
@@ -239,8 +235,6 @@ instance [h.IsInner] [h.IsProper] : h.pairing.IsInner where
 def AncestralRel (s t : h.ι) : Prop :=
   s ≠ t ∧ h.type₂ s < h.type₁ t
 
-set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 lemma ancestralRel_iff (s t : h.ι) :
     h.AncestralRel s t ↔ h.pairing.AncestralRel (h.equivII s) (h.equivII t) := by
   simp [AncestralRel, Pairing.AncestralRel]
@@ -250,7 +244,6 @@ is regular. -/
 class IsRegular (h : A.PairingCore) extends h.IsProper where
   wf (h) : WellFounded h.AncestralRel
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance [h.IsRegular] : h.pairing.IsRegular where
   wf := by
     have := IsRegular.wf h
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Rank.lean b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Rank.lean
index 99440f0f9894a4..32ce90ba13d5f0 100644
--- a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Rank.lean
+++ b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Rank.lean
@@ -127,7 +127,6 @@ structure WeakRankFunction where
   rank : h.ι → α
   lt {x y : h.ι} : h.AncestralRel x y → h.dim x = h.dim y → rank x < rank y
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- Rank functions for `h : A.PairingCore` correspond to
 rank functions for `h.pairing : A.Pairing`. -/
 noncomputable def rankFunctionEquiv :
@@ -147,7 +146,6 @@ noncomputable def rankFunctionEquiv :
   left_inv _ := by simp
   right_inv _ := by simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- Weak rank functions for `h : A.PairingCore` correspond to
 weak rank functions for `h.pairing : A.Pairing`. -/
 noncomputable def weakRankFunctionEquiv :
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/RelativeCellComplex.lean b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/RelativeCellComplex.lean
index 54b26dc945f846..73179262d2625f 100644
--- a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/RelativeCellComplex.lean
+++ b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/RelativeCellComplex.lean
@@ -25,8 +25,6 @@ cell complex with basic cells given by horn inclusions.
 
 -/
 
-set_option backward.defeqAttrib.useBackward true
-
 @[expose] public section
 
 universe v u
@@ -81,12 +79,10 @@ abbrev map : Δ[c.dim + 1] ⟶ X :=
   yonedaEquiv.symm
     ((P.p c.s).val.cast (P.isUniquelyCodimOneFace c.s).dim_eq).simplex
 
-set_option backward.defeqAttrib.useBackward true in
 @[simp]
 lemma range_map : Subcomplex.range c.map = (P.p c.s).val.subcomplex := by
   rw [range_eq_ofSimplex, Equiv.apply_symm_apply, S.ofSimplex_eq_subcomplex_mk,
     ← S.cast_eq_self _ (P.dim_p c.s)]
-  dsimp [S.subcomplex]
 
 lemma map_app_objEquiv_symm_δ_index :
     c.map.app (op ⦋c.dim⦌) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index)) =
@@ -126,6 +122,7 @@ noncomputable abbrev basicCell (i : ι) (c : f.Cell i) : (c.horn : SSet) ⟶ Δ[
 
 /-- The filtration of a simplicial set given by a rank function
 for a proper pairing of a subcomplex. -/
+@[implicit_reducible]
 def filtration (i : ι) : X.Subcomplex :=
   A ⊔ ⨆ (j : ι) (_ : j < i) (c : f.Cell j), (P.p c.s).val.subcomplex
 
@@ -389,13 +386,12 @@ lemma Cell.ι_t_app {j : ι} (c : f.Cell j) (x : SimplexCategoryᵒᵖ) :
     c.ιSigmaHorn.app x ≫ (f.t j).app x = c.mapHorn.app x :=
   NatTrans.congr_app c.ι_t x
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- Given a rank `j` cell `c` for a rank function `f` for a proper
 pairing of a subcomplex of a simplicial set, this is
 the nondegenerate simplex in `f.sigmaStdSimplex j`
 not in the image of `f.m j : f.sigmaHorn j ⟶ f.sigmaStdSimplex j`
 which corresponds to `c.ιSigmaStdSimplex`. -/
-@[simps]
+@[implicit_reducible, simps]
 noncomputable def Cell.type₁ {j : ι} (c : f.Cell j) : (Subcomplex.range (f.m j)).N where
   simplex := c.ιSigmaStdSimplex.app _ (stdSimplex.objEquiv.symm (𝟙 _))
   nonDegenerate := by
@@ -409,13 +405,12 @@ noncomputable def Cell.type₁ {j : ι} (c : f.Cell j) : (Subcomplex.range (f.m
     obtain ⟨rfl, rfl⟩ := hy
     exact objEquiv_symm_notMem_horn_of_isIso _ _ hy'
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- Given a rank `j` cell `c` for a rank function `f` for a proper
 pairing of a subcomplex of a simplicial set, this is
 the nondegenerate simplex in `f.sigmaStdSimplex j`
 not in the image of `f.m j : f.sigmaHorn j ⟶ f.sigmaStdSimplex j`
 which corresponds to the `c.index`th-face of `c.type₁`. -/
-@[simps]
+@[implicit_reducible, simps]
 noncomputable def Cell.type₂ {j : ι} (c : f.Cell j) : (Subcomplex.range (f.m j)).N where
   simplex := c.ιSigmaStdSimplex.app _
     (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index))
@@ -430,7 +425,6 @@ noncomputable def Cell.type₂ {j : ι} (c : f.Cell j) : (Subcomplex.range (f.m
     obtain ⟨rfl, rfl⟩ := hy
     simpa using (objEquiv_symm_δ_mem_horn_iff _ _).mp hy'
 
-set_option backward.isDefEq.respectTransparency false in
 lemma exists_or_of_range_m_N {j : ι} (s : (Subcomplex.range (f.m j)).N) :
     ∃ (c : f.Cell j), s = c.type₁ ∨ s = c.type₂ := by
   obtain ⟨d, s, hs, hs', rfl⟩ := s.mk_surjective
@@ -475,7 +469,6 @@ lemma w (j : ι) :
   ext c : 1
   simp [← cancel_mono (Subcomplex.ι _)]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma isPullback (j : ι) :
     IsPullback (f.t j) (f.m j) (homOfLE (f.filtration_monotone (Order.le_succ j))) (f.b j) where
   w := f.w j
@@ -501,7 +494,6 @@ lemma isPullback (j : ι) :
     · rw [← NatTrans.comp_app_apply]
       simp)⟩
 
-set_option backward.isDefEq.respectTransparency false in
 lemma range_homOfLE_app_union_range_b_app (j : ι) (d : SimplexCategoryᵒᵖ) :
     Set.range ((homOfLE (f.filtration_monotone (Order.le_succ j))).app d) ⊔
       Set.range ((f.b j).app d) = Set.univ := by
@@ -525,7 +517,6 @@ corresponding to an element in `(Subcomplex.range (f.m j)).N`. -/
 noncomputable def mapN {j : ι} (x : (Subcomplex.range (f.m j)).N) : X.S :=
   S.mk ((f.b j).app _ x.simplex).val
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp]
 lemma mapN_type₁ {j : ι} (c : f.Cell j) : f.mapN c.type₁ = S.mk (P.p c.s).val.simplex := by
   dsimp only [Cell.type₁, mapN]
@@ -534,7 +525,6 @@ lemma mapN_type₁ {j : ι} (c : f.Cell j) : f.mapN c.type₁ = S.mk (P.p c.s).v
   rw [S.ext_iff, c.ι_b_app_apply]
   apply yonedaEquiv_symm_app_id
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma mapN_type₂ {j : ι} (c : f.Cell j) : f.mapN c.type₂ = S.mk c.s.val.simplex := by
   dsimp [mapN]
@@ -565,7 +555,6 @@ private lemma isPushout_aux₃ {j : ι} :
     Function.Injective fun (x : (Subcomplex.range (f.m j)).N) ↦ S.mk ((f.b j).app _ x.simplex) :=
   fun _ _ h ↦ f.isPushout_aux₂ (congr_arg (S.map (Subcomplex.ι _)) h)
 
-set_option backward.isDefEq.respectTransparency false in
 lemma isPushout (j : ι) :
     IsPushout (f.t j) (f.m j) (homOfLE (f.filtration_monotone (Order.le_succ j))) (f.b j) where
   w := f.w j
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/UnionProd.lean b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/UnionProd.lean
index 4ed67e905a0d01..befcd8a2916f87 100644
--- a/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/UnionProd.lean
+++ b/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/UnionProd.lean
@@ -67,19 +67,8 @@ namespace prodStdSimplex
 variable {m : ℕ} {k : Fin (m + 1)} {n : ℕ}
   (x : (Subcomplex.unionProd.{u} Λ[m + 1, k.castSucc] ∂Δ[n]).N) {d : ℕ}
 
-#adaptation_note
-/-- `respectTransparency.types true` changes the auto-generated lemmas' signature -/
-set_option backward.isDefEq.respectTransparency.types false in
-@[simp]
-lemma objEquiv_apply_fst' (hd : x.dim = d) (i : Fin (d + 1)) :
-    dsimp% ((objEquiv (x.cast hd).simplex) i).1 = (x.cast hd).simplex.1 i := rfl
-
-#adaptation_note
-/-- `respectTransparency.types true` changes the auto-generated lemmas' signature -/
-set_option backward.isDefEq.respectTransparency.types false in
-@[simp]
-lemma objEquiv_apply_snd' (hd : x.dim = d) (i : Fin (d + 1)) :
-    dsimp% ((objEquiv (x.cast hd).simplex) i).2 = (x.cast hd).simplex.2 i := rfl
+@[deprecated (since := "2026-08-23")] alias objEquiv_apply_fst' := objEquiv_apply_fst
+@[deprecated (since := "2026-08-23")] alias objEquiv_apply_snd' := objEquiv_apply_snd
 
 namespace pairingCore
 
@@ -146,14 +135,12 @@ does not belong to `Λ[m + 1, k.castSucc].unionProd ∂Δ[n]`. This is
 the smallest `l : Fin (d + 1)` such that `x l` is of the form `(k.succ, _)`. -/
 noncomputable def min : Fin (d + 1) := (finset x hd).min' (nonempty_finset x hd)
 
-set_option backward.isDefEq.respectTransparency.types false in
 lemma simplex_fst_min : dsimp% (x.cast hd).simplex.1 (min x hd) = k.succ := by
   rw [← mem_finset_iff]
   apply Finset.min'_mem
 
-set_option backward.isDefEq.respectTransparency false in
 lemma simplex_fst_le_castSucc_iff (i : Fin (d + 1)) :
-    dsimp% (x.cast hd).simplex.1 i ≤ k.castSucc ↔ i < min x hd := by
+    (x.cast hd).simplex.1 i ≤ k.castSucc ↔ i < min x hd := by
   contrapose!
   refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
   · rw [Fin.castSucc_lt_iff_succ_le] at h
@@ -228,7 +215,7 @@ noncomputable abbrev δ :
   simplex := (Δ[m + 1] ⊗ Δ[n]).δ l.castSucc (x.cast hd).simplex
   nonDegenerate := nonDegenerate_δ (x.cast hd).nonDegenerate _
   notMem := by
-    dsimp
+    simp only [Monoidal.tensorObj_obj]
     -- `simp? [Subcomplex.mem_unionProd_iff, mem_boundary_iff_notMem_range,
     --   mem_horn_iff_notMem_range,stdSimplex.δ_apply]` says:
     simp only [Subcomplex.mem_unionProd_iff, prod_δ_snd, mem_boundary_iff_notMem_range,
@@ -240,7 +227,6 @@ noncomputable abbrev δ :
       obtain rfl | ⟨i, rfl⟩ := Fin.eq_self_or_eq_succAbove l.castSucc i
       · refine ⟨l, ?_⟩
         rw [Fin.succAbove_castSucc_self, ← hi, ← hl.simplex_snd_succ]
-        rfl
       · exact ⟨_, hi⟩
     · obtain ⟨i, hi⟩ := mem_range_left x hd j hj
       dsimp at hi
@@ -338,7 +324,6 @@ lemma φ_of_gt (i : Fin (d + 2)) (hi : (min x hd).castSucc < i) :
   rw [φ_of_ne _ _ _ hi.ne', Fin.predAbove_of_castSucc_lt _ _ hi]
 
 set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 @[simp]
 lemma φ_succ_snd : (φ x hd (min x hd).succ).2 = (φ x hd (min x hd).castSucc).2 := by
   have := φ_succAbove x hd (min x hd)
@@ -418,10 +403,8 @@ lemma notMem_simplex :
   exact (Subcomplex.unionProd.{u} Λ[m + 1, k.castSucc] ∂Δ[n]).map
     (SimplexCategory.δ (min x hd).castSucc).op h
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 /-- The type (I) simplex reconstructed from a type (II) simplex. -/
-@[simps]
+@[implicit_reducible, simps]
 noncomputable def type₁ : Type₁ k n where
   x :=
     Subcomplex.N.mk (hx.simplex hd) (hx.simplex_mem_nonDegenerate hd)
@@ -439,23 +422,20 @@ variable {hd : x.dim = d + 1} {l : Fin (d + 1)} (hl : IsIndex x hd l.succ)
 
 include hl
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 lemma min_δ : min (d := d) hl.δ rfl = l := by
   refine le_antisymm (Finset.min'_le _ _ ?_)
     (Finset.le_min' _ _ _ (fun y hy ↦ ?_))
   · simp only [mem_finset_iff]
-    simp only [Monoidal.tensorObj_obj, S.cast_dim, S.cast_simplex_rfl, prod_δ_fst,
+    simp only [Monoidal.tensorObj_obj, S.cast_simplex_rfl, prod_δ_fst,
       stdSimplex.δ_apply, Fin.succAbove_castSucc_self]
     exact hl.simplex_fst_succ
-  · simp only [mem_finset_iff, Monoidal.tensorObj_obj, S.cast_dim,
+  · simp only [mem_finset_iff, Monoidal.tensorObj_obj,
       S.cast_simplex_rfl, prod_δ_fst, stdSimplex.δ_apply] at hy
     by_contra!
     rw [Fin.succAbove_of_castSucc_lt _ _ (by grind)] at hy
     grind [(hl.succ_le_simplex_fst_iff y.castSucc).1 hy.symm.le]
 
 set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 lemma isType₂_δ : IsType₂ hl.δ := by
   intro _ rfl t ht
   dsimp at t ht
@@ -467,8 +447,6 @@ lemma isType₂_δ : IsType₂ hl.δ := by
   dsimp [stdSimplex.δ_apply] at hl ht ⊢
   aesop
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 variable {x} in
 lemma eq_of_isType₂_δ {u : (Subcomplex.unionProd.{u} Λ[m + 1, k.castSucc] ∂Δ[n]).N}
     (hu : IsType₂ u) (i : Fin (d + 2))
@@ -481,7 +459,7 @@ lemma eq_of_isType₂_δ {u : (Subcomplex.unionProd.{u} Λ[m + 1, k.castSucc] 
     refine (hu _ rfl l.succ ?_).elim
     simp [isIndex_succ, S.cast_simplex_rfl, hu', stdSimplex.δ_apply,
       Fin.succAbove_of_lt_succ i l.castSucc hi,
-      Fin.succAbove_of_lt_succ i l.succ (by grind), dsimp% hl.simplex_fst_succ,
+      Fin.succAbove_of_lt_succ i l.succ (by grind), hl.simplex_fst_succ,
       dsimp% hl.simplex_snd_succ, dsimp% hl.simplex_fst_castSucc]
   · exact Or.inl rfl
   · obtain rfl | hi := (Fin.castSucc_lt_iff_succ_le.1 hi).eq_or_lt
@@ -491,12 +469,11 @@ lemma eq_of_isType₂_δ {u : (Subcomplex.unionProd.{u} Λ[m + 1, k.castSucc] 
       simp [isIndex_succ, hu', stdSimplex.δ_apply,
         Fin.succAbove_of_castSucc_lt i l.castSucc (by grind),
         Fin.succAbove_of_castSucc_lt i l.succ (by grind),
-        dsimp% hl.simplex_fst_castSucc, dsimp% hl.simplex_snd_succ,
-        dsimp% hl.simplex_fst_succ]
+        hl.simplex_fst_castSucc, hl.simplex_snd_succ,
+        hl.simplex_fst_succ]
 
 end IsIndex
 
-set_option backward.isDefEq.respectTransparency.types false in
 lemma IsType₂.type₁_eq_of_δ_eq
     {t : (Subcomplex.unionProd.{u} Λ[m + 1, k.castSucc] ∂Δ[n]).N}
     (ht : IsType₂ t) (s : Type₁.{u} k n) (hst : s.δ = t) {d : ℕ} (hd : t.dim = d) :
@@ -525,7 +502,7 @@ lemma IsType₂.type₁_eq_of_δ_eq
       (s.index.castSucc.succAbove ((min s.δ rfl).predAbove i)) = _
     congr 1
     rw [← s.isIndex.min_δ]
-    exact Fin.succAbove_predAbove hi -- `simp [hi]` should work but doesn't
+    simp [hi]
 
 lemma Type₁.isType₂_δ (s : Type₁.{u} k n) : IsType₂ s.δ :=
   s.isIndex.isType₂_δ
@@ -671,7 +648,6 @@ instance {m : ℕ} (k : Fin m) (n : ℕ) :
     dsimp [pairingCore]
     simp
 
-set_option backward.defeqAttrib.useBackward true in
 /-- A regular pairing for `Subcomplex.unionProd.{u} Λ[m + 1, k.castSucc] ∂Δ[n]`
 when `k : Fin (m + 1)` and `n : ℕ`. -/
 noncomputable def pairing {m : ℕ} (k : Fin (m + 2)) (n : ℕ) :
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesSubcomplex.lean b/Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesSubcomplex.lean
index 24194269bedfba..c9f695cdfc66cd 100644
--- a/Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesSubcomplex.lean
+++ b/Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesSubcomplex.lean
@@ -44,7 +44,7 @@ lemma mk'_surjective (s : A.N) :
 
 /-- Constructor for the type of nondegenerate simplices which
 do not belong to a given subcomplex of a simplicial set. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def mk {n : ℕ} (x : X _⦋n⦌) (hx : x ∈ X.nonDegenerate n)
     (hx' : x ∉ A.obj _) : A.N where
   simplex := x
@@ -112,7 +112,7 @@ unif_hint {X : SSet.{u}} {A : X.Subcomplex} (s : A.N) (d : ℕ)
   ⊢ (s.cast hd).dim ≟ d
 
 /-- The bijection `A.op.N ≃ A.N` for a subcomplex `A` of a simplicial set.. -/
-@[simps -isSimp apply symm_apply]
+@[implicit_reducible, simps -isSimp apply symm_apply]
 def opEquiv : A.op.N ≃o A.N where
   toFun x := N.mk' (SSet.N.opEquiv x.toN) x.notMem
   invFun y := N.mk' (SSet.N.opEquiv.symm y.toN) y.notMem
@@ -123,7 +123,7 @@ def opEquiv : A.op.N ≃o A.N where
 /-- The bijection `A.N ≃ B.N` on nondegenerate simplices not belonging
 to a certain subcomplex that is induced by an isomorphism `X ≅ Y` of
 simplicial sets which maps `A : X.Subcomplex` to `B : Y.Subcomplex`. -/
-@[simps -isSimp apply symm_apply]
+@[implicit_reducible, simps -isSimp apply symm_apply]
 def orderIsoOfIso {Y : SSet.{u}} {B : Y.Subcomplex} (e : X ≅ Y)
     (hA : B.preimage e.hom = A) : A.N ≃o B.N where
   toFun x := N.mk' (SSet.N.orderIsoOfIso e x.toN) (by subst hA; exact x.notMem)
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean
index ea827da6b9dd82..05a7a8caaed2f9 100644
--- a/Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean
+++ b/Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean
@@ -76,7 +76,7 @@ variable (s : X.S) {d : ℕ} (hd : s.dim = d)
 
 /-- When `s : X.S` is such that `s.dim = d`, this is a term
 that is equal to `s`, but whose dimension if definitionally equal to `d`. -/
-@[simps dim]
+@[implicit_reducible, simps dim]
 def cast : X.S where
   dim := d
   simplex := _root_.cast (by simp only [hd]) s.simplex
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean b/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean
index 15287453dc5f90..a3d7886ae1ba19 100644
--- a/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean
+++ b/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean
@@ -848,23 +848,16 @@ def toOfSimplex : Δ[n] ⟶ ofSimplex x :=
 lemma toOfSimplex_ι :
     toOfSimplex x ≫ (ofSimplex x).ι = yonedaEquiv.symm x := rfl
 
-@[simp]
 lemma yonedaEquiv_toOfSimplex :
     yonedaEquiv (toOfSimplex x) = ⟨x, mem_ofSimplex_obj x⟩ :=
   yonedaEquiv.symm.injective (by cat_disch)
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 instance : Epi (toOfSimplex x) := by
   rw [← range_eq_top_iff]
   ext m ⟨_, u, rfl⟩
   simp only [range_eq_ofSimplex, yonedaEquiv_toOfSimplex, Subfunctor.top_obj,
     Set.top_eq_univ, Set.mem_univ, iff_true]
-  refine ⟨u, ?_⟩
-  dsimp
-  ext
-  rw [← yonedaEquiv.right_inv x]
-  aesop
+  exact ⟨u, by dsimp⟩
 
 lemma isIso_toOfSimplex_iff :
     IsIso (toOfSimplex x) ↔ Mono (yonedaEquiv.symm x) := by
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Preorder/PrincipalSeg.lean b/Mathlib/CategoryTheory/Limits/Shapes/Preorder/PrincipalSeg.lean
index ad5fbbe2f08326..3b4f6fa7402c3a 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Preorder/PrincipalSeg.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Preorder/PrincipalSeg.lean
@@ -24,7 +24,7 @@ open CategoryTheory Category Limits
 
 /-- When `f : α <i β` and a functor `F : β ⥤ C`, this is the cocone
 for `f.monotone.functor ⋙ F : α ⥤ C` whose point is `F.obj f.top`. -/
-@[simps]
+@[implicit_reducible, simps]
 def PrincipalSeg.cocone {α β : Type*} [PartialOrder α] [PartialOrder β]
     (f : α <i β) {C : Type*} [Category* C] (F : β ⥤ C) : Cocone (f.monotone.functor ⋙ F) where
   pt := F.obj f.top
diff --git a/Mathlib/CategoryTheory/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean
index 4990e8716361fe..e86d4cb8485c5f 100644
--- a/Mathlib/CategoryTheory/Monoidal/Category.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Category.lean
@@ -453,7 +453,7 @@ lemma whiskerRightIso_symm {X Y : C} (f : X ≅ Y) (W : C) :
     (whiskerRightIso f W).symm = whiskerRightIso f.symm W := rfl
 
 /-- The tensor product of two isomorphisms is an isomorphism. -/
-@[simps]
+@[implicit_reducible, simps]
 def tensorIso {X Y X' Y' : C} (f : X ≅ Y)
     (g : X' ≅ Y') : X ⊗ X' ≅ Y ⊗ Y' where
   hom := f.hom ⊗ₘ g.hom
diff --git a/Mathlib/CategoryTheory/Monoidal/Functor.lean b/Mathlib/CategoryTheory/Monoidal/Functor.lean
index 92b8152e1e43d5..795cfcd62b99ac 100644
--- a/Mathlib/CategoryTheory/Monoidal/Functor.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Functor.lean
@@ -401,13 +401,13 @@ section
 variable (F : C ⥤ D) [F.Monoidal]
 
 /-- The isomorphism `𝟙_ D ≅ F.obj (𝟙_ C)` when `F` is a monoidal functor. -/
-@[simps]
+@[implicit_reducible, simps]
 def εIso : 𝟙_ D ≅ F.obj (𝟙_ C) where
   hom := ε F
   inv := η F
 
 /-- The isomorphism `F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)` when `F` is a monoidal functor. -/
-@[simps]
+@[implicit_reducible, simps]
 def μIso (X Y : C) : F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y) where
   hom := μ F X Y
   inv := δ F X Y
diff --git a/Mathlib/CategoryTheory/Sites/Subsheaf.lean b/Mathlib/CategoryTheory/Sites/Subsheaf.lean
index 528d518d367616..c8ddd5dfe7b187 100644
--- a/Mathlib/CategoryTheory/Sites/Subsheaf.lean
+++ b/Mathlib/CategoryTheory/Sites/Subsheaf.lean
@@ -151,7 +151,6 @@ noncomputable def Subfunctor.sheafifyLift (f : G.toFunctor ⟶ F') (h : Presieve
     refine Eq.trans ?_ (Presieve.IsSheafFor.valid_glue (h _ s.2)
       ((G.family_of_elements_compatible s.1).map f) (j ≫ i.unop) ?_).symm
     · simp [Presieve.FamilyOfElements.map, Subfunctor.familyOfElementsOfSection]
-      rfl
     · dsimp [Presieve.FamilyOfElements.map] at hj ⊢
       rwa [Functor.map_comp, comp_apply]
 
diff --git a/Mathlib/CategoryTheory/Subfunctor/Basic.lean b/Mathlib/CategoryTheory/Subfunctor/Basic.lean
index 3a8c4a86fc0c43..4c1f8a80122669 100644
--- a/Mathlib/CategoryTheory/Subfunctor/Basic.lean
+++ b/Mathlib/CategoryTheory/Subfunctor/Basic.lean
@@ -137,7 +137,7 @@ instance : Nonempty (Subfunctor F) :=
   inferInstance
 
 /-- The subfunctor as a functor. -/
-@[simps obj map]
+@[implicit_reducible, simps obj map]
 def toFunctor : C ⥤ Type w where
   obj U := G.obj U
   map i := ↾fun x => ⟨F.map i x, G.map i x.prop⟩
diff --git a/Mathlib/CategoryTheory/Types/Basic.lean b/Mathlib/CategoryTheory/Types/Basic.lean
index 7c5bf48a9e36ae..7f722ca493b954 100644
--- a/Mathlib/CategoryTheory/Types/Basic.lean
+++ b/Mathlib/CategoryTheory/Types/Basic.lean
@@ -437,7 +437,7 @@ open CategoryTheory
 variable {X Y : Type u}
 
 /-- Any isomorphism between types gives an equivalence. -/
-@[simps]
+@[implicit_reducible, simps]
 def toEquiv (i : X ≅ Y) : X ≃ Y where
   toFun := i.hom
   invFun := i.inv
diff --git a/Mathlib/Order/Interval/Set/InitialSeg.lean b/Mathlib/Order/Interval/Set/InitialSeg.lean
index 008ac57a7f0569..c5181be11f0a77 100644
--- a/Mathlib/Order/Interval/Set/InitialSeg.lean
+++ b/Mathlib/Order/Interval/Set/InitialSeg.lean
@@ -22,7 +22,7 @@ variable {α : Type*} [Preorder α] {i j : α}
 
 set_option backward.isDefEq.respectTransparency false in
 /-- `Iic j` is an initial segment. -/
-@[simps]
+@[implicit_reducible, simps]
 def initialSegIic (j : α) : Iic j ≤i α where
   toFun j := j
   inj' _ _ _ := by aesop
@@ -30,7 +30,7 @@ def initialSegIic (j : α) : Iic j ≤i α where
   mem_range_of_rel' x k h := by simpa using h.le.trans x.2
 
 /-- `Iio j` is a principal segment. -/
-@[simps]
+@[implicit_reducible, simps]
 def principalSegIio (j : α) : Iio j <i α where
   top := j
   toFun j := j