Rel Loc Formal Sol improve

theorem RelLoc.FormalSol.improve (𝓕 : FormalSol R) (h_hol : ∀ᶠ x near L.C, 𝓕.IsHolonomicAt x) :    ∃ H : HtpyJetSec E F,      (∀ᶠ t near Iic 0, H t = 𝓕) ∧        (∀ᶠ t near Ici 1, H t = H 1) ∧          (∀ᶠ x near L.C, ∀ t, H t x = 𝓕 x) ∧            (∀ x ∉ L.K₁, ∀ t, H t x = 𝓕 x) ∧              (∀ x t, ‖(H t).f x - 𝓕.f x‖ ≤ ε) ∧                (∀ t, (H t).IsFormalSol R) ∧ ∀ᶠ x near L.K₀, (H 1).IsHolonomicAt x := by  let n := Module.finrank ℝ E  let e := Module.finBasis ℝ E  let E' := e.flag  suffices    ∀ k : Fin (n + 1),      ∀ δ > (0 : ℝ),        ∃ H : HtpyJetSec E F,          (∀ᶠ t near Iic 0, H t = 𝓕) ∧            (∀ᶠ t near Ici 1, H t = H 1) ∧              (∀ᶠ x near L.C, ∀ t, H t x = 𝓕 x) ∧                (∀ x ∉ L.K₁, ∀ t, H t x = 𝓕 x) ∧                  (∀ x t, ‖(H t).f x - 𝓕.f x‖ ≤ δ) ∧                    (∀ t, (H t).IsFormalSol R) ∧ ∀ᶠ x near L.K₀, (H 1).IsPartHolonomicAt (E' k) x by    simpa only [show E' (Fin.last n) = ⊤ from e.flag_last, JetSec.isPartHolonomicAt_top] using      this (Fin.last n) ε ε_pos  intro k  induction k using Fin.induction with  | zero =>    intro δ δ_pos    use 𝓕.toJetSec.constHtpy    simp [show E' 0 = ⊥ from e.flag_zero, le_of_lt δ_pos]  | succ k HH =>    rintro δ δ_pos    rcases HH (δ / 2) (half_pos δ_pos) with ⟨H, hH₀, _, hHC, hHK₁, hHc0, hH_sol, hH_hol⟩; clear HH    let S : StepLandscape E :=      { 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 }    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₁ :=      { h_op        hK₀ := hH_hol.mono (fun x hx ↦ hx)        hShort := fun x ↦ h_ample.isShortAt H₁ S.p x        hC := by          apply h_hol.congr (FormalSol.isHolonomicAt_congr _ _ _)          apply hHC.mono (fun x h ↦ (h 1).symm) }    have hH₁_rel_C : ∀ᶠ x : E near S.C, H₁ x = 𝓕 x := hHC.mono (fun x hx ↦ hx _)    have hH₁_K₁ : ∀ x ∉ (L.K₁), H₁ x = 𝓕 x := by      intro x hx      apply hHK₁ x hx    obtain ⟨N, ⟨hN_close, hN_sol⟩, hNneq⟩ :=      (((improveStep_c0_close acc <| half_pos δ_pos).and (improveStep_formalSol acc)).and <|          eventually_ne_atTop (0 : ℝ)).exists    have glue : H 1 = S.improveStep acc N 0 := by      rw [improveStep_rel_t_eq_0]      rfl    refine ⟨H.comp (S.improveStep acc N) glue, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩    · apply (H.comp_le_0 _ _).mono      · intro t ht        rw [ht]        exact hH₀.self_of_nhdsSet 0 self_mem_Iic    -- t = 0    · apply (H.comp_ge_1 _ _).mono      · intro t ht        rw [ht, H.comp_1]    · -- rel C      apply (hHC.and <| hH₁_rel_C.and <| improveStep_rel_C acc N).mono      rintro x ⟨hx, hx', hx''⟩ t      by_cases ht : t ≤ 1 / 2      · simp only [ht, hx, HtpyJetSec.comp_of_le]      · simp only [ht, hx', hx'', HtpyJetSec.comp_of_not_le, not_false_iff]    · -- rel K₁      intro x hx t      by_cases ht : t ≤ 1 / 2      · simp only [ht, hx, hHK₁, HtpyJetSec.comp_of_le, not_false_iff]      · simp only [ht, hx, hH₁_K₁, improveStep_rel_compl_K₁, HtpyJetSec.comp_of_not_le,          not_false_iff, S]    · -- C⁰-close      intro x t      by_cases ht : t ≤ 1 / 2      · apply le_trans _ (half_le_self <| le_of_lt δ_pos)        simp only [ht, hHc0, HtpyJetSec.comp_of_le]      · simp only [ht, HtpyJetSec.comp_of_not_le, not_false_iff]        rw [← add_halves δ]        exact (norm_sub_le_norm_sub_add_norm_sub _ _ _).trans <| add_le_add (hN_close _ _)          (hHc0 _ _)    · -- formal solution      intro t      by_cases ht : t ≤ 1 / 2      · simp only [ht, hH_sol, HtpyJetSec.comp_of_le]      · simp only [ht, hN_sol, HtpyJetSec.comp_of_not_le, not_false_iff]    · -- part-hol E' (k + 1)      rw [h_span, HtpyJetSec.comp_1]      apply improveStep_part_hol acc hNneq