diff --git a/lean-toolchain b/lean-toolchain
index b0b85aeb4..af91fa0dc 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-08-06
+leanprover/lean4-pr-releases:pr-release-14536-bb2ac20
diff --git a/mathlib4/Mathlib/Algebra/AddConstMap/Basic.lean b/mathlib4/Mathlib/Algebra/AddConstMap/Basic.lean
index 4e52663a0..d15aa99d4 100644
--- a/mathlib4/Mathlib/Algebra/AddConstMap/Basic.lean
+++ b/mathlib4/Mathlib/Algebra/AddConstMap/Basic.lean
@@ -289,6 +289,8 @@ theorem monotone_iff_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G]
   ⟨(Monotone.monotoneOn · _), fun hf ↦ monotone_iff_forall_lt.2 <|
     AddConstMapClass.rel_map_of_Icc ha fun _x hx _y hy hxy ↦ hf hx hy hxy.le⟩
 
+-- Defeq abuse: there is no `AddConstMapClass _ _ Hᵒᵈ _ _`.
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem antitone_iff_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G]
     [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H]
     [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) :
@@ -301,6 +303,8 @@ theorem strictMono_iff_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid
     StrictMono f ↔ StrictMonoOn f (Icc l (l + a)) :=
   ⟨(StrictMono.strictMonoOn · _), AddConstMapClass.rel_map_of_Icc ha⟩
 
+-- Defeq abuse: there is no `AddConstMapClass _ _ Hᵒᵈ _ _`.
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem strictAnti_iff_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G]
     [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H]
     [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) :
diff --git a/mathlib4/Mathlib/Algebra/Algebra/NonUnitalHom.lean b/mathlib4/Mathlib/Algebra/Algebra/NonUnitalHom.lean
index 5ddd9c839..17bdad6d8 100644
--- a/mathlib4/Mathlib/Algebra/Algebra/NonUnitalHom.lean
+++ b/mathlib4/Mathlib/Algebra/Algebra/NonUnitalHom.lean
@@ -100,6 +100,9 @@ variable [Semiring R] [Semiring S] {φ : R →+* S}
   {A B : Type*} [NonUnitalNonAssocSemiring A] [Module R A]
   [NonUnitalNonAssocSemiring B] [Module S B]
 
+-- This needs `DFunLike.coe φ = DFunLike.coe (φ : R →* S)` to hold at `instances` transparency,
+-- which seems reasonable but isn't true at the moment.
+set_option backward.isDefEq.respectTransparency.instances false in
 -- see Note [lower instance priority]
 instance (priority := 100) {F R S A B : Type*}
     {_ : Semiring R} {_ : Semiring S} {φ : R →+* S}
diff --git a/mathlib4/Mathlib/Algebra/Azumaya/Matrix.lean b/mathlib4/Mathlib/Algebra/Azumaya/Matrix.lean
index dda8ae32d..d31903665 100644
--- a/mathlib4/Mathlib/Algebra/Azumaya/Matrix.lean
+++ b/mathlib4/Mathlib/Algebra/Azumaya/Matrix.lean
@@ -54,8 +54,7 @@ lemma AlgHom.mulLeftRightMatrix.comp_inv :
   apply (Matrix.stdBasis _ _ _).ext
   intro ⟨i, j⟩
   simp only [LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, map_sum,
-    map_smul, stdBasis_eq_single, LinearMap.coe_sum, Finset.sum_apply,
-    LinearMap.smul_apply, LinearMap.id_coe, id_eq]
+    stdBasis_eq_single, LinearMap.coe_sum, Finset.sum_apply, LinearMap.id_coe, id_eq]
   ext k l
   simp [sum_apply, Matrix.mul_apply, single, Fintype.sum_prod_type, ite_and]
 
diff --git a/mathlib4/Mathlib/Algebra/Category/CommAlgCat/Monoidal.lean b/mathlib4/Mathlib/Algebra/Category/CommAlgCat/Monoidal.lean
index 008f859d5..937c48161 100644
--- a/mathlib4/Mathlib/Algebra/Category/CommAlgCat/Monoidal.lean
+++ b/mathlib4/Mathlib/Algebra/Category/CommAlgCat/Monoidal.lean
@@ -95,6 +95,7 @@ variable (A B) in
 variable (A B) in
 @[simp] lemma braiding_inv_hom : (β_ A B).inv.hom = (comm R B A).toAlgHom := rfl
 
+set_option backward.isDefEq.respectTransparency.instances false in
 attribute [local ext] Quiver.Hom.unop_inj in
 instance : CartesianMonoidalCategory (CommAlgCat.{u} R)ᵒᵖ where
   isTerminalTensorUnit := terminalOpOfInitial isInitialSelf
