wip: bump to 4.29.0

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 ?_
@@ -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,7 +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.one_def, TangentSpace,
       ContinuousLinearMap.id_comp] at this
     exact this.2.2.contDiffAt
 
@@ -85,6 +85,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
 
@@ -195,7 +197,7 @@ theorem oneJetBundle_trivializationAt (x₀ x : J¹MM') :
       inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀.proj.1 x.proj.1 x₀.proj.2 x.proj.2
         x.2 := by
   delta OneJetSpace
-  rw [continuousLinearMap_trivializationAt, Trivialization.continuousLinearMap_apply]
+  erw [continuousLinearMap_trivializationAt, Trivialization.continuousLinearMap_apply]
   simp only [inCoordinates]
   congr 2
   exact Trivialization.pullback_symmL ContMDiffMap.fst
@@ -214,6 +216,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 +229,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 +302,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 +330,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 +362,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₀ ∧
@@ -464,7 +471,7 @@ theorem ContMDiff.oneJet_add {f : N → M} {g : N → M'} {ϕ ϕ' : ∀ x : N, O
   simp_rw +unfoldPartialApp [inTangentCoordinates, inCoordinates]
   conv =>
     enter [4, x, 2]
-    rw [ContinuousLinearMap.add_comp]
+    erw [ContinuousLinearMap.add_comp]
   simp only [ContinuousLinearMap.comp_add]
   exact hϕ.2.2.add hϕ'.2.2
 
@@ -478,6 +485,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 +541,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 +646,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

@@ -87,7 +87,7 @@ theorem relativize_slice {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
     have hup : ((0 : EP), u) ∈ p.π.ker := (h2pq u).trans hu
     erw [q.update_apply _ hu, ← Prod.zero_mk_add_zero_mk, map_add, p.update_ker_pi _ _ hup, ←
       Prod.smul_zero_mk, map_smul]
-    conv_lhs => rw [← sub_add_cancel (0, q.v) p.v]
+    conv_lhs => erw [← sub_add_cancel (0, q.v) p.v]
     erw [map_add, p.update_ker_pi _ _ hv, p.update_v, bundleSnd_eq]
     rfl
   erw [← preimage_vadd_neg, mem_preimage, mem_slice, R.mem_relativize]
@@ -134,6 +134,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 +151,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
+  simp only [uncurry_bs, bs_eq_coe_bs, add_eq_right]
+  -- adaptation note: the proof used to be done now!
+  exact ContinuousLinearMap.map_zero _
 
 def FamilyFormalSol.uncurry (S : FamilyFormalSol IP P R) : FormalSol (R.relativize IP P) := by
   refine ⟨S.toFamilyOneJetSec.uncurry, ?_⟩
@@ -207,6 +210,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 +225,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 +242,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
@@ -183,6 +184,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,6 +517,7 @@ instance (y : Y) : NormedAddCommGroup (TY y) := by assumption
 
 instance (y : Y) : NormedSpace ℝ (TY y) := by assumption
 
+set_option backward.isDefEq.respectTransparency false in
 omit [IsManifold IX ∞ X] [IsManifold IM ∞ M]
   [IsManifold IY ∞ Y] [IsManifold IN ∞ N] in
 /-- Ampleness survives localization -/
@@ -558,6 +561,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
 
+set_option maxHeartbeats 800000 in -- adaptation note: this is required since the bump
+-- from version 4.28.0 to version 4.29.0-rc6
+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,7 +576,9 @@ 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 ↦ ?_)
-    erw [← ψ.fderiv_coe, ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe,
+    rw [← ψ.fderiv_coe]
+    rw [ContinuousLinearMap.comp_apply]
+    erw [ContinuousLinearEquiv.coe_coe,
       ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.apply_symm_apply,
       ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.apply_symm_apply]
     rfl
@@ -583,6 +591,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 :
@@ -604,6 +613,7 @@ 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 :-(
+set_option backward.isDefEq.respectTransparency false in
 @[simps]
 def OneJetBundle.embedding : OpenSmoothEmbedding IXY J¹XY IMN J¹MN where
   toFun := φ.transfer ψ

SphereEversion/Global/TwistOneJetSec.lean

@@ -148,6 +148,7 @@ tangent space to `V` is canonically isomorphic to `V`. -/
 def incl (v : J¹[𝕜, E, I, M, V] × V) : OneJetBundle I M 𝓘(𝕜, V) V :=
   ⟨(v.1.1, v.2), v.1.2⟩
 
+set_option backward.isDefEq.respectTransparency false in
 theorem contMDiff_incl : ContMDiff ((I.prod 𝓘(𝕜, E →L[𝕜] V)).prod 𝓘(𝕜, V))
     ((I.prod 𝓘(𝕜, V)).prod 𝓘(𝕜, E →L[𝕜] V)) ∞ (incl I M V) := by
   intro x₀
@@ -218,6 +219,7 @@ def familyJoin {f : N × M → V} (hf : ContMDiff (J.prod I) 𝓘(ℝ, V) ∞ f)
     convert (contMDiff_incl I M V).comp (s.contMDiff.prodMk hf)
     ext : 1 <;> simp
 
+set_option backward.isDefEq.respectTransparency false in
 def familyTwist (s : OneJetEuclSec I M V) (i : N × M → V →L[ℝ] V')
     (hi : ∀ x₀ : N × M, ContMDiffAt (J.prod I) 𝓘(ℝ, V →L[ℝ] V') ∞ i x₀) :
     FamilyOneJetEuclSec I M V' J N

SphereEversion/Indexing.lean

@@ -80,6 +80,7 @@ variable {n : ℕ}
 theorem IndexType.not_lt_zero (j : IndexType n) : ¬j < 0 :=
   Nat.casesOn n Nat.not_lt_zero (fun _ ↦ Fin.not_lt_zero) j
 
+set_option backward.isDefEq.respectTransparency false in
 theorem IndexType.zero_le (i : IndexType n) : 0 ≤ i := by cases n <;> dsimp at * <;> simp
 
 def IndexType.succ {N : ℕ} : IndexType N → IndexType N := Order.succ
@@ -118,6 +119,7 @@ theorem IndexType.toNat_succ (i : IndexType n) (hi : ¬IsMax i) :
 theorem IndexType.not_isMax (n : IndexType 0) : ¬IsMax n :=
   not_isMax_of_lt <| Nat.lt_succ_self n
 
+set_option backward.isDefEq.respectTransparency false in
 @[elab_as_elim]
 theorem IndexType.induction_from {P : IndexType n → Prop} {i₀ : IndexType n} (h₀ : P i₀)
     (ih : ∀ i ≥ i₀, ¬IsMax i → P i → P i.succ) : ∀ i ≥ i₀, P i := by
@@ -153,7 +155,7 @@ theorem IndexType.exists_by_induction {α : Type*} (P : IndexType n → α → P
   cases n with
   | zero =>
     intro P Q h₀ ih
-    rcases exists_by_induction' P Q h₀ (by simpa using ih) with ⟨f, hf⟩
+    rcases exists_by_induction' P Q h₀ (fun n a hn ↦ ih n a hn (not_isMax n)) with ⟨f, hf⟩
     exact ⟨f, fun n ↦ ⟨(hf n).1, fun _ ↦ (hf n).2⟩⟩
   | succ N =>
     -- dsimp only [IndexType, IndexType.succ]