[Merged by Bors] - chore: adaptations for nightly-2026-04-20

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -153,6 +153,7 @@ lemma prod_filter_not_mul_prod_filter (s : Finset ι) (p : ι → Prop) [Decidab
     (∏ x ∈ s with ¬p x, f x) * ∏ x ∈ s with p x, f x = ∏ x ∈ s, f x := by
   rw [mul_comm, prod_filter_mul_prod_filter_not]
 
+set_option backward.isDefEq.respectTransparency false in
 @[to_additive]
 theorem prod_filter_xor (p q : ι → Prop) [DecidablePred p] [DecidablePred q] :
     (∏ x ∈ s with (Xor' (p x) (q x)), f x) =

Mathlib/Algebra/Homology/DerivedCategory/Basic.lean

@@ -94,6 +94,7 @@ variable {C}
 /-- The localization functor `CochainComplex C ℤ ⥤ DerivedCategory C`. -/
 def Q : CochainComplex C ℤ ⥤ DerivedCategory C := HomologicalComplexUpToQuasiIso.Q
 
+set_option backward.isDefEq.respectTransparency false in
 instance : (Q (C := C)).IsLocalization
     (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) := by
   dsimp only [Q, DerivedCategory]
@@ -114,6 +115,7 @@ variable (C)
 def quotientCompQhIso : HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh ≅ Q :=
   HomologicalComplexUpToQuasiIso.quotientCompQhIso C (ComplexShape.up ℤ)
 
+set_option backward.isDefEq.respectTransparency false in
 instance : Qh.IsLocalization (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) := by
   dsimp [Qh, DerivedCategory]
   infer_instance

Mathlib/Algebra/Lie/Free.lean

@@ -181,6 +181,7 @@ def of : X → FreeLieAlgebra R X := fun x => Quot.mk _ (lib.of R x)
 
 variable {L : Type w} [LieRing L] [LieAlgebra R L]
 
+set_option backward.isDefEq.respectTransparency false in
 /-- An auxiliary definition used to construct the equivalence `lift` below. -/
 def liftAux (f : X → CommutatorRing L) :=
   lib.lift R f
@@ -197,6 +198,7 @@ theorem liftAux_map_mul (f : X → L) (a b : lib R X) :
     liftAux R f (a * b) = ⁅liftAux R f a, liftAux R f b⁆ :=
   map_mul _ a b
 
+set_option backward.isDefEq.respectTransparency false in
 theorem liftAux_spec (f : X → L) (a b : lib R X) (h : FreeLieAlgebra.Rel R X a b) :
     liftAux R f a = liftAux R f b := by
   induction h with
@@ -208,6 +210,7 @@ theorem liftAux_spec (f : X → L) (a b : lib R X) (h : FreeLieAlgebra.Rel R X a
   | mul_left c' _ h₂ => simp only [liftAux_map_mul, h₂]
   | mul_right c' _ h₂ => simp only [liftAux_map_mul, h₂]
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The quotient map as a `NonUnitalAlgHom`. -/
 def mk : lib R X →ₙₐ[R] CommutatorRing (FreeLieAlgebra R X) where
   toFun := Quot.mk (Rel R X)

Mathlib/Algebra/Lie/NonUnitalNonAssocAlgebra.lean

@@ -78,6 +78,7 @@ namespace LieHom
 variable {R L}
 variable {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂]
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Regarding the `LieRing` of a `LieAlgebra` as a `NonUnitalNonAssocRing`, we can
 regard a `LieHom` as a `NonUnitalAlgHom`. -/
 @[simps]
@@ -87,6 +88,7 @@ def toNonUnitalAlgHom (f : L →ₗ⁅R⁆ L₂) : CommutatorRing L →ₙₐ[R]
     map_zero' := f.toLinearMap.map_zero
     map_mul' := f.map_lie }
 
+set_option backward.isDefEq.respectTransparency false in
 theorem toNonUnitalAlgHom_injective :
     Function.Injective (toNonUnitalAlgHom : _ → CommutatorRing L →ₙₐ[R] CommutatorRing L₂) :=
   fun _ _ h => ext <| NonUnitalAlgHom.congr_fun h

Mathlib/Analysis/CStarAlgebra/Matrix.lean

@@ -152,6 +152,7 @@ def l2OpNormedRingAux : NormedRing (Matrix n n 𝕜) :=
 open Bornology Filter
 open scoped Topology Uniformity
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The metric on `Matrix m n 𝕜` arising from the operator norm given by the identification with
 (continuous) linear maps of `EuclideanSpace`. -/
 @[instance_reducible]

Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean

@@ -135,6 +135,7 @@ section
 
 variable (C)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Our normalization procedure works by first defining a functor `F C ⥤ (N C ⥤ N C)` (which turns
 out to be very easy), and then obtain a functor `F C ⥤ N C` by plugging in the normal object
 `𝟙_ C`. -/

Mathlib/CategoryTheory/Pi/Basic.lean

@@ -102,6 +102,7 @@ def comapComp (f : K → J) (g : J → I) : comap C g ⋙ comap (C ∘ g) f ≅
   { app := fun X b => 𝟙 (X (g (f b)))
     naturality := fun X Y f' => by simp only [comap, Function.comp]; funext; simp }
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The natural isomorphism between pulling back then evaluating, and just evaluating. -/
 @[simps!]
 def comapEvalIsoEval (h : J → I) (j : J) : comap C h ⋙ eval (C ∘ h) j ≅ eval C (h j) :=
@@ -117,6 +118,7 @@ instance sumElimCategory : ∀ s : I ⊕ J, Category.{v₁} (Sum.elim C D s)
   | Sum.inl i => inferInstanceAs <| Category (C i)
   | Sum.inr j => inferInstanceAs <| Category (D j)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The bifunctor combining an `I`-indexed family of objects with a `J`-indexed family of objects
 to obtain an `I ⊕ J`-indexed family of objects.
 -/

Mathlib/CategoryTheory/Shift/Adjunction.lean

@@ -610,6 +610,7 @@ this constructs the unique compatible `CommShift` structure on `E.functor`.
 noncomputable def commShiftFunctor [E.inverse.CommShift A] : E.functor.CommShift A :=
   E.symm.toAdjunction.rightAdjointCommShift A
 
+set_option backward.isDefEq.respectTransparency false in
 lemma commShift_of_inverse [E.inverse.CommShift A] :
     letI := E.commShiftFunctor A
     E.CommShift A := by

Mathlib/CategoryTheory/Shift/Twist.lean

@@ -92,6 +92,7 @@ identify to the shift functors on `C`. -/
 noncomputable def shiftIso (m : A) : shiftFunctor t.Category m ≅ shiftFunctor C m :=
   Iso.refl _
 
+set_option backward.isDefEq.respectTransparency false in
 lemma shiftFunctor_map {X Y : t.Category} (f : X ⟶ Y) (m : A) :
     (shiftFunctor t.Category m).map f =
       (t.shiftIso m).hom.app X ≫ (shiftFunctor C m).map f ≫ (t.shiftIso m).inv.app Y := by

Mathlib/CategoryTheory/Triangulated/Adjunction.lean

@@ -201,6 +201,7 @@ instance [h : E.inverse.IsTriangulated] : E.symm.functor.IsTriangulated := h
 lemma mk' (h : E.functor.IsTriangulated) : E.IsTriangulated where
   rightAdjoint_isTriangulated := E.toAdjunction.isTriangulated_rightAdjoint
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Constructor for `Equivalence.IsTriangulated`. -/
 lemma mk'' (h : E.inverse.IsTriangulated) : E.IsTriangulated where
   leftAdjoint_isTriangulated := (mk' E.symm h).rightAdjoint_isTriangulated

Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean

@@ -344,6 +344,7 @@ private lemma sum_ne_add_mod_eq_sub_one {c : ℕ} :
     rw [Nat.add_mod_mod, ← add_assoc, ← one_add_mul, show 1 + (r - 1) = r by lia,
       Nat.mul_add_mod_self_left]
 
+set_option backward.isDefEq.respectTransparency false in
 lemma card_edgeFinset_turanGraph_add :
     #(turanGraph (n + r) r).edgeFinset =
     #(turanGraph n r).edgeFinset + n * (r - 1) + r.choose 2 := by

Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean

@@ -57,6 +57,7 @@ variable
   {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M]
   {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} {s s' : Set ℝ} (t₀ : ℝ) {x₀ : M}
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Existence of local integral curves for a $C^1$ vector field at interior points of a `C^1`
 manifold. -/
 theorem exists_isMIntegralCurveAt_of_contMDiffAt [CompleteSpace E]

Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

@@ -514,6 +514,7 @@ theorem writtenInExtChartAt_comp (h : ContinuousWithinAt f s x) :
 variable {f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}
   {g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))}
 
+set_option backward.isDefEq.respectTransparency false in
 /-- `UniqueMDiffWithinAt` achieves its goal: it implies the uniqueness of the derivative. -/
 protected nonrec theorem UniqueMDiffWithinAt.eq (U : UniqueMDiffWithinAt I s x)
     (h : HasMFDerivWithinAt I I' f s x f') (h₁ : HasMFDerivWithinAt I I' f s x f₁') : f' = f₁' := by
@@ -717,6 +718,7 @@ lemma mfderivWithin_of_isOpen (hs : IsOpen s) (hx : x ∈ s) :
     mfderivWithin I I' f s x = mfderiv I I' f x :=
   mfderivWithin_of_mem_nhds (hs.mem_nhds hx)
 
+set_option backward.isDefEq.respectTransparency false in
 theorem hasMFDerivWithinAt_insert {y : M} :
     HasMFDerivWithinAt I I' f (insert y s) x f' ↔ HasMFDerivWithinAt I I' f s x f' := by
   have : T1Space M := I.t1Space M
@@ -1115,6 +1117,7 @@ theorem mfderiv_congr {f' : M → M'} (h : f = f') :
 
 variable (x)
 
+set_option backward.isDefEq.respectTransparency false in
 theorem HasMFDerivWithinAt.comp (hg : HasMFDerivWithinAt I' I'' g u (f x) g')
     (hf : HasMFDerivWithinAt I I' f s x f') (hst : s ⊆ f ⁻¹' u) :
     HasMFDerivWithinAt I I'' (g ∘ f) s x (g'.comp f') := by

Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean

@@ -50,6 +50,7 @@ the simpNF linter complains about this being `@[simp]`. -/
 theorem writtenInExtChartAt_model_space : writtenInExtChartAt 𝓘(𝕜, E) 𝓘(𝕜, E') x f = f :=
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 theorem hasMFDerivWithinAt_iff_hasFDerivWithinAt {f'} :
     HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x f' ↔ HasFDerivWithinAt f f' s x := by
   simpa only [HasMFDerivWithinAt, and_iff_right_iff_imp, mfld_simps] using

Mathlib/Geometry/Manifold/Riemannian/Basic.lean

@@ -238,6 +238,7 @@ attribute [local instance] normedSpaceTangentSpaceVectorSpace
 
 variable (I)
 
+set_option backward.isDefEq.respectTransparency false in
 lemma eventually_norm_mfderiv_extChartAt_lt (x : M) :
     ∃ C > 0, ∀ᶠ y in 𝓝 x, ‖mfderiv% (extChartAt I x) y‖ < C := by
   rcases eventually_norm_trivializationAt_lt E (fun (x : M) ↦ TangentSpace I x) x
@@ -247,6 +248,7 @@ lemma eventually_norm_mfderiv_extChartAt_lt (x : M) :
   filter_upwards [hC, hx] with y hy h'y
   rwa [← TangentBundle.continuousLinearMapAt_trivializationAt h'y]
 
+set_option backward.isDefEq.respectTransparency false in
 lemma eventually_enorm_mfderiv_extChartAt_lt (x : M) :
     ∃ C > (0 : ℝ≥0), ∀ᶠ y in 𝓝 x, ‖mfderiv% (extChartAt I x) y‖ₑ < C := by
   rcases eventually_norm_mfderiv_extChartAt_lt I x with ⟨C, C_pos, hC⟩
@@ -257,6 +259,7 @@ lemma eventually_enorm_mfderiv_extChartAt_lt (x : M) :
   simp only [enorm, nnnorm]
   exact_mod_cast hy
 
+set_option backward.isDefEq.respectTransparency false in
 lemma eventually_norm_mfderivWithin_symm_extChartAt_comp_lt (x : M) :
     ∃ C > 0, ∀ᶠ y in 𝓝 x, ‖mfderiv[range I] (extChartAt I x).symm (extChartAt I x y)‖ < C := by
   rcases eventually_norm_symmL_trivializationAt_lt E (fun (x : M) ↦ TangentSpace I x) x
@@ -269,6 +272,7 @@ lemma eventually_norm_mfderivWithin_symm_extChartAt_comp_lt (x : M) :
     (extChartAt I x).left_inv (by simpa using h'y)
   convert hy using 3 <;> congr
 
+set_option backward.isDefEq.respectTransparency false in
 lemma eventually_norm_mfderivWithin_symm_extChartAt_lt (x : M) :
     ∃ C > 0, ∀ᶠ y in 𝓝[range I] (extChartAt I x x),
     ‖mfderiv[range I] (extChartAt I x).symm y‖ < C := by
@@ -283,6 +287,7 @@ lemma eventually_norm_mfderivWithin_symm_extChartAt_lt (x : M) :
   simp only [preimage_setOf_eq, mem_setOf_eq] at hy
   convert hy
 
+set_option backward.isDefEq.respectTransparency false in
 lemma eventually_enorm_mfderivWithin_symm_extChartAt_lt (x : M) :
     ∃ C > (0 : ℝ≥0), ∀ᶠ y in 𝓝[range I] (extChartAt I x x),
     ‖mfderiv[range I] (extChartAt I x).symm y‖ₑ < C := by
@@ -294,6 +299,7 @@ lemma eventually_enorm_mfderivWithin_symm_extChartAt_lt (x : M) :
   simp only [enorm, nnnorm]
   exact_mod_cast hy
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Around any point `x`, the Riemannian distance between two points is controlled by the distance
 in the extended chart. In other words, the extended chart is locally Lipschitz. -/
 lemma eventually_riemannianEDist_le_edist_extChartAt (x : M) :
@@ -378,6 +384,7 @@ lemma eventually_riemannianEDist_lt (x : M) {c : ℝ≥0∞} (hc : 0 < c) :
   · exact Or.inl (mod_cast C_pos.ne')
   · simp
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Any neighborhood of `x` contains all the points which are close enough to `x` for the
 Riemannian distance, `ℝ≥0` version. -/
 lemma setOf_riemannianEDist_lt_subset_nhds [RegularSpace M] {x : M} {s : Set M} (hs : s ∈ 𝓝 x) :

Mathlib/Geometry/Manifold/VectorField/LieBracket.lean

@@ -207,6 +207,7 @@ theorem mlieBracketWithin_eventually_congr_set (h : s =ᶠ[𝓝 x] t) :
     mlieBracketWithin I V W s =ᶠ[𝓝 x] mlieBracketWithin I V W t :=
   mlieBracketWithin_eventually_congr_set' x <| h.filter_mono inf_le_left
 
+set_option backward.isDefEq.respectTransparency false in
 theorem _root_.Filter.EventuallyEq.mlieBracketWithin_vectorField_eq
     (hV : V₁ =ᶠ[𝓝[s] x] V) (hxV : V₁ x = V x) (hW : W₁ =ᶠ[𝓝[s] x] W) (hxW : W₁ x = W x) :
     mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x := by

MathlibTest/GCongr/GCongr.lean

@@ -48,7 +48,7 @@ a b c d : ℕ
 h : b~d
 ⊢ a~a
 
-case a.a
+case a
 a b c d : ℕ
 h : b~d
 ⊢ c~c

MathlibTest/GRewrite.lean

@@ -215,7 +215,7 @@ the inequality goes in the wrong direction). -/
 /--
 error: Tactic `grewrite` failed: could not discharge x ≤ y using x ≥ y
 
-case h₁.hbc
+case hbc
 x y b : ℚ
 h : x ≥ y
 ⊢ x ≤ y
@@ -257,7 +257,7 @@ example {Prime : ℕ → Prop} {a a' : ℕ} (h₁ : Prime (a + 1)) (h₂ : a = a
 /--
 error: Tactic `grewrite` failed: could not discharge b ≤ a using a ≤ b
 
-case h₂.hbc
+case hbc
 a b c : ℚ
 h₁ : a ≤ b
 h₂ : 0 ≤ c

MathlibTest/Linarith/Basic.lean

@@ -728,7 +728,6 @@ example (x : ℤ) : 0 ≤ x * wrapped x := by nlinarith
 def tightlyWrapped (z : ℤ) : ℤ := z
 /--
 error: linarith failed to find a contradiction
-case h
 x : ℤ
 a✝ : x * tightlyWrapped x < 0
 ⊢ False

MathlibTest/congr.lean

@@ -332,7 +332,6 @@ example (inst1 : BEq α) [LawfulBEq α] (inst2 : BEq α) [LawfulBEq α] (xs : Li
 
 /--
 error: unsolved goals
-case h.e'_2
 α : Type
 inst1 : BEq α
 inst✝¹ : LawfulBEq α

MathlibTest/conv_widget.lean

@@ -83,8 +83,7 @@ conv =>
     enter [1, x, 5]
     skip
 ---
-trace: case h
-x : False
+trace: x : False
 | true
 -/
 #guard_msgs in
@@ -115,8 +114,7 @@ conv =>
     enter [1, 0, x, 1]
     skip
 ---
-trace: case h
-x : Unit
+trace: x : Unit
 | false
 -/
 #guard_msgs in
@@ -384,8 +382,7 @@ conv =>
     enter [1, 0, x0, x1, x2, 2]
     skip
 ---
-trace: case h.h.h
-x0 x1 x2 : Bool → Nat
+trace: x0 x1 x2 : Bool → Nat
 | x2 true
 -/
 #guard_msgs in

lake-manifest.json

@@ -35,20 +35,20 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2db6054a44326f8c0230ee0570e2ddb894816511",
+   "rev": "82d457fb3bdd9efadbae06608ff337d689efdddf",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.98",
+   "inputRev": "v0.0.97",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bf91f5d1e444cf2bd9795bd2499658b802759af7",
+   "rev": "94778bc57a7fced2cdb8cda599c6e2672193d708",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "bf91f5d1e444cf2bd9795bd2499658b802759af7",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",

lakefile.lean

@@ -8,7 +8,7 @@ open Lake DSL
 
 require "leanprover-community" / "batteries" @ git "nightly-testing"
 require "leanprover-community" / "Qq" @ git "nightly-testing"
-require "leanprover-community" / "aesop" @ git "bf91f5d1e444cf2bd9795bd2499658b802759af7"
+require "leanprover-community" / "aesop" @ git "nightly-testing"
 require "leanprover-community" / "proofwidgets" @ git "v0.0.98"
   with NameMap.empty.insert `errorOnBuild
     "ProofWidgets failed to reuse pre-built JS code. \

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-04-19
+leanprover/lean4:nightly-2026-04-20