diff --git a/mathlib4/Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean b/mathlib4/Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean
new file mode 100644
index 000000000..fcd3c6a73
--- /dev/null
+++ b/mathlib4/Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean
@@ -0,0 +1,220 @@
+/-
+Copyright (c) 2025 Richard Hill. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Hill, Andrew Yang
+-/
+module
+
+public import Mathlib.Algebra.Category.ModuleCat.Topology.Homology
+public import Mathlib.Algebra.Homology.Embedding.Restriction
+public import Mathlib.Algebra.Homology.Functor
+public import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
+public import Mathlib.CategoryTheory.Action.Limits
+public import Mathlib.Topology.ContinuousMap.Algebra
+
+/-!
+
+# Continuous cohomology
+
+We define continuous cohomology as the homology of homogeneous cochains.
+
+## Implementation details
+
+We define homogeneous cochains as `g`-invariant continuous function in `C(G, C(G,...,C(G, M)))`
+instead of the usual `C(Gⁿ, M)` to allow more general topological groups other than locally compact
+ones. For this to work, we also work in `Action (TopModuleCat R) G`, where the `G` action on `M`
+is only continuous on `M`, and not necessarily continuous in both variables, because the `G` action
+on `C(G, M)` might not be continuous on both variables even if it is on `M`.
+
+For the differential map, instead of a finite sum we use the inductive definition
+`d₋₁ : M → C(G, M) := const : m ↦ g ↦ m` and
+`dₙ₊₁ : C(G, _) → C(G, C(G, _)) := const - C(G, dₙ) : f ↦ g ↦ f - dₙ (f (g))`
+See `ContinuousCohomology.MultiInd.d`.
+
+## Main definition
+- `ContinuousCohomology.homogeneousCochains`:
+  The functor taking an `R`-linear `G`-representation to the complex of homogeneous cochains.
+- `continuousCohomology`:
+  The functor taking an `R`-linear `G`-representation to its `n`-th continuous cohomology.
+
+## TODO
+- Show that it coincides with `groupCohomology` for discrete groups.
+- Give the usual description of cochains in terms of `n`-ary functions for locally compact groups.
+- Show that short exact sequences induce long exact sequences in certain scenarios.
+-/
+
+set_option backward.defeqAttrib.useBackward true
+
+@[expose] public section
+
+open CategoryTheory Functor ContinuousMap
+
+variable (R G : Type*) [CommRing R] [Group G] [TopologicalSpace R]
+
+namespace ContinuousCohomology
+
+variable [TopologicalSpace G] [IsTopologicalGroup G]
+
+variable {R G} in
+/-- The `G` representation `C(G, rep)` given a representation `rep`.
+The `G` action is defined by `g • f := x ↦ g • f (g⁻¹ * x)`. -/
+abbrev Iobj (rep : Action (TopModuleCat R) G) : Action (TopModuleCat R) G where
+  V := .of R C(G, rep.V)
+  ρ :=
+  { toFun g := TopModuleCat.ofHom
+      { toFun f := .comp (rep.ρ g).hom (f.comp (Homeomorph.mulLeft g⁻¹))
+        map_add' _ _ := by ext; simp
+        map_smul' _ _ := by ext; simp
+        cont := (continuous_postcomp _).comp (continuous_precomp _) }
+    map_one' := ConcreteCategory.ext (by ext; simp)
+    map_mul' _ _ := ConcreteCategory.ext (by ext; simp [mul_assoc]) }
+
+lemma Iobj_ρ_apply (rep : Action (TopModuleCat R) G) (g f x) :
+    ((Iobj rep).ρ g).hom f x = (rep.ρ g).hom (f (g⁻¹ * x)) := rfl
+
+/-- The functor taking a representation `rep` to the representation `C(G, rep)`. -/
+@[simps]
+def I : Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G where
+  obj := Iobj
+  map {M N} φ :=
+  { hom := TopModuleCat.ofHom (ContinuousLinearMap.compLeftContinuous _ _ φ.hom.hom)
+    comm g := by
+      ext f g'
+      change (M.ρ g ≫ φ.hom).hom (f (g⁻¹ * g')) = (φ.hom ≫ N.ρ g).hom (f (g⁻¹ * g'))
+      rw [φ.comm] }
+  map_id _ := rfl
+  map_comp _ _ := rfl
+
+instance : (I R G).Additive where
+instance : (I R G).Linear R where
+
+/-- The constant function `rep ⟶ C(G, rep)` as a natural transformation. -/
+@[simps]
+def const : 𝟭 _ ⟶ I R G where
+  app _ := { hom := TopModuleCat.ofHom (.const _ _), comm _ := rfl }
+  naturality _ _ _ := rfl
+
+namespace MultiInd
+
+set_option linter.style.whitespace false in -- manual alignment is not recognised
+/-- The n-th functor taking `M` to `C(G, C(G,...,C(G, M)))` (with n `G`s).
+These functors form a complex, see `MultiInd.complex`. -/
+def functor : ℕ → Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G
+  | 0     => 𝟭 _
+  | n + 1 => functor n ⋙ I R G
+
+set_option linter.style.whitespace false in -- manual alignment is not recognised
+set_option backward.isDefEq.respectTransparency.instances false in
+/-- The differential map in `MultiInd.complex`. -/
+def d : ∀ n : ℕ, functor R G n ⟶ functor R G (n + 1)
+  | 0     => const R G
+  | n + 1 => whiskerLeft (functor R G (n + 1)) (const R G) - (by exact whiskerRight (d n) (I R G))
+
+lemma d_zero : d R G 0 = const R G := rfl
+
+set_option backward.isDefEq.respectTransparency.instances false in
+lemma d_succ (n : ℕ) :
+    d R G (n + 1) = whiskerLeft (functor R G (n + 1)) (const R G) -
+      (by exact whiskerRight (d R G n) (I R G)) := rfl
+
+set_option backward.isDefEq.respectTransparency false in
+@[reassoc (attr := simp)]
+lemma d_comp_d (n : ℕ) :
+    d R G n ≫ d R G (n + 1) = 0 := by
+  induction n with
+  | zero =>
+    rw [d_succ, Preadditive.comp_sub, sub_eq_zero]
+    rfl
+  | succ n ih =>
+    rw [d_succ R G (n + 1), Preadditive.comp_sub]
+    nth_rw 2 [d_succ]
+    rw [Preadditive.sub_comp, ← whiskerRight_comp, ih,
+      Functor.whiskerRight_zero, sub_zero, sub_eq_zero]
+    rfl
+
+/-- The complex of functors whose behaviour pointwise takes an `R`-linear `G`-representation `M`
+to the complex `M → C(G, M) → ⋯ → C(G, C(G,...,C(G, M))) → ⋯`
+The `G`-invariant submodules of it is the homogeneous cochains (shifted by one). -/
+def complex : CochainComplex (Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) ℕ :=
+  CochainComplex.of (functor R G) (d R G) (d_comp_d R G)
+
+end MultiInd
+
+/-- The functor taking an `R`-linear `G`-representation to its `G`-invariant submodule. -/
+def invariants : Action (TopModuleCat R) G ⥤ TopModuleCat R where
+  obj M := .of R
+    { carrier := { x | ∀ g : G, (M.ρ g).hom x = x }
+      add_mem' hx hy g := by simp [hx g, hy g]
+      zero_mem' := by simp
+      smul_mem' r x hx g := by simp [hx g] : Submodule R M.V }
+  map f := TopModuleCat.ofHom
+    { toLinearMap := f.hom.hom.restrict fun x hx g ↦
+        congr($(f.comm g) x).symm.trans congr(f.hom.hom $(hx g))
+      cont := continuous_induced_rng.mpr (f.hom.hom.2.comp continuous_subtype_val) }
+
+instance : (invariants R G).Linear R where
+instance : (invariants R G).Additive where
+
+/-- `homogeneousCochains R G` is the functor taking
+an `R`-linear `G`-representation to the complex of homogeneous cochains. -/
+def homogeneousCochains : Action (TopModuleCat R) G ⥤ CochainComplex (TopModuleCat R) ℕ :=
+  (MultiInd.complex R G).asFunctor ⋙ (invariants R G).mapHomologicalComplex _ ⋙
+    (ComplexShape.embeddingUp'Add 1 1).restrictionFunctor _
+
+/-- `continuousCohomology R G n` is the functor taking
+an `R`-linear `G`-representation to its `n`-th continuous cohomology. -/
+noncomputable
+def _root_.continuousCohomology (n : ℕ) : Action (TopModuleCat R) G ⥤ TopModuleCat R :=
+  homogeneousCochains R G ⋙ HomologicalComplex.homologyFunctor _ _ n
+
+set_option backward.isDefEq.respectTransparency false in
+/-- The `0`-homogeneous cochains are isomorphic to `Xᴳ`. -/
+def kerHomogeneousCochainsZeroEquiv
+    (X : Action (TopModuleCat R) G) (n : ℕ) (hn : n = 1) :
+    (((homogeneousCochains R G).obj X).d 0 n).hom.ker ≃L[R] (invariants R G).obj X where
+  toFun x :=
+  { val := DFunLike.coe (F := C(G, _)) x.1.1 1
+    property g := by
+      subst hn
+      obtain ⟨⟨x : C(G, _), hx⟩, hx'⟩ := x
+      have : (X.ρ g).hom (x (g⁻¹ * 1)) = x 1 := congr(DFunLike.coe (F := C(G, _)) $(hx g) 1)
+      have hx' : x (g⁻¹ * 1) - x 1 = 0 :=
+        congr(DFunLike.coe (F := C(G, _)) (DFunLike.coe (F := C(G, _)) ($hx').1 1) (g⁻¹ * 1))
+      rw [sub_eq_zero] at hx'
+      exact congr((X.ρ g).hom $hx').symm.trans this }
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+  invFun x := by
+    refine ⟨⟨ContinuousLinearMap.const R _ x.1, fun g ↦ ContinuousMap.ext fun a ↦
+      by subst hn; exact x.2 g⟩, ?_⟩
+    subst hn
+    exact Subtype.ext (ContinuousMap.ext fun a ↦
+      ContinuousMap.ext fun b ↦ show x.1 - x.1 = (0 : X.V) by simp)
+  left_inv x := by
+    subst hn
+    obtain ⟨⟨x : C(G, _), hx⟩, hx'⟩ := x
+    refine Subtype.ext (Subtype.ext <| ContinuousMap.ext fun a ↦ ?_)
+    have hx' : x 1 - x a = 0 :=
+      congr(DFunLike.coe (F := C(G, _)) (DFunLike.coe (F := C(G, _)) ($hx').1 a) 1)
+    rwa [sub_eq_zero] at hx'
+  right_inv _ := rfl
+  continuous_toFun := continuous_induced_rng.mpr ((continuous_eval_const (F := C(G, _)) 1).comp
+      (continuous_subtype_val.comp continuous_subtype_val))
+  continuous_invFun := continuous_induced_rng.mpr
+    (continuous_induced_rng.mpr ((ContinuousLinearMap.const R G).cont.comp continuous_subtype_val))
+
+set_option backward.isDefEq.respectTransparency false in
+open ShortComplex HomologyData in
+/-- `H⁰_cont(G, X) ≅ Xᴳ`. -/
+noncomputable
+def continuousCohomologyZeroIso : (continuousCohomology R G 0) ≅ invariants R G :=
+  NatIso.ofComponents (fun X ↦ (ofIsLimitKernelFork _ (by simp) _
+    (TopModuleCat.isLimitKer _)).left.homologyIso ≪≫ TopModuleCat.ofIso
+      (kerHomogeneousCochainsZeroEquiv R G X _ (by simp))) fun {X Y} f ↦ by
+  dsimp [continuousCohomology, HomologicalComplex.homologyMap]
+  rw [Category.assoc, ← Iso.inv_comp_eq]
+  rw [LeftHomologyData.leftHomologyIso_inv_naturality_assoc, Iso.inv_hom_id_assoc,
+    ← cancel_epi (LeftHomologyData.π _), leftHomologyπ_naturality'_assoc]
+  rfl
+
+end ContinuousCohomology
diff --git a/mathlib4/Mathlib/Algebra/Category/FGModuleCat/Basic.lean b/mathlib4/Mathlib/Algebra/Category/FGModuleCat/Basic.lean
index 1de129acf..38f8e641a 100644
--- a/mathlib4/Mathlib/Algebra/Category/FGModuleCat/Basic.lean
+++ b/mathlib4/Mathlib/Algebra/Category/FGModuleCat/Basic.lean
@@ -110,6 +110,8 @@ variable {R} in
 instance (V : FGModuleCat.{v} R) : Module.Finite R V :=
   V.property
 
+-- Needs to unfold the `forget₂` at `instances` transparency.
+set_option backward.isDefEq.respectTransparency.instances false in
 instance : (forget₂ (FGModuleCat.{v} R) (ModuleCat.{v} R)).Full where
   map_surjective f := ⟨ofHom f.hom, rfl⟩
 
diff --git a/mathlib4/Mathlib/Algebra/Category/Grp/Colimits.lean b/mathlib4/Mathlib/Algebra/Category/Grp/Colimits.lean
index bcef27d14..fda41af16 100644
--- a/mathlib4/Mathlib/Algebra/Category/Grp/Colimits.lean
+++ b/mathlib4/Mathlib/Algebra/Category/Grp/Colimits.lean
@@ -301,6 +301,13 @@ namespace AddCommGrpCat
 
 open QuotientAddGroup
 
+#adaptation_note
+/--
+This definition fails without `respectTransparency false`. Removing `lift_mk` from the `dsimp only`
+set in `inv_hom_id` would help. A more sustainable fix would probably be to revisit the `lift_mk`
+refl lemma: Its LHS and RHS are not defeq at implicit transparency. Either the lemma shouldn't be
+a refl lemma or more declarations need to be implicit-reducible.
+-/
 set_option backward.isDefEq.respectTransparency false in
 set_option backward.defeqAttrib.useBackward true in
 /-- The categorical cokernel of a morphism in `AddCommGrpCat`
@@ -321,8 +328,8 @@ noncomputable def cokernelIsoQuotient {G H : AddCommGrpCat.{u}} (f : G ⟶ H) :
     rfl
   inv_hom_id := by
     ext x
-    dsimp only [hom_comp, hom_ofHom, hom_zero, AddMonoidHom.coe_comp, coe_mk',
-      Function.comp_apply, AddMonoidHom.zero_apply, id_eq, lift_mk, hom_id, AddMonoidHom.coe_id]
+    dsimp only [hom_comp, hom_ofHom, hom_zero, AddMonoidHom.coe_comp, coe_mk', lift_mk,
+      Function.comp_apply, AddMonoidHom.zero_apply, id_eq, hom_id, AddMonoidHom.coe_id]
     exact QuotientAddGroup.induction_on (α := H) x <| cokernel.π_desc_apply f _ _
 
 end AddCommGrpCat
diff --git a/mathlib4/Mathlib/Algebra/Category/Grp/FiniteGrp.lean b/mathlib4/Mathlib/Algebra/Category/Grp/FiniteGrp.lean
index 9773380df..dc08ec8eb 100644
--- a/mathlib4/Mathlib/Algebra/Category/Grp/FiniteGrp.lean
+++ b/mathlib4/Mathlib/Algebra/Category/Grp/FiniteGrp.lean
@@ -48,6 +48,8 @@ instance : CoeSort FiniteGrp.{u} (Type u) where
 instance : Category FiniteGrp :=
   inferInstanceAs <| Category (InducedCategory _ FiniteGrp.toGrp)
 
+-- Would need to have a new type synonym for the `FunLike` instance for the induced category.
+set_option backward.isDefEq.respectTransparency.instances false in
 @[to_additive]
 instance : ConcreteCategory FiniteGrp (· →* ·) :=
   inferInstanceAs <| ConcreteCategory (InducedCategory _ toGrp) _
diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
index ecd029ee9..8b79b35a8 100644
--- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
+++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@@ -98,6 +98,7 @@ lemma forget₂_map_restrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ri
     (forget₂ _ Ab).map ((ModuleCat.restrictScalars f).map g) = (forget₂ _ Ab).map g :=
   rfl
 
+set_option backward.isDefEq.respectTransparency.instances false in
 instance {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
     (restrictScalars.{v} f).Faithful where
   map_injective h := by
@@ -652,8 +653,10 @@ protected noncomputable def counit' : coextendScalars f ⋙ restrictScalars f 
 
 end RestrictionCoextensionAdj
 
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 -- Porting note: very fiddly universes
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Restriction of scalars is left adjoint to coextension of scalars. -/
 -- @[simps] Porting note: not in normal form and not used
 def restrictCoextendScalarsAdj {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean
index 63b60eb1d..0e207dcfc 100644
--- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean
+++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean
@@ -78,6 +78,34 @@ variable (d : M.Derivation φ)
 @[simp] lemma d_one (X : Dᵒᵖ) : d.d (X := X) 1 = 0 := by
   simpa using d.d_mul (X := X) 1 1
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized, writing `Y` for
+`Opposite.op (F.obj (Opposite.unop X))`:
+`FunLike (↑(M.obj Y) →ₗ[↑(R.obj Y)] ↑(N.obj Y)) ↑(M.obj Y) ↑(N.obj Y)`
+It is needed by the `rw [map_zero]` in `d_app` below; the accompanying `ZeroHomClass` fails the
+same way.
+
+The failure happens while applying `@LinearMap.instFunLike`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type
+is `Module ↑(R.obj Y) ↑(M.obj Y)`, whereas the assigned value `(M.obj (F.op.obj X)).isModule` has
+type `Module ↑((R ⋙ forget₂ CommRingCat RingCat).obj (F.op.obj X)) ↑(M.obj (F.op.obj X))`. The
+comparison bottoms out at
+`(R.obj Y).1 =?= ((R ⋙ forget₂ CommRingCat RingCat).obj (F.op.obj X)).1`, which would require
+unfolding `Functor.comp` and `Functor.op`; both are `@[implicit_reducible]` and therefore do not
+unfold at the `.instances` transparency that instance search runs at. Lean falls back to synthesize
+an instance of the correct type, which succeeds, but it returns `(M.obj Y).isModule`, which is again
+not defeq to the assigned value, stalling at `F.op.1 X =?= Opposite.op (F.obj (Opposite.unop X))`.
+That comparison, too, runs at `.instances`, since `respectTransparency false` suppresses the
+transparency bump that instance-implicit arguments would otherwise receive.
+
+Potential fix: see `# Fix` below — mark `ModuleCat.restrictScalars` and
+`ModuleCat.RestrictScalars.obj'` implicit-reducible. Then `respectTransparency false` and
+`instanceTypes false` can both go, and the `erw` becomes an `rw`.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The postcomposition of a derivation by a morphism of presheaves of modules. -/
@@ -201,6 +229,7 @@ noncomputable def relativeDifferentials' :
 
 attribute [simp] relativeDifferentials'_obj
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 lemma relativeDifferentials'_map_d {X Y : Dᵒᵖ} (f : X ⟶ Y) (x : R.obj X) :
     DFunLike.coe (α := CommRingCat.KaehlerDifferential (φ'.app X))
diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean
index a2f9f7c75..dce82a3a4 100644
--- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean
+++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean
@@ -156,8 +156,7 @@ def colimitCocone : Cocone F where
     { app := coconeMorphism F
       naturality _ _ f := by
         ext
-        simpa using! (Types.TypeMax.colimitCocone
-          (F ⋙ forget (ModuleCat R))).ι.naturality_apply f _ }
+        simpa using! (F ⋙ forget (ModuleCat R)).ιColimitType_map f _ }
 
 set_option backward.isDefEq.respectTransparency false in
 /-- Given a cocone `t` of `F`, the induced monoid linear map from the colimit to the cocone point.
diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/InjectiveDimension.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/InjectiveDimension.lean
index 384f9e816..a697dbe72 100644
--- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/InjectiveDimension.lean
+++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/InjectiveDimension.lean
@@ -137,6 +137,7 @@ lemma hasInjectiveDimensionLE_iff_of_semiLinearEquiv [Small.{v'} R']
     hasInjectiveDimensionLE_iff_of_linearEquiv_aux eN]
   exact hasInjectiveDimensionLE_iff_of_semiLinearEquiv_aux eR ((eM.symm.trans e).trans eN) n
 
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma injectiveDimension_eq_of_semiLinearEquiv [Small.{v'} R']
     {M : ModuleCat.{v} R} {N : ModuleCat.{v'} R'} (e : M ≃ₛₗ[RingHomClass.toRingHom eR] N) :
     injectiveDimension M = injectiveDimension N := by
diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean
index 119610224..8b4c0f546 100644
--- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean
+++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean
@@ -76,6 +76,29 @@ theorem ihom_ev_app (M N : ModuleCat.{u} R) :
   apply TensorProduct.ext'
   apply monoidalClosed_uncurry
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`Module R (TensorProduct R ↑(unop (op M)) ↑((𝟭 (ModuleCat R)).obj N))`
+
+The failure happens while applying `@TensorProduct.leftModule`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type is
+`Module R ↑((𝟭 (ModuleCat R)).obj N)`, whereas the assigned value `N.isModule` has type
+`Module R ↑N`. Lean falls back to synthesize an instance of the correct type, but it returns
+`((𝟭 (ModuleCat R)).obj N).isModule`, which is again not defeq to `N.isModule`: seeing that
+`(𝟭 (ModuleCat R)).obj N` is `N` requires unfolding `𝟭`, which is `@[implicit_reducible]` and
+therefore does not unfold at the `.instances` transparency that instance search runs at.
+
+Potential fix: Concentrate on removing `respectTransparency false` first.
+For example, do this by making `TensorProduct` implicit-reducible.
+Without the backward-compatibility flag `respectTransparency false`, Lean bumps transparency for
+instance-implicit arguments to `implicit`, thereby comparing the synthesized and unified instances
+at implicit transparency instead of the stricter instance transparency.
+After that, you can remove `instanceTypes false`, too.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 /-- Describes the unit of the adjunction `M ⊗ - ⊣ Hom(M, -)`. Given an `R`-module `N` this should
 define a map `N ⟶ Hom(M, M ⊗ N)`, which is given by flipping the arguments in the natural
diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
index fa7349e10..a582eec7b 100644
--- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
+++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
@@ -149,6 +149,7 @@ noncomputable def presheaf : Cᵒᵖ ⥤ Ab where
 lemma presheaf_obj_coe (X : Cᵒᵖ) :
     (M.presheaf.obj X : Type _) = M.obj X := rfl
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 lemma presheaf_map_apply_coe {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : M.obj X) :
     DFunLike.coe (α := M.obj X) (β := fun _ ↦ M.obj Y) (M.presheaf.map f).hom x = M.map f x := rfl
@@ -176,6 +177,7 @@ noncomputable def toPresheaf : PresheafOfModules.{v} R ⥤ Cᵒᵖ ⥤ Ab where
 lemma toPresheaf_obj_coe (X : Cᵒᵖ) :
     (((toPresheaf R).obj M).obj X : Type _) = M.obj X := rfl
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 lemma toPresheaf_map_app_apply (f : M₁ ⟶ M₂) (X : Cᵒᵖ) (x : M₁.obj X) :
     DFunLike.coe (α := M₁.obj X) (β := fun _ ↦ M₂.obj X)
diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/ChangeOfRings.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/ChangeOfRings.lean
index 424ada441..67319552f 100644
--- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/ChangeOfRings.lean
+++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/ChangeOfRings.lean
@@ -27,6 +27,7 @@ namespace PresheafOfModules
 
 variable {C : Type u'} [Category.{v'} C] {R R' : Cᵒᵖ ⥤ RingCat.{u}}
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- The restriction of scalars of presheaves of modules, on objects. -/
 @[simps]
 noncomputable def restrictScalarsObj (M' : PresheafOfModules.{v} R') (α : R ⟶ R') :
diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean
index e7f98beb3..acdcd9ed7 100644
--- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean
+++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean
@@ -40,6 +40,37 @@ namespace Monoidal
 
 variable (M₁ M₂ M₃ M₄ : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`TensorProduct.CompatibleSMul ↑(R.obj Y) ↑(R.obj Y) ↑(M₁.obj Y) ↑(M₂.obj Y)`
+
+The failure happens while applying `@TensorProduct.CompatibleSMul.isScalarTower`: assigning one of
+its instance-implicit-argument metavariables is rejected because the metavariable's type and the
+type of the assigned value do not match at `.instances` transparency. The metavariable's expected
+type is `DistribMulAction ↑(R.obj Y) ↑(M₂.obj Y)`, whereas the assigned value
+`ModuleCat.instModuleCarrierObjRestrictScalars.toDistribMulAction` has type
+```
+DistribMulAction ↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)
+  ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj
+      (M₂.obj Y))
+```
+Lean falls back to synthesize an instance of the correct type, but it returns
+`(M₂.obj Y).isModule.toDistribMulAction`, which is again not defeq to the assigned value. Both
+comparisons bottom out at `↑(R.obj Y) =?= ↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)`, the same
+ring bundled once as a `CommRingCat` and once as a `RingCat`; seeing that these agree requires
+unfolding `⋙`, which is `@[implicit_reducible]`.
+
+Potential fix: Concentrate on removing `respectTransparency false` first.
+For example, do this by making `ModuleCat.RestrictScalars.obj'` and `ModuleCat.restrictScalars`
+implicit-reducible *at their definition site*.
+Without the backward-compatibility flag `respectTransparency false`, Lean bumps transparency for
+instance-implicit arguments to `implicit`, thereby comparing the synthesized and unified instances
+at implicit transparency instead of the stricter instance transparency.
+After that, you can remove `instanceTypes false`, too.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 /-- Auxiliary definition for `tensorObj`. -/
 noncomputable def tensorObjMap {X Y : Cᵒᵖ} (f : X ⟶ Y) : M₁.obj X ⊗ M₂.obj X ⟶
@@ -75,6 +106,33 @@ noncomputable def tensorObj : PresheafOfModules (R ⋙ forget₂ _ _) where
 
 variable {M₁ M₂ M₃ M₄}
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`Module ↑(R.obj Y)
+  ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj
+      (M₁.obj Y))`
+
+The failure happens while applying `@ModuleCat.isModule`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type
+is `Ring ↑(R.obj Y)`, whereas the assigned value `RingCat.instRingObjForgetRingHomCarrier` has type
+`Ring ((forget RingCat).obj ((R ⋙ forget₂ CommRingCat RingCat).obj X))`. Lean falls back to
+synthesize an instance of the correct type, but it returns
+`CommRingCat.instCommRingObjForgetRingHomCarrier.toRing`, which is again not defeq to the assigned
+value. As for `tensorObjMap` above, both comparisons bottom out at
+`(R.obj Y).1 =?= ((R ⋙ forget₂ CommRingCat RingCat).obj X).1`.
+
+Potential fix: Concentrate on removing `respectTransparency false` first.
+For example, do this by making `ModuleCat.RestrictScalars.obj'` and `ModuleCat.restrictScalars`
+implicit-reducible  *at their definition site*.
+Without the backward-compatibility flag `respectTransparency false`, Lean bumps transparency for
+instance-implicit arguments to `implicit`, thereby comparing the synthesized and unified instances
+at implicit transparency instead of the stricter instance transparency.
+After that, you can remove `instanceTypes false`, too.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma tensorObj_map_tmul {X Y : Cᵒᵖ} (f : X ⟶ Y) (m₁ : M₁.obj X) (m₂ : M₂.obj X) :
diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Pushforward.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Pushforward.lean
index 7f42f3237..74a6251a8 100644
--- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Pushforward.lean
+++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Pushforward.lean
@@ -108,6 +108,38 @@ lemma pushforward_obj_map_apply (M : PresheafOfModules.{v} R) {X Y : Cᵒᵖ} (f
     (m : (ModuleCat.restrictScalars (φ.app X).hom).obj (M.obj (Opposite.op (F.obj X.unop)))) :
       (((pushforward φ).obj M).map f).hom m = M.map (F.map f.unop).op m := rfl
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized, writing `P Z` for
+`(ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app Z))).obj (((pushforward₀ F R).obj M).obj Z)`:
+```
+DFunLike (↑(P X) →ₗ[↑(S.obj X)]
+    ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (S.map f))).obj (P Y))) _ _
+```
+It is needed to elaborate the `DFunLike.coe` in the statement below, whose `F` annotation spells
+domain and codomain on the `restrictScalars` side.
+
+The failure happens while applying `@LinearMap.instFunLike`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type
+is `Module ↑(S.obj X) ↑(P X)`, whereas the assigned value `(((pushforward φ).obj M).obj X).isModule`
+has type `Module ↑(S.obj X) ↑(((pushforward φ).obj M).obj X)`. The comparison bottoms out at
+`(ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).1 =?= ((pushforward φ).obj M).1`, the same
+module written once through `pushforward` and once through `restrictScalars`. Lean falls back to
+synthesize an instance of the correct type, which succeeds, but it returns
+```
+((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (((pushforward₀ F R).obj M).obj
+X)).isModule
+```
+This again not defeq to the assigned value, stalling in the same way. That second comparison runs at
+`.implicit`, but `pushforward` does not unfold there either.
+
+Potential fix: Mark `pushforward`, `PresheafOfModules.restrictScalars` and
+`PresheafOfModules.restrictScalarsObj` implicit-reducible; then both backward compatibility options
+can go.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency.types false in
 /-- `@[simp]`-normal form of `pushforward_obj_map_apply`. -/
 @[simp]
@@ -122,6 +154,27 @@ lemma pushforward_map_app_apply {M N : PresheafOfModules.{v} R} (α : M ⟶ N) (
     (m : (ModuleCat.restrictScalars (φ.app X).hom).obj (M.obj (Opposite.op (F.obj X.unop)))) :
     (((pushforward φ).map α).app X).hom m = α.app (Opposite.op (F.obj X.unop)) m := rfl
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized, writing `P Z` for
+`(ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app Z))).obj (((pushforward₀ F R).obj M).obj Z)`:
+`DFunLike (↑(P X) →ₗ[↑(S.obj X)] ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj
+  (((pushforward₀ F R).obj N).obj X))) _ _`
+It is needed to elaborate the `DFunLike.coe` in the statement below.
+
+This is the same failure as for `pushforward_obj_map_apply'` above, again while applying
+`@LinearMap.instFunLike`: the metavariable's expected type is `Module ↑(S.obj X) ↑(P X)`, the
+assigned value is `(((pushforward φ).obj M).obj X).isModule` of type
+`Module ↑(S.obj X) ↑(((pushforward φ).obj M).obj X)`, and both the direct `.instances` check and the
+comparison against the re-synthesized instance bottom out at
+`(ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).1 =?= ((pushforward φ).obj M).1`.
+
+Potential fix: Mark `pushforward`, `PresheafOfModules.restrictScalars` and
+`PresheafOfModules.restrictScalarsObj` implicit-reducible; then both backward compatibility options
+can go.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency.types false in
 /-- `@[simp]`-normal form of `pushforward_map_app_apply`. -/
 @[simp]
diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean
index 6e1d44b59..e0005acb4 100644
--- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean
+++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean
@@ -338,6 +338,43 @@ noncomputable def toSheafify : M₀ ⟶ (restrictScalars α).obj (sheafify α φ
 lemma toSheafify_app_apply (X : Cᵒᵖ) (x : M₀.obj X) :
     ((toSheafify α φ).app X).hom x = φ.app X x := rfl
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+```
+DFunLike (↑(M₀.obj X) →ₗ[↑(R₀.obj X)]
+    ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj ((sheafify α φ).val.obj X)))
+  ↑(M₀.obj X) _
+```
+It is needed to elaborate the `DFunLike.coe` in the statement below.
+
+The failure happens while applying `@LinearMap.instFunLike`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type is
+```
+Module ↑(R₀.obj X) ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj
+((sheafify α φ).val.obj X))
+```
+The assigned value
+```
+(((restrictScalars α).obj (sheafify α φ).val).obj X).isModule
+```
+has type `Module ↑(R₀.obj X) ↑(((restrictScalars α).obj (sheafify α φ).val).obj X)`, which is the
+same module written once through `PresheafOfModules.restrictScalars` and once through
+`ModuleCat.restrictScalars`. Lean falls back to synthesize an instance of the correct type, which
+succeeds, but the candidate is again not defeq to the assigned value. Both comparisons bottom out at
+```
+((restrictScalars α).obj (sheafify α φ).val).1 =?=
+(ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).1
+```
+The second one runs at `.implicit`, where `PresheafOfModules.restrictScalars` does not unfold
+either.
+
+Potential fix: Mark `PresheafOfModules.restrictScalars` and `PresheafOfModules.restrictScalarsObj`
+implicit-reducible; then both backward compatibility options can go.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency.types false in
 /-- `@[simp]`-normal form of `toSheafify_app_apply`. -/
 @[simp]
diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Submodule.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Submodule.lean
index 8becc6ba6..e7c9fb2cc 100644
--- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Submodule.lean
+++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Submodule.lean
@@ -53,6 +53,7 @@ lemma ext {N₁ N₂ : M.Submodule} (h : ∀ X, N₁.obj X = N₂.obj X) :
     N₁ = N₂ := by
   cases N₁; cases N₂; congr 1; ext X : 1; exact h X
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[grind .]
 lemma map_mem {X Y : Cᵒᵖ} (f : X ⟶ Y) {x : M.obj X} (hx : x ∈ N.obj X) :
     M.map f x ∈ N.obj Y :=
diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean
index de496361c..7e830e326 100644
--- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean
+++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean
@@ -86,6 +86,7 @@ lemma hasProjectiveDimensionLE_of_semiLinearEquiv (e' : M ≃ₛₗ[RingHomClass
 alias _root_.CategoryTheory.hasProjectiveDimensionLE_of_semiLinearEquiv :=
   hasProjectiveDimensionLE_of_semiLinearEquiv
 
+set_option backward.isDefEq.respectTransparency.instances false in
 attribute [local instance] RingHomInvPair.of_ringEquiv in
 lemma projectiveDimension_eq_of_semiLinearEquiv (e' : M ≃ₛₗ[RingHomClass.toRingHom e] N) :
     projectiveDimension M = projectiveDimension N := by
diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean
index 71a5dfc5d..fe3563471 100644
--- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean
+++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean
@@ -403,6 +403,8 @@ def freeObj (X : TopCat.{v}) : TopModuleCat.{max v u} R :=
 
 lemma coe_freeObj (X : TopCat.{v}) : freeObj R X = (X →₀ R) := rfl
 
+set_option backward.isDefEq.respectTransparency.instances false in
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 /-- The free topological module over a topological space is functorial. -/
 noncomputable
@@ -420,9 +422,11 @@ def freeMap {X Y : TopCat.{v}} (f : X ⟶ Y) : freeObj R X ⟶ freeObj R Y :=
     ext x
     simp [coe_freeObj]⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma freeMap_map {X Y : TopCat.{v}} (f : X ⟶ Y) (v : X →₀ R) :
     (freeMap R f : (X →₀ R) → (Y →₀ R)) v = Finsupp.mapDomain f.hom v := rfl
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- The free topological module over a topological space as a functor.
 This is left adjoint to the forgetful functor. -/
 @[simps] noncomputable
@@ -432,6 +436,8 @@ def free : TopCat.{v} ⥤ TopModuleCat.{max v u} R :=
     map_id M := by ext x; exact DFunLike.congr_fun (Finsupp.lmapDomain_id _ _) x
     map_comp f g := by ext; exact DFunLike.congr_fun (Finsupp.lmapDomain_comp _ _ f.hom g.hom) _ }
 
+set_option backward.isDefEq.instanceTypes false in
+set_option backward.isDefEq.respectTransparency.instances false in
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The free-forgetful adjoint for `TopModuleCat R`. -/
diff --git a/mathlib4/Mathlib/Algebra/Category/Ring/EqualizerPushout.lean b/mathlib4/Mathlib/Algebra/Category/Ring/EqualizerPushout.lean
index 3a05fba09..c2b9c00e3 100644
--- a/mathlib4/Mathlib/Algebra/Category/Ring/EqualizerPushout.lean
+++ b/mathlib4/Mathlib/Algebra/Category/Ring/EqualizerPushout.lean
@@ -33,6 +33,7 @@ section Fork
 
 variable {R S : CommRingCat.{u}} (f : R ⟶ S)
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- If `f : R ⟶ S` is a faithfully flat map in `CommRingCat`, then the fork
 ```
         S ---inl---> pushout f f
diff --git a/mathlib4/Mathlib/Algebra/Category/Ring/FilteredColimits.lean b/mathlib4/Mathlib/Algebra/Category/Ring/FilteredColimits.lean
index 6daebb16d..428cec9e8 100644
--- a/mathlib4/Mathlib/Algebra/Category/Ring/FilteredColimits.lean
+++ b/mathlib4/Mathlib/Algebra/Category/Ring/FilteredColimits.lean
@@ -124,7 +124,7 @@ def colimitCocone : Cocone F where
               (F ⋙ forget₂ SemiRingCat.{max v u} AddCommMonCat)).ι.app j).hom with }
       naturality _ _ f := by
         ext
-        simpa using! (Types.TypeMax.colimitCocone (F ⋙ forget SemiRingCat)).ι.naturality_apply f _ }
+        simpa using! (F ⋙ forget SemiRingCat).ιColimitType_map f _ }
 
 namespace colimitCoconeIsColimit
 
@@ -223,8 +223,7 @@ def colimitCocone : Cocone F where
           (F ⋙ forget₂ CommSemiRingCat SemiRingCat.{max v u})).ι.app X).hom
       naturality _ _ f := by
         ext
-        simpa using! (Types.TypeMax.colimitCocone
-          (F ⋙ forget CommSemiRingCat)).ι.naturality_apply f _ }
+        simpa using! (F ⋙ forget CommSemiRingCat).ιColimitType_map f _ }
 
 /-- The proposed colimit cocone is a colimit in `CommSemiRingCat`. -/
 def colimitCoconeIsColimit : IsColimit <| colimitCocone.{v, u} F :=
@@ -281,7 +280,7 @@ def colimitCocone : Cocone F where
           (F ⋙ forget₂ RingCat SemiRingCat.{max v u})).ι.app X).hom
       naturality _ _ f := by
         ext
-        simpa using! (Types.TypeMax.colimitCocone (F ⋙ forget RingCat)).ι.naturality_apply f _ }
+        simpa using! (F ⋙ forget RingCat).ιColimitType_map f _ }
 
 /-- The proposed colimit cocone is a colimit in `Ring`. -/
 def colimitCoconeIsColimit : IsColimit <| colimitCocone.{v, u} F :=
@@ -344,7 +343,7 @@ def colimitCocone : Cocone F where
           (F ⋙ forget₂ CommRingCat RingCat.{max v u})).ι.app X).hom
       naturality _ _ f := by
         ext
-        simpa using! (Types.TypeMax.colimitCocone (F ⋙ forget CommRingCat)).ι.naturality_apply f _ }
+        simpa using! (F ⋙ forget CommRingCat).ιColimitType_map f _ }
 
 /-- The proposed colimit cocone is a colimit in `CommRingCat`. -/
 def colimitCoconeIsColimit : IsColimit <| colimitCocone.{v, u} F :=
diff --git a/mathlib4/Mathlib/Algebra/Group/Hom/Defs.lean b/mathlib4/Mathlib/Algebra/Group/Hom/Defs.lean
index 5aa3b8cc6..0284322a8 100644
--- a/mathlib4/Mathlib/Algebra/Group/Hom/Defs.lean
+++ b/mathlib4/Mathlib/Algebra/Group/Hom/Defs.lean
@@ -259,7 +259,7 @@ theorem ne_one_of_map {R S F : Type*} [One R] [One S] [FunLike F R S] [OneHomCla
 
 /-- Turn an element of a type `F` satisfying `OneHomClass F M N` into an actual
 `OneHom`. This is declared as the default coercion from `F` to `OneHom M N`. -/
-@[to_additive (attr := coe)
+@[to_additive (attr := coe, instance_reducible)
 /-- Turn an element of a type `F` satisfying `ZeroHomClass F M N` into an actual
 `ZeroHom`. This is declared as the default coercion from `F` to `ZeroHom M N`. -/]
 def OneHomClass.toOneHom [OneHomClass F M N] (f : F) : OneHom M N where
@@ -332,7 +332,7 @@ lemma map_comp_mul [MulHomClass F M N] (f : F) (g h : ι → M) : f ∘ (g * h)
 
 /-- Turn an element of a type `F` satisfying `MulHomClass F M N` into an actual
 `MulHom`. This is declared as the default coercion from `F` to `M →ₙ* N`. -/
-@[to_additive (attr := coe)
+@[to_additive (attr := coe, instance_reducible)
 /-- Turn an element of a type `F` satisfying `AddHomClass F M N` into an actual
 `AddHom`. This is declared as the default coercion from `F` to `M →ₙ+ N`. -/]
 def MulHomClass.toMulHom [MulHomClass F M N] (f : F) : M →ₙ* N where
@@ -400,7 +400,7 @@ variable [FunLike F M N]
 
 /-- Turn an element of a type `F` satisfying `MonoidHomClass F M N` into an actual
 `MonoidHom`. This is declared as the default coercion from `F` to `M →* N`. -/
-@[to_additive (attr := coe)
+@[to_additive (attr := coe, instance_reducible)
 /-- Turn an element of a type `F` satisfying `AddMonoidHomClass F M N` into an
 actual `MonoidHom`. This is declared as the default coercion from `F` to `M →+ N`. -/]
 def MonoidHomClass.toMonoidHom [MonoidHomClass F M N] (f : F) : M →* N :=
diff --git a/mathlib4/Mathlib/Algebra/Homology/Embedding/AreComplementary.lean b/mathlib4/Mathlib/Algebra/Homology/Embedding/AreComplementary.lean
index bb6317c8d..4668f5903 100644
--- a/mathlib4/Mathlib/Algebra/Homology/Embedding/AreComplementary.lean
+++ b/mathlib4/Mathlib/Algebra/Homology/Embedding/AreComplementary.lean
@@ -309,6 +309,7 @@ noncomputable def shortComplexTruncLEX₃ToTruncGE :
     (K.shortComplexTruncLE e₁).X₃ ⟶ K.truncGE e₂ :=
   cokernel.desc _ (K.πTruncGE e₂) (ac.hom_ext _)
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[reassoc (attr := simp)]
 lemma g_shortComplexTruncLEX₃ToTruncGE :
     (K.shortComplexTruncLE e₁).g ≫ K.shortComplexTruncLEX₃ToTruncGE ac = K.πTruncGE e₂ :=
diff --git a/mathlib4/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean b/mathlib4/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
index d7dba586b..daba20952 100644
--- a/mathlib4/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
+++ b/mathlib4/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@@ -292,6 +292,39 @@ lemma rightShift_smul (a n' : ℤ) (hn' : n' + a = n) (x : R) :
   dsimp
   simp only [rightShift_v _ a n' hn' p q hpq _ rfl, smul_v, Linear.smul_comp]
 
+#adaptation_note
+/--
+We had to mark `CochainComplex.shiftFunctor` implicit-reducible locally to make an instance search
+succeed. Concretely, the following instance cannot be synthesized:
+`SMulCommClass R ℤˣ (K.X (p + a) ⟶ L.X q)`
+It is needed because `leftShift` carries a sign `u : ℤˣ`, so the closing `simp only` fires
+`smul_comm x`.
+
+The failure happens while applying `@Units.smulCommClass_right`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type
+is `SMul R (K.X (p + a) ⟶ L.X q)`, whereas the assigned value
+`DistribMulAction.toDistribSMul.toSMul` has type
+```
+SMul R (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).X p ⟶ L.X q)
+```
+Lean falls back to synthesize an instance of the correct type, but the candidate is again not defeq
+to the result. Both comparisons bottom out at
+```
+K.X (p + a) ⟶ L.X q =?= ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).X p ⟶ L.X q
+```
+Since `SMulCommClass` stays unsynthesizable, `smul_comm x` never fires and the goal
+`u • x • f = x • u • f` is left unsolved.
+
+`CategoryTheory.shiftFunctor` is already `@[implicit_reducible]`, but the
+`CochainComplex.shiftFunctor` underneath it is semireducible, so the two hom types cannot be seen
+to agree at either transparency. Marking it implicit-reducible makes the assignment go through,
+since Lean bumps transparency for instance-implicit arguments to `implicit`.
+
+Potential fix: mark `CochainComplex.shiftFunctor` implicit-reducible at its definition site; then
+the local `attribute` and `allowUnsafeReducibility` here can be dropped.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma leftShift_smul (a n' : ℤ) (hn' : n + a = n') (x : R) :
diff --git a/mathlib4/Mathlib/Algebra/Homology/SpectralObject/Cycles.lean b/mathlib4/Mathlib/Algebra/Homology/SpectralObject/Cycles.lean
index 8720cc8a2..457f4629d 100644
--- a/mathlib4/Mathlib/Algebra/Homology/SpectralObject/Cycles.lean
+++ b/mathlib4/Mathlib/Algebra/Homology/SpectralObject/Cycles.lean
@@ -294,6 +294,7 @@ noncomputable def toCycles (n : ℤ) :
     (X.H n).obj (mk₁ fg) ⟶ X.cycles f g n :=
   kernel.lift _ ((X.H n).map (twoδ₁Toδ₀ f g fg h)) (by simp)
 
+set_option backward.isDefEq.respectTransparency.instances false in
 instance (n : ℤ) : Epi (X.toCycles f g fg h n) :=
   (ShortComplex.exact_iff_epi_kernel_lift _).1 (X.exact₃ f g fg h n (n + 1))
 
@@ -325,6 +326,7 @@ noncomputable def fromOpcycles (n : ℤ) :
     X.opcycles f g n ⟶ (X.H n).obj (mk₁ fg) :=
   cokernel.desc _ ((X.H n).map (twoδ₂Toδ₁ f g fg h)) (by simp)
 
+set_option backward.isDefEq.respectTransparency.instances false in
 instance (n : ℤ) : Mono (X.fromOpcycles f g fg h n) :=
   (ShortComplex.exact_iff_mono_cokernel_desc _).1 (X.exact₁ f g fg h (n - 1) n)
 
diff --git a/mathlib4/Mathlib/Algebra/Lie/Subalgebra.lean b/mathlib4/Mathlib/Algebra/Lie/Subalgebra.lean
index 08df1c027..c0100e63d 100644
--- a/mathlib4/Mathlib/Algebra/Lie/Subalgebra.lean
+++ b/mathlib4/Mathlib/Algebra/Lie/Subalgebra.lean
@@ -548,6 +548,7 @@ variable {K K'} in
 
 variable (R L)
 
+set_option backward.isDefEq.respectTransparency.instances false in
 instance wellFoundedGT_of_noetherian [IsNoetherian R L] : WellFoundedGT (LieSubalgebra R L) :=
   RelHomClass.isWellFounded (⟨toSubmodule, @fun _ _ h ↦ h⟩ : _ →r (· > ·))
 
diff --git a/mathlib4/Mathlib/Algebra/Lie/Submodule.lean b/mathlib4/Mathlib/Algebra/Lie/Submodule.lean
index c7d9b6bfb..01f465b63 100644
--- a/mathlib4/Mathlib/Algebra/Lie/Submodule.lean
+++ b/mathlib4/Mathlib/Algebra/Lie/Submodule.lean
@@ -518,6 +518,9 @@ variable (R L M)
     inj' := toSubmodule_injective
     map_rel_iff' := Iff.rfl }
 
+-- Defeq abuse: need `FunLike _ (LieSubmodule R L M) (Submodule R M)ᵒᵈ`, get
+-- `FunLike _ (LieSubmodule R L M)ᵒᵈ (Submodule R M)ᵒᵈ`.
+set_option backward.isDefEq.respectTransparency.instances false in
 instance wellFoundedGT_of_noetherian [IsNoetherian R M] : WellFoundedGT (LieSubmodule R L M) :=
   RelHomClass.isWellFounded (toSubmodule_orderEmbedding R L M).dual.ltEmbedding
 
@@ -727,6 +730,9 @@ variable (f : M →ₗ⁅R,L⁆ M') (N N₂ : LieSubmodule R L M) (N' : LieSubmo
 
 /-- A morphism of Lie modules `f : M → M'` pushes forward Lie submodules of `M` to Lie submodules
 of `M'`. -/
+-- Later we will want to know that `LieSubmodule.map` and `Submodule.map` are related in order for`
+-- the `FunLike` instances to be compatible.
+@[instance_reducible]
 def map : LieSubmodule R L M' :=
   { (N : Submodule R M).map (f : M →ₗ[R] M') with
     lie_mem := fun {x m'} h ↦ by
diff --git a/mathlib4/Mathlib/Algebra/Module/Equiv/Defs.lean b/mathlib4/Mathlib/Algebra/Module/Equiv/Defs.lean
index 14a412f25..495ed6143 100644
--- a/mathlib4/Mathlib/Algebra/Module/Equiv/Defs.lean
+++ b/mathlib4/Mathlib/Algebra/Module/Equiv/Defs.lean
@@ -584,7 +584,27 @@ def _root_.RingEquiv.toSemilinearEquiv (f : R ≃+* S) :
     toFun := f
     map_smul' := f.map_mul }
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` and `respectTransparency` backward compatibility flags to make an
+instance search succeed. Concretely, the following instance cannot be synthesized:
+`CoeFun (R ≃ₛₗ[↑f] S) ?m`
+so without them the application below reports
+`Function expected at f.symm.toSemilinearEquiv.symm`.
+
+The failure happens while applying `@instEquivLike` to `EquivLike (R ≃ₛₗ[↑f] S) ?α ?β`: assigning
+one of its instance-implicit-argument metavariables is rejected because the metavariable's type and
+the type of the assigned value do not match at `.instances` transparency. The metavariable's
+expected type is `RingHomInvPair ↑f ↑f.symm`, whereas the assigned value
+`RingHomInvPair.symm ↑f.symm ↑f.symm.symm` has type `RingHomInvPair ↑f.symm.symm ↑f.symm`. Lean
+falls back to synthesizing `RingHomInvPair ↑f ↑f.symm`, but no such instnace is found, so the
+assignment fails.
+
+This is the intended behavior.
+A quick fix could be to provide the required instance via `haveI` or as a local instance.
+-/
 set_option backward.isDefEq.respectTransparency false in
+set_option backward.isDefEq.instanceTypes false in
 @[simp]
 lemma _root_.RingEquiv.symm_toSemilinearEquiv_symm_apply (f : R ≃+* S) (x : R) :
   f.symm.toSemilinearEquiv.symm (σ' := RingHomClass.toRingHom f) x = f x := rfl
diff --git a/mathlib4/Mathlib/Algebra/Module/LinearMap/Index.lean b/mathlib4/Mathlib/Algebra/Module/LinearMap/Index.lean
index 8da65af7f..cd8d91ce2 100644
--- a/mathlib4/Mathlib/Algebra/Module/LinearMap/Index.lean
+++ b/mathlib4/Mathlib/Algebra/Module/LinearMap/Index.lean
@@ -65,6 +65,31 @@ public lemma index_of_surjective (hf : Surjective f) :
   rw [index_eq_finrank_sub, range_eq_top.mpr hf]
   simp [finrank_eq_zero_of_subsingleton]
 
+#adaptation_note
+/--
+We had to mark `LinearMap.ker` implicit-reducible locally to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`Module.Free R ↥⊥`
+It is needed by `finrank_eq_zero_of_subsingleton` in the closing `simp`.
+
+The failure happens while applying `Free.of_subsingleton`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type
+is `AddCommMonoid ↥⊥`, whereas the assigned value `id.ker.addCommMonoid` has type
+`AddCommMonoid ↥id.ker`. Lean falls back to synthesize an instance of the correct type, but the
+candidate is again not defeq to the result `⊥.addCommMonoid`. Both comparisons bottom out at
+`id.ker =?= ⊥`, and `ker` is semireducible, so it does not unfold at the `.instances` transparency
+that instance search runs at.
+
+The two spellings meet because `simp` mixes them: after `range_id`, the `@[simp]` `rfl`-lemma
+`ker_id` rewrites the carrier `↥(ker id)` to `↥⊥` but keeps the old `id.ker.*` instance arguments.
+Since `Free` stays unsynthesizable, `finrank R ↥⊥` is left unrewritten and the goal
+`finrank R ↥⊥ = 0` is not closed.
+
+Potential fix: mark `LinearMap.ker` implicit-reducible, then remove both backward compatibility
+options.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency.types false in
 @[simp] public lemma index_id :
     (id : M →ₗ[R] M).index = 0 := by
diff --git a/mathlib4/Mathlib/Algebra/Module/Presentation/Differentials.lean b/mathlib4/Mathlib/Algebra/Module/Presentation/Differentials.lean
index 97d84e50e..160f6c542 100644
--- a/mathlib4/Mathlib/Algebra/Module/Presentation/Differentials.lean
+++ b/mathlib4/Mathlib/Algebra/Module/Presentation/Differentials.lean
@@ -84,6 +84,30 @@ lemma hom₁_single (r : σ) :
     hom₁ pres (Finsupp.single r 1) = Extension.Cotangent.mk ⟨pres.relation r, by simp⟩ := by
   simp [hom₁]
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`RingHomSurjective (RingHom.id pres.Ring)`
+It is needed by the `rw [Submodule.map_span_le]` below.
+
+The failure happens while applying `@RingHomSurjective.ids`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type is
+`Semiring pres.Ring`, whereas the assigned value `CommRing.toCommSemiring.toSemiring` has type
+`Semiring pres.toExtension.Ring`. The comparison bottoms out at
+`AddMonoidAlgebra R (ι →₀ ℕ) =?= pres.toExtension.1`: the left-hand side is what `pres.Ring` reduces
+to, while the right-hand side is stuck, since `Generators.toExtension` is a semireducible `def` and
+therefore does not unfold at the `.instances` transparency instance search runs at. Lean
+falls back to synthesize an instance of the correct type, which succeeds and returns
+`AddMonoidAlgebra.semiring`, but that is again not defeq to the assigned value, stalling at the same
+boundary. That comparison, too, runs at `.instances`, since `respectTransparency false` suppresses
+the transparency bump that instance-implicit arguments would otherwise receive.
+
+Potential fix: Mark `Generators.toExtension` implicit-reducible; then `respectTransparency false`
+and `instanceTypes false` can both go.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 lemma surjective_hom₁ : Function.Surjective (hom₁ pres) := by
diff --git a/mathlib4/Mathlib/Algebra/Order/Hom/Monoid.lean b/mathlib4/Mathlib/Algebra/Order/Hom/Monoid.lean
index e9156ad8f..e3b6c7f86 100644
--- a/mathlib4/Mathlib/Algebra/Order/Hom/Monoid.lean
+++ b/mathlib4/Mathlib/Algebra/Order/Hom/Monoid.lean
@@ -232,12 +232,16 @@ theorem monotone_iff_map_nonneg [iamhc : AddMonoidHomClass F α β] :
 
 variable [iamhc : AddMonoidHomClass F α β]
 
+-- Defeq abuse: `iamhc` is not an instance about `βᵒᵈ`.
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem antitone_iff_map_nonpos : Antitone (f : α → β) ↔ ∀ a, 0 ≤ a → f a ≤ 0 :=
   monotone_toDual_comp_iff.symm.trans <| monotone_iff_map_nonneg (β := βᵒᵈ) (iamhc := iamhc) _
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem monotone_iff_map_nonpos : Monotone (f : α → β) ↔ ∀ a ≤ 0, f a ≤ 0 :=
   antitone_comp_ofDual_iff.symm.trans <| antitone_iff_map_nonpos (α := αᵒᵈ) (iamhc := iamhc) _
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem antitone_iff_map_nonneg : Antitone (f : α → β) ↔ ∀ a ≤ 0, 0 ≤ f a :=
   monotone_comp_ofDual_iff.symm.trans <| monotone_iff_map_nonneg (α := αᵒᵈ) (iamhc := iamhc) _
 
@@ -249,12 +253,15 @@ theorem strictMono_iff_map_pos :
   · rw [← sub_add_cancel b a, map_add f]
     exact lt_add_of_pos_left _ (h _ <| sub_pos.2 hl)
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem strictAnti_iff_map_neg : StrictAnti (f : α → β) ↔ ∀ a, 0 < a → f a < 0 :=
   strictMono_toDual_comp_iff.symm.trans <| strictMono_iff_map_pos (β := βᵒᵈ) (iamhc := iamhc) _
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem strictMono_iff_map_neg : StrictMono (f : α → β) ↔ ∀ a < 0, f a < 0 :=
   strictAnti_comp_ofDual_iff.symm.trans <| strictAnti_iff_map_neg (α := αᵒᵈ) (iamhc := iamhc) _
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem strictAnti_iff_map_pos : StrictAnti (f : α → β) ↔ ∀ a < 0, 0 < f a :=
   strictMono_comp_ofDual_iff.symm.trans <| strictMono_iff_map_pos (α := αᵒᵈ) (iamhc := iamhc) _
 
diff --git a/mathlib4/Mathlib/Algebra/RingQuot.lean b/mathlib4/Mathlib/Algebra/RingQuot.lean
index 3fe3f3b96..e3e4ef0ee 100644
--- a/mathlib4/Mathlib/Algebra/RingQuot.lean
+++ b/mathlib4/Mathlib/Algebra/RingQuot.lean
@@ -530,6 +530,7 @@ irreducible_def liftAlgHom {s : A → A → Prop} :
                  AlgHom.coe_comp, AlgHom.coe_mk, RingHom.coe_mk,
                  MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply] }
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 theorem liftAlgHom_mkAlgHom_apply (f : A →ₐ[S] B) {s : A → A → Prop}
     (w : ∀ ⦃x y⦄, s x y → f x = f y) (x) : (liftAlgHom S ⟨f, w⟩) ((mkAlgHom S s) x) = f x := by
diff --git a/mathlib4/Mathlib/Algebra/Star/TensorProduct.lean b/mathlib4/Mathlib/Algebra/Star/TensorProduct.lean
index 2ba906bc0..73b725302 100644
--- a/mathlib4/Mathlib/Algebra/Star/TensorProduct.lean
+++ b/mathlib4/Mathlib/Algebra/Star/TensorProduct.lean
@@ -40,6 +40,9 @@ noncomputable instance : InvolutiveStar (A ⊗[R] B) where
 noncomputable instance : StarAddMonoid (A ⊗[R] B) where
   star_add := map_add _
 
+-- Would require `DFunLike.coe (starRingEnd R) = star` at `instances` transparency, which sounds
+-- reasonable but does not hold at the moment.
+set_option backward.isDefEq.respectTransparency.instances false in
 instance : StarModule R (A ⊗[R] B) where
   star_smul := map_smulₛₗ _
 
diff --git a/mathlib4/Mathlib/AlgebraicGeometry/Cover/Open.lean b/mathlib4/Mathlib/AlgebraicGeometry/Cover/Open.lean
index f776366f9..3e6ccb4fd 100644
--- a/mathlib4/Mathlib/AlgebraicGeometry/Cover/Open.lean
+++ b/mathlib4/Mathlib/AlgebraicGeometry/Cover/Open.lean
@@ -200,6 +200,7 @@ lemma OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom
   convert! pullbackSymmetry_inv_comp_fst ((𝒰.X i.1).affineCover.f i.2) (pullback.fst _ _)
   exact pullbackRightPullbackFstIso_hom_fst _ _ _
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- A family of elements spanning the unit ideal of `R` gives an affine open cover of `Spec R`. -/
 @[simps]
 noncomputable
diff --git a/mathlib4/Mathlib/AlgebraicGeometry/EffectiveEpi.lean b/mathlib4/Mathlib/AlgebraicGeometry/EffectiveEpi.lean
index faf69c1b8..f00263dc5 100644
--- a/mathlib4/Mathlib/AlgebraicGeometry/EffectiveEpi.lean
+++ b/mathlib4/Mathlib/AlgebraicGeometry/EffectiveEpi.lean
@@ -53,6 +53,7 @@ instance effectiveEpi_base_of_flat {X Y : Scheme.{u}} {f : X ⟶ Y} [Flat f] [Su
 
 namespace EffectiveEpiConstruction
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- If `π : X ⟶ Y` is a surjective and flat morphism between affine schemes, then any morphism
 `f : X ⟶ S` to an affine scheme `S` whose two pullbacks to `X ×[Y] X` agree descends to a morphism
 `u : Y ⟶ S` with `π ≫ u = f`. -/
diff --git a/mathlib4/Mathlib/AlgebraicGeometry/Geometrically/Connected.lean b/mathlib4/Mathlib/AlgebraicGeometry/Geometrically/Connected.lean
index 060f36132..73c6dad02 100644
--- a/mathlib4/Mathlib/AlgebraicGeometry/Geometrically/Connected.lean
+++ b/mathlib4/Mathlib/AlgebraicGeometry/Geometrically/Connected.lean
@@ -63,6 +63,7 @@ instance (s : S) [GeometricallyConnected f] :
     GeometricallyConnected (f.fiberToSpecResidueField s) :=
   MorphismProperty.pullback_snd _ _ inferInstance
 
+set_option backward.isDefEq.respectTransparency.instances false in
 instance (s : S) [GeometricallyConnected f] : ConnectedSpace (f.fiber s) :=
   GeometricallyConnected.geometrically_connectedSpace _ _ _ (.of_hasPullback _ _)
 
diff --git a/mathlib4/Mathlib/AlgebraicGeometry/Geometrically/Integral.lean b/mathlib4/Mathlib/AlgebraicGeometry/Geometrically/Integral.lean
index 2dc55ece5..8eade6294 100644
--- a/mathlib4/Mathlib/AlgebraicGeometry/Geometrically/Integral.lean
+++ b/mathlib4/Mathlib/AlgebraicGeometry/Geometrically/Integral.lean
@@ -82,6 +82,7 @@ instance (s : S) [GeometricallyIntegral f] :
     GeometricallyIntegral (f.fiberToSpecResidueField s) :=
   MorphismProperty.pullback_snd _ _ inferInstance
 
+set_option backward.isDefEq.respectTransparency.instances false in
 instance (s : S) [GeometricallyIntegral f] : IsIntegral (f.fiber s) :=
   GeometricallyIntegral.geometrically_isIntegral _ _ _ (.of_hasPullback _ _)
 
diff --git a/mathlib4/Mathlib/AlgebraicGeometry/Geometrically/Irreducible.lean b/mathlib4/Mathlib/AlgebraicGeometry/Geometrically/Irreducible.lean
index 0a421c973..e6072e861 100644
--- a/mathlib4/Mathlib/AlgebraicGeometry/Geometrically/Irreducible.lean
+++ b/mathlib4/Mathlib/AlgebraicGeometry/Geometrically/Irreducible.lean
@@ -65,6 +65,7 @@ instance (s : S) [GeometricallyIrreducible f] :
     GeometricallyIrreducible (f.fiberToSpecResidueField s) :=
   MorphismProperty.pullback_snd _ _ inferInstance
 
+set_option backward.isDefEq.respectTransparency.instances false in
 instance (s : S) [GeometricallyIrreducible f] : IrreducibleSpace (f.fiber s) :=
   GeometricallyIrreducible.geometrically_irreducibleSpace _ _ _ (.of_hasPullback _ _)
 
diff --git a/mathlib4/Mathlib/AlgebraicGeometry/Geometrically/Reduced.lean b/mathlib4/Mathlib/AlgebraicGeometry/Geometrically/Reduced.lean
index 5934193fc..e7e7f0362 100644
--- a/mathlib4/Mathlib/AlgebraicGeometry/Geometrically/Reduced.lean
+++ b/mathlib4/Mathlib/AlgebraicGeometry/Geometrically/Reduced.lean
@@ -67,6 +67,7 @@ instance (s : S) [GeometricallyReduced f] :
     GeometricallyReduced (f.fiberToSpecResidueField s) :=
   MorphismProperty.pullback_snd _ _ inferInstance
 
+set_option backward.isDefEq.respectTransparency.instances false in
 instance (s : S) [GeometricallyReduced f] : IsReduced (f.fiber s) :=
   GeometricallyReduced.geometrically_isReduced _ _ _ (.of_hasPullback _ _)
 
diff --git a/mathlib4/Mathlib/AlgebraicGeometry/Limits.lean b/mathlib4/Mathlib/AlgebraicGeometry/Limits.lean
index fe1f9c51d..9e0aee575 100644
--- a/mathlib4/Mathlib/AlgebraicGeometry/Limits.lean
+++ b/mathlib4/Mathlib/AlgebraicGeometry/Limits.lean
@@ -232,9 +232,38 @@ noncomputable instance [Small.{u} σ] : CoproductsOfShapeDisjoint Scheme.{u} σ
 instance : HasFiniteCoproducts Scheme.{u} where
   out := inferInstance
 
+set_option linter.style.longLine false in
+#adaptation_note
+/--
+We had to add `(X := X)` in the `inferInstanceAs` below to make an instance search succeed.
+
+Was:
+```lean
 set_option backward.isDefEq.respectTransparency.types false in
 instance : MonoCoprod Scheme.{u} :=
-  .mk' fun X Y ↦ ⟨.mk coprod.inl coprod.inr, coprodIsCoprod X Y, inferInstanceAs <| Mono coprod.inl⟩
+  .mk' fun X Y ↦
+    ⟨.mk coprod.inl coprod.inr, coprodIsCoprod X Y, inferInstanceAs <| Mono coprod.inl⟩
+```
+Concretely, without the pin the following instance cannot be synthesized:
+`Mono coprod.inl`
+
+The failure happens while applying `@Mono.inl_of_binaryCoproductDisjoint`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type
+is `HasBinaryCoproduct ((pair X Y).obj { as := WalkingPair.left }) Y`, whereas the assigned value
+`Scheme.IsLocallyDirected.instHasColimit (pair X Y)` has type `HasColimit (pair X Y)`. Lean falls
+back to synthesize an instance of the correct type, which succeeds, but the candidate is again not
+defeq to the result. The direct check bottoms out at
+`(pair X Y).obj { as := WalkingPair.left } =?= X` and the fallback comparison at the same pair the
+other way around, so `pair` unfolds neither at `.instances` nor at `.implicit`.
+
+The unpinned `inferInstanceAs` leaves the elaborator free to spell the coproduct leg as
+`(pair X Y).obj { as := WalkingPair.left }` rather than `X`; pinning `(X := X)` fixes that
+spelling up front. An alternative fix is to make `pair` implicit-reducible.
+-/
+instance : MonoCoprod Scheme.{u} :=
+  .mk' fun X Y ↦
+    ⟨.mk coprod.inl coprod.inr, coprodIsCoprod X Y, inferInstanceAs <| Mono coprod.inl (X := X)⟩
 
 /-- The cover of `∐ X` by the `Xᵢ`. -/
 @[simps!]
@@ -328,15 +357,18 @@ lemma nonempty_isColimit_cofanMk_of [Small.{u} σ]
 
 variable (X Y : Scheme.{u})
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- (Implementation Detail)
 The coproduct of the two schemes is given by indexed coproducts over `WalkingPair`. -/
 noncomputable
 def coprodIsoSigma : X ⨿ Y ≅ ∐ fun i : ULift.{u} WalkingPair ↦ i.1.casesOn X Y :=
   Sigma.whiskerEquiv Equiv.ulift.symm (fun _ ↦ by exact Iso.refl _)
 
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma ι_left_coprodIsoSigma_inv : Sigma.ι _ ⟨.left⟩ ≫ (coprodIsoSigma X Y).inv = coprod.inl :=
   Sigma.ι_comp_map' _ _ _
 
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma ι_right_coprodIsoSigma_inv : Sigma.ι _ ⟨.right⟩ ≫ (coprodIsoSigma X Y).inv = coprod.inr :=
   Sigma.ι_comp_map' _ _ _
 
diff --git a/mathlib4/Mathlib/AlgebraicGeometry/Modules/Tilde.lean b/mathlib4/Mathlib/AlgebraicGeometry/Modules/Tilde.lean
index dee5b8e11..bc2a390b3 100644
--- a/mathlib4/Mathlib/AlgebraicGeometry/Modules/Tilde.lean
+++ b/mathlib4/Mathlib/AlgebraicGeometry/Modules/Tilde.lean
@@ -423,6 +423,7 @@ def tildeSelf : tilde (ModuleCat.of R R) ≅ SheafOfModules.unit.{u} _ := .refl
 instance : IsIso (Scheme.Modules.fromTildeΓ (SheafOfModules.unit.{u} (Spec R).ringCatSheaf)) :=
   isIso_fromTildeΓ_iff.mpr ⟨_, ⟨tildeSelf⟩⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Tilde of direct sums of `R` as an `R`-module is isomorphic to the free sheaf. -/
 noncomputable
 def tildeFinsupp (ι : Type u) : tilde (ModuleCat.of R (ι →₀ R)) ≅ SheafOfModules.free.{u} ι :=
diff --git a/mathlib4/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean b/mathlib4/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean
index bee804f02..8245fe731 100644
--- a/mathlib4/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean
+++ b/mathlib4/Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean
@@ -111,6 +111,7 @@ instance universallyClosed_isZariskiLocalAtTarget : IsZariskiLocalAtTarget @Univ
 instance (f : X ⟶ Y) (V : Y.Opens) [UniversallyClosed f] : UniversallyClosed (f ∣_ V) :=
   IsZariskiLocalAtTarget.restrict ‹_› V
 
+set_option backward.isDefEq.respectTransparency.instances false in
 open Scheme.Pullback _root_.PrimeSpectrum MvPolynomial in
 /-- If `X` is universally closed over a field, then `X` is quasi-compact. -/
 lemma compactSpace_of_universallyClosed
diff --git a/mathlib4/Mathlib/AlgebraicGeometry/OpenImmersion.lean b/mathlib4/Mathlib/AlgebraicGeometry/OpenImmersion.lean
index bfe8038c5..d56d38d37 100644
--- a/mathlib4/Mathlib/AlgebraicGeometry/OpenImmersion.lean
+++ b/mathlib4/Mathlib/AlgebraicGeometry/OpenImmersion.lean
@@ -44,6 +44,7 @@ instance IsOpenImmersion.comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
 
 namespace LocallyRingedSpace.IsOpenImmersion
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- To show that a locally ringed space is a scheme, it suffices to show that it has a jointly
 surjective family of open immersions from affine schemes. -/
 protected def scheme (X : LocallyRingedSpace.{u})
diff --git a/mathlib4/Mathlib/AlgebraicGeometry/Restrict.lean b/mathlib4/Mathlib/AlgebraicGeometry/Restrict.lean
index 8c0d8521d..b7b0a0769 100644
--- a/mathlib4/Mathlib/AlgebraicGeometry/Restrict.lean
+++ b/mathlib4/Mathlib/AlgebraicGeometry/Restrict.lean
@@ -119,6 +119,7 @@ lemma ι_image_le (W : U.toScheme.Opens) : U.ι ''ᵁ W ≤ U := by
 lemma ι_preimage_self : U.ι ⁻¹ᵁ U = ⊤ :=
   Opens.inclusion'_map_eq_top _
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 lemma mem_ι_image_iff {x : U} {V : Opens U} : (x : X) ∈ U.ι ''ᵁ V ↔ x ∈ V :=
   U.ι.apply_mem_image_iff
@@ -151,6 +152,7 @@ def stalkIso {X : Scheme.{u}} (U : X.Opens) (x : U) :
     U.toScheme.presheaf.stalk x ≅ X.presheaf.stalk x.1 :=
   X.restrictStalkIso (Opens.isOpenEmbedding _) _
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[reassoc (attr := simp)]
 lemma germ_stalkIso_hom {X : Scheme.{u}} (U : X.Opens)
     {V : U.toScheme.Opens} (x : U) (hx : x ∈ V) :
@@ -158,6 +160,7 @@ lemma germ_stalkIso_hom {X : Scheme.{u}} (U : X.Opens)
         X.presheaf.germ (U.ι ''ᵁ V) x.1 ⟨x, hx, rfl⟩ :=
     PresheafedSpace.restrictStalkIso_hom_eq_germ _ U.isOpenEmbedding _ _ _
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[reassoc]
 lemma germ_stalkIso_inv {X : Scheme.{u}} (U : X.Opens) (V : U.toScheme.Opens) (x : U)
     (hx : x ∈ V) : X.presheaf.germ (U.ι ''ᵁ V) x ⟨x, hx, rfl⟩ ≫
@@ -230,6 +233,7 @@ lemma Scheme.Opens.ι_image_basicOpen_topIso_inv (r : Γ(X, U)) :
   simp only [Scheme.Opens.toScheme_presheaf_obj]
   rw [ι_image_basicOpen', basicOpen_res_eq, topIso_inv, basicOpen_res_eq X]
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 lemma Scheme.Opens.mem_basicOpen_toScheme {U : X.Opens} {V : Scheme.Opens U} {r : Γ(U, V)} {x : U} :
     x ∈ U.toScheme.basicOpen r ↔ (x : X) ∈ X.basicOpen r := by
diff --git a/mathlib4/Mathlib/AlgebraicGeometry/StructureSheaf.lean b/mathlib4/Mathlib/AlgebraicGeometry/StructureSheaf.lean
index 68e666459..941f30261 100644
--- a/mathlib4/Mathlib/AlgebraicGeometry/StructureSheaf.lean
+++ b/mathlib4/Mathlib/AlgebraicGeometry/StructureSheaf.lean
@@ -47,7 +47,6 @@ boundaries.
 
 -/
 
-
 universe u
 
 noncomputable section
@@ -66,6 +65,7 @@ namespace AlgebraicGeometry
 
 variable (R) in
 /-- The prime spectrum as an object of `TopCat`. -/
+@[instance_reducible]
 def PrimeSpectrum.Top : TopCat := TopCat.of (PrimeSpectrum R)
 
 namespace StructureSheaf
@@ -493,6 +493,33 @@ theorem exists_le_iSup_basicOpen_and_smul_eq_smul_and_eq_const
       simp [Submonoid.smul_def, pow_succ', mul_smul]
     · simp
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`IsConcreteLE (Opens (PrimeSpectrum R)) ↑(PrimeSpectrum.Top R)`
+It is needed by `← SetLike.coe_subset_coe` in the `simpa … using iU` below.
+
+The failure happens while applying `instIsConcreteLE`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type
+is `SetLike (Opens (PrimeSpectrum R)) ↑(PrimeSpectrum.Top R)`, whereas the assigned value
+`Opens.instSetLike` has type `SetLike (Opens ↑(PrimeSpectrum.Top R)) ↑(PrimeSpectrum.Top R)`. The
+two differ in the first argument, and comparing them bottoms out at
+`PrimeSpectrum R =?= (PrimeSpectrum.Top R).1`, where `PrimeSpectrum.Top` is semireducible and hence
+does not unfold at the `.instances` transparency that instance search runs at. Lean falls back to
+synthesize an instance of the correct type, but that synthesis fails as well: it hits the very same
+problem one level down, for the assignment of a metavariable of type
+`TopologicalSpace (PrimeSpectrum R)` to `(PrimeSpectrum.Top R).str`, whose own fallback returns
+`PrimeSpectrum.zariskiTopology`; again not defeq to `(PrimeSpectrum.Top R).str` at `.instances`.
+
+With no `IsConcreteLE` instance found, `← SetLike.coe_subset_coe` never fires and `simpa` reports a
+type mismatch for `iU`.
+
+Potential fix: mark `PrimeSpectrum.Top` implicit-reducible, then remove both backward compatibility
+options.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 theorem toBasicOpenₗ_surjective (f : R) : Function.Surjective (toBasicOpenₗ R M f) := by
   intro s
@@ -653,6 +680,7 @@ theorem toOpenₗ_germ (U : Opens (PrimeSpectrum.Top R)) (x : PrimeSpectrum.Top
   rw [toStalkₗ', ← Presheaf.germ_res _ (homOfLE le_top) _ hx, ← Category.assoc]
   rfl
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem isUnit_toStalk (x : PrimeSpectrum.Top R) (f : R) (hf : x ∈ basicOpen f) :
     IsUnit (toStalk R x f) := by
   convert! (isUnit_basicOpen f).map ((structurePresheafInCommRingCat R).germ _ x hf).hom
@@ -958,6 +986,7 @@ instance to_basicOpen_epi (r : R) :
   ⟨fun _ _ h => CommRingCat.hom_ext (IsLocalization.ringHom_ext (Submonoid.powers r)
     (CommRingCat.hom_ext_iff.mp h))⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- The ring isomorphism between the ring `R` and the global sections `Γ(X, 𝒪ₓ)`. -/
 @[simps! inv]
 def globalSectionsIso : CommRingCat.of R ≅ (structureSheaf R).1.obj (op ⊤) :=
diff --git a/mathlib4/Mathlib/AlgebraicTopology/DoldKan/Projections.lean b/mathlib4/Mathlib/AlgebraicTopology/DoldKan/Projections.lean
index e960ff9b0..4e67f4f89 100644
--- a/mathlib4/Mathlib/AlgebraicTopology/DoldKan/Projections.lean
+++ b/mathlib4/Mathlib/AlgebraicTopology/DoldKan/Projections.lean
@@ -71,6 +71,7 @@ theorem P_add_Q (q : ℕ) : P q + Q q = 𝟙 K[X] := by
   rw [Q]
   abel
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem P_add_Q_f (q n : ℕ) : (P q).f n + (Q q).f n = 𝟙 (X _⦋n⦌) :=
   HomologicalComplex.congr_hom (P_add_Q q) n
 
diff --git a/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/TopAdj.lean b/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/TopAdj.lean
index b54bd10e8..b112f6b40 100644
--- a/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/TopAdj.lean
+++ b/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/TopAdj.lean
@@ -35,6 +35,8 @@ namespace SimplexCategory
 
 open SSet
 
+-- Needs to unfold `toTop` at `instances` transparency
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- The homeomorphism between the topological realization of a standard simplex
 in `SSet` and the corresponding topological standard simplex. -/
 noncomputable def toTopHomeo (n : SimplexCategory) :
diff --git a/mathlib4/Mathlib/Analysis/Calculus/VectorField.lean b/mathlib4/Mathlib/Analysis/Calculus/VectorField.lean
index 59828087f..5b7cfcb19 100644
--- a/mathlib4/Mathlib/Analysis/Calculus/VectorField.lean
+++ b/mathlib4/Mathlib/Analysis/Calculus/VectorField.lean
@@ -127,7 +127,7 @@ lemma lieBracketWithin_smul_right {f : E → 𝕜} (hf : DifferentiableWithinAt
     (hW : DifferentiableWithinAt 𝕜 W s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
     lieBracketWithin 𝕜 V (fun y ↦ f y • W y) s x =
       (fderivWithin 𝕜 f s x) (V x) • (W x) + (f x) • lieBracketWithin 𝕜 V W s x := by
-  simp [lieBracketWithin, fderivWithin_fun_smul hs hf hW, map_smul, add_comm, smul_sub,
+  simp [lieBracketWithin, fderivWithin_fun_smul hs hf hW, add_comm, smul_sub,
     add_sub_assoc]
 
 /--
diff --git a/mathlib4/Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean b/mathlib4/Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
index 58bd84cca..06f1e15d1 100644
--- a/mathlib4/Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
+++ b/mathlib4/Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
@@ -151,6 +151,7 @@ lemma exists_apply_ne_zero : (∃ ψ : AddChar α ℂ, ψ a ≠ 1) ↔ a ≠ 0 :
 lemma forall_apply_eq_zero : (∀ ψ : AddChar α ℂ, ψ a = 1) ↔ a = 0 := by
   simpa using exists_apply_ne_zero.not
 
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma doubleDualEmb_injective : Injective (doubleDualEmb : α → AddChar (AddChar α ℂ) ℂ) :=
   doubleDualEmb.ker_eq_bot_iff.1 <| eq_bot_iff.2 fun a ha ↦
     forall_apply_eq_zero.1 fun ψ ↦ by simpa using! DFunLike.congr_fun ha (Additive.ofMul ψ)
diff --git a/mathlib4/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/mathlib4/Mathlib/Analysis/InnerProductSpace/Adjoint.lean
index 6276f3325..377bc37f5 100644
--- a/mathlib4/Mathlib/Analysis/InnerProductSpace/Adjoint.lean
+++ b/mathlib4/Mathlib/Analysis/InnerProductSpace/Adjoint.lean
@@ -266,6 +266,7 @@ instance : StarMul (E →L[𝕜] E) :=
 instance : StarRing (E →L[𝕜] E) :=
   ⟨map_add adjoint⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 instance : StarModule 𝕜 (E →L[𝕜] E) :=
   ⟨map_smulₛₗ adjoint⟩
 
@@ -712,6 +713,7 @@ instance : StarMul (E →ₗ[𝕜] E) :=
 instance : StarRing (E →ₗ[𝕜] E) :=
   ⟨map_add adjoint⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 instance : StarModule 𝕜 (E →ₗ[𝕜] E) :=
   ⟨map_smulₛₗ adjoint⟩
 
diff --git a/mathlib4/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean b/mathlib4/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
index eaded7181..02fc27ba5 100644
--- a/mathlib4/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
+++ b/mathlib4/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
@@ -234,6 +234,7 @@ variable {A : E →ₗ.[𝕜] E}
 
 theorem isSelfAdjoint_def : IsSelfAdjoint A ↔ A† = A := Iff.rfl
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Every self-adjoint `LinearPMap` has dense domain.
 
 This is not true by definition since we define the adjoint without the assumption that the
diff --git a/mathlib4/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/mathlib4/Mathlib/Analysis/InnerProductSpace/PiL2.lean
index a938a909f..c5ee7fd29 100644
--- a/mathlib4/Mathlib/Analysis/InnerProductSpace/PiL2.lean
+++ b/mathlib4/Mathlib/Analysis/InnerProductSpace/PiL2.lean
@@ -563,6 +563,7 @@ protected theorem orthogonalProjectionOnto_apply_eq_sum {U : Submodule 𝕜 E}
 @[deprecated (since := "2026-05-05")] alias orthogonalProjection_apply_eq_sum :=
   OrthonormalBasis.orthogonalProjectionOnto_apply_eq_sum
 
+set_option backward.isDefEq.respectTransparency.instances false in
 protected theorem orthogonalProjectionOnto_eq_sum_rankOne {U : Submodule 𝕜 E}
     [U.HasOrthogonalProjection] (b : OrthonormalBasis ι 𝕜 U) :
     U.orthogonalProjectionOnto = ∑ i, InnerProductSpace.rankOne 𝕜 (b i) (b i : E) := by
@@ -571,6 +572,7 @@ protected theorem orthogonalProjectionOnto_eq_sum_rankOne {U : Submodule 𝕜 E}
 @[deprecated (since := "2026-05-05")] alias orthogonalProjection_eq_sum_rankOne :=
   OrthonormalBasis.orthogonalProjectionOnto_eq_sum_rankOne
 
+set_option backward.isDefEq.respectTransparency.instances false in
 protected theorem starProjection_eq_sum_rankOne {U : Submodule 𝕜 E} [U.HasOrthogonalProjection]
     (b : OrthonormalBasis ι 𝕜 U) :
     U.starProjection = ∑ i, InnerProductSpace.rankOne 𝕜 (b i : E) (b i : E) := by
diff --git a/mathlib4/Mathlib/Analysis/InnerProductSpace/ProdL2.lean b/mathlib4/Mathlib/Analysis/InnerProductSpace/ProdL2.lean
index 263b0b741..8bbdea5db 100644
--- a/mathlib4/Mathlib/Analysis/InnerProductSpace/ProdL2.lean
+++ b/mathlib4/Mathlib/Analysis/InnerProductSpace/ProdL2.lean
@@ -139,6 +139,7 @@ theorem sndL_comp_coe_orthogonalDecomposition :
     WithLp.sndL 2 𝕜 K Kᗮ ∘L K.orthogonalDecomposition = Kᗮ.orthogonalProjectionOnto := by
   ext; simp
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- If a subspace `K` of an inner product space `E` admits an orthogonal projection, then the
 quotient `E ⧸ K` is isometrically isomorphic to the orthogonal complement `Kᗮ` of `K`. -/
 def quotientEquivOrthogonal : (E ⧸ K) ≃ₗᵢ[𝕜] ↥Kᗮ where
@@ -154,29 +155,35 @@ def quotientEquivOrthogonal : (E ⧸ K) ≃ₗᵢ[𝕜] ↥Kᗮ where
     · rw [sInf_image', ← Equiv.iInf_comp (Equiv.neg K)]
       simp
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 theorem coe_quotientEquivOrthogonal :
     ⇑K.quotientEquivOrthogonal = K.quotientEquivOfIsCompl Kᗮ K.isCompl_orthogonal :=
   rfl
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 theorem coe_quotientEquivOrthogonal_symm :
     ⇑K.quotientEquivOrthogonal.symm = (K.quotientEquivOfIsCompl Kᗮ K.isCompl_orthogonal).symm :=
   rfl
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 lemma toLinearEquiv_quotientEquivOrthogonal :
     (quotientEquivOrthogonal K).toLinearEquiv = K.quotientEquivOfIsCompl _ K.isCompl_orthogonal :=
   rfl
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem quotientEquivOrthogonal_mk (x : E) (hx : x ∈ Kᗮ) :
     K.quotientEquivOrthogonal (Quotient.mk x) = ⟨x, hx⟩ := by
   simp [← K.quotientEquivOfIsCompl_apply_mk_right K.isCompl_orthogonal ⟨x, hx⟩]
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem quotientEquivOrthogonal_symm_eq_mk (x : E) (hx : x ∈ Kᗮ) :
     K.quotientEquivOrthogonal.symm ⟨x, hx⟩ = Quotient.mk x := by
   simp
 
+set_option backward.isDefEq.respectTransparency.instances false in
 noncomputable instance instQuotientInnerProductSpace :
     InnerProductSpace 𝕜 (E ⧸ K) where
   inner x y := ⟪K.quotientEquivOrthogonal x, K.quotientEquivOrthogonal y⟫_𝕜
@@ -185,11 +192,13 @@ noncomputable instance instQuotientInnerProductSpace :
   conj_inner_symm x y := inner_conj_symm _ _
   norm_sq_eq_re_inner y := by rw [inner_self_eq_norm_sq, LinearIsometryEquiv.norm_map]
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 theorem inner_quotient_eq (x y : E ⧸ K) :
     ⟪x, y⟫_𝕜 = ⟪K.quotientEquivOrthogonal x, K.quotientEquivOrthogonal y⟫_𝕜 :=
   rfl
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem Quotient.inner_mk_mk (x y : E) (hx : x ∈ Kᗮ) (hy : y ∈ Kᗮ) :
     ⟪Quotient.mk (p := K) x, Quotient.mk y⟫_𝕜 = ⟪x, y⟫_𝕜 := by
   simp [K.quotientEquivOrthogonal_mk x hx, K.quotientEquivOrthogonal_mk y hy]
diff --git a/mathlib4/Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean b/mathlib4/Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean
index 4db359d9b..04202f5a0 100644
--- a/mathlib4/Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean
+++ b/mathlib4/Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean
@@ -132,6 +132,8 @@ should prefer the generic API, especially because it will make rewriting easier.
 protected noncomputable def cfc (f : ℝ → ℝ) : Matrix n n 𝕜 :=
   conjStarAlgAut 𝕜 _ hA.eigenvectorUnitary (diagonal (RCLike.ofReal ∘ f ∘ hA.eigenvalues))
 
+-- Abuses the `defeq` that `IsSelfAdjoint` and `IsHermitian` coincide.
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma cfcHom_eq_cfcAux : cfcHom hA.isSelfAdjoint = hA.cfcAux :=
   cfcHom_eq_of_continuous_of_map_id hA hA.cfcAux
     hA.isClosedEmbedding_cfcAux.continuous hA.cfcAux_id
diff --git a/mathlib4/Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean b/mathlib4/Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
index a5fa1a704..bbe74f3ee 100644
--- a/mathlib4/Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
+++ b/mathlib4/Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
@@ -692,7 +692,9 @@ universe u v
 variable {K : Type u} [NontriviallyNormedField K] {L : Type v} [Field L] [Algebra K L]
   [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K]
 
-set_option allowUnsafeReducibility true
+@[implicit_reducible]
+private def myId {α : Sort u} (a : α) : α :=
+  a
 
 /-- If `K` is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and
   `L/K` is an algebraic extension, then any power-multiplicative `K`-algebra norm on `L` coincides
@@ -701,7 +703,7 @@ theorem spectralNorm_unique [CompleteSpace K] {f : AlgebraNorm K L} (hf_pm : IsP
     f = spectralAlgNorm K L := by
   apply eq_of_powMul_faithful f hf_pm _ spectralAlgNorm_isPowMul
   intro x
-  let E : Type v := id K⟮x⟯
+  let E : Type v := myId K⟮x⟯
   let : Field E := id <| show Field K⟮x⟯ by infer_instance
   let : Module K E := id <| show Module K K⟮x⟯ by infer_instance
   let id1 : K⟮x⟯ →ₗ[K] E := LinearMap.id
diff --git a/mathlib4/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean b/mathlib4/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
index 5f22186bb..f3c9133ea 100644
--- a/mathlib4/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
+++ b/mathlib4/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
@@ -203,6 +203,8 @@ lemma top_mem_range (A₀ : Subobject X) {J : Type w} [LinearOrder J] [OrderBot
   top_mem_range_transfiniteIterate (largerSubobject hG) A₀ (lt_largerSubobject hG) (by simp)
     (fun h ↦ by simpa [hasCardinalLT_iff_cardinal_mk_lt] using hJ.of_injective _ h)
 
+set_option backward.isDefEq.instanceTypes false in
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma exists_ordinal (A₀ : Subobject X) :
     ∃ (o : Ordinal.{w}) (j : o.ToType), transfiniteIterate (largerSubobject hG) j A₀ = ⊤ := by
   let κ := Order.succ (Cardinal.mk (Shrink.{w} (Subobject X)))
diff --git a/mathlib4/Mathlib/CategoryTheory/EssentiallySmall.lean b/mathlib4/Mathlib/CategoryTheory/EssentiallySmall.lean
index 6dd489241..8a54e4db4 100644
--- a/mathlib4/Mathlib/CategoryTheory/EssentiallySmall.lean
+++ b/mathlib4/Mathlib/CategoryTheory/EssentiallySmall.lean
@@ -200,7 +200,8 @@ instance {T : Type u} [Unique T] : Unique (ShrinkHoms.{u} T) where
 
 instance {T : Type u} [Category.{v} T] [IsDiscrete T] : IsDiscrete (ShrinkHoms.{u} T) where
   subsingleton _ _ := { allEq _ _ := Shrink.ext (Subsingleton.elim _ _) }
-  eq_of_hom f := IsDiscrete.eq_of_hom (C := T) ((equivShrink _).symm f)
+  eq_of_hom {X Y} f := IsDiscrete.eq_of_hom (C := T)
+    ((equivShrink (fromShrinkHoms X ⟶ fromShrinkHoms Y)).symm f)
 
 end ShrinkHoms
 
diff --git a/mathlib4/Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean b/mathlib4/Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean
index b4d3226a7..b18ab8934 100644
--- a/mathlib4/Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean
+++ b/mathlib4/Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean
@@ -34,8 +34,36 @@ section Small
 variable {A : Type u₁} [SmallCategory A] {B : Type u₁} [SmallCategory B]
 variable {T : Type u₁} [SmallCategory T]
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`HasColimitsOfShape (CostructuredArrow L (R.obj b)) (Type u₁)`
+It is needed by `filtered_colim_preservesFiniteLimits` in the `haveI` below. The `simp only`
+preceding it rewrites the shape of `colim` to `CostructuredArrow L (R.obj b)` via
+`Cat.of_α`, but leaves that `colim`'s `Category` instance typed at the old spelling
+`↑(Cat.of (CostructuredArrow L (R.obj b)))`, and the synthesis has to reproduce that mismatch.
+
+The failure happens while applying `@Types.hasColimitsOfShape`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type is
+`Category (CostructuredArrow L (R.obj b))`, whereas the assigned value
+`(Cat.of (CostructuredArrow L (R.obj b))).str` has type
+`Category ↑(Cat.of (CostructuredArrow L (R.obj b)))`. The comparison bottoms out at
+`CostructuredArrow L (R.obj b) =?= (Cat.of (CostructuredArrow L (R.obj b))).1`, where `Cat.of` is a
+plain semireducible `def` and therefore does not unfold at the `.instances` transparency that
+instance search runs at. Lean falls back to synthesize an instance of the correct type, which
+succeeds, but it returns `instCategoryCostructuredArrow_1 L (R.obj b)`, which is again not defeq to
+the assigned value: that comparison bottoms out at the same `Cat.of` boundary, and it too runs at
+`.instances`, since `respectTransparency false` suppresses the transparency bump that
+instance-implicit arguments would otherwise receive.
+
+Potential fix: Mark `Cat.of` and `Bundled.of` implicit-reducible and then remove
+`instanceTypes false` and `respectTransparency false`.
+-/
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
+set_option backward.isDefEq.instanceTypes false in
 private lemma isFiltered_of_isFiltered_costructuredArrow_small (L : A ⥤ T) (R : B ⥤ T)
     [IsFiltered B] [Final R] [∀ b, IsFiltered (CostructuredArrow L (R.obj b))] : IsFiltered A := by
   refine isFiltered_of_nonempty_limit_colimit_to_colimit_limit fun J {_ _} F => ⟨?_⟩
diff --git a/mathlib4/Mathlib/CategoryTheory/FintypeCat.lean b/mathlib4/Mathlib/CategoryTheory/FintypeCat.lean
index 4fa0b1cc0..2fdeb827b 100644
--- a/mathlib4/Mathlib/CategoryTheory/FintypeCat.lean
+++ b/mathlib4/Mathlib/CategoryTheory/FintypeCat.lean
@@ -235,9 +235,14 @@ attribute [local instance] FintypeCat.fintype in
 @[simp]
 theorem incl_mk_nat_card (n : ℕ) :
     Fintype.card (incl.obj (mk n)) = n := by
-  convert! Finset.card_fin n
-  dsimp [incl, mk, len]
-  convert! (Fintype.ofEquiv_card Equiv.ulift).symm
+  -- Use `unfold` rather than `simp only` to keep instances in sync.
+  unfold incl mk len at *
+  dsimp only
+  conv_rhs => rw [← Fintype.card_fin n]
+  -- This `convert` would not be necessary if `Fintype.card_congr'` and `Fintype.ofEquiv_card` had
+  -- the `Fintype` instances as implicit arguments, which would make more sense for this and many
+  -- other lemmas in that file.
+  convert! Eq.trans (Fintype.ofEquiv_card Equiv.ulift).symm (@Fintype.card_congr' _ _ _ _ rfl)
 
 end Skeleton
 
diff --git a/mathlib4/Mathlib/CategoryTheory/Functor/TypeValuedFlat.lean b/mathlib4/Mathlib/CategoryTheory/Functor/TypeValuedFlat.lean
index 889298a51..a73c3dc02 100644
--- a/mathlib4/Mathlib/CategoryTheory/Functor/TypeValuedFlat.lean
+++ b/mathlib4/Mathlib/CategoryTheory/Functor/TypeValuedFlat.lean
@@ -73,6 +73,8 @@ def fromOverSubfunctor : Subfunctor (Over.forget X ⋙ F) where
   obj U := F.map U.hom ⁻¹' {x}
   map _ _ _ := by simpa [← comp_apply, ← Functor.map_comp]
 
+-- Would need `(Over.forget X ⋙ F).obj U = F.obj U.left` at `instances` transparency.
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 lemma mem_fromOverSubfunctor_iff {U : Over X} (u : F.obj U.left) :
     u ∈ (fromOverSubfunctor F x).obj U ↔ F.map U.hom u = x := Iff.rfl
diff --git a/mathlib4/Mathlib/CategoryTheory/Galois/Equivalence.lean b/mathlib4/Mathlib/CategoryTheory/Galois/Equivalence.lean
index b9a933908..a1cb6f6e2 100644
--- a/mathlib4/Mathlib/CategoryTheory/Galois/Equivalence.lean
+++ b/mathlib4/Mathlib/CategoryTheory/Galois/Equivalence.lean
@@ -54,6 +54,7 @@ instance {F : C ⥤ FintypeCat.{u₁}} [FiberFunctor F] : (functorToContAction F
     obtain ⟨A, ⟨i⟩⟩ := exists_lift_of_continuous (F := F) X
     exact ⟨A, ⟨ObjectProperty.isoMk _ i⟩⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 instance : (functorToContAction F).EssSurj := by
   let F' : C ⥤ FintypeCat.{u₁} := F ⋙ FintypeCat.uSwitch.{w, u₁}
   let : FiberFunctor F' := FiberFunctor.comp_right _
diff --git a/mathlib4/Mathlib/CategoryTheory/GradedObject/Monoidal.lean b/mathlib4/Mathlib/CategoryTheory/GradedObject/Monoidal.lean
index 738eb3784..f7ccb1af7 100644
--- a/mathlib4/Mathlib/CategoryTheory/GradedObject/Monoidal.lean
+++ b/mathlib4/Mathlib/CategoryTheory/GradedObject/Monoidal.lean
@@ -558,6 +558,7 @@ variable [DecidableEq I] [HasInitial C]
   [HasTensor (tensorObj X₁ tensorUnit) X₃] [HasTensor X₁ (tensorObj tensorUnit X₃)]
   [HasGoodTensor₁₂Tensor X₁ tensorUnit X₃] [HasGoodTensorTensor₂₃ X₁ tensorUnit X₃]
 
+set_option backward.isDefEq.respectTransparency.instances false in
 set_option backward.defeqAttrib.useBackward true in
 lemma triangle :
     (associator X₁ tensorUnit X₃).hom ≫ tensorHom (𝟙 X₁) (leftUnitor X₃).hom =
diff --git a/mathlib4/Mathlib/CategoryTheory/Limits/Shapes/Images.lean b/mathlib4/Mathlib/CategoryTheory/Limits/Shapes/Images.lean
index 6723da2e5..246b9f177 100644
--- a/mathlib4/Mathlib/CategoryTheory/Limits/Shapes/Images.lean
+++ b/mathlib4/Mathlib/CategoryTheory/Limits/Shapes/Images.lean
@@ -148,7 +148,7 @@ def ofIsoComp {X' : C} (g : X' ⟶ X) [IsIso g] (F : MonoFactorisation (g ≫ f)
 
 /-- If `f` and `g` are isomorphic arrows, then a mono factorisation of `f`
 gives a mono factorisation of `g` -/
-@[simps]
+@[implicit_reducible, simps]
 def ofArrowIso {f g : Arrow C} (F : MonoFactorisation f.hom) (sq : f ⟶ g) [IsIso sq] :
     MonoFactorisation g.hom where
   I := F.I
@@ -742,10 +742,7 @@ instance (priority := 100) hasImageMapOfIsIso {f g : Arrow C} [HasImage f.hom] [
     (sq : f ⟶ g) [IsIso sq] : HasImageMap sq :=
   HasImageMap.mk
     { map := image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq))
-      map_ι := by
-        erw [← cancel_mono (inv sq).right, Category.assoc, ← MonoFactorisation.ofArrowIso_m,
-          image.lift_fac, Category.assoc, ← Comma.comp_right, IsIso.hom_inv_id, Comma.id_right,
-          Category.comp_id] }
+      map_ι := by simp [ ← image.lift_fac ((Image.monoFactorisation g.hom).ofArrowIso (inv sq))] }
 
 instance HasImageMap.comp {f g h : Arrow C} [HasImage f.hom] [HasImage g.hom] [HasImage h.hom]
     (sq1 : f ⟶ g) (sq2 : g ⟶ h) [HasImageMap sq1] [HasImageMap sq2] : HasImageMap (sq1 ≫ sq2) :=
diff --git a/mathlib4/Mathlib/CategoryTheory/Localization/StructuredArrow.lean b/mathlib4/Mathlib/CategoryTheory/Localization/StructuredArrow.lean
index 427184c48..45fa9fcb0 100644
--- a/mathlib4/Mathlib/CategoryTheory/Localization/StructuredArrow.lean
+++ b/mathlib4/Mathlib/CategoryTheory/Localization/StructuredArrow.lean
@@ -63,6 +63,8 @@ section
 variable (W : MorphismProperty C) {X : C}
   (P : StructuredArrow (W.Q.obj X) W.Q → Prop)
 
+-- The new goal given in the `suffices` clause is not type-correct
+set_option backward.isDefEq.respectTransparency.instances false in
 open Construction in
 private lemma induction_structuredArrow'
     (hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X))))
diff --git a/mathlib4/Mathlib/CategoryTheory/Monoidal/Bimod.lean b/mathlib4/Mathlib/CategoryTheory/Monoidal/Bimod.lean
index f97cef76e..13256fddc 100644
--- a/mathlib4/Mathlib/CategoryTheory/Monoidal/Bimod.lean
+++ b/mathlib4/Mathlib/CategoryTheory/Monoidal/Bimod.lean
@@ -622,6 +622,7 @@ set_option backward.defeqAttrib.useBackward true in
 noncomputable def hom : TensorBimod.X (regular R) P ⟶ P.X :=
   coequalizer.desc P.actLeft (by dsimp; rw [Category.assoc, left_assoc])
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- The underlying morphism of the inverse component of the left unitor isomorphism. -/
 noncomputable def inv : P.X ⟶ TensorBimod.X (regular R) P :=
   (λ_ P.X).inv ≫ (η[R.X] ▷ _) ≫ coequalizer.π _ _
@@ -685,6 +686,7 @@ set_option backward.defeqAttrib.useBackward true in
 noncomputable def hom : TensorBimod.X P (regular S) ⟶ P.X :=
   coequalizer.desc P.actRight (by dsimp; rw [Category.assoc, right_assoc, Iso.hom_inv_id_assoc])
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- The underlying morphism of the inverse component of the right unitor isomorphism. -/
 noncomputable def inv : P.X ⟶ TensorBimod.X P (regular S) :=
   (ρ_ P.X).inv ≫ (_ ◁ η[S.X]) ≫ coequalizer.π _ _
diff --git a/mathlib4/Mathlib/CategoryTheory/Monoidal/Cartesian/ShrinkYoneda.lean b/mathlib4/Mathlib/CategoryTheory/Monoidal/Cartesian/ShrinkYoneda.lean
index 1c85a0fd1..b1efd3549 100644
--- a/mathlib4/Mathlib/CategoryTheory/Monoidal/Cartesian/ShrinkYoneda.lean
+++ b/mathlib4/Mathlib/CategoryTheory/Monoidal/Cartesian/ShrinkYoneda.lean
@@ -48,6 +48,7 @@ noncomputable def shrinkYonedaMon :
 
 open MonObj
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- The type `(shrinkYonedaMon.obj M).obj Y` is equivalent to `Y.unop ⟶ M.X`. -/
 noncomputable def shrinkYonedaMonObjObjEquiv {M : Mon C} {Y : Cᵒᵖ} :
     (shrinkYonedaMon.{w}.obj M).obj Y ≃* (Y.unop ⟶ M.X) :=
@@ -83,6 +84,7 @@ noncomputable def shrinkYonedaGrp :
   obj X := GrpCat.shrinkFunctor (yonedaGrp.obj X)
   map f := GrpCat.shrinkFunctorMap (yonedaGrp.map f)
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- The type `(shrinkYonedaGrp.obj M).obj Y` is equivalent to `Y.unop ⟶ M.X`. -/
 noncomputable def shrinkYonedaGrpObjObjEquiv {M : Grp C} {Y : Cᵒᵖ} :
     (shrinkYonedaGrp.{w}.obj M).obj Y ≃* (Y.unop ⟶ M.X) :=
diff --git a/mathlib4/Mathlib/CategoryTheory/Shift/Adjunction.lean b/mathlib4/Mathlib/CategoryTheory/Shift/Adjunction.lean
index 1628ddc03..a7108080b 100644
--- a/mathlib4/Mathlib/CategoryTheory/Shift/Adjunction.lean
+++ b/mathlib4/Mathlib/CategoryTheory/Shift/Adjunction.lean
@@ -551,7 +551,7 @@ instance : (Equivalence.refl (C := C)).inverse.CommShift A :=
 The identity equivalence is compatible with shifts.
 -/
 instance : (Equivalence.refl (C := C)).CommShift A :=
-  inferInstanceAs <| Adjunction.id.CommShift A
+  inferInstanceAs <| (Adjunction.id (C := C)).CommShift A
 
 /--
 If an equivalence `E : C ≌ D` is compatible with shifts, so is `E.symm`.
diff --git a/mathlib4/Mathlib/CategoryTheory/Sites/LocalSite.lean b/mathlib4/Mathlib/CategoryTheory/Sites/LocalSite.lean
index 426891151..b545204e8 100644
--- a/mathlib4/Mathlib/CategoryTheory/Sites/LocalSite.lean
+++ b/mathlib4/Mathlib/CategoryTheory/Sites/LocalSite.lean
@@ -160,6 +160,7 @@ instance (A : Type u') [Category.{v'} A] [HasColimitsOfSize.{v, v} A]
 instance : (coconstantSheaf.{w} J A).IsRightAdjoint :=
   ⟨Γ J A, ⟨ΓCoconstantSheafAdj J A⟩⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 set_option backward.defeqAttrib.useBackward true in
 /-- The global sections of the coconstant sheaf on a type are naturally isomorphic to that type. -/
 noncomputable def coconstantSheafΓNatIsoId :
diff --git a/mathlib4/Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean b/mathlib4/Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
index 97112b1dc..e8c87a468 100644
--- a/mathlib4/Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
+++ b/mathlib4/Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
@@ -155,6 +155,30 @@ isomorphisms on the right side. -/
 def propArrow : MorphismProperty (Arrow C) := fun _ _ f ↦
   (coproducts.{w} I).pushouts f.left ∧ (isomorphisms C) f.right
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`Category.{max u v, max u v} (Comma (𝟭 C) (𝟭 C) ⥤ Comma (𝟭 C) (𝟭 C))`
+It is needed by the `⟨F⟩` pattern in the opening `intro`, which re-elaborates `ofHoms.mk F` against
+a goal where the carrier `Arrow C ⥤ Arrow C` is exposed at its `Comma (𝟭 C) (𝟭 C)` spelling.
+
+The failure happens while applying `@Functor.category`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type
+is `Category (Comma (𝟭 C) (𝟭 C))`, whereas the assigned value `instCategoryArrow` has type
+`Category (Arrow C)`. The comparison bottoms out at `Comma (𝟭 C) (𝟭 C) =?= Arrow C`, where `Arrow`
+is a plain semireducible `def` and therefore does not unfold at the `.instances` transparency that
+instance search runs at. Lean falls back to synthesize an instance of the correct type, but it
+returns `commaCategory`, which is again not defeq to `instCategoryArrow`: that comparison runs at
+`.implicit`, and `Arrow` does not unfold there either.
+
+With the metavariable unsolved, the `intro` argument `⟨F⟩` has type `ofHoms ?m.69 (?m.69 F)`,
+which fails to unify with `(succStruct I κ).prop f✝`.
+
+Potential fix: mark `Arrow` and `Arrow.Hom` implicit-reducible, then remove `instanceTypes false`.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency.types false in
 set_option backward.defeqAttrib.useBackward true in
 lemma succStruct_prop_le_propArrow :
diff --git a/mathlib4/Mathlib/CategoryTheory/Subobject/Lattice.lean b/mathlib4/Mathlib/CategoryTheory/Subobject/Lattice.lean
index f89923ac3..b3362517b 100644
--- a/mathlib4/Mathlib/CategoryTheory/Subobject/Lattice.lean
+++ b/mathlib4/Mathlib/CategoryTheory/Subobject/Lattice.lean
@@ -66,6 +66,7 @@ def pullbackTop (f : X ⟶ Y) : (pullback f).obj ⊤ ≅ ⊤ :=
   iso_of_both_ways (leTop _)
     (homMk (pullback.lift f (𝟙 _) (by simp)) (pullback.lift_snd _ _ _))
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- There is a morphism from `⊤ : MonoOver A` to the pullback of a monomorphism along itself;
 as the category is thin this is an isomorphism. -/
 def topLEPullbackSelf {A B : C} (f : A ⟶ B) [Mono f] :
diff --git a/mathlib4/Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean b/mathlib4/Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
index dd7f6ab71..803067464 100644
--- a/mathlib4/Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
+++ b/mathlib4/Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
@@ -574,7 +574,7 @@ O'Donnell. -/
 lemma moebius_inversion_bot (f g : α → 𝕜) (h : ∀ x, g x = ∑ y ∈ Iic x, f y) (x : α) :
     f x = ∑ y ∈ Iic x, mu 𝕜 y x * g y := by
   convert! moebius_inversion_top (α := αᵒᵈ) f g h x using 3
-  rw [← mu_toDual]; rfl
+  · rw [← mu_toDual]; rfl
 
 end InversionBot
 
diff --git a/mathlib4/Mathlib/Combinatorics/Quiver/ConnectedComponent.lean b/mathlib4/Mathlib/Combinatorics/Quiver/ConnectedComponent.lean
index 3653855a3..e3f0e624e 100644
--- a/mathlib4/Mathlib/Combinatorics/Quiver/ConnectedComponent.lean
+++ b/mathlib4/Mathlib/Combinatorics/Quiver/ConnectedComponent.lean
@@ -181,6 +181,9 @@ lemma stronglyConnectedComponent_singleton_iff (v : V) :
       exists_path_of_stronglyConnectedComponent_eq (a := w) (b := v) h_same_scc
     exact (h_no_bidir w hw_ne) ⟨hba, hab⟩
 
+-- Defeq abuse: `h` does not apply to `a` and `b`, as `a b : Symmetrify V` and this leaks into
+-- `p`, which has type `@Path V inst✝ a b` which makes no sense at `instances` transparency.
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma IsStronglyConnected.isStronglyConnected_symmetrify (h : IsStronglyConnected V) :
     IsStronglyConnected (Symmetrify V) := by
   intro a b
diff --git a/mathlib4/Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean b/mathlib4/Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean
index 8116036b0..e7f9563f2 100644
--- a/mathlib4/Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean
+++ b/mathlib4/Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean
@@ -112,6 +112,7 @@ theorem Coloring.mem_colorClasses {v : V} : C.colorClass (C v) ∈ C.colorClasse
 theorem Coloring.colorClasses_finite [Finite α] : C.colorClasses.Finite :=
   Setoid.finite_classes_ker _
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem Coloring.card_colorClasses_le [Fintype α] [Fintype C.colorClasses] :
     Fintype.card C.colorClasses ≤ Fintype.card α := by
   simp only [colorClasses]
diff --git a/mathlib4/Mathlib/Computability/RecursiveIn.lean b/mathlib4/Mathlib/Computability/RecursiveIn.lean
index 7acac8fe8..0302b00c6 100644
--- a/mathlib4/Mathlib/Computability/RecursiveIn.lean
+++ b/mathlib4/Mathlib/Computability/RecursiveIn.lean
@@ -219,7 +219,7 @@ theorem partrec_of_oracle
   Nat.RecursiveIn.partrec_of_oracle (by simpa only [Partrec.nat_iff] using hO) hf
 
 /-- If a function is recursive in a constant partial function, then it is partial recursive. -/
-lemma partrec_of_const {s} (hf : RecursiveIn {fun _ => s} f) : Partrec f :=
+lemma partrec_of_const {s} (hf : RecursiveIn {(fun _ => s : ℕ →. ℕ)} f) : Partrec f :=
   hf.partrec_of_oracle
     (fun g hg => by rw [Set.mem_singleton_iff.mp hg]; exact .const' s)
 
diff --git a/mathlib4/Mathlib/Condensed/Light/Sequence.lean b/mathlib4/Mathlib/Condensed/Light/Sequence.lean
index 406aff7aa..e375ac820 100644
--- a/mathlib4/Mathlib/Condensed/Light/Sequence.lean
+++ b/mathlib4/Mathlib/Condensed/Light/Sequence.lean
@@ -183,6 +183,7 @@ lemma S'_compactSpace [TopologicalSpace S] [T2Space S] [TopologicalSpace T]
 
 end
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- This object is used to show that a certain map `T ⟶ X` descends
 to a map `S ⊗ N∪{∞} → X`. Because epimorphisms in `LightProfinite`
 are effective, it does so if the two maps `pullback π π → T → S ⊗ N∪{∞}`
diff --git a/mathlib4/Mathlib/Condensed/TopCatAdjunction.lean b/mathlib4/Mathlib/Condensed/TopCatAdjunction.lean
index e5935ba38..3097c176b 100644
--- a/mathlib4/Mathlib/Condensed/TopCatAdjunction.lean
+++ b/mathlib4/Mathlib/Condensed/TopCatAdjunction.lean
@@ -91,7 +91,40 @@ noncomputable def topCatAdjunctionCounit (X : TopCat.{u + 1}) : X.toCondensedSet
       rw [continuous_coinduced_dom]
       continuity }
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`DFunLike C(C(PUnit, ↑X), ↑X) ?m ?m`
+It is needed by the `DFunLike.coe` below, whose `F` annotation leaves the topology on `C(PUnit, X)`
+to be determined by unification.
+
+The failure happens while applying `@ContinuousMap.instFunLike`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type
+is `TopologicalSpace C(PUnit, ↑X)`, whereas the assigned value `X.toCondensedSet.toTopCat.str` has
+type `TopologicalSpace ↑X.toCondensedSet.toTopCat`. The two carrier spellings are defeq at
+`.default`, but seeing that requires unfolding the whole `toCondensedSet`/`toTopCat` chain down to
+`ContinuousMap =?= X.toCondensedSet.obj.1`, which does not happen at `.instances`. Lean falls back
+to synthesize an instance of the correct type, which succeeds, but it returns
+`ContinuousMap.compactOpen`, which is a genuinely different topology from the coinduced one carried
+by `X.toCondensedSet.toTopCat.str`, so it is not defeq to the assigned value at any transparency
+(see the `apply_rfl` example below). Hence the fallback cannot repair this case, and only the direct
+check could: that would need the carrier chain to unfold at `.instances`.
+
+With the metavariable unsolved, `DFunLike` synthesis fails and `x` is no longer known to be a
+function.
+
+Potential fix: Unclear. With an explicit type on the `x : C(PUnit, X)` parameter, the explicit
+`F` argument is no longer needed to make the lemma elaborate. However, that would change the
+lemma's statement and also its discrimination key. A last resort is to explicitly supply the
+desired instance. Alternatively, one could investigate whether `ContinuousMap.compactOpen` and
+`X.toCondensedSet.toTopCat.str` can be made defeq at implicit transparency, but this should be done
+with care: If many declarations need to be made implicit-reducible, it might degrade performance
+in other places.
+-/
 set_option backward.isDefEq.respectTransparency.types false in
+set_option backward.isDefEq.instanceTypes false in
 /-- `simp`-normal form of the lemma that `@[simps]` would generate. -/
 @[simp] lemma topCatAdjunctionCounit_hom_apply (X : TopCat) (x) :
     -- We have to specify here to not infer the `TopologicalSpace` instance on `C(PUnit, X)`,
diff --git a/mathlib4/Mathlib/Data/Matrix/Mul.lean b/mathlib4/Mathlib/Data/Matrix/Mul.lean
index 35e734e21..9092607f7 100644
--- a/mathlib4/Mathlib/Data/Matrix/Mul.lean
+++ b/mathlib4/Mathlib/Data/Matrix/Mul.lean
@@ -602,7 +602,7 @@ theorem RingEquiv.isStablyFiniteRing_iff [EquivLike F R S] [RingEquivClass F R S
 
 instance (priority := low) [SetLike F R] [SubsemiringClass F R] (S : F) [IsStablyFiniteRing R] :
     IsStablyFiniteRing S :=
-  .of_injective _ (Subsemiring.subtype_injective <| .ofClass S)
+  .of_injective _ (SubsemiringClass.subtype_injective S)
 
 end IsStablyFiniteRing
 
diff --git a/mathlib4/Mathlib/Data/Nat/Cast/SetInterval.lean b/mathlib4/Mathlib/Data/Nat/Cast/SetInterval.lean
index fa1e67e5c..960524a45 100644
--- a/mathlib4/Mathlib/Data/Nat/Cast/SetInterval.lean
+++ b/mathlib4/Mathlib/Data/Nat/Cast/SetInterval.lean
@@ -26,7 +26,7 @@ namespace Nat
 
 @[simp]
 theorem range_cast_int : range ((↑) : ℕ → ℤ) = Ici 0 :=
-  Subset.antisymm (range_subset_iff.2 Int.natCast_nonneg) CanLift.prf
+  Subset.antisymm (range_subset_iff.2 Int.natCast_nonneg) (by intro x; simpa using CanLift.prf x)
 
 theorem image_cast_int_Icc (a b : ℕ) : (↑) '' Icc a b = Icc (a : ℤ) b :=
   (castOrderEmbedding (α := ℤ)).image_Icc (by simp [ordConnected_Ici]) a b
diff --git a/mathlib4/Mathlib/Data/PFun.lean b/mathlib4/Mathlib/Data/PFun.lean
index aa1790226..42be7fb7e 100644
--- a/mathlib4/Mathlib/Data/PFun.lean
+++ b/mathlib4/Mathlib/Data/PFun.lean
@@ -58,6 +58,9 @@ open Function
 
 /-- `PFun α β`, or `α →. β`, is the type of partial functions from
   `α` to `β`. It is defined as `α → Part β`. -/
+-- `#check (fun _ => 1 : ℕ →. ℕ)` yields `ℕ → Part ℕ` and this leads to trouble down the line with
+--  `({fun _ => 1} : Set (ℕ →. ℕ))` if `PFun` is not sufficiently reducible.
+@[instance_reducible]
 def PFun (α β : Type*) :=
   α → Part β
 
diff --git a/mathlib4/Mathlib/Data/Vector3.lean b/mathlib4/Mathlib/Data/Vector3.lean
index 3447f55f9..e60524ecf 100644
--- a/mathlib4/Mathlib/Data/Vector3.lean
+++ b/mathlib4/Mathlib/Data/Vector3.lean
@@ -26,6 +26,7 @@ universe u
 variable {α : Type*} {m n : ℕ}
 
 /-- Alternate definition of `Vector` based on `Fin2`. -/
+@[instance_reducible]
 def Vector3 (α : Type u) (n : ℕ) : Type u :=
   Fin2 n → α
 
diff --git a/mathlib4/Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean b/mathlib4/Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean
index b4b354c63..70875a1a4 100644
--- a/mathlib4/Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean
+++ b/mathlib4/Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean
@@ -161,7 +161,7 @@ instance : AddCommGroup (LeftInvariantDerivation I G) :=
 
 instance : SMul 𝕜 (LeftInvariantDerivation I G) where
   smul r X := ⟨r • X.1, fun g => by
-    simp only [LinearMap.map_smul_of_tower, map_smul]; rw [left_invariant']⟩
+    simp only [LinearMap.map_smul_of_tower]; rw [left_invariant']⟩
 
 variable (r)
 
diff --git a/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean b/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
index cb00db35f..12a41f73d 100644
--- a/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
+++ b/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
@@ -53,6 +53,7 @@ variable (I)
 
 /-! #### Model with corners -/
 
+set_option backward.isDefEq.respectTransparency.types false in
 protected theorem hasMFDerivAt {x} : HasMFDerivAt I 𝓘(𝕜, E) I x (ContinuousLinearMap.id _ _) :=
   ⟨I.continuousAt, (hasFDerivWithinAt_id _ _).congr' I.rightInvOn (mem_range_self _)⟩
 
@@ -71,6 +72,7 @@ protected theorem mdifferentiableOn {s} : MDiff[s] I := fun _ _ =>
 
 protected theorem mdifferentiable : MDiff I := fun _ => I.mdifferentiableAt
 
+set_option backward.isDefEq.respectTransparency.types false in
 theorem hasMFDerivWithinAt_symm {x} (hx : x ∈ range I) :
     HasMFDerivWithinAt 𝓘(𝕜, E) I I.symm (range I) x (ContinuousLinearMap.id _ _) :=
   ⟨I.continuousWithinAt_symm,
@@ -309,6 +311,11 @@ lemma mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt
     simp only [Function.comp_def, PartialEquiv.left_inv (extChartAt I x) hz, id_eq]
   · simp only [Function.comp_def, PartialEquiv.right_inv (extChartAt I x) hy, id_eq]
 
+#adaptation_note
+/--
+Suggested fix: Make `TangentSpace` implicit-reducible, then remove `respectTransparency false`.
+-/
+set_option backward.isDefEq.respectTransparency false in
 /-- The composition of the derivative of the inverse of `extChartAt` with the derivative of
 `extChartAt` gives the identity.
 Version where the basepoint belongs to `(extChartAt I x).source`. -/
@@ -318,7 +325,6 @@ lemma mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt'
       = ContinuousLinearMap.id _ _ := by
   have : y = (extChartAt I x).symm (extChartAt I x y) := ((extChartAt I x).left_inv hy).symm
   convert! mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt ((extChartAt I x).map_source hy)
-  rw [(extChartAt I x).left_inv (by simpa using hy)]
 
 lemma isInvertible_mfderivWithin_extChartAt_symm {y : E} (hy : y ∈ (extChartAt I x).target) :
     (mfderiv[range I] (extChartAt I x).symm y).IsInvertible :=
diff --git a/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean b/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
index 327537cd8..11a7c910e 100644
--- a/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
+++ b/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
@@ -493,6 +493,12 @@ theorem writtenInExtChartAt_comp (h : ContinuousWithinAt f s x) :
 variable {f' f₀' f₁' : TangentSpace% x →L[𝕜] TangentSpace% (f x)}
   {g' : TangentSpace% (f x) →L[𝕜] TangentSpace% (g (f x))}
 
+#adaptation_note
+/--
+Suggested fix: Make `TangentSpace` implicit-reducible, then remove `respectTransparency false`.
+After that, `instanceTypes false` can be removed, too.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 /-- `UniqueMDiffWithinAt` achieves its goal: it implies the uniqueness of the derivative. -/
 protected nonrec theorem UniqueMDiffWithinAt.eq (U : UniqueMDiffAt[s] x)
@@ -516,11 +522,23 @@ theorem mfderivWithin_univ : mfderiv[univ] f = mfderiv% f := by
   simp only [mfderivWithin, mfderiv, mfld_simps]
   rw [mdifferentiableWithinAt_univ]
 
+#adaptation_note
+/--
+Suggested fix: Make `TangentSpace` implicit-reducible, then remove `respectTransparency false`.
+After that, `instanceTypes false` can be removed, too.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 theorem mfderivWithin_zero_of_not_mdifferentiableWithinAt (h : ¬MDiffAt[s] f x) :
     mfderiv[s] f x = 0 := by
   simp only [mfderivWithin, h, ite_eq_right, not_false_iff]
 
+#adaptation_note
+/--
+Suggested fix: Make `TangentSpace` implicit-reducible, then remove `respectTransparency false`.
+After that, `instanceTypes false` can be removed, too.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 theorem mfderiv_zero_of_not_mdifferentiableAt (h : ¬MDiffAt f x) :
     mfderiv% f x = 0 := by simp only [mfderiv, h, ite_eq_right, not_false_iff]
@@ -561,11 +579,13 @@ theorem mdifferentiableAt_of_isInvertible_mfderiv (hf : (mfderiv% f x).IsInverti
     MDiffAt f x :=
   mdifferentiableAt_of_mfderiv_injective hf.injective
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem HasMFDerivWithinAt.mono (h : HasMFDerivAt[t] f x f') (hst : s ⊆ t) :
     HasMFDerivAt[s] f x f' :=
   ⟨ContinuousWithinAt.mono h.1 hst,
     HasFDerivWithinAt.mono h.2 (inter_subset_inter (preimage_mono hst) (Subset.refl _))⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem HasMFDerivAt.hasMFDerivWithinAt (h : HasMFDerivAt% f x f') : HasMFDerivAt[s] f x f' :=
   ⟨ContinuousAt.continuousWithinAt h.1, HasFDerivWithinAt.mono h.2 inter_subset_right⟩
 
@@ -585,6 +605,12 @@ theorem hasMFDerivAt_unique (h₀ : HasMFDerivAt% f x f₀') (h₁ : HasMFDerivA
   rw [← hasMFDerivWithinAt_univ] at h₀ h₁
   exact (uniqueMDiffWithinAt_univ I).eq h₀ h₁
 
+#adaptation_note
+/--
+Suggested fix: Make `TangentSpace` implicit-reducible, then remove `respectTransparency false`.
+After that, `instanceTypes false` can be removed, too.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 theorem hasMFDerivWithinAt_inter' (h : t ∈ 𝓝[s] x) :
     HasMFDerivAt[s ∩ t] f x f' ↔ HasMFDerivAt[s] f x f' := by
@@ -592,6 +618,12 @@ theorem hasMFDerivWithinAt_inter' (h : t ∈ 𝓝[s] x) :
     hasFDerivWithinAt_inter', continuousWithinAt_inter' h]
   exact extChartAt_preimage_mem_nhdsWithin h
 
+#adaptation_note
+/--
+Suggested fix: Make `TangentSpace` implicit-reducible, then remove `respectTransparency false`.
+After that, `instanceTypes false` can be removed, too.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 theorem hasMFDerivWithinAt_inter (h : t ∈ 𝓝 x) :
     HasMFDerivAt[s ∩ t] f x f' ↔ HasMFDerivAt[s] f x f' := by
@@ -599,6 +631,7 @@ theorem hasMFDerivWithinAt_inter (h : t ∈ 𝓝 x) :
     continuousWithinAt_inter h]
   exact extChartAt_preimage_mem_nhds h
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem HasMFDerivWithinAt.union (hs : HasMFDerivAt[s] f x f') (ht : HasMFDerivAt[t] f x f') :
     HasMFDerivAt[s ∪ t] f x f' := by
   constructor
@@ -858,6 +891,7 @@ theorem preimage_extChartAt_eventuallyEq_compl_singleton (y : M) (h : s =ᶠ[
 
 /-! ### Congruence lemmas for derivatives on manifolds -/
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- If two sets coincide locally, except maybe at a point, then it is equivalent to have a manifold
 derivative within one or the other. -/
 theorem hasMFDerivWithinAt_congr_set' (y : M) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
@@ -918,6 +952,7 @@ theorem HasMFDerivWithinAt.congr_mfderiv (h : HasMFDerivAt[s] f x f') (h' : f' =
     HasMFDerivAt[s] f x f₁' :=
   h' ▸ h
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem HasMFDerivWithinAt.congr_of_eventuallyEq
     (h : HasMFDerivAt[s] f x f') (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
     HasMFDerivAt[s] f₁ x f' := by
diff --git a/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/Defs.lean b/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/Defs.lean
index 8ff76e4c1..bee59ca37 100644
--- a/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/Defs.lean
+++ b/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/Defs.lean
@@ -283,6 +283,7 @@ variable (I I') in
 def OpenPartialHomeomorph.MDifferentiable (f : OpenPartialHomeomorph M M') :=
   MDifferentiableOn I I' f f.source ∧ MDifferentiableOn I' I f.symm f.target
 
+set_option backward.isDefEq.respectTransparency.instances false in
 variable (I I') in
 /-- `HasMFDerivWithinAt I I' f s x f'` indicates that the function `f` between manifolds
 has, at the point `x` and within the set `s`, the derivative `f'`. Here, `f'` is a continuous linear
@@ -301,6 +302,7 @@ def HasMFDerivWithinAt (f : M → M') (s : Set M) (x : M)
     HasFDerivWithinAt (writtenInExtChartAt I I' x f : E → E') f'
       ((extChartAt I x).symm ⁻¹' s ∩ range I) ((extChartAt I x) x)
 
+set_option backward.isDefEq.respectTransparency.instances false in
 variable (I I') in
 /-- `HasMFDerivAt I I' f x f'` indicates that the function `f` between manifolds
 has, at the point `x`, the derivative `f'`. Here, `f'` is a continuous linear
diff --git a/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean b/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
index 39d5c7eee..b67969a0f 100644
--- a/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
+++ b/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
@@ -579,6 +579,8 @@ lemma mvfderiv_smul {x : M} {a : M → 𝕜} (ha : MDiffAt a x) {g : M → F} (h
   ext v
   simp [mvfderiv, -Pi.smul_apply', fromTangentSpace_mfderiv_smul_apply ha hg]
 
+set_option allowUnsafeReducibility true in
+attribute [local semireducible] TangentSpace in
 @[simp, to_fun mvfderiv_fun_mul]
 lemma mvfderiv_mul {f g : M → 𝕜} {x : M} (hf : MDiffAt f x) (hg : MDiffAt g x) :
     d% (f * g) x = f x • d% g x + (g x) • (d% f x) := by
diff --git a/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean b/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
index 5540f1fbc..96573a838 100644
--- a/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
+++ b/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
@@ -125,6 +125,7 @@ section id
 
 /-! #### Identity -/
 
+set_option backward.isDefEq.respectTransparency.types false in
 theorem hasMFDerivAt_id (x : M) :
     HasMFDerivAt% (@id M) x (ContinuousLinearMap.id 𝕜 (TangentSpace% x)) := by
   refine ⟨continuousAt_id, ?_⟩
@@ -479,6 +480,7 @@ theorem MDifferentiableOn.prodMap (hf : MDiff[s] f) (hg : MDiff[r] g) :
 theorem MDifferentiable.prodMap (hf : MDiff f) (hg : MDiff g) : MDiff (Prod.map f g) := fun p ↦
   (hf p.1).prodMap' (hg p.2)
 
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma HasMFDerivWithinAt.prodMap {s : Set <| M × M'} {p : M × M'} {f : M → N} {g : M' → N'}
     {df : TangentSpace% p.1 →L[𝕜] TangentSpace% (f p.1)}
     (hf : HasMFDerivAt[Prod.fst '' s] f p.1 df)
@@ -661,6 +663,7 @@ lemma writtenInExtChartAt_sumSwap_eventuallyEq_id :
       refine ⟨I.continuousWithinAt_symm.preimage_mem_nhdsWithin ?_, self_mem_nhdsWithin⟩
       exact (chartAt H x).open_target.mem_nhds (by simp)
 
+set_option backward.isDefEq.respectTransparency.types false in
 theorem hasMFDerivAt_sumSwap :
     HasMFDerivAt% (@Sum.swap M M') p (ContinuousLinearMap.id 𝕜 (TangentSpace% p)) := by
   refine ⟨by fun_prop, ?_⟩
@@ -705,6 +708,7 @@ lemma writtenInExtChartAt_sumInr_eventuallyEq_id :
     Sum.inr_injective.extend_apply <| chartAt H q',
     (chartAt H q').right_inv (by simpa [Set.mem_preimage, I.left_inv] using hyT)]
 
+set_option backward.isDefEq.respectTransparency.types false in
 theorem hasMFDerivWithinAt_inl :
     HasMFDerivAt[s] (@Sum.inl M M') q (ContinuousLinearMap.id 𝕜 (TangentSpace% q)) := by
   refine ⟨by fun_prop, ?_⟩
@@ -719,6 +723,7 @@ theorem hasMFDerivAt_inl :
     HasMFDerivAt% (@Sum.inl M M') q (ContinuousLinearMap.id 𝕜 (TangentSpace% p)) := by
   simpa [HasMFDerivAt, hasMFDerivWithinAt_univ] using! hasMFDerivWithinAt_inl (s := Set.univ)
 
+set_option backward.isDefEq.respectTransparency.types false in
 theorem hasMFDerivWithinAt_inr {t : Set M'} :
     HasMFDerivAt[t] (@Sum.inr M M') q' (ContinuousLinearMap.id 𝕜 (TangentSpace% q')) := by
   refine ⟨by fun_prop, ?_⟩
diff --git a/mathlib4/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean b/mathlib4/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean
index 2121cd479..e937c878f 100644
--- a/mathlib4/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean
+++ b/mathlib4/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean
@@ -103,6 +103,37 @@ lemma mlieBracketWithin_eq_lieBracketWithin {V W : Π (x : E), TangentSpace 𝓘
 @[simp] lemma mlieBracketWithin_univ :
     mlieBracketWithin I V W univ = mlieBracket I V W := (rfl)
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`FunLike (TangentSpace 𝓘(𝕜, E) (↑I (↑(chartAt H x) x)) →L[𝕜] TangentSpace I x) _ _`
+It is needed by `map_zero` in the first bullet's `simp only`. That same `simp only` unfolds
+`extChartAt`, which rewrites `↑(extChartAt I x) x` in the type index to `↑I (↑(chartAt H x) x)`,
+while the instance arguments inside the term keep the old spelling `↑(extChartAt I x) x`.
+
+The failure happens while applying `@ContinuousLinearMap.funLike`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type is
+`TopologicalSpace (TangentSpace 𝓘(𝕜, E) (↑I (↑(chartAt H x) x)))`, whereas the assigned value
+`instTopologicalSpaceTangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)` has type
+`TopologicalSpace (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x))`. The comparison bottoms out at
+`(extChartAt I x).1 =?= @ModelWithCorners.toFun'`. Lean falls back to synthesize an instance of the
+correct type, which succeeds and returns
+`instTopologicalSpaceTangentSpace 𝓘(𝕜, E) (↑I (↑(chartAt H x) x))`, but that is again not defeq to
+the assigned value, stalling at the same comparison. It, too, runs at `.instances`, since
+`respectTransparency false` suppresses the transparency bump that instance-implicit arguments would
+otherwise receive.
+
+With no `FunLike` instance found, `map_zero` does not fire and the goal
+`(mfderiv% (↑I ∘ ↑(chartAt H x)) x).inverse 0 = 0` is left open.
+
+Potential fix: mark `TangentSpace` implicit-reducible, then remove `respectTransparency false`; the
+bumped comparison then unfolds both `TangentSpace`'s to `E`, so the point no longer
+matters. The annotation has to be at the definition site of `TangentSpace`; a `local` attribute here
+is not enough.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 lemma mlieBracketWithin_eq_zero_of_eq_zero (hV : V x = 0) (hW : W x = 0) :
     mlieBracketWithin I V W s x = 0 := by
@@ -135,6 +166,23 @@ lemma mlieBracket_swap_apply : mlieBracket I V W x = - mlieBracket I W V x :=
 lemma mlieBracket_swap : mlieBracket I V W = - mlieBracket I W V :=
   mlieBracketWithin_swap
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+This is the same failure as for `mlieBracketWithin_eq_zero_of_eq_zero` above, reached through the
+`simp` below instead: the instance
+`FunLike (TangentSpace 𝓘(𝕜, E) (↑I (↑(chartAt H x✝) x✝)) →L[𝕜] TangentSpace I x✝) _ _` cannot be
+synthesized, because while applying `@ContinuousLinearMap.funLike` the metavariable of type
+`TopologicalSpace (TangentSpace 𝓘(𝕜, E) (↑I (↑(chartAt H x✝) x✝)))` is assigned
+`instTopologicalSpaceTangentSpace 𝓘(𝕜, E) (↑(extChartAt I x✝) x✝)`, whose type spells the point as
+`↑(extChartAt I x✝) x✝`. Both the direct `.instances` check and the comparison against the
+re-synthesized instance bottom out at `(extChartAt I x✝).1 =?= @ModelWithCorners.toFun'`, and the
+goal `(mfderiv% (↑I ∘ ↑(chartAt H x✝)) x✝).inverse 0 = 0` is left open.
+
+Potential fix: mark `TangentSpace` implicit-reducible at its definition site, then remove
+`respectTransparency false`.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 @[simp] lemma mlieBracketWithin_self : mlieBracketWithin I V V = 0 := by
   ext x; simp [mlieBracketWithin, mpullback]
@@ -335,6 +383,44 @@ private lemma mfderiv_extChart_inverse_comp_aux :
       ((mfderiv[range I] φ.symm (φ x)).inverse) (W (φ.symm (φ x))) = W x := by
   rw [mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm, extChartAt_to_inv]
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`HSMul (TangentSpace 𝓘(𝕜, 𝕜) (f x)) (TangentSpace I x) ?m`
+It is needed for the `•` in the statement below, and reduces through the `instHSMul`/`SMul`/…/
+`Module` chain sketched in the section header to
+`Module (TangentSpace 𝓘(𝕜, 𝕜) (f x)) (TangentSpace I x)`.
+
+The failure happens while applying `@instModuleTangentSpace`. This seems to make sense
+mathematically: it makes `TangentSpace I x` a `𝕜`-module, but not a
+`TangentSpace 𝓘(𝕜, 𝕜) (f x)`-module as needed.
+
+Unlike for the two adaptations above, marking `TangentSpace` implicit-reducible at its definition
+site does not fix this one. It does make `respectTransparency false` removable, but
+`instanceTypes false` is still needed afterwards.
+
+The technical reason for the failure: assigning one of the instane's instance-implicit-argument
+metavariables is rejected because the metavariable's type and the type of the assigned value do not
+match at `.instances` transparency. The metavariable's expected type is
+`NontriviallyNormedField (TangentSpace 𝓘(𝕜, 𝕜) (f x))`, whereas the assigned value is the ambient
+instance of type `NontriviallyNormedField 𝕜`. The comparison bottoms out at
+`TangentSpace 𝓘(𝕜, 𝕜) (f x) =?= 𝕜`, where `TangentSpace` is a plain semireducible `def` and
+therefore does not unfold at the `.instances` transparency that instance search runs at. Lean falls
+back to synthesize an instance of the expected type, but that synthesis fails as well.
+
+Instance search follows this path:
+
+```
+  HSMul (TangentSpace 𝓘(𝕜,𝕜) (f x)) (TangentSpace I x) ?m.238
+    └ @instHSMul
+      └ @SMulZeroClass.toSMul
+        └ @SMulWithZero.toSMulZeroClass
+          └ MulActionWithZero.toSMulWithZero
+            └ @Module.toMulActionWithZero
+```
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 /-- Pulling back through `extChartAt` the scalar multiplication of a vector field by
 the derivative of a scalar function equals the scalar multiplication by the manifold derivative. -/
diff --git a/mathlib4/Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean b/mathlib4/Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
index 745a3c0c6..eccc2d643 100644
--- a/mathlib4/Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
+++ b/mathlib4/Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
@@ -440,12 +440,14 @@ lemma stalkMap_inv_hom_apply (e : X ≅ Y) (x : X) (y) :
       X.presheaf.stalkSpecializes (specializes_of_eq <| by simp) y :=
   DFunLike.congr_fun (CommRingCat.hom_ext_iff.mp (stalkMap_inv_hom e x)) y
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[reassoc (attr := simp)]
 lemma stalkMap_germ (U : Opens Y) (x : X) (hx : f.base x ∈ U) :
     Y.presheaf.germ U (f.base x) hx ≫ f.stalkMap x =
       f.c.app (op U) ≫ X.presheaf.germ ((Opens.map f.base).obj U) x hx :=
   PresheafedSpace.stalkMap_germ f.toHom U x hx
 
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma stalkMap_germ_apply (U : Opens Y) (x : X) (hx : f.base x ∈ U) (y) :
     f.stalkMap x (Y.presheaf.germ U (f.base x) hx y) =
       X.presheaf.germ ((Opens.map f.base).obj U) x hx (f.c.app (op U) y) :=
diff --git a/mathlib4/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean b/mathlib4/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
index c013865e9..e018dcdd2 100644
--- a/mathlib4/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
+++ b/mathlib4/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
@@ -79,6 +79,7 @@ lemma evaluation_eq_zero_iff_notMem_basicOpen (x : U) (f : X.presheaf.obj (op U)
   rw [X.toRingedSpace.mem_basicOpen f x.1 x.2, ← not_iff_not, not_not]
   exact (IsLocalRing.residue_ne_zero_iff_isUnit _)
 
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma evaluation_ne_zero_iff_mem_basicOpen (x : U) (f : X.presheaf.obj (op U)) :
     X.evaluation x f ≠ 0 ↔ x.val ∈ X.toRingedSpace.basicOpen f := by
   simp
@@ -89,11 +90,13 @@ lemma basicOpen_eq_bot_iff_forall_evaluation_eq_zero (f : X.presheaf.obj (op U))
   exact ⟨fun h ↦ h ▸ fun a _ hc ↦ hc,
     fun h ↦ eq_bot_iff.mpr <| fun a ha ↦ h a (X.toRingedSpace.basicOpen_le f ha) ha⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 lemma Γevaluation_eq_zero_iff_notMem_basicOpen (x : X) (f : X.presheaf.obj (op ⊤)) :
     X.Γevaluation x f = 0 ↔ x ∉ X.toRingedSpace.basicOpen f :=
   evaluation_eq_zero_iff_notMem_basicOpen X ⟨x, show x ∈ ⊤ by trivial⟩ f
 
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma Γevaluation_ne_zero_iff_mem_basicOpen (x : X) (f : X.presheaf.obj (op ⊤)) :
     X.Γevaluation x f ≠ 0 ↔ x ∈ X.toRingedSpace.basicOpen f :=
   evaluation_ne_zero_iff_mem_basicOpen X ⟨x, show x ∈ ⊤ by trivial⟩ f
diff --git a/mathlib4/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/mathlib4/Mathlib/Geometry/RingedSpace/OpenImmersion.lean
index cc16fc4c4..7f803142f 100644
--- a/mathlib4/Mathlib/Geometry/RingedSpace/OpenImmersion.lean
+++ b/mathlib4/Mathlib/Geometry/RingedSpace/OpenImmersion.lean
@@ -194,7 +194,6 @@ theorem inv_naturality {U V : (Opens X)ᵒᵖ} (i : U ⟶ V) :
     TopCat.Presheaf.pushforward_obj_map]
   congr 1
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance (U : Opens X) : IsIso (invApp f U) := by delta invApp; infer_instance
 
 set_option backward.isDefEq.respectTransparency.types false in
diff --git a/mathlib4/Mathlib/GroupTheory/PresentedGroup.lean b/mathlib4/Mathlib/GroupTheory/PresentedGroup.lean
index f02de660f..ddb70af74 100644
--- a/mathlib4/Mathlib/GroupTheory/PresentedGroup.lean
+++ b/mathlib4/Mathlib/GroupTheory/PresentedGroup.lean
@@ -107,8 +107,7 @@ theorem generated_by (rels : Set (FreeGroup α)) (H : Subgroup (PresentedGroup r
   · exact h _
   · exact (Subgroup.inv_mem_iff H).mpr (by assumption)
   rename_i h1 h2
-  change QuotientGroup.mk _ ∈ H.carrier
-  rw [QuotientGroup.mk_mul]
+  -- This is defeq abuse.
   exact Subgroup.mul_mem _ h1 h2
 
 section ToGroup
diff --git a/mathlib4/Mathlib/GroupTheory/SpecificGroups/ZGroup.lean b/mathlib4/Mathlib/GroupTheory/SpecificGroups/ZGroup.lean
index cf1257ee3..207a503b3 100644
--- a/mathlib4/Mathlib/GroupTheory/SpecificGroups/ZGroup.lean
+++ b/mathlib4/Mathlib/GroupTheory/SpecificGroups/ZGroup.lean
@@ -72,6 +72,8 @@ theorem of_injective [hG' : IsZGroup G'] (hf : Function.Injective f) : IsZGroup
 
 instance [IsZGroup G] (H : Subgroup G) : IsZGroup H := of_injective H.subtype_injective
 
+-- Needs to unfold `Sylow.mapSurjective`.
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem of_surjective [Finite G] [hG : IsZGroup G] (hf : Function.Surjective f) : IsZGroup G' := by
   rw [isZGroup_iff] at hG ⊢
   intro p hp P
@@ -246,6 +248,7 @@ theorem le_center_or_le_commutator [P.Normal] : P ≤ Subgroup.center G ∨ P 
   · rw [← h, commutator_def]
     exact Subgroup.commutator_mono le_top le_top
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- A cyclic Sylow subgroup is either central in its normalizer or contained in the commutator
   subgroup. -/
 theorem normalizer_le_centralizer_or_le_commutator :
diff --git a/mathlib4/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean b/mathlib4/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
index 59f30001e..55d5d7097 100644
--- a/mathlib4/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
+++ b/mathlib4/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
@@ -170,7 +170,7 @@ def domCoprod' :
       simp only [Quotient.liftOn'_mk'', coe_add, coe_smul, _root_.smul_apply,
         ← MultilinearMap.domCoprod'_apply]
       simp only [TensorProduct.add_tmul, ← TensorProduct.smul_tmul', TensorProduct.tmul_add,
-        TensorProduct.tmul_smul, map_add, map_smul]
+        TensorProduct.tmul_smul, map_add]
       first | rw [← smul_add] | rw [smul_comm]
       rfl
 
diff --git a/mathlib4/Mathlib/LinearAlgebra/Contraction.lean b/mathlib4/Mathlib/LinearAlgebra/Contraction.lean
index d6a838fd4..5d357a932 100644
--- a/mathlib4/Mathlib/LinearAlgebra/Contraction.lean
+++ b/mathlib4/Mathlib/LinearAlgebra/Contraction.lean
@@ -421,9 +421,9 @@ theorem dualDistrib_dualDistribInvOfBasis_left_inverse (b : Basis ι R M) (c : B
   rintro ⟨i', j'⟩
   simp only [dualDistrib, Basis.coe_dualBasis, coe_comp, Function.comp_apply,
     dualDistribInvOfBasis_apply, Basis.coord_apply, Basis.tensorProduct_repr_tmul_apply,
-    Basis.repr_self, _root_.map_sum, map_smul, homTensorHomMap_apply, compRight_apply,
-    Basis.tensorProduct_apply, LinearMap.coe_sum, Finset.sum_apply, smul_apply, LinearEquiv.coe_coe,
-    map_tmul, lid_tmul, smul_eq_mul, id_coe, id_eq]
+    Basis.repr_self, _root_.map_sum, compRight_apply,
+    Basis.tensorProduct_apply, LinearMap.coe_sum, Finset.sum_apply, LinearEquiv.coe_coe,
+    smul_eq_mul, id_coe, id_eq]
   rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
   · simpa using mul_comm _ _
   all_goals { intros; simp [*] at * }
diff --git a/mathlib4/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean b/mathlib4/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean
index 36f51dded..815509585 100644
--- a/mathlib4/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean
+++ b/mathlib4/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean
@@ -47,6 +47,45 @@ noncomputable def equivPiTensorComplSingletonTensor (i₀ : ι) :
 
 variable (i₀ : ι)
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`AddCommMonoid (⨂[R] (i₁ : { i // ¬i = i₀ }), M ↑i₁)`
+The companion searches `Module R (⨂[R] (i₁ : { i // ¬i = i₀ }), M ↑i₁)` and the two `PUnit`-indexed
+variants fail in the same way. They are needed by the `rw [dsimp% …]` below, after `Equiv.symm_symm`
+has rewritten the index type to `{ i // ¬i = i₀ }` while the instance arguments in the term stay
+phrased through the equivalence.
+
+The failure happens while applying `@PiTensorProduct.instAddCommMonoid`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type of
+the assigned value do not match at `.instances` transparency. The metavariable's expected type is
+`(i : { i // ¬i = i₀ }) → AddCommMonoid (M ↑i)`, whereas the assigned value
+`fun i ↦ inst✝ ((Equiv.subtypeNeSumPUnit i₀) (Sum.inl i))` has type
+`(i : { i // i ≠ i₀ }) → AddCommMonoid (M ((Equiv.subtypeNeSumPUnit i₀) (Sum.inl i)))`. The
+comparison bottoms out at `i.1 =?= (Equiv.subtypeNeSumPUnit i₀).1 (Sum.inl i)`, i.e. at actually
+computing the equivalence on `Sum.inl i`. Lean falls back to synthesize an instance of the correct
+type, which succeeds, but it returns `fun i ↦ inst✝ ↑i`, which is again not defeq to the assigned
+value, for the same reason. The `respectTransparency false` backward-compatibility flag blocks Lean
+from bumping to implicit, so the comparison happens at `.instances` again.
+
+Validated, but perhaps too invasive, fix: Make all of the following definitions implicit-reducible:
+
+```
+  Equiv.trans
+  Equiv.optionSubtype
+  Equiv.optionEquivSumPUnit
+  Equiv.refl
+  Set.singleton
+  Option.casesOn'
+  Equiv.optionSubtypeNe
+  Sum.elim
+```
+
+Then both backward compatibility options can go: first `respectTransparency false`, then
+`instanceTypes false`.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma equivPiTensorComplSingletonTensor_tprod (i₀ : ι) (m : ∀ i, M i) :
diff --git a/mathlib4/Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean b/mathlib4/Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
index 1278e7eb1..3aea93810 100644
--- a/mathlib4/Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
+++ b/mathlib4/Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
@@ -74,6 +74,8 @@ theorem borel_eq_generateFrom_Iio : borel α = .generateFrom (range Iio) := by
     intro a
     exact GenerateMeasurable.basic _ isOpen_Iio
 
+-- Applying an instance about `α` to `αᵒᵈ`.
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem borel_eq_generateFrom_Ioi : borel α = .generateFrom (range Ioi) :=
   @borel_eq_generateFrom_Iio αᵒᵈ _ (by infer_instance : SecondCountableTopology α) _ _
 
diff --git a/mathlib4/Mathlib/MeasureTheory/Measure/Haar/Extension.lean b/mathlib4/Mathlib/MeasureTheory/Measure/Haar/Extension.lean
index 39f6ec2c5..944f3c6e1 100644
--- a/mathlib4/Mathlib/MeasureTheory/Measure/Haar/Extension.lean
+++ b/mathlib4/Mathlib/MeasureTheory/Measure/Haar/Extension.lean
@@ -162,11 +162,15 @@ noncomputable def integrate : CompactlySupportedContinuousMap B E →ₗ[ℝ] E
     rw [map_smul]
     exact integral_smul x (H.pushforward μA f)
 
+set_option backward.isDefEq.instanceTypes false in
+set_option backward.isDefEq.respectTransparency.instances false in
 @[to_additive]
 theorem integrate_apply (f : CompactlySupportedContinuousMap B E) :
     H.integrate μA μC f = ∫ c, pushforward H μA f c ∂μC :=
   rfl
 
+set_option backward.isDefEq.instanceTypes false in
+set_option backward.isDefEq.respectTransparency.instances false in
 @[to_additive]
 theorem integrate_mono {f g : CompactlySupportedContinuousMap B ℝ} (h : f ≤ g) :
     integrate H μA μC f ≤ integrate H μA μC g :=
@@ -175,6 +179,8 @@ theorem integrate_mono {f g : CompactlySupportedContinuousMap B ℝ} (h : f ≤
 
 variable [T2Space B] [MeasurableSpace B] [BorelSpace B]
 
+set_option backward.isDefEq.instanceTypes false in
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- If `φ : A →* B` and `ψ : B →* C` define a short exact sequence of topological groups, then we
 can define a Haar measure on `B` induced by the Haar measures on `A` and `C`. -/
 @[to_additive /-- If `φ : A →+ B` and `ψ : B →+ C` define a short exact sequence of additive
@@ -183,15 +189,21 @@ and `C`. -/]
 noncomputable def inducedMeasure : Measure B :=
   RealRMK.rieszMeasure ⟨integrate H μA μC, fun _ _ ↦ integrate_mono H μA μC⟩
 
+set_option backward.isDefEq.instanceTypes false in
+set_option backward.isDefEq.respectTransparency.instances false in
 @[to_additive]
 instance inducedMeasure_regular : (inducedMeasure H μA μC).Regular :=
   RealRMK.regular_rieszMeasure _
 
+set_option backward.isDefEq.instanceTypes false in
+set_option backward.isDefEq.respectTransparency.instances false in
 @[to_additive]
 theorem integral_inducedMeasure (f : CompactlySupportedContinuousMap B ℝ) :
     ∫ b : B, f b ∂(inducedMeasure H μA μC) = integrate H μA μC f := by
   apply RealRMK.integral_rieszMeasure
 
+set_option backward.isDefEq.instanceTypes false in
+set_option backward.isDefEq.respectTransparency.instances false in
 @[to_additive]
 instance isHaarMeasure_inducedMeasure : IsHaarMeasure (inducedMeasure H μA μC) where
   lt_top_of_isCompact K hK := by
@@ -230,6 +242,8 @@ instance isHaarMeasure_inducedMeasure : IsHaarMeasure (inducedMeasure H μA μC)
     exact (pullback H ⟨f, hf2⟩ _).continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero
       (pullback H ⟨f, hf2⟩ _).hasCompactSupport (fun x ↦ (hf4 _).1) ha
 
+set_option backward.isDefEq.instanceTypes false in
+set_option backward.isDefEq.respectTransparency.instances false in
 set_option backward.isDefEq.respectTransparency.types false in
 /-- If `φ : A →* B` and `ψ : B →* C` define a short exact sequence of topological groups, and if
 `ψ` is injective on an open set `U`, then the induced measure on `U` is bounded above by
diff --git a/mathlib4/Mathlib/ModelTheory/Types.lean b/mathlib4/Mathlib/ModelTheory/Types.lean
index 8f9efd01e..457a59c75 100644
--- a/mathlib4/Mathlib/ModelTheory/Types.lean
+++ b/mathlib4/Mathlib/ModelTheory/Types.lean
@@ -237,6 +237,33 @@ def realizedTypes (α : Type w) : Set (T.CompleteType α) :=
 
 section
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`(L.lhomWithConstants α).IsExpansionOn ↑(ModelType.reduct (L.lhomWithConstants α)
+(M.subtheoryModel ⋯))`
+It is needed by the `@Formula.realize_equivSentence_symm_con` application below, which passes
+`M.struc` explicitly.
+
+The failure happens while applying `@LHom.isExpansionOn_reduct`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type of
+the assigned value do not match at `.instances` transparency. The metavariable's expected type is
+`L[[α]].Structure ↑(ModelType.reduct (L.lhomWithConstants α) (M.subtheoryModel ⋯))`, whereas the
+supplied `M.struc` has type `L[[α]].Structure ↑M`. The comparison bottoms out at
+`ModelType.reduct (L.lhomWithConstants α) (M.subtheoryModel ⋯) =?= M`, which would require
+`ModelType.reduct` and `ModelType.subtheoryModel` to unfold; both are plain semireducible `def`s and
+therefore do not unfold at the `.instances` transparency that instance search runs at. Lean falls
+back to synthesize an instance of the correct type, but that synthesis fails as well: its only
+candidate `@ModelType.struc` needs to unify `T` with a metavariable of type `L[[α]].Theory`, and
+`L[[α]].Theory` and `L.Theory` do not even agree at `.default`.
+
+Potential fix: mark `ModelType.reduct` and `ModelType.subtheoryModel`
+implicit-reducible and replace `M.struc` with `cast rfl M.struc`, so that it gets the correct type.
+The `cast rfl` there is a quick and dirty way of ensuring that the `Structure` instance has the
+expected type.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 theorem exists_modelType_is_realized_in (p : T.CompleteType α) :
     ∃ M : Theory.ModelType.{u, v, max u v w} T, p ∈ T.realizedTypes M α := by
diff --git a/mathlib4/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean b/mathlib4/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
index 9e37588ae..5e74556f7 100644
--- a/mathlib4/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
+++ b/mathlib4/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
@@ -402,6 +402,7 @@ theorem logEmbeddingQuot_apply (x : (𝓞 K)ˣ) :
     logEmbeddingQuot K (Additive.ofMul (QuotientGroup.mk x)) =
       logEmbedding K (Additive.ofMul x) := rfl
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem logEmbeddingQuot_injective :
     Function.Injective (logEmbeddingQuot K) := by
   unfold logEmbeddingQuot
diff --git a/mathlib4/Mathlib/NumberTheory/Padics/WithVal.lean b/mathlib4/Mathlib/NumberTheory/Padics/WithVal.lean
index 641d6ab71..83e353c35 100644
--- a/mathlib4/Mathlib/NumberTheory/Padics/WithVal.lean
+++ b/mathlib4/Mathlib/NumberTheory/Padics/WithVal.lean
@@ -35,7 +35,41 @@ variable {p : ℕ} [Fact p.Prime]
 
 open NNReal WithZero UniformSpace
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+```
+MonoidWithZeroHomClass ((MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ →*₀
+  WithZero (Multiplicative ℤ)) (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀
+  (WithZero (Multiplicative ℤ))
+```
+It is needed in the second bullet below, whose final `simp_all` otherwise leaves the goal
+`1 ≤ padicValRat p (x.ofVal - y.ofVal) + (embedding ↑γ).log` unsolved.
+
+The failure happens while applying `@MonoidWithZeroHom.monoidWithZeroHomClass`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type
+is `MulZeroOneClass (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀`, whereas the assigned value
+`instMulZeroOneClass` has type
+`MulZeroOneClass (WithZero ↥(MonoidWithZeroHom.ofClass Valued.v).valueGroup)`.
+Lean falls back to synthesize an instance of the correct type, which
+succeeds, but it returns a `instMulZeroOneClass` instance that is not defeq to the assigned one
+at `.implicit` transparency.
+
+Potential fix: make the following definitions implicit-reducible:
+
+```
+  Rat.padicValuation
+  Valuation.restrict
+  coe
+  exp
+```
+
+Then both backward compatibility options can go.
+-/
 set_option backward.isDefEq.respectTransparency.types false in
+set_option backward.isDefEq.instanceTypes false in
 open MonoidWithZeroHom.ValueGroup₀ in
 lemma isUniformInducing_cast_withVal : IsUniformInducing ((Rat.castHom ℚ_[p]).comp
     (WithVal.equiv (Rat.padicValuation p)).toRingHom) := by
diff --git a/mathlib4/Mathlib/Order/Category/FinBoolAlg.lean b/mathlib4/Mathlib/Order/Category/FinBoolAlg.lean
index 92082732f..7dadc33bb 100644
--- a/mathlib4/Mathlib/Order/Category/FinBoolAlg.lean
+++ b/mathlib4/Mathlib/Order/Category/FinBoolAlg.lean
@@ -59,6 +59,8 @@ instance : Inhabited FinBoolAlg :=
 instance largeCategory : LargeCategory FinBoolAlg :=
   inferInstanceAs <| Category (InducedCategory _ toBoolAlg)
 
+-- Would need to have a new type synonym for the `FunLike` instance for the induced category.
+set_option backward.isDefEq.respectTransparency.instances false in
 instance concreteCategory : ConcreteCategory FinBoolAlg (BoundedLatticeHom · ·) :=
   inferInstanceAs <| ConcreteCategory (InducedCategory _ toBoolAlg) _
 
diff --git a/mathlib4/Mathlib/Order/Category/FinPartOrd.lean b/mathlib4/Mathlib/Order/Category/FinPartOrd.lean
index f44f1fe62..4a816124e 100644
--- a/mathlib4/Mathlib/Order/Category/FinPartOrd.lean
+++ b/mathlib4/Mathlib/Order/Category/FinPartOrd.lean
@@ -53,6 +53,8 @@ instance : Inhabited FinPartOrd :=
 instance largeCategory : LargeCategory FinPartOrd :=
   inferInstanceAs <| Category (InducedCategory _ toPartOrd)
 
+-- Would need to have a new type synonym for the `FunLike` instance for the induced category.
+set_option backward.isDefEq.respectTransparency.instances false in
 instance concreteCategory : ConcreteCategory FinPartOrd (· →o ·) :=
   inferInstanceAs <| ConcreteCategory (InducedCategory _ toPartOrd) _
 
diff --git a/mathlib4/Mathlib/Order/Category/NonemptyFinLinOrd.lean b/mathlib4/Mathlib/Order/Category/NonemptyFinLinOrd.lean
index b17955e0d..ad5702b6a 100644
--- a/mathlib4/Mathlib/Order/Category/NonemptyFinLinOrd.lean
+++ b/mathlib4/Mathlib/Order/Category/NonemptyFinLinOrd.lean
@@ -44,6 +44,8 @@ instance : CoeSort NonemptyFinLinOrd (Type _) where
 instance : LargeCategory NonemptyFinLinOrd :=
   inferInstanceAs <| Category (InducedCategory _ toLinOrd)
 
+-- Would need to have a new type synonym for the `FunLike` instance for the induced category.
+set_option backward.isDefEq.respectTransparency.instances false in
 instance : ConcreteCategory NonemptyFinLinOrd (· →o ·) :=
   inferInstanceAs <| ConcreteCategory (InducedCategory _ toLinOrd) _
 
diff --git a/mathlib4/Mathlib/Order/Interval/Finset/Gaps.lean b/mathlib4/Mathlib/Order/Interval/Finset/Gaps.lean
index b08c7057f..16cdb7a16 100644
--- a/mathlib4/Mathlib/Order/Interval/Finset/Gaps.lean
+++ b/mathlib4/Mathlib/Order/Interval/Finset/Gaps.lean
@@ -94,6 +94,9 @@ theorem intervalGapsWithin_snd_of_lt (hj : j < k) :
   simp only [coe_castPred, val_natCast, Nat.mod_succ_eq_iff_lt]
   lia
 
+-- Defeq abuse: `F.orderEmbOfFin_mem` infers the `LinearOrder (Lex (α × α))` as
+-- `LinearOrder (α × α)`.
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem intervalGapsWithin_mapsTo : (Set.Iio k).MapsTo
     (fun (j : ℕ) ↦ ((F.intervalGapsWithin h a b j).2, (F.intervalGapsWithin h a b j.succ).1))
     F := by
diff --git a/mathlib4/Mathlib/Order/Interval/Set/Defs.lean b/mathlib4/Mathlib/Order/Interval/Set/Defs.lean
index 068a14411..5f91d92c7 100644
--- a/mathlib4/Mathlib/Order/Interval/Set/Defs.lean
+++ b/mathlib4/Mathlib/Order/Interval/Set/Defs.lean
@@ -47,7 +47,7 @@ def Iic (b : α) := { x | x ≤ b }
 @[to_dual] theorem Iic_def (b : α) : { x | x ≤ b } = Iic b := rfl
 
 /-- `Ioo a b` is the left-open right-open interval $(a, b)$. -/
-@[to_dual self (reorder := a b)]
+@[instance_reducible, to_dual self (reorder := a b)]
 def Ioo (a b : α) := { x | a < x ∧ x < b }
 
 to_dual_insert_cast Ioo := by simp only [and_comm]
diff --git a/mathlib4/Mathlib/Order/KrullDimension.lean b/mathlib4/Mathlib/Order/KrullDimension.lean
index fdedd7636..d90ca439a 100644
--- a/mathlib4/Mathlib/Order/KrullDimension.lean
+++ b/mathlib4/Mathlib/Order/KrullDimension.lean
@@ -1138,7 +1138,7 @@ lemma coheight_le_of_krullDim_preimage_le (x : α) :
     Order.coheight x ≤ (m + 1) * Order.coheight (f x) + m := by
   rw [Order.coheight, Order.coheight]
   apply height_le_of_krullDim_preimage_le (f := f.dual)
-  exact fun x ↦ le_of_eq_of_le (krullDim_orderDual (α := f ⁻¹' {x})) (h x)
+  exact fun x ↦ le_of_eq_of_le (krullDim_orderDual (α := f ⁻¹' {OrderDual.ofDual x})) (h x)
 
 include f h in
 lemma krullDim_le_of_krullDim_preimage_le :
diff --git a/mathlib4/Mathlib/Order/RelIso/Set.lean b/mathlib4/Mathlib/Order/RelIso/Set.lean
index 69aea6ed9..dc7326068 100644
--- a/mathlib4/Mathlib/Order/RelIso/Set.lean
+++ b/mathlib4/Mathlib/Order/RelIso/Set.lean
@@ -35,6 +35,8 @@ theorem map_inf [SemilatticeInf α] [LinearOrder β] [FunLike F β α]
     a (m ⊓ n) = a m ⊓ a n :=
   (StrictMono.monotone fun _ _ => map_rel a).map_inf m n
 
+-- Defeq abuse: should mediate between `β` and `βᵒᵈ` explicitly
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem map_sup [SemilatticeSup α] [LinearOrder β] [FunLike F β α]
     [RelHomClass F (· > ·) (· > ·)] (a : F) (m n : β) :
     a (m ⊔ n) = a m ⊔ a n :=
diff --git a/mathlib4/Mathlib/Probability/Distributions/Gaussian/CharFun.lean b/mathlib4/Mathlib/Probability/Distributions/Gaussian/CharFun.lean
index 82d54b8d6..42f9b7b88 100644
--- a/mathlib4/Mathlib/Probability/Distributions/Gaussian/CharFun.lean
+++ b/mathlib4/Mathlib/Probability/Distributions/Gaussian/CharFun.lean
@@ -141,6 +141,7 @@ lemma IsGaussian.charFun_eq' [IsGaussian μ] (t : E) :
   · exact IsGaussian.integrable_id
   · exact IsGaussian.memLp_two_id
 
+-- See comment on `ProbabilityTheory.covarianceBilin`.
 set_option backward.isDefEq.respectTransparency.types false in
 /-- The measure `μ` is Gaussian if and only if there
 exist `m : E` and `f : E →L[ℝ]  E →L[ℝ] ℝ`
@@ -163,6 +164,7 @@ lemma isGaussian_iff_gaussian_charFun [IsFiniteMeasure μ] :
   · simp [charFun_eq_charFunDual_toDualMap, h, -InnerProductSpace.toContinuousLinearMap_toDualMap]
   · simp [← charFun_toDual_symm_eq_charFunDual, h]
 
+-- See comment on `ProbabilityTheory.covarianceBilin`.
 set_option backward.isDefEq.respectTransparency.types false in
 /-- If the characteristic function of `μ` takes the form of a gaussian characteristic function,
 then the parameters have to be the expectation and the covariance bilinear form. -/
diff --git a/mathlib4/Mathlib/Probability/Moments/CovarianceBilin.lean b/mathlib4/Mathlib/Probability/Moments/CovarianceBilin.lean
index a3271bda1..02a4ae2c9 100644
--- a/mathlib4/Mathlib/Probability/Moments/CovarianceBilin.lean
+++ b/mathlib4/Mathlib/Probability/Moments/CovarianceBilin.lean
@@ -45,6 +45,11 @@ namespace ProbabilityTheory
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
   [MeasurableSpace E] [BorelSpace E] {μ : Measure E}
 
+-- This requires `RingHomCompTriple (starRingEnd ℝ) (RingHom.id ℝ) (RingHom.id ℝ)`, but the instance
+-- `RingHomCompTriple.right_ids` forces it to be
+-- `RingHomCompTriple (starRingEnd ℝ) (RingHom.id ℝ) (starRingEnd ℝ)`, but the third parameter is
+-- an `outParam` so we can't just add the missing instance for `TrivialStar R`.
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Covariance of a measure on an inner product space, as a continuous bilinear form. -/
 noncomputable
 def covarianceBilin (μ : Measure E) : E →L[ℝ] E →L[ℝ] ℝ :=
@@ -184,6 +189,8 @@ section covarianceOperator
 
 variable [CompleteSpace E]
 
+-- See comment on `ProbabilityTheory.covarianceBilin`.
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- The covariance operator of the measure `μ`. This is the bounded operator `F : E →L[ℝ] E`
 associated to the continuous bilinear form `B : E →L[ℝ] E →L[ℝ] ℝ` such that
 `B x y = ∫ z, ⟪x, z⟫ * ⟪y, z⟫ ∂μ` (see `covarianceOperator_inner`). Namely we have
diff --git a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean
index c82388589..9c06581a3 100644
--- a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean
+++ b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean
@@ -559,6 +559,7 @@ def cocyclesOfIsCocycle₁ {f : G → A} (hf : IsCocycle₁ f) :
     cocycles₁ (Rep.ofDistribMulAction k G A) :=
   ⟨f, (mem_cocycles₁_iff (A := Rep.ofDistribMulAction k G A) f).2 hf⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem isCocycle₁_of_mem_cocycles₁
     (f : G → A) (hf : f ∈ cocycles₁ (Rep.ofDistribMulAction k G A)) :
     IsCocycle₁ f :=
@@ -572,6 +573,7 @@ def coboundariesOfIsCoboundary₁ {f : G → A} (hf : IsCoboundary₁ f) :
     coboundaries₁ (Rep.ofDistribMulAction k G A) :=
   ⟨f, hf.choose, funext hf.choose_spec⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem isCoboundary₁_of_mem_coboundaries₁
     (f : G → A) (hf : f ∈ coboundaries₁ (Rep.ofDistribMulAction k G A)) :
     IsCoboundary₁ f := by
@@ -586,6 +588,7 @@ def cocyclesOfIsCocycle₂ {f : G × G → A} (hf : IsCocycle₂ f) :
     cocycles₂ (Rep.ofDistribMulAction k G A) :=
   ⟨f, (mem_cocycles₂_iff (A := Rep.ofDistribMulAction k G A) f).2 hf⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem isCocycle₂_of_mem_cocycles₂
     (f : G × G → A) (hf : f ∈ cocycles₂ (Rep.ofDistribMulAction k G A)) :
     IsCocycle₂ f := (mem_cocycles₂_iff (A := Rep.ofDistribMulAction k G A) f).1 hf
@@ -598,6 +601,7 @@ def coboundariesOfIsCoboundary₂ {f : G × G → A} (hf : IsCoboundary₂ f) :
     coboundaries₂ (Rep.ofDistribMulAction k G A) :=
   ⟨f, hf.choose,funext fun g ↦ hf.choose_spec g.1 g.2⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem isCoboundary₂_of_mem_coboundaries₂
     (f : G × G → A) (hf : f ∈ coboundaries₂ (Rep.ofDistribMulAction k G A)) :
     IsCoboundary₂ f := by
@@ -691,6 +695,7 @@ def cocyclesOfIsMulCocycle₁ {f : G → M} (hf : IsMulCocycle₁ f) :
     cocycles₁ (Rep.ofMulDistribMulAction G M) :=
   ⟨Additive.ofMul ∘ f, (mem_cocycles₁_iff (A := Rep.ofMulDistribMulAction G M) f).2 hf⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem isMulCocycle₁_of_mem_cocycles₁
     (f : G → M) (hf : f ∈ cocycles₁ (Rep.ofMulDistribMulAction G M)) :
     IsMulCocycle₁ (Additive.toMul ∘ f) :=
@@ -704,6 +709,7 @@ def coboundariesOfIsMulCoboundary₁ {f : G → M} (hf : IsMulCoboundary₁ f) :
     coboundaries₁ (Rep.ofMulDistribMulAction G M) :=
   ⟨Additive.ofMul ∘ f, hf.choose, funext hf.choose_spec⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem isMulCoboundary₁_of_mem_coboundaries₁
     (f : G → M) (hf : f ∈ coboundaries₁ (Rep.ofMulDistribMulAction G M)) :
     IsMulCoboundary₁ (M := M) (Additive.ofMul ∘ f) := by
@@ -718,6 +724,7 @@ def cocyclesOfIsMulCocycle₂ {f : G × G → M} (hf : IsMulCocycle₂ f) :
     cocycles₂ (Rep.ofMulDistribMulAction G M) :=
   ⟨Additive.ofMul ∘ f, (mem_cocycles₂_iff (A := Rep.ofMulDistribMulAction G M) f).2 hf⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem isMulCocycle₂_of_mem_cocycles₂
     (f : G × G → M) (hf : f ∈ cocycles₂ (Rep.ofMulDistribMulAction G M)) :
     IsMulCocycle₂ (Additive.toMul ∘ f) :=
@@ -730,6 +737,7 @@ def coboundariesOfIsMulCoboundary₂ {f : G × G → M} (hf : IsMulCoboundary₂
     coboundaries₂ (Rep.ofMulDistribMulAction G M) :=
   ⟨Additive.ofMul ∘ f, hf.choose, funext fun g ↦ hf.choose_spec g.1 g.2⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem isMulCoboundary₂_of_mem_coboundaries₂
     (f : G × G → M) (hf : f ∈ coboundaries₂ (Rep.ofMulDistribMulAction G M)) :
     IsMulCoboundary₂ (M := M) (Additive.toMul ∘ f) := by
diff --git a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean
index 8041e0c71..5c2b8af84 100644
--- a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean
+++ b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean
@@ -114,7 +114,6 @@ theorem range_d₁₀_eq_coinvariantsKer :
       simpa [← hy, add_sub_add_comm, sum_add_index, d₁₀_single (G := G)]
         using! Submodule.add_mem _ (Coinvariants.mem_ker_of_eq _ _ _ rfl) (h rfl)
 
-set_option backward.isDefEq.respectTransparency false in
 set_option backward.defeqAttrib.useBackward true in
 @[reassoc (attr := simp), elementwise (attr := simp)]
 lemma d₁₀_comp_coinvariantsMk : d₁₀ A ≫ (coinvariantsMk k G).app A = 0 := by
@@ -636,6 +635,7 @@ def cyclesOfIsCycle₁ (x : G →₀ A) (hx : IsCycle₁ x) :
     cycles₁ (Rep.ofDistribMulAction k G A) :=
   ⟨x, (mem_cycles₁_iff (A := Rep.ofDistribMulAction k G A) x).2 hx⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem isCycle₁_of_mem_cycles₁
     (x : G →₀ A) (hx : x ∈ cycles₁ (Rep.ofDistribMulAction k G A)) :
     IsCycle₁ x := by
@@ -649,6 +649,7 @@ def boundariesOfIsBoundary₁ (x : G →₀ A) (hx : IsBoundary₁ x) :
     boundaries₁ (Rep.ofDistribMulAction k G A) :=
   ⟨x, hx⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem isBoundary₁_of_mem_boundaries₁
     (x : G →₀ A) (hx : x ∈ boundaries₁ (Rep.ofDistribMulAction k G A)) :
     IsBoundary₁ x := hx
@@ -661,6 +662,7 @@ def cyclesOfIsCycle₂ (x : G × G →₀ A) (hx : IsCycle₂ x) :
     cycles₂ (Rep.ofDistribMulAction k G A) :=
   ⟨x, (mem_cycles₂_iff (A := Rep.ofDistribMulAction k G A) x).2 hx⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem isCycle₂_of_mem_cycles₂
     (x : G × G →₀ A) (hx : x ∈ cycles₂ (Rep.ofDistribMulAction k G A)) :
     IsCycle₂ x := (mem_cycles₂_iff (A := Rep.ofDistribMulAction k G A) x).1 hx
@@ -673,6 +675,7 @@ def boundariesOfIsBoundary₂ (x : G × G →₀ A) (hx : IsBoundary₂ x) :
     boundaries₂ (Rep.ofDistribMulAction k G A) :=
   ⟨x, hx⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem isBoundary₂_of_mem_boundaries₂
     (x : G × G →₀ A) (hx : x ∈ boundaries₂ (Rep.ofDistribMulAction k G A)) :
     IsBoundary₂ x := hx
diff --git a/mathlib4/Mathlib/RepresentationTheory/Induced.lean b/mathlib4/Mathlib/RepresentationTheory/Induced.lean
index 2677fd901..7b892ac5a 100644
--- a/mathlib4/Mathlib/RepresentationTheory/Induced.lean
+++ b/mathlib4/Mathlib/RepresentationTheory/Induced.lean
@@ -179,7 +179,6 @@ variable {G H : Type u} [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : R
 open Representation
 
 set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 /-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear map
 `(Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G` sending `⟦h ⊗ₜ a⟧ ⊗ₜ b` to `⟦a ⊗ ρ(h)(b)⟧` for all
 `h : H`, `a : A`, and `b : B`. -/
@@ -198,7 +197,6 @@ noncomputable def coinvariantsTensorIndHom :
     ext; simp
 
 set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 variable {A B} in
 lemma coinvariantsTensorIndHom_mk_tmul_indVMk (h : H) (x : A) (y : B) :
     coinvariantsTensorIndHom φ A B (coinvariantsTensorMk _ _ (IndV.mk φ _ h x) y) =
@@ -206,7 +204,6 @@ lemma coinvariantsTensorIndHom_mk_tmul_indVMk (h : H) (x : A) (y : B) :
   simp [coinvariantsTensorIndHom, coinvariantsTensorMk]
 
 set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 /-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear map
 `(A ⊗ Res(φ)(B))_G ⟶ (Ind(φ)(A) ⊗ B))_H` sending `⟦a ⊗ₜ b⟧` to `⟦1 ⊗ₜ a⟧ ⊗ₜ b` for all
 `a : A`, and `b : B`. -/
@@ -223,7 +220,6 @@ noncomputable def coinvariantsTensorIndInv :
       simp [← Coinvariants.mk_inv_tmul]
 
 set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 variable {A B} in
 lemma coinvariantsTensorIndInv_mk_tmul_indMk (x : A) (y : B) :
     coinvariantsTensorIndInv φ A B (Coinvariants.mk
@@ -232,7 +228,6 @@ lemma coinvariantsTensorIndInv_mk_tmul_indMk (x : A) (y : B) :
   simp [coinvariantsTensorIndInv, coinvariantsTensorMk]
 
 set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 /-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear
 isomorphism `(Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G` sending `⟦h ⊗ₜ a⟧ ⊗ₜ b` to `⟦a ⊗ ρ(h)(b)⟧`
 for all `h : H`, `a : A`, and `b : B`. -/
@@ -252,7 +247,6 @@ noncomputable def coinvariantsTensorIndIso :
     simp [coinvariantsTensorIndInv, coinvariantsTensorMk, coinvariantsTensorIndHom]
 
 set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 /-- Given a group hom `φ : G →* H` and `A : Rep k G`, the functor `Rep k H ⥤ ModuleCat k` sending
 `B ↦ (Ind(φ)(A) ⊗ B))_H` is naturally isomorphic to the one sending `B ↦ (A ⊗ Res(φ)(B))_G`. -/
 @[simps! hom_app inv_app]
diff --git a/mathlib4/Mathlib/RepresentationTheory/Intertwining.lean b/mathlib4/Mathlib/RepresentationTheory/Intertwining.lean
index 428ad6f57..59254b7f5 100644
--- a/mathlib4/Mathlib/RepresentationTheory/Intertwining.lean
+++ b/mathlib4/Mathlib/RepresentationTheory/Intertwining.lean
@@ -486,6 +486,35 @@ instance : Module A (IntertwiningMap ρ σ) :=
   fast_instance%
   Function.Injective.module A (coeFnAddMonoidHom ρ σ) DFunLike.coe_injective (coe_smul ρ σ)
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`LinearMap.CompatibleSMul ρ.asModule σ.asModule A A[G]`
+It is needed by `LinearMap.map_smul_of_tower`, with which the `simp` in `invFun`'s `map_smul'`
+below has to rewrite the goal `f (a • v) = a • f v`.
+
+The failure happens while applying `@LinearMap.IsScalarTower.compatibleSMul`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type
+is `SMul A ρ.asModule`, whereas the assigned value `DistribMulAction.toDistribSMul.toSMul` has type
+`SMul A V`. The comparison bottoms out at `ρ.asModule =?= V`, where `asModule` is a plain
+semireducible `def` and therefore does not unfold at the `.instances` transparency that instance
+search runs at. Lean falls back to synthesize an instance of the correct type, which succeeds, but
+the candidate is again not defeq to the assigned value, stalling at
+`inst✝.toSemigroupAction.1 =?= instModuleAsModule._aux_1 ρ`. That comparison, too, runs at
+`.instances`, since `respectTransparency false` suppresses the transparency bump that
+instance-implicit arguments would otherwise receive.
+
+With no `CompatibleSMul` instance found, the rewrite does not fire and `simp` makes no progress.
+
+Potential fix: mark `asModule` implicit-reducible *at its definition site*. Then
+`respectTransparency false` becomes obsolete, and once it is removed, `instanceTypes false` can go
+as well: `asModule` being implicit-reducible, the `instModuleAsModule._aux_1` constant becomes
+implicit-reducible as well. The reason for this is that `instModuleAsModule`'s definition uses
+`inferInstanceAs`, which wraps the instance's fields into wrappers to encapsulate defeq abuse.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.isDefEq.respectTransparency false in
 /-- An intertwining map is the same thing as a linear map over the group ring. -/
 def equivLinearMapAsModule :
diff --git a/mathlib4/Mathlib/RepresentationTheory/Subrepresentation.lean b/mathlib4/Mathlib/RepresentationTheory/Subrepresentation.lean
index e855a1e86..2ef50abca 100644
--- a/mathlib4/Mathlib/RepresentationTheory/Subrepresentation.lean
+++ b/mathlib4/Mathlib/RepresentationTheory/Subrepresentation.lean
@@ -113,8 +113,11 @@ def asSubmodule (σ : Subrepresentation ρ) : Submodule A[G] ρ.asModule where
       rw [Representation.single_smul]
       exact σ.toSubmodule.smul_mem' a (σ.apply_mem_toSubmodule g hv)
 
+-- Type-correct statement would be `(Representation.asModuleEquiv ρ).symm v ∈ asSubmodule σ`.
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
-lemma mem_asSubmodule_iff {σ : Subrepresentation ρ} {v : W} : v ∈ asSubmodule σ ↔ v ∈ σ := by rfl
+lemma mem_asSubmodule_iff {σ : Subrepresentation ρ} {v : W} :
+    v ∈ asSubmodule σ ↔ v ∈ σ := by rfl
 
 /-- A subrepresentation of `ofModule M` can be thought of as an `A[G]` submodule of `M`.
 -/
@@ -130,6 +133,9 @@ def asSubmodule' (σ : Subrepresentation (Representation.ofModule (k := A) (G :=
       exact σ.toSubmodule.smul_mem' ((algebraMap A A) a) <| by
         simpa [Representation.ofModule, RestrictScalars.lsmul] using! σ.apply_mem_toSubmodule g hm
 
+-- Type-correct statement would be
+-- `m ∈ asSubmodule' σ ↔ Representation.asModuleEquiv (Representation.ofModule M) m ∈ σ`.
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 lemma mem_asSubmodule'_iff {σ : Subrepresentation (Representation.ofModule (k := A) (G := G) M)}
     {m : M} : m ∈ asSubmodule' σ ↔ m ∈ σ := by rfl
@@ -144,6 +150,9 @@ def ofSubmodule (N : Submodule A[G] M) :
     simpa [Representation.ofModule, RestrictScalars.lsmul] using!
       Submodule.smul_of_tower_mem N (MonoidAlgebra.single g 1) hv
 
+-- Type-correct statement would be
+-- `Representation.asModuleEquiv (Representation.ofModule M) m ∈ ofSubmodule N ↔ m ∈ N`.
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 lemma mem_ofSubmodule_iff {N : Submodule A[G] M} {m : M} : m ∈ ofSubmodule N ↔ m ∈ N := by rfl
 
@@ -160,6 +169,7 @@ def ofSubmodule' (N : Submodule A[G] ρ.asModule) : Subrepresentation ρ where
     rw [Representation.single_smul, one_smul] at h
     exact h
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 lemma mem_ofSubmodule'_iff {N : Submodule A[G] ρ.asModule} {w : W} : w ∈ ofSubmodule' N ↔ w ∈ N :=
   .rfl
diff --git a/mathlib4/Mathlib/RingTheory/Extension/Cotangent/Basis.lean b/mathlib4/Mathlib/RingTheory/Extension/Cotangent/Basis.lean
index 43b653c5d..e39bf3448 100644
--- a/mathlib4/Mathlib/RingTheory/Extension/Cotangent/Basis.lean
+++ b/mathlib4/Mathlib/RingTheory/Extension/Cotangent/Basis.lean
@@ -54,6 +54,7 @@ namespace Aux
 variable {P} {b}
 variable (D : Aux P b)
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- `T = R[X₁, ..., Xₙ] / (b₁, ..., bᵣ)` where the `bᵢ` are lifts of the basis elements
 of `I/I²` in `I`. -/
 abbrev T :=
@@ -236,7 +237,33 @@ set_option backward.isDefEq.respectTransparency false in
 def basisRight : Module.Basis Unit S D.presRight.toExtension.Cotangent :=
   Generators.basisCotangentAway S D.gbar
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`AddCommMonoid D.presRight.toExtension.Cotangent`
+It is needed by the `Module.Basis.prod` below.
+
+The search reduces via `@AddCommGroup.toAddCommMonoid` to
+`AddCommGroup D.presRight.toExtension.Cotangent`, and the failure happens while applying
+`@Extension.instAddCommGroupCotangent`: assigning one of its instance-implicit-argument
+metavariables is rejected because the metavariable's type and the type of the assigned value do not
+match at `.instances` transparency. The metavariable's expected type is `CommRing D.T`, whereas the
+assigned value `Ideal.Quotient.commRing (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))` has type
+`CommRing (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))`. `T` is an `abbrev`,
+so it unfolds and both sides become that same quotient; but the two ideals are taken over different
+rings, `P.toExtension.Ring` on one side and `MvPolynomial ι R` on the other. Comparing those bumps
+the transparency to `.implicit` and bottoms out at
+`P.toExtension.1 =?= AddMonoidAlgebra R (ι →₀ ℕ)`, where `Algebra.Generators.toExtension` is a plain
+semireducible `def` and therefore does not unfold. Lean falls back to synthesize an instance of the
+correct type, which succeeds, but it returns the same `Ideal.Quotient.commRing` term with the ideal
+over `P.toExtension.Ring`, which is again not defeq to the assigned value, for the same reason.
+
+Potential fix: make `Algebra.Generators.toExtension` implicit-reducible.
+Then both backward compatibility options can go.
+-/
 set_option backward.isDefEq.respectTransparency.types false in
+set_option backward.isDefEq.instanceTypes false in
 /-- The basis on the cotangent space of the constructed presentation. -/
 def basis [Nontrivial S] : Module.Basis (Unit ⊕ σ) S D.pres.toExtension.Cotangent :=
   (Module.Basis.prod D.basisRight D.basisLeft).map D.cotangentEquivProd.symm
@@ -247,7 +274,28 @@ lemma basis_inl [Nontrivial S] :
       D.cotangentEquivProd.symm (Generators.cMulXSubOneCotangent S D.gbar, 0) := by
   simpa [basis] using! Generators.basisCotangentAway_apply _ _
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following two instances cannot be synthesized:
+`OfNat D.presRight.toExtension.Cotangent 0`
+`AddCommMonoid (D.presRight.toExtension.Cotangent × S ⊗[D.T] D.presLeft.toExtension.Cotangent)`
+Both are needed by the pair `(0, D.basisLeft i)` below.
+
+Both searches reduce to `AddCommGroup D.presRight.toExtension.Cotangent` and then fail exactly as
+in `basis` above: applying `@Extension.instAddCommGroupCotangent`, the assignment to the
+instance-implicit-argument metavariable of type `CommRing D.T` is rejected, the assigned value
+`Ideal.Quotient.commRing (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))` having type
+`CommRing (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))`, with the two ideals
+taken over different rings; the comparison bottoms out at
+`P.toExtension.1 =?= AddMonoidAlgebra R (ι →₀ ℕ)`, and the fallback synthesis returns a term that is
+again not defeq to the assigned value.
+
+Potential fix: make `Algebra.Generators.toExtension` implicit-reducible.
+Then both backward compatibility options can go.
+-/
 set_option backward.isDefEq.respectTransparency.types false in
+set_option backward.isDefEq.instanceTypes false in
 lemma basis_inr [Nontrivial S] (i : σ) :
     D.basis (.inr i) = D.cotangentEquivProd.symm (0, D.basisLeft i) := by
   simp [basis]
@@ -273,6 +321,29 @@ end PresentationOfFreeCotangent.Aux
 
 end
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`LE (Submodule P.Ring P.toExtension.Cotangent)`
+It is needed by the `refine le_trans le_top (top_le_iff.mpr ?_)` below, as are the `Preorder`,
+`PartialOrder` and `OrderTop` instances on the same type, which fail in the same way.
+
+The failure happens while applying `@Submodule.completeLattice`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type
+is `Semiring P.Ring`, whereas the assigned value `CommRing.toCommSemiring.toSemiring` has type
+`Semiring P.toExtension.Ring`. The comparison bottoms out at
+`AddMonoidAlgebra R (α →₀ ℕ) =?= P.toExtension.1`, where `Algebra.Generators.toExtension` is a plain
+semireducible `def` and therefore does not unfold at the `.instances` transparency that instance
+search runs at. Lean falls back to synthesize an instance of the correct type, which succeeds, but
+it returns `AddMonoidAlgebra.semiring`, which is again not defeq to the assigned value; that second
+comparison also runs at `.instances`, `respectTransparency false` suppressing the transparency bump.
+
+Potential fix: make `Algebra.Generators.toExtension` implicit-reducible.
+Then `respectTransparency false` and `instanceTypes false` can both go.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 open PresentationOfFreeCotangent in
@@ -329,6 +400,7 @@ public lemma exists_presentation_of_basis_cotangent [Algebra.FinitePresentation
   exact hf _
 
 open PresentationOfFreeCotangent in
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Let `S` be a finitely presented `R`-algebra and suppose `P : R[X] → S` generates `S` with
 kernel `I`. If `I/I²` is free, there exists an `R`-presentation `P'` of `S` extending `P` with
 kernel `I'`, such that `I'/I'²` is free on the images of the relations of `P'`.
diff --git a/mathlib4/Mathlib/RingTheory/FractionalIdeal/Operations.lean b/mathlib4/Mathlib/RingTheory/FractionalIdeal/Operations.lean
index 077d7fa2c..9b639fe65 100644
--- a/mathlib4/Mathlib/RingTheory/FractionalIdeal/Operations.lean
+++ b/mathlib4/Mathlib/RingTheory/FractionalIdeal/Operations.lean
@@ -924,6 +924,9 @@ variable {R S : Type*} (K L : Type*) [CommRing R] [IsDomain R] [CommRing S] [IsD
 local instance (f : R ≃+* S) : RingHomInvPair (f : R →+* S) f.symm :=
   RingHomInvPair.of_ringEquiv f
 
+local instance (f : R ≃+* S) : RingHomInvPair (f.symm : S →+* R) f :=
+  RingHomInvPair.of_ringEquiv f.symm
+
 /-- If `f : R ≃+* S` is a ring isomorphism and `I : Submodule R K` is fractional with respect to
 `R⁰`, then `I.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap`
 is fractional with respect to `S⁰`.
diff --git a/mathlib4/Mathlib/RingTheory/Ideal/Nonunits.lean b/mathlib4/Mathlib/RingTheory/Ideal/Nonunits.lean
index 0c2acbd02..e574b6d62 100644
--- a/mathlib4/Mathlib/RingTheory/Ideal/Nonunits.lean
+++ b/mathlib4/Mathlib/RingTheory/Ideal/Nonunits.lean
@@ -93,7 +93,7 @@ section GroupWithZero
 variable [GroupWithZero α] [SubmonoidClass C α] {S : C} {a : S}
 
 theorem isUnit_iff_and : IsUnit a ↔ (a : α) ≠ 0 ∧ (a : α)⁻¹ ∈ S where
-  mp h := ⟨(h.map <| subtype <| ofClass S).ne_zero, inv_mem_of_isUnit h⟩
+  mp h := ⟨(h.map <| SubmonoidClass.subtype S).ne_zero, inv_mem_of_isUnit h⟩
   mpr h :=
     ⟨⟨a, ⟨_, h.2⟩, Subtype.ext (mul_inv_cancel₀ h.1), Subtype.ext (inv_mul_cancel₀ h.1)⟩, rfl⟩
 
diff --git a/mathlib4/Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean b/mathlib4/Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
index 8c6ce13b3..3b1983bbe 100644
--- a/mathlib4/Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
+++ b/mathlib4/Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
@@ -272,6 +272,7 @@ theorem span_singleton_absNorm {I : Ideal S} (hI : (Ideal.absNorm I).Prime) :
 
 variable [Module.Finite ℤ S]
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Let `e : S ≃ I` be an additive isomorphism (therefore a `ℤ`-linear equiv).
 Then an alternative way to compute the norm of `I` is given by taking the determinant of `e`.
 See `natAbs_det_basis_change` for a more familiar formulation of this result. -/
diff --git a/mathlib4/Mathlib/RingTheory/IdealFilter/Topology.lean b/mathlib4/Mathlib/RingTheory/IdealFilter/Topology.lean
index 260632839..770337cb0 100644
--- a/mathlib4/Mathlib/RingTheory/IdealFilter/Topology.lean
+++ b/mathlib4/Mathlib/RingTheory/IdealFilter/Topology.lean
@@ -124,6 +124,9 @@ lemma mem_nhds_zero_iff {s : Set (WithIdealFilter F)} :
     s ∈ 𝓝 0 ↔ ∃ I ∈ F, idealSet I ⊆ s := by
   simpa [zero_vadd] using mem_nhds_iff (a := 0) (s := s)
 
+-- Defeq abuse: uses `AddSubmonoidClass (Submodule A A) A` as
+-- `AddSubmonoidClass (Submodule A A) (WithIdealFilter F)`.
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- The topology is linear in the sense that `𝓝 0` has a basis of ideals. -/
 instance instIsLinearTopology : IsLinearTopology (WithIdealFilter F) (WithIdealFilter F) :=
   IsLinearTopology.mk_of_hasBasis' (R := (WithIdealFilter F))
diff --git a/mathlib4/Mathlib/RingTheory/Kaehler/Basic.lean b/mathlib4/Mathlib/RingTheory/Kaehler/Basic.lean
index 828517e10..bb0f69e93 100644
--- a/mathlib4/Mathlib/RingTheory/Kaehler/Basic.lean
+++ b/mathlib4/Mathlib/RingTheory/Kaehler/Basic.lean
@@ -192,6 +192,37 @@ theorem KaehlerDifferential.DLinearMap_apply (s : S) :
       (KaehlerDifferential.ideal R S).toCotangent
         ⟨1 ⊗ₜ s - s ⊗ₜ 1, KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R s⟩ := rfl
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`LinearMap.CompatibleSMul (↥(ideal R S)) (ideal R S).Cotangent S (S ⊗[R] S)`
+It is needed by the two `← LinearMap.map_smul_of_tower (ideal R S).toCotangent` rewrites in
+`leibniz'` below. The `have` just above them does not rescue the search: it is stated for `Ω[S⁄R]`,
+and `(ideal R S).Cotangent =?= Ω[S⁄R]` already fails at `.instances`.
+
+The failure happens while applying `@LinearMap.IsScalarTower.compatibleSMul`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type
+is `SMul S (ideal R S).Cotangent`, whereas the assigned value
+`DistribMulAction.toDistribSMul.toSMul` has type `SMul S Ω[S⁄R]`. The comparison bottoms out at
+`@Ideal.Cotangent =?= KaehlerDifferential`,
+where `KaehlerDifferential` is a plain semireducible `def` and therefore does not unfold at the
+`.instances` transparency that instance search runs at. Lean falls back to synthesize an instance of
+the correct type, which succeeds, but it returns `(ideal R S).instSMulCotangentOfAlgebra`, which
+is not defeq to the assigned value, the comparison bottoming out at
+`instSMulKaehlerDifferentialOfSMulCommClass._aux_1 =?= @Ideal.instSMulCotangentOfAlgebra._aux_1`.
+That second comparison also runs at `.instances`, `respectTransparency false` suppressing the
+transparency bump.
+
+Potential fix: mark `KaehlerDifferential` `@[implicit_reducible]` at its definition site.
+Then `instanceTypes false` and `respectTransparency false` can go, but only together: with
+`respectTransparency false` still in place, the comparison stays at `.instances`, where an
+implicit-reducible definition does not unfold, and the search fails as before.
+The `_aux_1` wrappers for the instance fields become implicit-reducible as soon as
+`KaehlerDifferential` is.
+-/
+set_option backward.isDefEq.instanceTypes false in
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- The universal derivation into `Ω[S⁄R]`. -/
@@ -734,7 +765,7 @@ lemma KaehlerDifferential.range_mapBaseChange :
     | zero => simp
     | tmul r s =>
       obtain ⟨x, rfl⟩ := linearCombination_surjective _ _ s
-      simp only [mapBaseChange_tmul, LinearMap.mem_ker, map_smul]
+      simp only [mapBaseChange_tmul, LinearMap.mem_ker]
       induction x using Finsupp.induction_linear
       · simp
       · simp [smul_add, *]
diff --git a/mathlib4/Mathlib/RingTheory/Kaehler/TensorProduct.lean b/mathlib4/Mathlib/RingTheory/Kaehler/TensorProduct.lean
index 82545a22e..9c88bcbb0 100644
--- a/mathlib4/Mathlib/RingTheory/Kaehler/TensorProduct.lean
+++ b/mathlib4/Mathlib/RingTheory/Kaehler/TensorProduct.lean
@@ -176,7 +176,7 @@ lemma tensorKaehlerEquiv_left_inv [Algebra.IsPushout R S A B] :
   induction y
   · simp only [map_zero, TensorProduct.tmul_zero]
   · simp only [LinearMap.restrictScalars_comp, Derivation.tensorProductTo_tmul, LinearMap.coe_comp,
-      LinearMap.coe_restrictScalars, Function.comp_apply, LinearMap.liftBaseChange_tmul, map_smul,
+      LinearMap.coe_restrictScalars, Function.comp_apply, LinearMap.liftBaseChange_tmul,
       map_D, LinearMap.map_smul_of_tower, Derivation.liftKaehlerDifferential_comp_D,
       LinearMap.id_coe, id_eq, derivationTensorProduct_algebraMap]
     rw [smul_comm, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
diff --git a/mathlib4/Mathlib/RingTheory/LocalProperties/Injective.lean b/mathlib4/Mathlib/RingTheory/LocalProperties/Injective.lean
index 209bc9413..84dc38f0c 100644
--- a/mathlib4/Mathlib/RingTheory/LocalProperties/Injective.lean
+++ b/mathlib4/Mathlib/RingTheory/LocalProperties/Injective.lean
@@ -112,6 +112,7 @@ variable
   [inst : ∀ (P : Ideal R) [P.IsMaximal], IsLocalizedModule P.primeCompl (f P)]
 
 set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency.instances false in
 attribute [local instance] RingHomInvPair.of_ringEquiv in
 include f in
 /--
diff --git a/mathlib4/Mathlib/RingTheory/LocalProperties/IntegrallyClosed.lean b/mathlib4/Mathlib/RingTheory/LocalProperties/IntegrallyClosed.lean
index fa70ddb50..b3d1c3fed 100644
--- a/mathlib4/Mathlib/RingTheory/LocalProperties/IntegrallyClosed.lean
+++ b/mathlib4/Mathlib/RingTheory/LocalProperties/IntegrallyClosed.lean
@@ -28,6 +28,7 @@ open Localization Ideal IsLocalization
 
 variable {R K : Type*} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K]
 
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem IsIntegrallyClosed.iInf {ι : Type*} (S : ι → Subalgebra R K)
     (h : ∀ i, IsIntegrallyClosed (S i)) :
     IsIntegrallyClosed (⨅ i, S i : Subalgebra R K) := by
diff --git a/mathlib4/Mathlib/RingTheory/Localization/FractionRing.lean b/mathlib4/Mathlib/RingTheory/Localization/FractionRing.lean
index 5b194d646..b191c1ad7 100644
--- a/mathlib4/Mathlib/RingTheory/Localization/FractionRing.lean
+++ b/mathlib4/Mathlib/RingTheory/Localization/FractionRing.lean
@@ -486,6 +486,9 @@ variable {A B : Type*} (K L : Type*) [CommRing A] [CommRing B] [CommRing K] [Com
 local instance : RingHomInvPair (f : A →+* B) f.symm :=
   RingHomInvPair.of_ringEquiv f
 
+local instance : RingHomInvPair (f.symm : B →+* A) f :=
+  RingHomInvPair.of_ringEquiv f.symm
+
 /-- Given rings `A, B` and localization maps to their fraction rings
 `f : A →+* K, g : B →+* L`, an isomorphism `h : A ≃+* B` induces a semilinear equivalence
 fraction rings `K ≃ₛₗ[f.toRingHom] L`. -/
diff --git a/mathlib4/Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean b/mathlib4/Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean
index b7e440521..87cbda33d 100644
--- a/mathlib4/Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean
+++ b/mathlib4/Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean
@@ -187,7 +187,6 @@ def universalFactorizationMapLiftEquiv (p : MonicDegreeEq S n) :
   left_inv f := by ext <;> simp
   right_inv q := by ext <;> simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 lemma ker_eval₂Hom_universalFactorizationMap :
     RingHom.ker (eval₂Hom (S₁ := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
       (universalFactorizationMap R n m k hn) (Sum.elim (.X · ⊗ₜ 1) (1 ⊗ₜ .X ·))) =
@@ -514,7 +513,6 @@ def UniversalFactorizationRing.presentation :
   letI := ((MvPolynomial.mapEquivMonic R _ n).symm p).toAlgebra
   (MvPolynomial.universalFactorizationMapPresentation R n m k hn).baseChange _
 
-set_option backward.isDefEq.respectTransparency.types false in
 lemma UniversalFactorizationRing.jacobian_resentation :
     (presentation m k hn p).jacobian =
       (-1) ^ n * (factor₁ m k hn p).1.resultant (factor₂ m k hn p).1 := by
diff --git a/mathlib4/Mathlib/RingTheory/Regular/RegularSequence.lean b/mathlib4/Mathlib/RingTheory/Regular/RegularSequence.lean
index 9b58c8f23..61f3150db 100644
--- a/mathlib4/Mathlib/RingTheory/Regular/RegularSequence.lean
+++ b/mathlib4/Mathlib/RingTheory/Regular/RegularSequence.lean
@@ -571,7 +571,38 @@ lemma map_first_exact_on_four_term_right_exact_of_isSMulRegular_last
 
 section Perm
 
+#adaptation_note
+/--
+We had to use the `instanceTypes` backward compatibility flag to make an instance search succeed.
+Concretely, the following instance cannot be synthesized:
+`FunLike (M ⧸ torsionBy R M b →ₗ[R] M) (M ⧸ torsionBy R M b) M`
+It is needed by the `ha.of_injective _ <| ker_eq_bot.mp <| ker_liftQ_eq_bot' _ (lsmul R M b) rfl`
+below.
+
+The failure happens while applying `@LinearMap.instFunLike`: assigning one of its
+instance-implicit-argument metavariables is rejected because the metavariable's type and the type
+of the assigned value do not match at `.instances` transparency. The metavariable's expected type
+is `Module R (M ⧸ torsionBy R M b)`, whereas the assigned value
+`Quotient.module ((lsmul R M) b).ker` has type `Module R (M ⧸ ((lsmul R M) b).ker)`.
+Lean falls back to synthesize an instance of the correct type, which succeeds, but it returns
+`Quotient.module (torsionBy R M b)`, which is again not defeq to the assigned value.
+That second comparison runs at `.implicit`.
+
+Potential fix: make the following definitions implicit-reducible:
+
+```
+torsionBy
+DistribSMul.toLinearMap
+LinearMap.lsmul
+LinearMap.mk₂
+LinearMap.mk₂'
+LinearMap.mk₂'ₛₗ
+```
+
+Then both backward compatibility options can go.
+-/
 set_option backward.isDefEq.respectTransparency.types false in
+set_option backward.isDefEq.instanceTypes false in
 open _root_.LinearMap in
 private lemma IsWeaklyRegular.swap {a b : R} (h1 : IsWeaklyRegular M [a, b])
     (h2 : torsionBy R M b = a • torsionBy R M b → torsionBy R M b = ⊥) :
diff --git a/mathlib4/Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean b/mathlib4/Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
index 35f86bc67..1e13f8b83 100644
--- a/mathlib4/Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
+++ b/mathlib4/Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
@@ -259,6 +259,7 @@ instance : Module.Free S (Generators.localizationAway S r).toExtension.Cotangent
   inferInstanceAs <|
     Module.Free S ((SubmersivePresentation.localizationAway S r).toExtension.Cotangent)
 
+set_option backward.isDefEq.respectTransparency.instances false in
 variable (S) in
 /-- The image of `g * X - 1` in `I/I²` if `I` is the kernel of the canonical presentation
 of the localization of `S` away from `g`. -/
@@ -266,6 +267,7 @@ noncomputable
 abbrev Generators.cMulXSubOneCotangent : (Generators.localizationAway S r).toExtension.Cotangent :=
   Extension.Cotangent.mk ⟨C r * X () - 1, C_mul_X_sub_one_mem_ker _⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma Generators.cMulXSubOneCotangent_eq :
     cMulXSubOneCotangent S r = Extension.Cotangent.mk ⟨C r * X () - 1, C_mul_X_sub_one_mem_ker _⟩ :=
   rfl
diff --git a/mathlib4/Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean b/mathlib4/Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean
index a52be8b7e..01c58fd0d 100644
--- a/mathlib4/Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean
+++ b/mathlib4/Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean
@@ -55,6 +55,7 @@ lemma mem_freeLocus {p} : p ∈ freeLocus R M ↔
     Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M) :=
   Iff.rfl
 
+set_option backward.isDefEq.respectTransparency.instances false in
 attribute [local instance] RingHomInvPair.of_ringEquiv in
 lemma mem_freeLocus_of_isLocalization (p : PrimeSpectrum R)
     (Rₚ Mₚ) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p.asIdeal]
diff --git a/mathlib4/Mathlib/RingTheory/Valuation/LocalSubring.lean b/mathlib4/Mathlib/RingTheory/Valuation/LocalSubring.lean
index de4963030..36f6345db 100644
--- a/mathlib4/Mathlib/RingTheory/Valuation/LocalSubring.lean
+++ b/mathlib4/Mathlib/RingTheory/Valuation/LocalSubring.lean
@@ -143,6 +143,7 @@ lemma LocalSubring.exists_le_valuationSubring (A : LocalSubring K) :
     apply hCA.2.1
     exact isUnit_iff_exists_inv.mpr ⟨⟨b, hCB.1 hbB⟩, Subtype.ext congr(($e).1)⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma Ideal.image_subset_nonunits_valuationSubring {A : Subring K} (I : Ideal A) (hI : I ≠ ⊤) :
     ∃ B : ValuationSubring K, A ≤ B.toSubring ∧ A.subtype '' I ⊆ B.nonunits := by
   have ⟨M, hM, le⟩ := I.exists_le_maximal hI
diff --git a/mathlib4/Mathlib/RingTheory/Valuation/RankOne.lean b/mathlib4/Mathlib/RingTheory/Valuation/RankOne.lean
index 57c6e6cbb..324cb1f1d 100644
--- a/mathlib4/Mathlib/RingTheory/Valuation/RankOne.lean
+++ b/mathlib4/Mathlib/RingTheory/Valuation/RankOne.lean
@@ -139,6 +139,7 @@ instance restrict_RankOne : RankOne (v.restrict) where
   hom' := (RankOne.hom v).comp embedding
   strictMono' := (strictMono v).comp embedding_strictMono
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 lemma restrict_RankOne_hom_eq :
   RankOne.hom v.restrict = (RankOne.hom v).comp embedding := rfl
diff --git a/mathlib4/Mathlib/RingTheory/WittVector/Isocrystal.lean b/mathlib4/Mathlib/RingTheory/WittVector/Isocrystal.lean
index cfe4966b0..3d56a10e8 100644
--- a/mathlib4/Mathlib/RingTheory/WittVector/Isocrystal.lean
+++ b/mathlib4/Mathlib/RingTheory/WittVector/Isocrystal.lean
@@ -90,6 +90,9 @@ scoped[Isocrystal] notation "φ(" p ", " k ")" => WittVector.FractionRing.froben
 instance inv_pair₁ : RingHomInvPair φ(p, k) (FractionRing.frobenius p k).symm :=
   RingHomInvPair.of_ringEquiv (FractionRing.frobenius p k)
 
+instance inv_pair₁_symm : RingHomInvPair (FractionRing.frobenius p k).symm φ(p, k)  :=
+  RingHomInvPair.of_ringEquiv (FractionRing.frobenius p k).symm
+
 instance inv_pair₂ : RingHomInvPair ((FractionRing.frobenius p k).symm : K(p, k) →+* K(p, k))
     (FractionRing.frobenius p k) :=
   RingHomInvPair.of_ringEquiv (FractionRing.frobenius p k).symm
@@ -164,6 +167,7 @@ section PerfectRing
 
 variable [IsDomain k] [CharP k p] [PerfectRing k p]
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- The standard one-dimensional isocrystal of slope `m : ℤ` is an isocrystal. -/
 instance (m : ℤ) : Isocrystal p k (StandardOneDimIsocrystal p k m) where
   frob :=
diff --git a/mathlib4/Mathlib/SetTheory/Ordinal/Basic.lean b/mathlib4/Mathlib/SetTheory/Ordinal/Basic.lean
index 7e71c38a4..d5e236d6c 100644
--- a/mathlib4/Mathlib/SetTheory/Ordinal/Basic.lean
+++ b/mathlib4/Mathlib/SetTheory/Ordinal/Basic.lean
@@ -571,7 +571,7 @@ theorem enum_zero_eq_bot {o : Ordinal} (ho : 0 < o) :
 
 theorem lt_wf : @WellFounded Ordinal (· < ·) :=
   wellFounded_iff_wellFounded_subrel.mpr (·.induction_on fun ⟨_, _, wo⟩ ↦
-    RelHomClass.wellFounded (enum _) wo.wf)
+    (RelHomClass.wellFounded (enum _) wo.wf :))
 
 instance wellFoundedRelation : WellFoundedRelation Ordinal :=
   ⟨(· < ·), lt_wf⟩
diff --git a/mathlib4/Mathlib/SetTheory/ZFC/Class.lean b/mathlib4/Mathlib/SetTheory/ZFC/Class.lean
index 9e12f7040..1183adcaa 100644
--- a/mathlib4/Mathlib/SetTheory/ZFC/Class.lean
+++ b/mathlib4/Mathlib/SetTheory/ZFC/Class.lean
@@ -31,7 +31,7 @@ universe u
 We define `Class` as `Set ZFSet`, as this allows us to get many instances automatically. However, in
 practice, we treat it as (the definitionally equal) `ZFSet → Prop`. This means, the preferred way to
 state that `x : ZFSet` belongs to `A : Class` is to write `A x`. -/
-@[pp_with_univ, use_set_notation_for_order]
+@[instance_reducible, pp_with_univ, use_set_notation_for_order]
 def Class :=
   Set ZFSet deriving LE, EmptyCollection, Nonempty, Union, Inter, Compl, SDiff
 
@@ -371,7 +371,7 @@ noncomputable def coeEquiv : ZFSet.{u} ≃ {s : Set ZFSet.{u} // Small.{u, u+1}
   right_inv s := private Subtype.coe_injective <| coe_equiv_aux s.2
 
 /-- The **Burali-Forti paradox**: ordinals form a proper class. -/
-theorem isOrdinal_notMem_univ : IsOrdinal ∉ Class.univ.{u} := by
+theorem isOrdinal_notMem_univ : { o | IsOrdinal o } ∉ Class.univ.{u} := by
   rintro ⟨x, hx, -⟩
   suffices IsOrdinal x by
     apply Class.mem_irrefl x
diff --git a/mathlib4/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Defs.lean b/mathlib4/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Defs.lean
index c4c06a367..b63b92d37 100644
--- a/mathlib4/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Defs.lean
+++ b/mathlib4/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Defs.lean
@@ -808,6 +808,7 @@ end Sorted
 
 section Approximates
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Coinductive predicate stating that `ms` approximates its attached function on `basis`.
 * If `basis = []`, i.e. `ms` is just a real number, `Approximates` holds unconditionally.
 * If `basis = basis_hd :: basis_tl` and `ms = nil`, then `f =ᶠ[atTop] 0`.
diff --git a/mathlib4/Mathlib/Tactic/NormNum/Basic.lean b/mathlib4/Mathlib/Tactic/NormNum/Basic.lean
index 93a721204..3418d30d3 100644
--- a/mathlib4/Mathlib/Tactic/NormNum/Basic.lean
+++ b/mathlib4/Mathlib/Tactic/NormNum/Basic.lean
@@ -559,10 +559,12 @@ theorem isRat_div {α : Type u} [DivisionRing α] : {a b : α} → {cn : ℤ} 
     IsRat (a * b⁻¹) cn cd → IsRat (a / b) cn cd
   | _, _, _, _, h => by simpa [div_eq_mul_inv] using h
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Helper function to synthesize a typed `DivisionSemiring α` expression. -/
 def inferDivisionSemiring {u : Level} (α : Q(Type u)) : MetaM Q(DivisionSemiring $α) :=
   return ← synthInstanceQ q(DivisionSemiring $α) <|> throwError "not a division semiring"
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Helper function to synthesize a typed `DivisionRing α` expression. -/
 def inferDivisionRing {u : Level} (α : Q(Type u)) : MetaM Q(DivisionRing $α) :=
   return ← synthInstanceQ q(DivisionRing $α) <|> throwError "not a division ring"
diff --git a/mathlib4/Mathlib/Tactic/NormNum/BigOperators.lean b/mathlib4/Mathlib/Tactic/NormNum/BigOperators.lean
index 1014da66c..74cc03e56 100644
--- a/mathlib4/Mathlib/Tactic/NormNum/BigOperators.lean
+++ b/mathlib4/Mathlib/Tactic/NormNum/BigOperators.lean
@@ -350,6 +350,7 @@ partial def evalFinsetBigop {α : Q(Type u)} {β : Q(Type v)}
       let eq : Q($op $s $f = $op (Finset.cons $a $s' $h) $f) := q(congr_fun (congr_arg _ $pf) _)
       pure (res.eq_trans eq)
 
+set_option backward.isDefEq.respectTransparency.instances false in
 attribute [local instance] monadLiftOptionMetaM in
 /-- `norm_num` plugin for evaluating products of finsets.
 
@@ -379,6 +380,7 @@ partial def evalFinsetProd : NormNumExt where eval {u β} e := do
       pure <| res.eq_trans eq)
     s
 
+set_option backward.isDefEq.respectTransparency.instances false in
 attribute [local instance] monadLiftOptionMetaM in
 /-- `norm_num` plugin for evaluating sums of finsets.
 
diff --git a/mathlib4/Mathlib/Tactic/NormNum/Inv.lean b/mathlib4/Mathlib/Tactic/NormNum/Inv.lean
index bfc8ad2f2..4abcded32 100644
--- a/mathlib4/Mathlib/Tactic/NormNum/Inv.lean
+++ b/mathlib4/Mathlib/Tactic/NormNum/Inv.lean
@@ -20,6 +20,7 @@ namespace Mathlib.Meta.NormNum
 
 open Lean.Meta Qq
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Helper function to synthesize a typed `CharZero α` expression given `Ring α`. -/
 def inferCharZeroOfRing {α : Q(Type u)} (_i : Q(Ring $α) := by with_reducible assumption) :
     MetaM Q(CharZero $α) :=
@@ -31,6 +32,7 @@ def inferCharZeroOfRing? {α : Q(Type u)} (_i : Q(Ring $α) := by with_reducible
     MetaM (Option Q(CharZero $α)) :=
   return (← trySynthInstanceQ q(CharZero $α)).toOption
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Helper function to synthesize a typed `CharZero α` expression given `AddMonoidWithOne α`. -/
 def inferCharZeroOfAddMonoidWithOne {α : Q(Type u)}
     (_i : Q(AddMonoidWithOne $α) := by with_reducible assumption) : MetaM Q(CharZero $α) :=
@@ -44,6 +46,7 @@ def inferCharZeroOfAddMonoidWithOne? {α : Q(Type u)}
       MetaM (Option Q(CharZero $α)) :=
   return (← trySynthInstanceQ q(CharZero $α)).toOption
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Helper function to synthesize a typed `CharZero α` expression given `DivisionRing α`. -/
 def inferCharZeroOfDivisionRing {α : Q(Type u)}
     (_i : Q(DivisionRing $α) := by with_reducible assumption) : MetaM Q(CharZero $α) :=
diff --git a/mathlib4/Mathlib/Tactic/NormNum/Result.lean b/mathlib4/Mathlib/Tactic/NormNum/Result.lean
index 8583027f5..d5163f6b0 100644
--- a/mathlib4/Mathlib/Tactic/NormNum/Result.lean
+++ b/mathlib4/Mathlib/Tactic/NormNum/Result.lean
@@ -51,15 +51,18 @@ def instAddMonoidWithOne {α : Type u} [Ring α] : AddMonoidWithOne α := inferI
 /-- A shortcut (non)instance for `Nat.AtLeastTwo (n + 2)` to shrink generated proofs. -/
 lemma instAtLeastTwo (n : ℕ) : Nat.AtLeastTwo (n + 2) := inferInstance
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Helper function to synthesize a typed `AddMonoidWithOne α` expression. -/
 meta def inferAddMonoidWithOne (α : Q(Type u)) : MetaM Q(AddMonoidWithOne $α) :=
   return ← synthInstanceQ q(AddMonoidWithOne $α) <|>
     throwError "not an AddMonoidWithOne"
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Helper function to synthesize a typed `Semiring α` expression. -/
 meta def inferSemiring (α : Q(Type u)) : MetaM Q(Semiring $α) :=
   return ← synthInstanceQ q(Semiring $α) <|> throwError "not a semiring"
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Helper function to synthesize a typed `Ring α` expression. -/
 meta def inferRing (α : Q(Type u)) : MetaM Q(Ring $α) :=
   return ← synthInstanceQ q(Ring $α) <|> throwError "not a ring"
diff --git a/mathlib4/Mathlib/Tactic/Simproc/ExistsAndEq.lean b/mathlib4/Mathlib/Tactic/Simproc/ExistsAndEq.lean
index 0684540ca..484cc6ee9 100644
--- a/mathlib4/Mathlib/Tactic/Simproc/ExistsAndEq.lean
+++ b/mathlib4/Mathlib/Tactic/Simproc/ExistsAndEq.lean
@@ -422,7 +422,7 @@ simproc ↓ existsAndEq (Exists _) := fun e => do
   lambdaBoundedTelescope p 1 fun xs (body : Q(Prop)) => withNewMCtxDepth do
     let some u := f.constLevels![0]? | unreachable!
     have α : Q(Sort $u) := α; have p : Q($α → Prop) := p
-    let some (a : Q($α)) := xs[0]? | return .continue
+    let some (a : Q($α)) := (xs[0]? :) | return .continue
     let some path ← findEqPath a body | return .continue
     let (fvars, lctx, newBody, a') ← findEq a body path
     withLCtx' lctx do
diff --git a/mathlib4/Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean b/mathlib4/Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean
index 8fdb74642..ac6e6ed44 100644
--- a/mathlib4/Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean
+++ b/mathlib4/Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean
@@ -93,6 +93,8 @@ def toLimit (P : ProfiniteGrp.{u}) : P ⟶ limit (diagram P) :=
   ofHom { toLimitFun P with
   continuous_toFun := toLimitFun_continuous P }
 
+-- Defeq abuse, see `change` below.
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- An auxiliary result, superseded by `toLimit_surjective` -/
 theorem denseRange_toLimit (P : ProfiniteGrp.{u}) : DenseRange (toLimit P) := by
   apply dense_iff_inter_open.mpr
diff --git a/mathlib4/Mathlib/Topology/Algebra/Module/UniformConvergence.lean b/mathlib4/Mathlib/Topology/Algebra/Module/UniformConvergence.lean
index 093a172af..41e74f81e 100644
--- a/mathlib4/Mathlib/Topology/Algebra/Module/UniformConvergence.lean
+++ b/mathlib4/Mathlib/Topology/Algebra/Module/UniformConvergence.lean
@@ -110,6 +110,10 @@ lemma UniformOnFun.continuousSMul_induced_of_image_bounded (φ : hom) (hφ : IsI
   refine UniformFun.continuousSMul_induced_of_range_bounded 𝕜 s E H φ' ⟨rfl⟩ fun u ↦ ?_
   simpa only [Set.image_eq_range] using! h u s hs
 
+variable (H : Submodule 𝕜 (α →ᵤ[𝔖] E))
+
+-- Abuses defeq `α →ᵤ[𝔖] E = α → E`.
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- Let `E` be a TVS, `𝔖 : Set (Set α)` and `H` a submodule of `α →ᵤ[𝔖] E`. If the image of any
 `S ∈ 𝔖` by any `u ∈ H` is bounded (in the sense of `Bornology.IsVonNBounded`), then `H`,
 equipped with the topology of `𝔖`-convergence, is a TVS.
diff --git a/mathlib4/Mathlib/Topology/Category/CompHausLike/Basic.lean b/mathlib4/Mathlib/Topology/Category/CompHausLike/Basic.lean
index 822b65506..6efae58bf 100644
--- a/mathlib4/Mathlib/Topology/Category/CompHausLike/Basic.lean
+++ b/mathlib4/Mathlib/Topology/Category/CompHausLike/Basic.lean
@@ -92,6 +92,8 @@ instance : CoeSort (CompHausLike P) (Type u) :=
 instance category : Category (CompHausLike P) :=
   inferInstanceAs <| Category (InducedCategory _ toTop)
 
+-- Would need to have a new type synonym for the `FunLike` instance for the induced category.
+set_option backward.isDefEq.respectTransparency.instances false in
 instance concreteCategory : ConcreteCategory (CompHausLike P) (C(·, ·)) :=
   inferInstanceAs <| ConcreteCategory (InducedCategory _ toTop) _
 
diff --git a/mathlib4/Mathlib/Topology/Category/CompHausLike/Cartesian.lean b/mathlib4/Mathlib/Topology/Category/CompHausLike/Cartesian.lean
index b6059b439..1bd5cf355 100644
--- a/mathlib4/Mathlib/Topology/Category/CompHausLike/Cartesian.lean
+++ b/mathlib4/Mathlib/Topology/Category/CompHausLike/Cartesian.lean
@@ -41,6 +41,7 @@ def productCone : BinaryFan X Y :=
   BinaryFan.mk (P := CompHausLike.of P (X × Y))
     (ofHom _ { toFun := Prod.fst }) (ofHom _ { toFun := Prod.snd })
 
+-- `continuity` getting confused about category theory
 /--
 When the predicate `P` is preserved under taking type-theoretic products, that product is a
 category-theoretic product in `CompHausLike P`.
diff --git a/mathlib4/Mathlib/Topology/Category/CompactlyGenerated.lean b/mathlib4/Mathlib/Topology/Category/CompactlyGenerated.lean
index 1509d32e5..46ab31b24 100644
--- a/mathlib4/Mathlib/Topology/Category/CompactlyGenerated.lean
+++ b/mathlib4/Mathlib/Topology/Category/CompactlyGenerated.lean
@@ -49,6 +49,8 @@ attribute [instance] is_compactly_generated
 instance : Category.{w, w + 1} CompactlyGenerated.{u, w} :=
   inferInstanceAs <| Category (InducedCategory _ toTop)
 
+-- Would need to have a new type synonym for the `FunLike` instance for the induced category.
+set_option backward.isDefEq.respectTransparency.instances false in
 instance : ConcreteCategory.{w} CompactlyGenerated.{u, w} (C(·, ·)) :=
   inferInstanceAs <| ConcreteCategory (InducedCategory _ toTop) _
 
diff --git a/mathlib4/Mathlib/Topology/Category/FinTopCat.lean b/mathlib4/Mathlib/Topology/Category/FinTopCat.lean
index 30c0a223d..9d37cb403 100644
--- a/mathlib4/Mathlib/Topology/Category/FinTopCat.lean
+++ b/mathlib4/Mathlib/Topology/Category/FinTopCat.lean
@@ -42,6 +42,8 @@ attribute [instance] fintype
 instance : Category FinTopCat :=
   inferInstanceAs <| Category (InducedCategory _ toTop)
 
+-- Would need to have a new type synonym for the `FunLike` instance for the induced category.
+set_option backward.isDefEq.respectTransparency.instances false in
 instance : ConcreteCategory FinTopCat (C(·, ·)) :=
   inferInstanceAs <| ConcreteCategory (InducedCategory _ toTop) _
 
diff --git a/mathlib4/Mathlib/Topology/Category/LightProfinite/Basic.lean b/mathlib4/Mathlib/Topology/Category/LightProfinite/Basic.lean
index 1523aa612..b8a0262fe 100644
--- a/mathlib4/Mathlib/Topology/Category/LightProfinite/Basic.lean
+++ b/mathlib4/Mathlib/Topology/Category/LightProfinite/Basic.lean
@@ -257,6 +257,8 @@ def toProfinite (S : LightDiagram) : Profinite := S.cone.pt
 instance : Category LightDiagram :=
   inferInstanceAs <| Category (InducedCategory _ toProfinite)
 
+-- Would need to have a new type synonym for the `FunLike` instance for the induced category.
+set_option backward.isDefEq.respectTransparency.instances false in
 instance hasForget : ConcreteCategory LightDiagram (fun X Y => C(X.toProfinite, Y.toProfinite)) :=
   inferInstanceAs <| ConcreteCategory (InducedCategory _ toProfinite) _
 
diff --git a/mathlib4/Mathlib/Topology/Category/Sequential.lean b/mathlib4/Mathlib/Topology/Category/Sequential.lean
index 493885ee6..b5fd3c922 100644
--- a/mathlib4/Mathlib/Topology/Category/Sequential.lean
+++ b/mathlib4/Mathlib/Topology/Category/Sequential.lean
@@ -44,6 +44,8 @@ attribute [instance] is_sequential
 instance : Category.{u, u + 1} Sequential.{u} :=
   inferInstanceAs <| Category (InducedCategory _ toTop)
 
+-- Would need to have a new type synonym for the `FunLike` instance for the induced category.
+set_option backward.isDefEq.respectTransparency.instances false in
 instance : ConcreteCategory.{u} Sequential.{u} (C(·, ·)) :=
   inferInstanceAs <| ConcreteCategory (InducedCategory _ toTop) _
 
diff --git a/mathlib4/Mathlib/Topology/Category/TopCat/Limits/Products.lean b/mathlib4/Mathlib/Topology/Category/TopCat/Limits/Products.lean
index 30cc99433..6cb768118 100644
--- a/mathlib4/Mathlib/Topology/Category/TopCat/Limits/Products.lean
+++ b/mathlib4/Mathlib/Topology/Category/TopCat/Limits/Products.lean
@@ -234,6 +234,8 @@ protected def binaryCofan (X Y : TopCat.{u}) : BinaryCofan X Y :=
   BinaryCofan.mk (ofHom ⟨Sum.inl, by fun_prop⟩) (ofHom ⟨Sum.inr, by fun_prop⟩)
 
 set_option backward.isDefEq.respectTransparency.types false in
+-- `continuity` can't unfold the category theory language properly.
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- The constructed binary coproduct cofan in `TopCat` is the coproduct. -/
 def binaryCofanIsColimit (X Y : TopCat.{u}) : IsColimit (TopCat.binaryCofan X Y) := by
   refine Limits.BinaryCofan.isColimitMk (fun s => ofHom
diff --git a/mathlib4/Mathlib/Topology/Category/TopCat/Monoidal.lean b/mathlib4/Mathlib/Topology/Category/TopCat/Monoidal.lean
index a75e372c1..8be64b3ab 100644
--- a/mathlib4/Mathlib/Topology/Category/TopCat/Monoidal.lean
+++ b/mathlib4/Mathlib/Topology/Category/TopCat/Monoidal.lean
@@ -130,10 +130,12 @@ def homeomorph : I ≃ₜ unitInterval := Homeomorph.ulift
 lemma ext {x y : I.{u}} (h : homeomorph x = homeomorph y) : x = y :=
   homeomorph.injective h
 
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- The symmetrization map `TopCat.I ⟶ TopCat.I`. -/
 def symm : I.{u} ⟶ I :=
   ofHom ⟨homeomorph.symm ∘ unitInterval.symm ∘ homeomorph, by fun_prop⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp]
 lemma homeomorph_symm (x : I) :
     homeomorph (symm x) = unitInterval.symm (homeomorph x) := rfl
@@ -141,6 +143,7 @@ lemma homeomorph_symm (x : I) :
 instance : OfNat I.{u} 0 := ⟨homeomorph.symm 0⟩
 instance : OfNat I.{u} 1 := ⟨homeomorph.symm 1⟩
 
+set_option backward.isDefEq.respectTransparency.instances false in
 @[simp] lemma homeomorph_zero : homeomorph (0 : I.{u}) = 0 := by simp [OfNat.ofNat]
 @[simp] lemma homeomorph_one : homeomorph (1 : I.{u}) = 1 := by simp [OfNat.ofNat]
 @[simp] lemma symm_one : I.symm 1 = 0 := by aesop
diff --git a/mathlib4/Mathlib/Topology/ContinuousMap/Basic.lean b/mathlib4/Mathlib/Topology/ContinuousMap/Basic.lean
index 70dfd5b86..d91eda2a6 100644
--- a/mathlib4/Mathlib/Topology/ContinuousMap/Basic.lean
+++ b/mathlib4/Mathlib/Topology/ContinuousMap/Basic.lean
@@ -454,7 +454,7 @@ variable (hf : IsQuotientMap f) (g : C(X, Z)) (h : Function.FactorsThrough g f)
 noncomputable def lift : C(Y, Z) where
   toFun := ((fun i ↦ Quotient.liftOn' i g (fun _ _ (hab : f _ = f _) ↦ h hab)) :
     Quotient (Setoid.ker f) → Z) ∘ hf.homeomorph.symm
-  continuous_toFun := Continuous.comp (continuous_quot_lift _ g.2) (Homeomorph.continuous _)
+  continuous_toFun := Continuous.comp (g.2.quotient_liftOn' _) (Homeomorph.continuous _)
 
 /--
 The obvious triangle induced by `IsQuotientMap.lift` commutes:
diff --git a/mathlib4/Mathlib/Topology/EMetricSpace/BoundedVariation.lean b/mathlib4/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
index 174e0498c..59b9efc7d 100644
--- a/mathlib4/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
+++ b/mathlib4/Mathlib/Topology/EMetricSpace/BoundedVariation.lean
@@ -660,6 +660,8 @@ theorem eVariationOn_on_inter_Iic_eq_Iio_add_edist
       sum_le_of_monotoneOn_Iic (by grind [MonotoneOn, StrictMonoOn]) (by grind)
     exact A.trans B
 
+set_option backward.isDefEq.instanceTypes false in
+set_option backward.isDefEq.respectTransparency false in
 /-- The variation of a function on `Ici a` is the sum of the variation on `Ioi a` and the
 contribution of `a`, i.e., the distance between the right limit and the value at `a`.
 We give a version relative to a set `s`. -/
@@ -683,6 +685,8 @@ lemma eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt
   · congr 1
     grind
 
+-- Defeq abuse: `h` should be translated into a statement about `aᵒᵈ`.
+set_option backward.isDefEq.respectTransparency.instances false in
 /-- If a function is continuous on the right at a point `a`, then its variations on `Ioi a` and
 on `Ici a` coincide. We give a version relative to a set `s`. -/
 lemma eVariationOn_inter_Ioi_eq_inter_Ici_of_continuousWithinAt
@@ -713,6 +717,7 @@ lemma eVariationOn_Ioc_eq_Icc_of_continuousWithinAt
   have : (𝓝[Ioi a] a).NeBot := nhdsGT_neBot_of_exists_gt ⟨b, hab⟩
   exact eVariationOn_Ioc_eq_Icc_of_continuousWithinAt' h'
 
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma eVariationOn_Ico_eq_Icc_of_continuousWithinAt'
     [TopologicalSpace α] [OrderTopology α] {f : α → E} {a b : α}
     [h : (𝓝[<] a).NeBot] (h' : ContinuousWithinAt f (Iic a) a) :
@@ -720,6 +725,7 @@ lemma eVariationOn_Ico_eq_Icc_of_continuousWithinAt'
   rw [← comp_ofDual f, ← comp_ofDual f, ← Ioc_toDual, ← Icc_toDual]
   exact eVariationOn_Ioc_eq_Icc_of_continuousWithinAt' h'
 
+set_option backward.isDefEq.respectTransparency.instances false in
 lemma eVariationOn_Ico_eq_Icc_of_continuousWithinAt
     [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {f : α → E} {a b : α}
     (h' : ContinuousWithinAt f (Iic a) a) :
diff --git a/mathlib4/Mathlib/Topology/Homotopy/TopCat/Path.lean b/mathlib4/Mathlib/Topology/Homotopy/TopCat/Path.lean
index 8c11261fa..b1e6c94a6 100644
--- a/mathlib4/Mathlib/Topology/Homotopy/TopCat/Path.lean
+++ b/mathlib4/Mathlib/Topology/Homotopy/TopCat/Path.lean
@@ -37,6 +37,8 @@ protected structure Path (x y : X) where
 
 attribute [simp] Path.hom₀ Path.hom₁
 
+-- Would need `(ULift.{u, 0} ↑unitInterval) = TopCat.I` at instances transparency
+set_option backward.isDefEq.respectTransparency.instances false in
 variable {X} in
 /-- The bijection between `TopCat.Path X x y` and `_root_.Path x y`. -/
 @[simps!]
diff --git a/mathlib4/Mathlib/Topology/Instances/Rat.lean b/mathlib4/Mathlib/Topology/Instances/Rat.lean
index 1e2408bbc..4184713fb 100644
--- a/mathlib4/Mathlib/Topology/Instances/Rat.lean
+++ b/mathlib4/Mathlib/Topology/Instances/Rat.lean
@@ -119,6 +119,8 @@ set_option linter.style.whitespace false in -- linter false positive
 @[simp ←, push_cast]
 lemma nndist_eq (p q : ℚ≥0) : nndist p q = nndist (p : ℚ) (q : ℚ) := rfl
 
+-- Defeq abuse, applying instances about `Subtype` to `ℚ≥0`.
+set_option backward.isDefEq.respectTransparency.instances false in
 instance : IsTopologicalSemiring ℚ≥0 where
   toContinuousAdd := continuousAdd_induced Nonneg.coeRingHom
   toContinuousMul := continuousMul_induced Nonneg.coeRingHom
diff --git a/mathlib4/Mathlib/Topology/Order/Category/AlexDisc.lean b/mathlib4/Mathlib/Topology/Order/Category/AlexDisc.lean
index 50cb21cc7..b4d978e1f 100644
--- a/mathlib4/Mathlib/Topology/Order/Category/AlexDisc.lean
+++ b/mathlib4/Mathlib/Topology/Order/Category/AlexDisc.lean
@@ -32,6 +32,8 @@ instance : CoeSort AlexDisc (Type _) :=
 instance category : Category AlexDisc :=
   inferInstanceAs <| Category (InducedCategory _ toTopCat)
 
+-- Would need to have a new type synonym for the `FunLike` instance for the induced category.
+set_option backward.isDefEq.respectTransparency.instances false in
 instance concreteCategory : ConcreteCategory AlexDisc (C(·, ·)) :=
   inferInstanceAs <| ConcreteCategory (InducedCategory _ toTopCat) _
 
diff --git a/mathlib4/Mathlib/Topology/Order/IsLUB.lean b/mathlib4/Mathlib/Topology/Order/IsLUB.lean
index c3dcdc6ce..086fb5957 100644
--- a/mathlib4/Mathlib/Topology/Order/IsLUB.lean
+++ b/mathlib4/Mathlib/Topology/Order/IsLUB.lean
@@ -154,6 +154,8 @@ theorem isLUB_iff_of_subset_of_subset_closure {α : Type*} [TopologicalSpace α]
   isLUB_congr <| (upperBounds_closure (s := s) ▸ upperBounds_mono_set hts).antisymm <|
     upperBounds_mono_set hst
 
+-- Defeq abuse: `hst` and `hts` should be translated into statements about the order dual.
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem isGLB_iff_of_subset_of_subset_closure {α : Type*} [TopologicalSpace α] [Preorder α]
     [ClosedIciTopology α] {s t : Set α} (hst : s ⊆ t) (hts : t ⊆ closure s) {x : α} :
     IsGLB s x ↔ IsGLB t x :=
diff --git a/mathlib4/Mathlib/Topology/Order/MonotoneConvergence.lean b/mathlib4/Mathlib/Topology/Order/MonotoneConvergence.lean
index d74c618da..40188ab20 100644
--- a/mathlib4/Mathlib/Topology/Order/MonotoneConvergence.lean
+++ b/mathlib4/Mathlib/Topology/Order/MonotoneConvergence.lean
@@ -257,18 +257,24 @@ theorem Monotone.ge_of_tendsto [TopologicalSpace α] [Preorder α] [OrderClosedT
   haveI : Nonempty β := Nonempty.intro b
   _root_.ge_of_tendsto ha ((eventually_ge_atTop b).mono fun _ hxy => hf hxy)
 
+-- Defeq abuse: `ha` should be translated into a statement about the order dual
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem Monotone.le_of_tendsto [TopologicalSpace α] [Preorder α] [OrderClosedTopology α]
     [Preorder β] [IsCodirectedOrder β] {f : β → α} {a : α} (hf : Monotone f)
     (ha : Tendsto f atBot (𝓝 a)) (b : β) :
     a ≤ f b :=
   hf.dual.ge_of_tendsto ha b
 
+-- Defeq abuse: `ha` should be translated into a statement about the order dual
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem Antitone.le_of_tendsto [TopologicalSpace α] [Preorder α] [OrderClosedTopology α]
     [Preorder β] [IsDirectedOrder β] {f : β → α} {a : α} (hf : Antitone f)
     (ha : Tendsto f atTop (𝓝 a)) (b : β) :
     a ≤ f b :=
   hf.dual_right.ge_of_tendsto ha b
 
+-- Defeq abuse: `ha` should be translated into a statement about the order dual
+set_option backward.isDefEq.respectTransparency.instances false in
 theorem Antitone.ge_of_tendsto [TopologicalSpace α] [Preorder α] [OrderClosedTopology α]
     [Preorder β] [IsCodirectedOrder β] {f : β → α} {a : α} (hf : Antitone f)
     (ha : Tendsto f atBot (𝓝 a)) (b : β) :
diff --git a/mathlib4/lakefile.lean b/mathlib4/lakefile.lean
index eed55e391..d5bcc970d 100644
--- a/mathlib4/lakefile.lean
+++ b/mathlib4/lakefile.lean
@@ -43,6 +43,7 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[
 abbrev mathlibLeanOptions := #[
     ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
     ⟨`autoImplicit, false⟩,
+    -- ⟨`backward.isDefEq.respectTransparency.outParams, false⟩,
     ⟨`maxSynthPendingDepth, .ofNat 3⟩,
   ] ++ -- options that are used in `lake build`
     mathlibOnlyLinters.map fun s ↦ { s with name := `weak ++ s.name }