feat: bump to 4.30 (#141)

I had to add 40 `set_option backward.isDefEq.respectTransparency false
in`s.
One `simp` broke, but there is a not too bad fix. (I still it were
better understood.)
One proof now takes a really long time; it would be good to understand
why!

Author: grunweg

SphereEversion/Global/Immersion.lean

@@ -44,19 +44,21 @@ theorem mem_immersionRel_iff {σ : OneJetBundle I M I' M'} :
     σ ∈ immersionRel I M I' M' ↔ Injective (σ.2 : TangentSpace I _ →L[ℝ] TangentSpace I' _) :=
   Iff.rfl
 
+set_option backward.isDefEq.respectTransparency false in
 /-- A characterisation of the immersion relation in terms of a local chart. -/
 theorem mem_immersionRel_iff' {σ σ' : OneJetBundle I M I' M'} (hσ' : σ' ∈ (ψJ σ).source) :
     σ' ∈ immersionRel I M I' M' ↔ Injective (ψJ σ σ').2 := by
   simp_rw [mem_immersionRel_iff]
   rw [oneJetBundle_chartAt_apply, inCoordinates_eq]
   · simp_rw [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, EquivLike.comp_injective,
-    EquivLike.injective_comp]
+      EquivLike.injective_comp]
   exacts [hσ'.1.1, hσ'.1.2]
 
 theorem chartAt_image_immersionRel_eq {σ : OneJetBundle I M I' M'} :
     ψJ σ '' ((ψJ σ).source ∩ immersionRel I M I' M') = (ψJ σ).target ∩ {q : HJ | Injective q.2} :=
   PartialEquiv.IsImage.image_eq fun _σ' hσ' ↦ (mem_immersionRel_iff' I I' hσ').symm
 
+set_option backward.isDefEq.respectTransparency false in
 theorem immersionRel_open [FiniteDimensional ℝ E] : IsOpen (immersionRel I M I' M') := by
   simp_rw [ChartedSpace.isOpen_iff HJ (immersionRel I M I' M'), chartAt_image_immersionRel_eq]
   refine fun σ ↦ (ψJ σ).open_target.inter ?_
@@ -168,7 +170,7 @@ variable (ω : Orientation ℝ E (Fin 3))
 theorem smooth_bs :
     ContMDiff (𝓘(ℝ, ℝ).prod (𝓡 2)) 𝓘(ℝ, E) ∞
       fun p : ℝ × (sphere (0 : E) 1) ↦ (1 - p.1) • (p.2 : E) + p.1 • -(p.2: E) := by
-  refine (ContMDiff.smul ?_ ?_).add (contMDiff_fst.smul ?_)
+  refine (ContMDiff.smul (I := 𝓘(ℝ)) ?_ ?_).add (contMDiff_fst.smul ?_)
   · exact (contDiff_const.sub contDiff_id).contMDiff.comp contMDiff_fst
   · exact (contMDiff_coe_sphere.of_le le_top).comp contMDiff_snd
   · exact (contDiff_neg.contMDiff.comp (contMDiff_coe_sphere.of_le le_top)).comp contMDiff_snd
@@ -214,6 +216,7 @@ theorem formalEversionHolAtZero {t : ℝ} (ht : t < 1 / 4) :
   congr with y
   simp [smoothStep.of_lt ht]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem formalEversionHolAtOne {t : ℝ} (ht : 3 / 4 < t) :
     (formalEversion E ω t).toOneJetSec.IsHolonomic := by
   intro x
@@ -253,12 +256,6 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {E F G : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
   [NormedAddCommGroup G] [NormedSpace 𝕜 G]
 
--- move to Analysis.Calculus.ContDiff.Basic, or so
-theorem contDiff_prod_iff (f : E → F × G) (n : ℕ∞) :
-    ContDiff 𝕜 n f ↔
-      ContDiff 𝕜 n (Prod.fst ∘ f) ∧ ContDiff 𝕜 n (Prod.snd ∘ f) :=
-  ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩
-
 -- move to Analysis.Calculus.ContDiff.Defs, or so
 lemma ContDiff.inr (x : E) (n : ℕ∞) : ContDiff 𝕜 n fun p : F ↦ (⟨x, p⟩ : E × F) := by
   rw [contDiff_prod_iff]

SphereEversion/Global/Localisation.lean

@@ -36,8 +36,7 @@ def OneJetSec.loc (F : OneJetSec 𝓘(ℝ, E) E 𝓘(ℝ, E') E') : JetSec E E'
     have : ContMDiffAt _ _ _ _ _ := F.contMDiff x₀
     simp_rw +unfoldPartialApp [contMDiffAt_oneJetBundle, inTangentCoordinates, inCoordinates,
       TangentBundle.symmL_model_space, TangentBundle.continuousLinearMapAt_model_space,
-      ContinuousLinearMap.one_def, ContinuousLinearMap.comp_id, TangentSpace,
-      ContinuousLinearMap.id_comp] at this
+      ContinuousLinearMap.one_def, TangentSpace] at this
     exact this.2.2.contDiffAt
 
 theorem OneJetSec.loc_hol_at_iff (F : OneJetSec 𝓘(ℝ, E) E 𝓘(ℝ, E') E') (x : E) :
@@ -85,6 +84,7 @@ theorem JetSec.unloc_hol_at_iff (𝓕 : JetSec E E') (x : E) :
   rw [mfderiv_eq_fderiv]
   exact Iff.rfl
 
+set_option backward.isDefEq.respectTransparency false in
 def HtpyJetSec.unloc (𝓕 : HtpyJetSec E E') : HtpyOneJetSec 𝓘(ℝ, E) E 𝓘(ℝ, E') E' where
   bs t := (𝓕 t).f
   ϕ t x := (𝓕 t x).2

SphereEversion/Global/OneJetBundle.lean

@@ -95,13 +95,11 @@ def OneJetSpace (p : M × M') : Type _ :=
   ((ContMDiffMap.fst : C^∞⟮I.prod I', M × M'; I, M⟯) *ᵖ (TangentSpace I)) p →SL[σ]
   ((ContMDiffMap.snd : C^∞⟮I.prod I', M × M'; I', M'⟯) *ᵖ (TangentSpace I')) p
 
-instance (p : M × M') : TopologicalSpace (OneJetSpace I I' p) := by
-  delta OneJetSpace
-  infer_instance
+instance (p : M × M') : TopologicalSpace (OneJetSpace I I' p) :=
+  inferInstanceAs <| TopologicalSpace (E →L[𝕜] E')
 
-instance (p : M × M') : AddCommGroup (OneJetSpace I I' p) := by
-  delta OneJetSpace
-  infer_instance
+instance (p : M × M') : AddCommGroup (OneJetSpace I I' p) :=
+  inferInstanceAs <| AddCommGroup (E →L[𝕜] E')
 
 variable {I I'}
 
@@ -148,34 +146,38 @@ section
 
 variable {M} (p : M × M')
 
-instance (x : M × M') : Module 𝕜 (FJ¹MM' x) := by
-  delta OneJetSpace
-  infer_instance
+instance (x : M × M') : Module 𝕜 (FJ¹MM' x) :=
+  inferInstanceAs <| Module 𝕜 (E →L[𝕜] E')
 
 end
 
+set_option backward.isDefEq.respectTransparency false in
 instance : TopologicalSpace J¹MM' := by
   delta OneJetSpace OneJetBundle
   infer_instance
 
+set_option backward.isDefEq.respectTransparency false in
 instance : FiberBundle (E →L[𝕜] E') FJ¹MM' := by
   delta OneJetSpace
   infer_instance
 
-
+set_option backward.isDefEq.respectTransparency false in
 instance : VectorBundle 𝕜 (E →L[𝕜] E') FJ¹MM' := by
   delta OneJetSpace
   infer_instance
 
+set_option backward.isDefEq.respectTransparency false in
 instance : ContMDiffVectorBundle ∞ (E →L[𝕜] E')
     (OneJetSpace I I' : M × M' → Type _) (I.prod I') := by
   delta OneJetSpace
   infer_instance
 
+set_option backward.isDefEq.respectTransparency false in
 instance : ChartedSpace HJ J¹MM' := by
   delta OneJetSpace OneJetBundle
   infer_instance
 
+set_option backward.isDefEq.respectTransparency false in
 instance : IsManifold ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ J¹MM' := by
   apply Bundle.TotalSpace.isManifold
 
@@ -190,6 +192,7 @@ theorem oneJetBundle_proj_continuous : Continuous (π (E →L[𝕜] E') FJ¹MM')
 -- Porting note: removed next line
 -- attribute [simps] ContMDiffMap.fst ContMDiffMap.snd
 
+set_option backward.isDefEq.respectTransparency false in
 theorem oneJetBundle_trivializationAt (x₀ x : J¹MM') :
     (trivializationAt (E →L[𝕜] E') (OneJetSpace I I') x₀.proj x).2 =
       inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀.proj.1 x.proj.1 x₀.proj.2 x.proj.2
@@ -214,6 +217,7 @@ theorem trivializationAt_oneJetBundle_target (x₀ : M × M') :
         Set.univ :=
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 /-- Computing the value of a chart around `v` at point `v'` in `J¹(M, M')`.
   The last component equals the continuous linear map `v'.2`, composed on both sides by an
   appropriate coordinate change function. -/
@@ -226,6 +230,7 @@ theorem oneJetBundle_chartAt_apply (v v' : OneJetBundle I M I' M') :
   rw [FiberBundle.chartedSpace_chartAt_snd]
   exact oneJetBundle_trivializationAt v v'
 
+set_option backward.isDefEq.respectTransparency false in
 /-- In `J¹(M, M')`, the source of a chart has a nice formula -/
 theorem oneJetBundle_chart_source (x₀ : J¹MM') :
     (chartAt HJ x₀).source =
@@ -298,6 +303,7 @@ lemma ContMDiffMap.snd_apply (x : M) (x' : M') :
 
 end
 
+set_option backward.isDefEq.respectTransparency false in
 /-- In `J¹(M, M')`, the target of a chart has a nice formula -/
 theorem oneJetBundle_chart_target (x₀ : J¹MM') :
     (chartAt HJ x₀).target = Prod.fst ⁻¹' (chartAt (ModelProd H H') x₀.proj).target := by
@@ -325,6 +331,7 @@ theorem oneJetBundle_chart_target (x₀ : J¹MM') :
 
 section Maps
 
+set_option backward.isDefEq.respectTransparency false in
 theorem contMDiff_oneJetBundle_proj :
     ContMDiff ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) (I.prod I') ∞ (π (E →L[𝕜] E') FJ¹MM') := by
   apply contMDiff_proj _
@@ -356,6 +363,7 @@ theorem oneJetBundle_mk_snd {x : M} {y : M'} {f : OneJetSpace I I' (x, y)} :
     (OneJetBundle.mk x y f).2 = f :=
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 theorem contMDiffAt_oneJetBundle {f : N → J¹MM'} {x₀ : N} :
     ContMDiffAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ f x₀ ↔
       CMDiffAt ∞ (fun x ↦ (f x).1.1) x₀ ∧
@@ -446,6 +454,7 @@ theorem ContMDiff.oneJet_comp {f1 : N' → M} (f2 : N' → M') {f3 : N' → N}
 
 variable {I'}
 
+set_option backward.isDefEq.respectTransparency false in
 open Trivialization in
 omit [IsManifold J ∞ N] in
 theorem ContMDiff.oneJet_add {f : N → M} {g : N → M'} {ϕ ϕ' : ∀ x : N, OneJetSpace I I' (f x, g x)}
@@ -478,6 +487,7 @@ protected def OneJetBundle.map (f : M → N) (g : M' → N')
 
 variable {I' J'}
 
+set_option backward.isDefEq.respectTransparency false in
 omit [IsManifold I ∞ M] [IsManifold I' ∞ M']
   [IsManifold I₂ ∞ M₂] [IsManifold I₃ ∞ M₃]
   [IsManifold J' ∞ N'] [IsManifold J ∞ N] in
@@ -533,6 +543,7 @@ theorem ContMDiffAt.oneJetBundle_map {f : M'' → M → N} {g : M'' → M' → N
 def mapLeft (f : M → N) (Dfinv : ∀ x : M, TangentSpace J (f x) →L[𝕜] TangentSpace I x) :
     J¹MM' → OneJetBundle J N I' M' := fun p ↦ OneJetBundle.mk (f p.1.1) p.1.2 (p.2 ∘L Dfinv p.1.1)
 
+set_option backward.isDefEq.respectTransparency false in
 set_option linter.style.multiGoal false in
 omit [IsManifold I ∞ M] [IsManifold I' ∞ M']
   [IsManifold I₂ ∞ M₂] [IsManifold I₃ ∞ M₃]
@@ -637,6 +648,7 @@ variable (I I')
 
 -- note: this proof works for all vector bundles where we have proven
 -- `∀ p, chartAt _ p = f.toPartialEquiv`
+set_option backward.isDefEq.respectTransparency false in
 /-- The canonical identification between the one-jet bundle to the model space and the product,
 as a homeomorphism -/
 def oneJetBundleModelSpaceHomeomorph : OneJetBundle I H I' H' ≃ₜ 𝓜 :=

SphereEversion/Global/OneJetSec.lean

@@ -102,6 +102,7 @@ of its base map at x. -/
 def IsHolonomicAt (F : OneJetSec I M I' M') (x : M) : Prop :=
   mfderiv% F.bs x = (F x).2
 
+set_option backward.isDefEq.respectTransparency false in
 /-- A section of J¹(M, M') is holonomic at (x : M) iff it coincides with the 1-jet extension of
 its base map at x. -/
 theorem isHolonomicAt_iff {F : OneJetSec I M I' M'} {x : M} :
@@ -265,7 +266,7 @@ theorem uncurry_ϕ' (S : FamilyOneJetSec I M I' M' IP P) (p : P × M) :
   convert
     mfderiv_comp p ((S.contMDiff_bs.comp (contMDiff_id.prodMk contMDiff_const)).mdifferentiable
       (by simp) p.1) (contMDiff_fst.mdifferentiable one_ne_zero p)
-  simp_rw [mfderiv_fst]
+  on_goal 1 => simp_rw [mfderiv_fst]
   rfl
 
 theorem isHolonomicAt_uncurry (S : FamilyOneJetSec I M I' M' IP P) {p : P × M} :

SphereEversion/Global/ParametricityForFree.lean

@@ -64,6 +64,7 @@ variable {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
 #check (R.relativize IP P).slice σ p
 #check (R.slice (bundleSnd σ) q : Set <| TangentSpace I' σ.proj.2) -/
 
+set_option backward.isDefEq.respectTransparency false in
 omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] [IsManifold IP ∞ P] in
 theorem relativize_slice {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
     {p : DualPair <| TangentSpace (IP.prod I) σ.1.1} (q : DualPair <| TangentSpace I σ.1.1.2)
@@ -134,6 +135,7 @@ theorem RelMfld.Ample.relativize (hR : R.Ample) : (R.relativize IP P).Ample := b
   rw [relativize_slice q rfl]
   exact (hR q).vadd
 
+set_option backward.isDefEq.respectTransparency false in
 theorem FamilyOneJetSec.uncurry_mem_relativize (S : FamilyOneJetSec I M I' M' IP P) {s : P}
     {x : M} : S.uncurry (s, x) ∈ R.relativize IP P ↔ S s x ∈ R := by
   simp_rw [RelMfld.relativize, mem_preimage, bundleSnd_eq, OneJetSec.coe_apply, mapLeft]
@@ -150,7 +152,9 @@ theorem FamilyOneJetSec.uncurry_mem_relativize (S : FamilyOneJetSec I M I' M' IP
   erw [S.uncurry_ϕ', ContinuousLinearMap.comp_apply, ContinuousLinearMap.add_apply,
     ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply, ContinuousLinearMap.coe_fst',
     ContinuousLinearMap.comp_apply]
-  simp
+  -- adaptation note: in Lean 4.28, all this proof was just `simp`
+  simp only [uncurry_bs, bs_eq_coe_bs, add_eq_right]
+  exact ContinuousLinearMap.map_zero _
 
 def FamilyFormalSol.uncurry (S : FamilyFormalSol IP P R) : FormalSol (R.relativize IP P) := by
   refine ⟨S.toFamilyOneJetSec.uncurry, ?_⟩
@@ -207,6 +211,7 @@ theorem FamilyOneJetSec.curry_ϕ' (S : FamilyOneJetSec (IP.prod I) (P × M) I' M
   rw [mfderiv_id, mfderiv_const]
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 theorem FormalSol.eq_iff {F₁ F₂ : FormalSol R} {x : M} :
     F₁ x = F₂ x ↔ F₁.bs x = F₂.bs x ∧ F₁.ϕ x = by apply F₂.ϕ x := by
   simp [Bundle.TotalSpace.ext_iff, FormalSol.fst_eq, FormalSol.snd_eq]
@@ -221,6 +226,7 @@ theorem FamilyOneJetSec.isHolonomicAt_curry (S : FamilyOneJetSec (IP.prod I) (P
   rw [id, hS]
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 theorem FamilyOneJetSec.curry_mem (S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N) {p : N × P}
     {x : M} (hR : S p.1 (p.2, x) ∈ R.relativize IP P) : S.curry p x ∈ R := by
   simp_rw [RelMfld.relativize, mem_preimage, bundleSnd_eq, OneJetSec.coe_apply, mapLeft] at hR ⊢
@@ -237,6 +243,7 @@ theorem FamilyFormalSol.curry_ϕ' (S : FamilyFormalSol J N (R.relativize IP P))
     (S.curry p).ϕ x = (S p.1).ϕ (p.2, x) ∘L ContinuousLinearMap.inr ℝ EP E :=
   S.toFamilyOneJetSec.curry_ϕ' p x
 
+set_option backward.isDefEq.respectTransparency false in
 theorem curry_eq_iff_eq_uncurry {𝓕 : FamilyFormalSol J N (R.relativize IP P)}
     {𝓕₀ : FamilyFormalSol IP P R} {t : N} {x : M} {s : P} (h : 𝓕 t (s, x) = 𝓕₀.uncurry (s, x)) :
     (𝓕.curry (t, s)) x = 𝓕₀ s x := by

SphereEversion/Global/Relation.lean

@@ -68,6 +68,7 @@ variable {R : RelMfld I M I' M'}
 structure FormalSol (R : RelMfld I M I' M') extends OneJetSec I M I' M' where
   is_sol' : ∀ x : M, toOneJetSec x ∈ R
 
+set_option backward.isDefEq.respectTransparency false in
 instance (R : RelMfld I M I' M') : FunLike (FormalSol R) M (OneJetBundle I M I' M')  where
   coe := fun F ↦ F.toOneJetSec
   coe_injective' := by
@@ -76,7 +77,6 @@ instance (R : RelMfld I M I' M') : FunLike (FormalSol R) M (OneJetBundle I M I'
     · exact congrArg Prod.snd (congrArg Bundle.TotalSpace.proj (congrFun h x))
     · simpa using (Bundle.TotalSpace.ext_iff.mp (congrFun h x)).2
 
-
 def mkFormalSol (F : M → OneJetBundle I M I' M') (hsec : ∀ x, (F x).1.1 = x) (hsol : ∀ x, F x ∈ R)
     (hsmooth : ContMDiff I ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ∞ F) : FormalSol R
     where
@@ -183,6 +183,7 @@ theorem mem_slice {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'} {p : Dua
     {w : TM' σ.1.2} : w ∈ R.slice σ p ↔ OneJetBundle.mk σ.1.1 σ.1.2 (p.update σ.2 w) ∈ R :=
   Iff.rfl
 
+set_option backward.isDefEq.respectTransparency false in
 omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
 theorem slice_mk_update {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'}
     {p : DualPair <| TM σ.1.1} (x : E') :
@@ -515,8 +516,8 @@ instance (y : Y) : NormedAddCommGroup (TY y) := by assumption
 
 instance (y : Y) : NormedSpace ℝ (TY y) := by assumption
 
-omit [IsManifold IX ∞ X] [IsManifold IM ∞ M]
-  [IsManifold IY ∞ Y] [IsManifold IN ∞ N] in
+set_option backward.isDefEq.respectTransparency false in
+omit [IsManifold IX ∞ X] [IsManifold IM ∞ M] [IsManifold IY ∞ Y] [IsManifold IN ∞ N] in
 /-- Ampleness survives localization -/
 theorem RelMfld.Ample.localize (hR : R.Ample) : (R.localize φ ψ).Ample := by
   intro x p
@@ -558,6 +559,9 @@ def OneJetSec.localize (hF : range (F.bs ∘ φ) ⊆ range ψ) : OneJetSec IX X
         (F.contMDiff_bs.comp φ.contMDiff_to).contMDiffAt
     · exact .oneJet_comp IM φ (F.contMDiff_eta.comp φ.contMDiff_to) φ.contMDiff_to.oneJetExt
 
+#adaptation_note /-- In Lean 4.28, this declaration was still reasonably fast -/
+set_option maxHeartbeats 600000 in
+set_option backward.isDefEq.respectTransparency false in
 theorem transfer_localize (hF : range (F.bs ∘ φ) ⊆ range ψ) (x : X) :
     φ.transfer ψ (F.localize φ ψ hF x) = F (φ x) := by
   rw [OneJetSec.coe_apply, OneJetSec.localize_bs, OneJetSec.localize_ϕ,
@@ -570,9 +574,16 @@ theorem transfer_localize (hF : range (F.bs ∘ φ) ⊆ range ψ) (x : X) :
     --  continuous_linear_equiv.coe_coe, continuous_linear_equiv.apply_symm_apply]
     -- Porting note: we are missing an ext lemma here.
     apply ContinuousLinearMap.ext_iff.2 (fun v ↦ ?_)
+    /- adaptation note: in Lean 4.28, this was
     erw [← ψ.fderiv_coe, ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe,
       ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.apply_symm_apply,
       ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.apply_symm_apply]
+    and much faster -/
+    rw [← ψ.fderiv_coe, ContinuousLinearMap.comp_apply]
+    erw [ContinuousLinearEquiv.coe_coe (e := (φ.fderiv x).symm)]
+    rw [ContinuousLinearMap.comp_apply]
+    erw [ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearMap.comp_apply,
+      ContinuousLinearEquiv.apply_symm_apply]
     rfl
 
 theorem OneJetSec.localize_bs_fun (hF : range (F.bs ∘ φ) ⊆ range ψ) :
@@ -583,6 +594,7 @@ theorem OneJetSec.localize_mem_iff (hF : range (F.bs ∘ φ) ⊆ range ψ) {x :
     F.localize φ ψ hF x ∈ R.localize φ ψ ↔ F (φ x) ∈ R := by
   rw [RelMfld.localize, mem_preimage, transfer_localize F φ ψ hF]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem isHolonomicAt_localize_iff (hF : range (F.bs ∘ φ) ⊆ range ψ) (x : X) :
     (F.localize φ ψ hF).IsHolonomicAt x ↔ F.IsHolonomicAt (φ x) := by
   have :
@@ -603,7 +615,8 @@ theorem isHolonomicAt_localize_iff (hF : range (F.bs ∘ φ) ⊆ range ψ) (x :
 
 /-! ## From embeddings `X ↪ M` and `Y ↪ N` to `J¹(X, Y) ↪ J¹(M, N)` -/
 
--- very slow to elaborate :-(
+-- slow to elaborate :-(
+set_option backward.isDefEq.respectTransparency false in
 @[simps]
 def OneJetBundle.embedding : OpenSmoothEmbedding IXY J¹XY IMN J¹MN where
   toFun := φ.transfer ψ