set_option

Author: kim-em

Mathlib/Algebra/Quaternion.lean

@@ -748,7 +748,10 @@ protected instance algebra [CommSemiring S] [Algebra S R] : Algebra S ℍ[R] :=
   inferInstanceAs <| Algebra S ℍ[R,-1,0,-1]
 
 instance : Star ℍ[R] := QuaternionAlgebra.instStarQuaternionAlgebra
+
 instance : StarRing ℍ[R] := QuaternionAlgebra.instStarRing
+
+set_option backward.isDefEq.respectTransparency.types false in
 instance : IsStarNormal a := inferInstanceAs <| IsStarNormal (R := ℍ[R,-1,0,-1]) a
 
 @[ext]

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean

@@ -25,6 +25,8 @@ simply by proving:
 2. `0 ≤ x ↔ IsSelfAdjoint x ∧ SpectrumRestricts Real.toNNReal x`.
 -/
 
+set_option backward.isDefEq.respectTransparency.types false
+
 @[expose] public section
 
 open Set Topology

Mathlib/CategoryTheory/Equivalence.lean

@@ -58,6 +58,8 @@ We write `C ≌ D` (`\backcong`, not to be confused with `≅`/`\cong`) for a bu
 
 -/
 
+set_option backward.isDefEq.respectTransparency.types false
+
 @[expose] public section
 
 namespace CategoryTheory

Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean

@@ -28,6 +28,8 @@ Operations on walks that produce a new walk in the same graph.
 walks
 -/
 
+set_option backward.isDefEq.respectTransparency.types false
+
 @[expose] public section
 
 open Function

Mathlib/Order/DirectedInverseSystem.lean

@@ -350,6 +350,8 @@ theorem piEquivSucc_self {x} :
   simp [piEquivSucc]
 
 variable {equiv e}
+
+set_option backward.isDefEq.respectTransparency.types false in
 theorem isNatEquiv_piEquivSucc [InverseSystem f] (H : ∀ x, (e x).1 = f (le_succ i) x)
     (nat : IsNatEquiv f equiv) : IsNatEquiv f (piEquivSucc equiv e hi) := fun j k hj hk h x ↦ by
   have lt_succ {j} := (lt_succ_iff_of_not_isMax (b := j) hi).mpr
@@ -445,6 +447,7 @@ theorem pEquivOn_apply_eq (h : IsLowerSet (s ∩ t))
        (e₂.restrict inter_subset_right).equiv ⟨i, his, hit⟩ from
   congr_fun (congr_arg _ <| unique_pEquivOn h) _
 
+set_option backward.isDefEq.respectTransparency.types false in
 /-- Extend a partial family of bijections by one step. -/
 def pEquivOnSucc [InverseSystem f] (hi : ¬IsMax i) (e : PEquivOn f equivSucc (Iic i))
     (H : ∀ ⦃i⦄ (hi : ¬ IsMax i) x, (equivSucc hi x).1 = f (le_succ i) x) :