benchmark respectTransparency

Archive/Hairer.lean

@@ -93,6 +93,7 @@ def L : MvPolynomial ι ℝ →ₗ[ℝ]
     (fun p f₁ f₂ ↦ by simp_rw [smul_eq_mul, ← integral_add (int p _) (int p _), ← mul_add]; rfl)
     fun r p f ↦ by simp_rw [← integral_smul, smul_comm r]; rfl
 
+set_option backward.isDefEq.respectTransparency.types false in
 lemma inj_L : Injective (L ι) :=
   (injective_iff_map_eq_zero _).mpr fun p hp ↦ by
     have H : ∀ᵐ x : EuclideanSpace ℝ ι, x ∈ ball 0 1 → eval x p = 0 :=

Archive/Imo/Imo1987Q1.lean

@@ -31,6 +31,7 @@ open Finset (range sum_const)
 
 namespace Imo1987Q1
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The set of pairs `(x : α, σ : Perm α)` such that `σ x = x` is equivalent to the set of pairs
 `(x : α, σ : Perm {x}ᶜ)`. -/
 def fixedPointsEquiv : { σx : α × Perm α // σx.2 σx.1 = σx.1 } ≃ Σ x : α, Perm ({x}ᶜ : Set α) :=
@@ -41,6 +42,7 @@ def fixedPointsEquiv : { σx : α × Perm α // σx.2 σx.1 = σx.1 } ≃ Σ x :
       (sigmaCongrRight fun x => Equiv.setCongr <| by simp only [SetCoe.forall]; simp)
     _ ≃ Σ x : α, Perm ({x}ᶜ : Set α) := sigmaCongrRight fun x => by apply Equiv.Set.compl
 
+set_option backward.isDefEq.respectTransparency false in
 theorem card_fixed_points :
     card { σx : α × Perm α // σx.2 σx.1 = σx.1 } = card α * (card α - 1)! := by
   simp only [card_congr (fixedPointsEquiv α), card_sigma, card_perm]

Archive/Imo/Imo2013Q1.lean

@@ -39,6 +39,8 @@ theorem prod_lemma (m : ℕ → ℕ+) (k : ℕ) (nm : ℕ+) :
 end Imo2013Q1
 
 open Imo2013Q1
+
+set_option backward.isDefEq.respectTransparency.types false in
 theorem imo2013_q1 (n : ℕ+) (k : ℕ) :
     ∃ m : ℕ → ℕ+, (1 : ℚ) + (2 ^ k - 1) / n = ∏ i ∈ Finset.range k, (1 + 1 / (m i : ℚ)) := by
   induction k generalizing n with

Archive/Imo/Imo2019Q2.lean

@@ -94,7 +94,7 @@ structure Imo2019q2Cfg where
   C_ne_Q₁ : C ≠ Q₁
 
 /-- A default choice of orientation, for lemmas that need to pick one. -/
-@[implicit_reducible]
+@[instance_reducible]
 def someOrientation [hd2 : Fact (finrank ℝ V = 2)] : Module.Oriented ℝ V (Fin 2) :=
   ⟨Basis.orientation (finBasisOfFinrankEq _ _ hd2.out)⟩
 

Archive/Imo/Imo2024Q5.lean

@@ -128,6 +128,7 @@ def MonsterData.reflect (m : MonsterData N) : MonsterData N where
   toFun := Fin.rev ∘ m
   inj' := fun i j hij ↦ by simpa using hij
 
+set_option backward.isDefEq.respectTransparency false in
 lemma MonsterData.reflect_reflect (m : MonsterData N) : m.reflect.reflect = m := by
   ext i
   simp [MonsterData.reflect]
@@ -149,7 +150,7 @@ lemma MonsterData.mk_mem_monsterCells_iff_of_le {m : MonsterData N} {r : Fin (N
   simp only [monsterCells, Set.mem_range, Prod.mk.injEq]
   refine ⟨?_, ?_⟩
   · rintro ⟨r', rfl, rfl⟩
-    simp only [Subtype.coe_eta]
+    simp only
   · rintro rfl
     exact ⟨⟨r, hr1, hrN⟩, rfl, rfl⟩
 
@@ -449,6 +450,7 @@ def Path.reflect (p : Path N) : Path N where
     simp_rw [Adjacent, Nat.dist, Cell.reflect, Fin.rev] at h ⊢
     lia
 
+set_option backward.isDefEq.respectTransparency false in
 lemma Path.firstMonster_reflect (p : Path N) (m : MonsterData N) :
     p.reflect.firstMonster m.reflect = (p.firstMonster m).map Cell.reflect := by
   simp_rw [firstMonster, reflect, List.find?_map]
@@ -524,6 +526,7 @@ lemma Strategy.ForcesWinIn.mono (s : Strategy N) {k₁ k₂ : ℕ} (h : s.Forces
 
 /-! ### Proof of lower bound with constructions used therein -/
 
+set_option backward.isDefEq.respectTransparency false in
 /-- An arbitrary choice of monster positions, which is modified to put selected monsters in
 desired places. -/
 def baseMonsterData (N : ℕ) : MonsterData N where
@@ -539,6 +542,7 @@ def baseMonsterData (N : ℕ) : MonsterData N where
 def monsterData12 (hN : 2 ≤ N) (c₁ c₂ : Fin (N + 1)) : MonsterData N :=
   ((baseMonsterData N).setValue (row2 hN) c₂).setValue (row1 hN) c₁
 
+set_option backward.isDefEq.respectTransparency false in
 lemma monsterData12_apply_row2 (hN : 2 ≤ N) {c₁ c₂ : Fin (N + 1)} (h : c₁ ≠ c₂) :
     monsterData12 hN c₁ c₂ (row2 hN) = c₂ := by
   rw [monsterData12, Function.Embedding.setValue_eq_of_ne]
@@ -729,6 +733,7 @@ def winningStrategy (hN : 2 ≤ N) : Strategy N
   | 1 => fun r => path1 hN ((r 0).getD 0).2
   | _ + 2 => fun r => path2 hN ((r 0).getD 0).2 ((r 1).getD 0).1
 
+set_option backward.isDefEq.respectTransparency false in
 lemma path0_firstMonster_eq_apply_row1 (hN : 2 ≤ N) (m : MonsterData N) :
     (path0 hN).firstMonster m = some (1, m (row1 hN)) := by
   simp_rw [path0, Path.firstMonster, Path.ofFn]
@@ -958,6 +963,7 @@ lemma winningStrategy_play_one_eq_none_or_play_two_eq_none_of_edge_zero (hN : 2
   exact path2OfEdge0_firstMonster_eq_none_of_path1OfEdge0_firstMonster_eq_some hN hx2N.1
     hx2N.2 hc₁0 hx.symm
 
+set_option backward.isDefEq.respectTransparency false in
 lemma winningStrategy_play_one_of_edge_N (hN : 2 ≤ N) {m : MonsterData N}
     (hc₁N : (m (row1 hN) : ℕ) = N) : (winningStrategy hN).play m 3 ⟨1, by simp⟩ =
       ((winningStrategy hN).play m.reflect 3 ⟨1, by simp⟩).map Cell.reflect := by
@@ -972,6 +978,7 @@ lemma winningStrategy_play_one_of_edge_N (hN : 2 ≤ N) {m : MonsterData N}
   simp_rw [winningStrategy_play_one hN, path1, path1OfEdgeN, dif_neg hc₁0, if_pos hc₁N,
     dif_pos hc₁r0, ← Path.firstMonster_reflect, MonsterData.reflect_reflect]
 
+set_option backward.isDefEq.respectTransparency false in
 lemma winningStrategy_play_two_of_edge_N (hN : 2 ≤ N) {m : MonsterData N}
     (hc₁N : (m (row1 hN) : ℕ) = N) : (winningStrategy hN).play m 3 ⟨2, by simp⟩ =
       ((winningStrategy hN).play m.reflect 3 ⟨2, by simp⟩).map Cell.reflect := by
@@ -994,6 +1001,7 @@ lemma winningStrategy_play_two_of_edge_N (hN : 2 ≤ N) {m : MonsterData N}
   · rcases h with ⟨x, hx⟩
     simp [hx, Cell.reflect]
 
+set_option backward.isDefEq.respectTransparency false in
 lemma winningStrategy_play_one_eq_none_or_play_two_eq_none_of_edge_N (hN : 2 ≤ N)
     {m : MonsterData N} (hc₁N : (m (row1 hN) : ℕ) = N) :
     (winningStrategy hN).play m 3 ⟨1, by simp⟩ = none ∨

Archive/MinimalSheffer.lean

@@ -46,7 +46,7 @@ class VeroffAlgebra (α : Type*) extends Inhabited α where
 variable {α : Type*}
 
 /-- Derive a Veroff algebra from a Boolean algebra. -/
-@[implicit_reducible]
+@[instance_reducible]
 def BooleanAlgebra.veroffAlgebra [BooleanAlgebra α] : VeroffAlgebra α where
   default := ⊥
   f a b := (a ⊓ b)ᶜ
@@ -207,7 +207,7 @@ class SingleShefferAlgebra (α : Type*) extends Inhabited α where
 variable {α : Type*}
 
 /-- Derive a `SingleShefferAlgebra` from a Boolean algebra. -/
-@[implicit_reducible]
+@[instance_reducible]
 def BooleanAlgebra.singleShefferAlgebra [BooleanAlgebra α] : SingleShefferAlgebra α where
   default := ⊥
   f a b := (a ⊓ b)ᶜ

Archive/Sensitivity.lean

@@ -407,6 +407,7 @@ theorem exists_eigenvalue (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
   rw [Set.toFinset_card] at hH
   linarith
 
+set_option backward.isDefEq.respectTransparency false in
 open Classical in
 /-- **Huang sensitivity theorem** also known as the **Huang degree theorem** -/
 theorem huang_degree_theorem (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :

Archive/Wiedijk100Theorems/FriendshipGraphs.lean

@@ -173,6 +173,7 @@ theorem isRegularOf_not_existsPolitician (hG' : ¬ExistsPolitician G) :
 
 open scoped Classical in
 include hG in
+set_option backward.isDefEq.respectTransparency.types false in
 /-- Let `A` be the adjacency matrix of a `d`-regular friendship graph, and let `v` be a vector
   all of whose components are `1`. Then `v` is an eigenvector of `A ^ 2`, and we can compute
   the eigenvalue to be `d * d`, or as `d + (Fintype.card V - 1)`, so those quantities must be equal.

Archive/Wiedijk100Theorems/Konigsberg.lean

@@ -17,6 +17,7 @@ between them has no Eulerian trail.
 
 namespace Konigsberg
 
+set_option backward.isDefEq.respectTransparency.types false in
 /-- The vertices for the Königsberg graph; four vertices for the bodies of land and seven
 vertices for the bridges. -/
 inductive Verts : Type

Archive/ZagierTwoSquares.lean

@@ -113,6 +113,7 @@ def complexInvo : Function.End (zagierSet k) := fun ⟨⟨x, y, z⟩, h⟩ =>
 
 variable [hk : Fact (4 * k + 1).Prime]
 
+set_option backward.isDefEq.respectTransparency false in
 /-- `complexInvo k` is indeed an involution. -/
 theorem complexInvo_sq : complexInvo k ^ 2 = 1 := by
   change complexInvo k ∘ complexInvo k = id
@@ -139,6 +140,7 @@ theorem complexInvo_sq : complexInvo k ^ 2 = 1 := by
       ← Nat.add_sub_assoc less, ← add_assoc, Nat.sub_add_cancel more, Nat.sub_sub _ _ y,
       ← two_mul, add_comm, Nat.add_sub_cancel]
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Any fixed point of `complexInvo k` must be `(1, 1, k)`. -/
 theorem eq_of_mem_fixedPoints {t : zagierSet k} (mem : t ∈ fixedPoints (complexInvo k)) :
     t.val = (1, 1, k) := by
@@ -169,6 +171,7 @@ theorem eq_of_mem_fixedPoints {t : zagierSet k} (mem : t ∈ fixedPoints (comple
 def singletonFixedPoint : Finset (zagierSet k) :=
   {⟨(1, 1, k), (by simp only [zagierSet, Set.mem_setOf_eq]; linarith)⟩}
 
+set_option backward.isDefEq.respectTransparency false in
 /-- `complexInvo k` has exactly one fixed point. -/
 theorem card_fixedPoints_eq_one : Fintype.card (fixedPoints (complexInvo k)) = 1 := by
   rw [show 1 = Finset.card (singletonFixedPoint k) by rfl, ← Set.toFinset_card]

Counterexamples/AharoniKorman.lean

@@ -206,6 +206,7 @@ lemma induction_on_level {n : ℕ} {p : (x : Hollom) → x ∈ level n → Prop}
   rintro x y _ rfl
   exact h _ _
 
+set_option backward.isDefEq.respectTransparency false in
 /--
 For each `n`, there is an order embedding from ℕ × ℕ (which has the product order) to the Hollom
 partial order.
@@ -219,6 +220,7 @@ lemma embed_apply (n : ℕ) (x y : ℕ) : embed n (x, y) = h(x, y, n) := rfl
 
 lemma embed_strictMono {n : ℕ} : StrictMono (embed n) := (embed n).strictMono
 
+set_option backward.isDefEq.respectTransparency false in
 lemma level_eq_range (n : ℕ) : level n = Set.range (embed n) := by
   simp [level, Set.range, embed]
 
@@ -810,6 +812,7 @@ variable {n : ℕ}
 
 lemma R_subset_level : R n C ⊆ level n := Set.sep_subset (level n) _
 
+set_option backward.isDefEq.respectTransparency false in
 /--
 A helper lemma to show `square_subset_R`.  In particular shows that if `C ∩ level n` is finite, the
 set of points `x` such that `x` is at least as large as every element of `C ∩ level n` contains an
@@ -851,6 +854,7 @@ lemma square_subset_above (h : (C ∩ level n).Finite) :
     specialize hab _ _ hfg
     lia
 
+set_option backward.isDefEq.respectTransparency false in
 lemma square_subset_R (h : (C ∩ level n).Finite) :
     ∀ᶠ a in atTop, embed n '' Set.Ici (a, a) ⊆ R n C \ (C ∩ level n) := by
   filter_upwards [square_subset_above h] with a ha
@@ -933,6 +937,7 @@ lemma S_subset_R : S n C ⊆ R n C := by
 
 lemma S_subset_level : S n C ⊆ level n := S_subset_R.trans R_subset_level
 
+set_option backward.isDefEq.respectTransparency false in
 /--
 Assuming `C ∩ level n` is finite, and `C ∩ level (n + 1)` is finite, that there exists cofinitely
 many `a` such that `{(x, y, n) | x ≥ a ∧ y ≥ a} ⊆ S \ (C ∩ level n)`.

Counterexamples/MapFloor.lean

@@ -59,6 +59,7 @@ instance isOrderedAddMonoid : IsOrderedAddMonoid ℤ[ε] :=
   Function.Injective.isOrderedAddMonoid
     (toLex ∘ coeff) (fun _ _ => funext fun _ => coeff_add _ _ _) .rfl
 
+set_option backward.isDefEq.respectTransparency false in
 theorem pos_iff {p : ℤ[ε]} : 0 < p ↔ 0 < p.trailingCoeff := by
   rw [trailingCoeff]
   refine
@@ -118,6 +119,7 @@ theorem forgetEpsilons_floor_lt (n : ℤ) :
   exact (if_neg <| by rw [coeff_sub, intCast_coeff_zero]; simp [this]).trans (by
     rw [coeff_sub, intCast_coeff_zero]; simp)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The ceil of `n + ε` is `n + 1` but its image under `forgetEpsilons` is `n`, whose ceil is
 itself. -/
 theorem lt_forgetEpsilons_ceil (n : ℤ) :

Counterexamples/Phillips.lean

@@ -288,13 +288,13 @@ theorem exists_discrete_support_nonpos (f : BoundedAdditiveMeasure α) :
       simp only [u, not_exists, mem_iUnion, mem_diff]
       tauto
     · congr 1
-      simp only [G, s, Function.iterate_succ', Subtype.coe_mk, union_diff_left, Function.comp]
+      simp only [G, s, Function.iterate_succ', union_diff_left, Function.comp]
   have I2 : ∀ n : ℕ, (n : ℝ) * (ε / 2) ≤ f ↑(s n) := by
     intro n
     induction n with
     | zero =>
       simp only [s, empty, BoundedAdditiveMeasure.empty, id, Nat.cast_zero, zero_mul,
-        Function.iterate_zero, Subtype.coe_mk, le_rfl]
+        Function.iterate_zero, le_rfl]
     | succ n IH =>
       have : (s (n + 1)).1 = (s (n + 1)).1 \ (s n).1 ∪ (s n).1 := by
         simpa only [s, Function.iterate_succ', union_diff_self]

Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean

@@ -217,6 +217,7 @@ theorem f111 : ofLex (Finsupp.single (1 : F) (1 : F)) 1 = 1 :=
 theorem f110 : ofLex (Finsupp.single (1 : F) (1 : F)) 0 = 0 :=
   single_apply_eq_zero.mpr fun h => h.symm
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Here we see that (not-necessarily strict) monotonicity of addition on `Lex (F →₀ F)` is not
 a consequence of monotonicity of addition on `F`.  Strict monotonicity of addition on `F` is
 enough and is the content of `Finsupp.Lex.addLeftStrictMono`. -/

Mathlib/Algebra/Algebra/Epi.lean

@@ -122,6 +122,7 @@ section Module
 
 variable (M : Type*) [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M]
 
+set_option backward.isDefEq.respectTransparency false in
 /-- If an `R`-algebra `A` is epi, then the scalar multiplication `A ⊗[R] M → M` is injective, for
 any `A`-module `M`. -/
 lemma injective_lift_lsmul :

Mathlib/Algebra/Algebra/Equiv.lean

@@ -885,6 +885,7 @@ variable {R S M₁ M₂ : Type*} [CommSemiring R] [AddCommMonoid M₁] [Module R
   [SMulCommClass S R M₁] [SMulCommClass S R M₂] [SMul R S] [IsScalarTower R S M₁]
   [IsScalarTower R S M₂]
 
+set_option backward.isDefEq.respectTransparency false in
 variable (R) in
 /-- A linear equivalence of two modules induces an equivalence of algebras of their
 endomorphisms. -/

Mathlib/Algebra/Algebra/NonUnitalHom.lean

@@ -317,6 +317,7 @@ theorem coe_inverse (f : A →ₙₐ[R] B₁) (g : B₁ → A) (h₁ : Function.
     (h₂ : Function.RightInverse g f) : (inverse f g h₁ h₂ : B₁ → A) = g :=
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The inverse of a bijective morphism is a morphism. -/
 def inverse' (f : A →ₛₙₐ[φ] B) (g : B → A)
     (k : Function.RightInverse φ' φ)
@@ -368,6 +369,7 @@ def snd : A × B →ₙₐ[R] B where
 variable {R A B}
 variable [DistribMulAction R C]
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The prod of two morphisms is a morphism. -/
 @[simps toFun]
 def prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : A →ₙₐ[R] B × C where

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -998,6 +998,8 @@ instance instIsMulCommutative_iSup {ι : Type*} [Nonempty ι] [Preorder ι] [IsD
     IsMulCommutative (⨆ i, S i : NonUnitalSubalgebra R A) :=
   isMulCommutative_iSup S.monotone.directed_le
 
+-- TODO: fails since `Set.Mem` is implicit-reducible
+set_option backward.isDefEq.respectTransparency.types false in
 /-- Define an algebra homomorphism on a directed supremum of non-unital subalgebras by defining
 it on each non-unital subalgebra, and proving that it agrees on the intersection of
 non-unital subalgebras. -/

Mathlib/Algebra/Algebra/Operations.lean

@@ -719,6 +719,7 @@ noncomputable def span.ringHom : SetSemiring A →+* Submodule R A where
   map_add' := span_union
   map_mul' s t := by simp_rw [SetSemiring.down_mul, span_mul_span]
 
+set_option backward.isDefEq.respectTransparency false in
 variable (R) in
 /-- `(span R {·})` as a `MonoidWithZeroHom`. -/
 noncomputable def spanSingleton : A →*₀ Submodule R A where

Mathlib/Algebra/Algebra/Opposite.lean

@@ -41,6 +41,7 @@ variable [IsScalarTower R S A]
 
 namespace MulOpposite
 
+set_option backward.isDefEq.respectTransparency false in
 instance instAlgebra : Algebra R Aᵐᵒᵖ where
   algebraMap := (algebraMap R A).toOpposite fun _ _ => Algebra.commutes _ _
   smul_def' c x := unop_injective <| by

Mathlib/Algebra/Algebra/Spectrum/Quasispectrum.lean

@@ -268,6 +268,7 @@ instance quasispectrum.instZero [Nontrivial R] (a : A) : Zero (quasispectrum R a
 
 variable {R}
 
+set_option backward.isDefEq.respectTransparency false in
 /-- A version of `NonUnitalAlgHom.quasispectrum_apply_subset` which allows for `quasispectrum R`,
 where `R` is a *semi*ring, but `φ` must still function over a scalar ring `S`. In this case, we
 need `S` to be explicit. The primary use case is, for instance, `R := ℝ≥0` and `S := ℝ` or

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -287,7 +287,7 @@ instance toCommRing {R A} [CommRing R] [CommRing A] [Algebra R A] (S : Subalgebr
 end
 
 /-- The forgetful map from `Subalgebra` to `Submodule` as an `OrderEmbedding` -/
-@[implicit_reducible] -- Not `@[reducible]` because it is an order embedding rather than a function.
+@[instance_reducible] -- Not `@[reducible]` because it is an order embedding rather than a function.
 def toSubmodule : Subalgebra R A ↪o Submodule R A where
   toEmbedding :=
     { toFun := fun S =>

Mathlib/Algebra/Algebra/Subalgebra/Directed.lean

@@ -51,6 +51,8 @@ instance instIsMulCommutative_iSup [Preorder ι] [IsDirectedOrder ι]
 
 variable (K)
 
+-- TODO: `respectTransparency.types false` necessary since `Set.Mem` was made implicit-reducible
+set_option backward.isDefEq.respectTransparency.types false in
 /-- Define an algebra homomorphism on a directed supremum of subalgebras by defining
 it on each subalgebra, and proving that it agrees on the intersection of subalgebras. -/
 noncomputable def iSupLift (dir : Directed (· ≤ ·) K) (f : ∀ i, K i →ₐ[R] B)
@@ -88,6 +90,7 @@ noncomputable def iSupLift (dir : Directed (· ≤ ·) K) (f : ∀ i, K i →ₐ
   exact liftSup.comp (inclusion hT)
 
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem iSupLift_inclusion {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}
     {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)}
@@ -103,6 +106,7 @@ theorem iSupLift_comp_inclusion {dir : Directed (· ≤ ·) K} {f : ∀ i, K i 
     {T : Subalgebra R A} {hT : T ≤ iSup K} {i : ι} (h : K i ≤ T) :
     (iSupLift K dir f hf T hT).comp (inclusion h) = f i := by ext; simp
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem iSupLift_mk {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}
     {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)}
@@ -111,6 +115,7 @@ theorem iSupLift_mk {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}
   dsimp [iSupLift, inclusion]
   rw [Set.iUnionLift_mk]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem iSupLift_of_mem {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}
     {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)}
     {T : Subalgebra R A} {hT : T ≤ iSup K} {i : ι} (x : T) (hx : (x : A) ∈ K i) :

Mathlib/Algebra/Algebra/ZMod.lean

@@ -50,7 +50,7 @@ abbrev algebra (p : ℕ) [CharP R p] : Algebra (ZMod p) R :=
 set_option backward.isDefEq.respectTransparency false in
 /-- Any ring with a `ZMod p`-module structure can be upgraded to a `ZMod p`-algebra. Not an
 instance because this is usually not the default way, and this will cause typeclass search loop. -/
-@[implicit_reducible]
+@[instance_reducible]
 def algebraOfModule (n : ℕ) (R : Type*) [Ring R] [Module (ZMod n) R] : Algebra (ZMod n) R :=
   Algebra.ofModule' (proof · · |>.1) (proof · · |>.2) where
   proof (r : ZMod n) (x : R) : r • 1 * x = r • x ∧ x * r • 1 = r • x := by

Mathlib/Algebra/BigOperators/Expect.lean

@@ -280,6 +280,7 @@ end bij
 @[simp] lemma expect_neg_index [DecidableEq ι] [InvolutiveNeg ι] (s : Finset ι) (f : ι → M) :
     𝔼 i ∈ -s, f i = 𝔼 i ∈ s, f (-i) := expect_image neg_injective.injOn
 
+set_option backward.isDefEq.respectTransparency false in
 lemma _root_.map_expect {F : Type*} [FunLike F M N] [LinearMapClass F ℚ≥0 M N]
     (g : F) (f : ι → M) (s : Finset ι) :
     g (𝔼 i ∈ s, f i) = 𝔼 i ∈ s, g (f i) := by simp only [expect, map_smul, map_sum]