chore: bump to mathlib 4.31.0

SphereEversion/Global/Immersion.lean

@@ -50,7 +50,7 @@ theorem mem_immersionRel_iff' {σ σ' : OneJetBundle I M I' M'} (hσ' : σ' ∈
     σ' ∈ 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,
+  · simp_rw [ContinuousLinearMap.coe_comp, ContinuousLinearEquiv.coe_coe, EquivLike.comp_injective,
       EquivLike.injective_comp]
   exacts [hσ'.1.1, hσ'.1.2]
 
@@ -62,7 +62,7 @@ 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 ?_
-  convert isOpen_univ.prod ContinuousLinearMap.isOpen_injective
+  convert! isOpen_univ.prod ContinuousLinearMap.isOpen_injective
   · ext x
     -- Porting note: `mem_prod` is a simp lemma, but the next line is still needed.
     rw [mem_prod]
@@ -228,8 +228,8 @@ theorem formalEversionHolAtOne {t : ℝ} (ht : 3 / 4 < t) :
   · congr 2 with y
     simp [smoothStep.of_gt ht]
   ext v
-  erw [mfderiv_neg, ContinuousLinearMap.coe_comp', Function.comp_apply,
-       ContinuousLinearMap.neg_apply, smoothStep.of_gt ht]
+  erw [mfderiv_neg, ContinuousLinearMap.coe_comp, Function.comp_apply, _root_.neg_apply,
+    smoothStep.of_gt ht]
   rw [ω.rot_one]; · rfl
   rw [← range_mfderiv_coe_sphere (n := 2) x]
   exact LinearMap.mem_range_self ..
@@ -325,12 +325,12 @@ theorem sphere_eversion :
   refine ⟨f, h₁, ?_, ?_, ?_/-h₅-/⟩
   · ext x
     rw [this (0, x) (by simp)]
-    convert formalEversion_zero E ω x
+    convert! formalEversion_zero E ω x
   · ext x
     rw [this (1, x) (by simp)]
-    convert formalEversion_one E ω x
+    convert! formalEversion_one E ω x
   · exact fun t ↦ {
-      contMDiff := ContMDiff.uncurry_left 𝓘(ℝ, ℝ) (𝓡 2) 𝓘(ℝ, E) h₁ t
+      contMDiff := h₁.uncurry_left 𝓘(ℝ, ℝ) (𝓡 2) 𝓘(ℝ, E) t
       diff_injective := h₅ t
     }
 

SphereEversion/Global/OneJetBundle.lean

@@ -112,7 +112,7 @@ variable (I I')
 instance (p : M × M') : FunLike (OneJetSpace I I' p) (TangentSpace I p.1) (TangentSpace I' p.2)
 where
   coe := fun φ ↦ φ.toFun
-  coe_injective' := fun _ _ h ↦ ContinuousLinearMap.ext (congrFun h)
+  coe_injective := fun _ _ h ↦ ContinuousLinearMap.ext (congrFun h)
 
 variable (M M')
 
@@ -243,7 +243,7 @@ theorem oneJetBundle_chart_source (x₀ : J¹MM') :
     PartialEquiv.trans_source,
     OpenPartialHomeomorph.prod_toPartialEquiv,
     PartialEquiv.prod_source,
-    OpenPartialHomeomorph.coe_coe,
+    OpenPartialHomeomorph.coe_toPartialEquiv,
     Trivialization.coe_coe,
     OpenPartialHomeomorph.refl_partialEquiv,
     PartialEquiv.refl_source,
@@ -278,10 +278,10 @@ end
 
 section
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
-[NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
-{H : Type*} [TopologicalSpace H] {H' : Type*} [TopologicalSpace H']
-{I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type*} [TopologicalSpace M]
-[ChartedSpace H M] {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞}
+  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
+  {H : Type*} [TopologicalSpace H] {H' : Type*} [TopologicalSpace H']
+  {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type*} [TopologicalSpace M]
+  [ChartedSpace H M] {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞}
 
 @[simp]
 lemma ContMDiffMap.coe_fst :
@@ -615,7 +615,7 @@ theorem oneJetBundle_model_space_chartAt (p : OneJetBundle I H I' H') :
       (Bundle.TotalSpace.toProd (H × H') (E →L[𝕜] E')).toPartialEquiv := by
   apply partialEquiv_eq_equiv
   · intro x
-    rw [OpenPartialHomeomorph.coe_coe, oneJetBundle_chartAt_apply p x,
+    rw [OpenPartialHomeomorph.coe_toPartialEquiv, oneJetBundle_chartAt_apply p x,
       inCoordinates_tangent_bundle_core_model_space]
     ext <;> rfl
   · simp_rw [oneJetBundle_chart_source, prodChartedSpace_chartAt, chartAt_self_eq,
@@ -641,7 +641,7 @@ theorem oneJetBundle_model_space_coe_chartAt_symm (p : OneJetBundle I H I' H') :
   ext x
   · rfl
   · rfl
-  · rw [← OpenPartialHomeomorph.coe_coe_symm, oneJetBundle_model_space_chartAt]
+  · rw [← OpenPartialHomeomorph.coe_toPartialEquiv_symm, oneJetBundle_model_space_chartAt]
     rfl
 
 variable (I I')

SphereEversion/Global/OneJetSec.lean

@@ -53,7 +53,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 
 instance : FunLike (OneJetSec I M I' M') M (OneJetBundle I M I' M') where
   coe := fun S x ↦ OneJetBundle.mk x (S.bs x) (S.ϕ x)
-  coe_injective' := by
+  coe_injective := by
     intro S T h
     dsimp at h
     ext x
@@ -186,7 +186,7 @@ instance : FunLike (FamilyOneJetSec I M I' M' J N) N (OneJetSec I M I' M') where
     { bs := S.bs t
       ϕ := S.ϕ t
       contMDiff' x := (S.contMDiff' (t, x)).comp x <| contMDiffAt_const.prodMk contMDiffAt_id }
-  coe_injective' := by
+  coe_injective := by
     intro S T h
     ext n : 2
     · exact (OneJetSec.mk.inj (congrFun h n)).1

SphereEversion/Global/ParametricityForFree.lean

@@ -142,11 +142,11 @@ theorem FamilyOneJetSec.uncurry_mem_relativize (S : FamilyOneJetSec I M I' M' IP
   -- Porting note: we are missing an ext lemma here.
   apply ContinuousLinearMap.ext_iff.2 (fun v ↦ ?_)
   change ((S.uncurry.ϕ (s, x)).comp (ContinuousLinearMap.inr ℝ EP E)) v = _
-  erw [S.uncurry_ϕ', ContinuousLinearMap.comp_apply, ContinuousLinearMap.add_apply,
+  erw [S.uncurry_ϕ', ContinuousLinearMap.comp_apply, add_apply,
     ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply, ContinuousLinearMap.coe_fst',
     ContinuousLinearMap.comp_apply]
   -- adaptation note: in Lean 4.28, all this proof was just `simp`
-  simp only [uncurry_bs, bs_eq_coe_bs, add_eq_right]
+  simp only [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
@@ -223,7 +223,7 @@ 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 ⊢
-  convert hR
+  convert! hR
   -- Porting note: we are missing an ext lemma here.
   apply ContinuousLinearMap.ext_iff.2 (fun v ↦ ?_)
   rw [S.curry_ϕ']
@@ -244,7 +244,7 @@ theorem curry_eq_iff_eq_uncurry {𝓕 : FamilyFormalSol J N (R.relativize IP P)}
   refine ⟨h.1, ?_⟩
   rw [𝓕.curry_ϕ', h.2, 𝓕₀.uncurry_ϕ']
   ext v
-  erw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.add_apply,
+  erw [ContinuousLinearMap.comp_apply, add_apply,
     ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply, ContinuousLinearMap.coe_fst',
     ContinuousLinearMap.comp_apply, ContinuousLinearMap.coe_snd', ContinuousLinearMap.map_zero,
     zero_add]

SphereEversion/Global/Relation.lean

@@ -71,11 +71,11 @@ structure FormalSol (R : RelMfld I M I' M') extends OneJetSec I M I' M' where
 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
+  coe_injective := by
     intro F G h
     ext x : 2
     · exact congrArg Prod.snd (congrArg Bundle.TotalSpace.proj (congrFun h x))
-    · simpa using (Bundle.TotalSpace.ext_iff.mp (congrFun h x)).2
+    · 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
@@ -191,7 +191,7 @@ theorem slice_mk_update {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'}
   ext1 w
   rw [mem_slice]
   change _ ↔ OneJetBundle.mk σ.proj.1 σ.proj.2 (DualPair.update p σ.snd w) ∈ R
-  convert Iff.rfl using 3
+  convert! Iff.rfl using 3
   rw [oneJetBundle_mk_snd, p.update_update]
 
 /-- A differential relation is ample if all its slices are ample sets. -/
@@ -219,7 +219,7 @@ structure FamilyFormalSol (R : RelMfld I M I' M') extends FamilyOneJetSec I M I'
 
 instance : FunLike (FamilyFormalSol J N R) N (FormalSol R) where
   coe := fun S n ↦ ⟨S.toFamilyOneJetSec n, S.is_sol' n⟩
-  coe_injective' := by
+  coe_injective := by
     intro S T
     rcases S with ⟨S, -⟩
     rcases T with ⟨T, -⟩
@@ -634,7 +634,7 @@ def OneJetBundle.embedding : OpenSmoothEmbedding IXY J¹XY IMN J¹MN where
     · rw [OpenSmoothEmbedding.invFun_comp_coe]
     · rw [OpenSmoothEmbedding.invFun_comp_coe]
     · ext x v; simp_rw [ContinuousLinearMap.comp_apply]
-      convert (φ.fderiv x).symm_apply_apply v
+      convert! (φ.fderiv x).symm_apply_apply v
       erw [φ.left_inv]; rfl
   isOpen_range := φ.isOpen_range_transfer ψ
   contMDiff_to := φ.smooth_transfer ψ

SphereEversion/Global/SmoothEmbedding.lean

@@ -253,11 +253,7 @@ def openSmoothEmbOfDiffeoSubsetChartTarget (x : M) {f : OpenPartialHomeomorph F
   left_inv' {y} := by
     obtain ⟨z, hz, hz'⟩ := hf₄ (mem_range_self y)
     have aux : f.symm (IF z) = y := by rw [hz']; exact f.left_inv (hf₁.symm ▸ mem_univ _)
-    simp only [← hz', (chartAt H x).right_inv hz, extChartAt, OpenPartialHomeomorph.extend,
-      PartialEquiv.coe_trans, OpenPartialHomeomorph.invFun_eq_coe,
-      ModelWithCorners.toPartialEquiv_coe, OpenPartialHomeomorph.coe_coe,
-      PartialEquiv.coe_trans_symm, OpenPartialHomeomorph.coe_coe_symm,
-      ModelWithCorners.left_inv, ModelWithCorners.toPartialEquiv_coe_symm, Function.comp_apply, aux]
+    simp [← hz', (chartAt H x).right_inv hz, aux]
   isOpen_range :=
     IsOpenMap.isOpen_range fun u hu ↦ by
       have aux : IsOpen (f '' u) := f.isOpen_image_of_subset_source hu (hf₁.symm ▸ subset_univ u)
@@ -347,7 +343,7 @@ theorem nice_atlas' {ι : Type*} {s : ι → Set M} (s_op : ∀ j, IsOpen <| s j
     rintro ⟨⟨x, r⟩, hxr⟩
     obtain ⟨hr : 0 < r, -, -⟩ := ht₂ _ hxr
     exact monotone_image (range_diffeomorphToNhd_subset_ball _ hr)
-  · simpa only [iUnion_coe_set] using ht₃
+  · simpa only [iUnion_coe_set] using! ht₃
 
 variable [Nonempty M]
 

SphereEversion/Global/TwistOneJetSec.lean

@@ -89,7 +89,7 @@ variable {I M V}
 
 instance : DFunLike (OneJetEuclSec I M V) M fun _  ↦ J¹[𝕜, E, I, M, V] where
   coe := OneJetEuclSec.toFun
-  coe_injective' := by
+  coe_injective := by
     intro S T h
     ext x <;> rw [h]
 
@@ -190,7 +190,7 @@ structure FamilyOneJetEuclSec where
 
 instance : FunLike (FamilyOneJetEuclSec I M V J N) (N × M) J¹[ℝ, E, I, M, V] where
   coe := FamilyOneJetEuclSec.toFun
-  coe_injective' := by
+  coe_injective := by
     intro S T h
     ext x <;> rw [h]
 
@@ -230,6 +230,6 @@ def familyTwist (s : OneJetEuclSec I M V) (i : N × M → V →L[ℝ] V')
     have : ContMDiffAt (J.prod I) _ ∞ (fun x : N × M  ↦ _) x₀ := s.contMDiff.comp contMDiff_snd x₀
     rw [contMDiffAt_one_jet_eucl_bundle'] at this
     refine (hi x₀).clm_comp ?_
-    convert this.2 <;> simp [s.is_sec]
+    convert! this.2 <;> simp [s.is_sec]
 
 end familyTwist

SphereEversion/InductiveConstructions.lean

@@ -170,16 +170,16 @@ theorem set_juggling {X : Type*} [TopologicalSpace X] [NormalSpace X] [T2Space X
     normal_exists_closure_subset hK U_op hKU
   refine ⟨K₁ ∪ closure (K₂ ∩ U'), K₂ \ U', U₁ ∪ U, U₂ \ K,
     U₁_op.union U_op, U₂_op.sdiff hK, ?_, K₂_cpct.diff U'_op, subset_union_left,
-    ?_, by gcongr, ?_, by grind, ?_, diff_subset⟩
+    ?_, by gcongr, ?_, by grind, ?_, sdiff_subset⟩
   · exact K₁_cpct.union (K₂_cpct.closure_of_subset inter_subset_left)
   · gcongr; grw [← hU'U]
     gcongr
     exact inter_subset_right
   · rw [union_assoc]
     congr
     apply subset_antisymm
-    · exact union_subset (K₂_cpct.isClosed.closure_subset_iff.mpr inter_subset_left) diff_subset
-    · calc K₂ = K₂ ∩ U' ∪ K₂ \ U' := (inter_union_diff K₂ U').symm
+    · exact union_subset (K₂_cpct.isClosed.closure_subset_iff.mpr inter_subset_left) sdiff_subset
+    · calc K₂ = K₂ ∩ U' ∪ K₂ \ U' := (inter_union_sdiff K₂ U').symm
         _     ⊆ closure (K₂ ∩ U') ∪ K₂ \ U' := union_subset_union_left (K₂ \ U') subset_closure
   · rw [union_comm]
 
@@ -366,7 +366,7 @@ theorem inductive_htpy_construction' {X Y : Type*} [TopologicalSpace X] {N : ℕ
         · rintro (rfl : t = 0)
           exact (lt_irrefl _ ((T_nonneg i.toNat).trans_lt ht)).elim
         · simpa only [mul_sub, neg_mul]
-            using hP₂ ((2 : ℝ) ^ (i.toNat + 1)) (-(2 : ℝ) ^ (i.toNat + 1) * T i.toNat)
+            using! hP₂ ((2 : ℝ) ^ (i.toNat + 1)) (-(2 : ℝ) ^ (i.toNat + 1) * T i.toNat)
               (t, x) (↿F') (h₂F' _)
     · intro hi x t ht
       rw [i.toNat_succ hi] at ht ⊢

SphereEversion/Local/Corrugation.lean

@@ -183,8 +183,8 @@ theorem fderiv_corrugated_map (hN : N ≠ 0) (hγ_diff : 𝒞 1 ↿γ) {f : E 
   ext v
   erw [fderiv_add (hf.differentiable (by simp)).differentiableAt
       ((corrugation.contDiff _ N hγ_diff).differentiable (by simp)).differentiableAt]
-  simp_rw [ContinuousLinearMap.add_apply, corrugation.fderiv_apply _ N hN hγ_diff, hfγ,
-    DualPair.update, ContinuousLinearMap.add_apply, p.π.comp_toSpanSingleton_apply, add_assoc]
+  simp_rw [add_apply, corrugation.fderiv_apply _ N hN hγ_diff, hfγ,
+    DualPair.update, add_apply, p.π.comp_toSpanSingleton_apply, add_assoc]
 
 open scoped ContDiff
 
@@ -195,7 +195,6 @@ theorem Remainder.smooth {γ : G → E → Loop F} (hγ_diff : 𝒞 ∞ ↿γ) {
   · let ψ : E → H × ℝ → F := fun x q ↦ (γ (g q.1) x).normalize q.2
     change  𝒞 ∞ fun q : H × ℝ ↦ ∂₁ ψ (x q.1) (q.1, q.2)
     refine (ContDiff.contDiff_top_partial_fst ?_).comp₂ hx.fst' (contDiff_fst.prodMk contDiff_snd)
-    dsimp [Loop.normalize]
     apply ContDiff.sub
     · apply hγ_diff.comp₃ hg.fst'.snd' contDiff_fst contDiff_snd.snd
     · apply contDiff_average

SphereEversion/Local/DualPair.lean

@@ -101,7 +101,7 @@ theorem update_self (p : DualPair E) (φ : E →L[ℝ] F) : p.update φ (φ p.v)
 @[simp]
 theorem update_update (p : DualPair E) (φ : E →L[ℝ] F) (w w' : F) :
     p.update (p.update φ w') w = p.update φ w := by
-  simp_rw [update, add_apply, coe_comp', (· ∘ ·), toSpanSingleton_apply, p.pairing, one_smul,
+  simp_rw [update, add_apply, coe_comp, (· ∘ ·), toSpanSingleton_apply, p.pairing, one_smul,
     add_sub_cancel, add_assoc, ← ContinuousLinearMap.add_comp, ← toSpanSingleton_add,
     sub_add_eq_add_sub, add_sub_cancel]
 

SphereEversion/Local/HPrinciple.lean

@@ -372,13 +372,12 @@ theorem improveStep_part_hol {N : ℝ} (hN : N ≠ 0) :
     rcases Submodule.mem_span_singleton.mp hu with ⟨l, rfl⟩
     rw [(D 𝓕'.f x).map_smul, (𝓕'.φ x).map_smul]
     apply congr_arg
-    erw [fderiv_𝓕', ContinuousLinearMap.add_apply, L.p.update_v, ContinuousLinearMap.add_apply,
-         L.p.update_v]
+    erw [fderiv_𝓕', add_apply, L.p.update_v, add_apply, L.p.update_v]
     rfl
   · intro u hu
     have hu_ker := L.hEp hu
-    erw [fderiv_𝓕', ContinuousLinearMap.add_apply, L.p.update_ker_pi _ _ hu_ker,
-      ContinuousLinearMap.add_apply, L.p.update_ker_pi _ _ hu_ker, hx u hu]
+    erw [fderiv_𝓕', add_apply, L.p.update_ker_pi _ _ hu_ker,
+      add_apply, L.p.update_ker_pi _ _ hu_ker, hx u hu]
 
 theorem improveStep_formalSol : ∀ᶠ N in atTop, ∀ t, (L.improveStep h N t).IsFormalSol R := by
   set γ := L.loop h
@@ -486,7 +485,7 @@ theorem RelLoc.FormalSol.improve (𝓕 : FormalSol R) (h_hol : ∀ᶠ x near L.C
       { L with
         E' := E' k.castSucc
         p := e.dualPair k
-        hEp := by simpa only [E', Module.Basis.dualPair] using e.flag_le_ker_dual k }
+        hEp := by simpa only [E', Module.Basis.dualPair] using! e.flag_le_ker_dual k }
     set H₁ : FormalSol R := (hH_sol 1).formalSol
     have h_span : E' k.succ = S.p.spanV ⊔ S.E' := e.flag_succ k
     have acc : S.Accepts R H₁ :=

SphereEversion/Local/OneJet.lean

@@ -57,7 +57,7 @@ variable {E F}
 
 instance : FunLike (JetSec E F) E (F × (E →L[ℝ] F)) where
   coe 𝓕 := fun x ↦ (𝓕.f x, 𝓕.φ x)
-  coe_injective' := by
+  coe_injective := by
     rintro ⟨⟩ ⟨⟩ h; congr
     exacts [congr_arg (Prod.fst ∘ ·) h, congr_arg (Prod.snd ∘ ·) h]
 
@@ -149,7 +149,7 @@ instance : FunLike (FamilyJetSec E F P) P (JetSec E F) where
       f_diff := S.f_diff.comp (contDiff_const.prodMk contDiff_id)
       φ := S.φ t
       φ_diff := S.φ_diff.comp (contDiff_const.prodMk contDiff_id) }
-  coe_injective' := by
+  coe_injective := by
     rintro ⟨⟩ ⟨⟩ h
     simp only [funext_iff, DFunLike.ext_iff, JetSec.mk_apply, Prod.ext_iff] at h
     congr <;> ext <;> simp [h]

SphereEversion/Local/ParametricHPrinciple.lean

@@ -151,7 +151,7 @@ theorem FamilyJetSec.uncurry_mem_relativize (S : FamilyJetSec E F P) {s : P} {x
       (ContinuousLinearMap.inr ℝ P E) = JetSec.φ (S s) x by
     rw [this]; rfl
   ext v
-  simp_rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.add_apply,
+  simp_rw [ContinuousLinearMap.comp_apply, add_apply,
     ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply, ContinuousLinearMap.coe_fst',
     ContinuousLinearMap.coe_snd', ContinuousLinearMap.map_zero, zero_add]
   rfl
@@ -248,7 +248,7 @@ theorem curry_eq_iff_eq_uncurry_loc {𝓕 : FamilyFormalSol G (R.relativize P)}
   change ((D (fun (z : P) ↦ 𝓕₀.toFamilyJetSec.f z x) s).comp (fst ℝ P E)
     + (𝓕₀.toFamilyJetSec.φ s x).comp (snd ℝ P E)).comp (inr ℝ P E) = ((𝓕₀ s) x).snd
   ext v
-  simp_rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.add_apply,
+  simp_rw [ContinuousLinearMap.comp_apply, add_apply,
     ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply, ContinuousLinearMap.coe_fst',
     ContinuousLinearMap.coe_snd', ContinuousLinearMap.map_zero, zero_add]
   rfl