Rel Mfld Satisfies HPrinciple With bs

theorem RelMfld.SatisfiesHPrincipleWith.bs {R : RelMfld I M IX X} {C : Set (P × M)} {ε : M → ℝ}    (h : R.SatisfiesHPrincipleWith IP C ε) (𝓕₀ : FamilyFormalSol IP P R)    (h2 : ∀ᶠ p : P × M near C, (𝓕₀ p.1).toOneJetSec.IsHolonomicAt p.2) :    ∃ f : P → M → X,      (CMDiff ∞ (uncurry f)) ∧        (∀ᶠ p : P × M near C, f p.1 p.2 = 𝓕₀.bs p.1 p.2) ∧          (∀ p m, dist (f p m) ((𝓕₀ p).bs m) ≤ ε m) ∧ ∀ p m, oneJetExt I IX (f p) m ∈ R := by  rcases h 𝓕₀ h2 with ⟨𝓕, _, h₂, h₃, h₄⟩  refine ⟨fun s ↦ (𝓕 (1, s)).bs, ?_, ?_, ?_, ?_⟩  · let j : C^∞⟮IP, P; 𝓘(ℝ, ℝ).prod IP, ℝ × P⟯ :=      ⟨fun p ↦ (1, p), contMDiff_const.prodMk contMDiff_id⟩    rw [show        (uncurry fun s ↦ (𝓕 (1, s)).bs) =          Prod.snd ∘ π _ (OneJetSpace I IX) ∘ fun p : P × M ↦ 𝓕.reindex j p.1 p.2          by ext; rfl]    exact (𝓕.reindex j).toFamilyOneJetSec.contMDiff_bs  · refine h₃.mono fun x hx ↦ ?_    simp_rw [OneJetSec.bs_eq, FormalSol.toOneJetSec_coe, hx, FamilyOneJetSec.bs_eq,      𝓕₀.toFamilyOneJetSec_coe]  · exact fun p m ↦ h₄ ..  · intro p m    suffices oneJetExt I IX (𝓕 (1, p)).bs m = (𝓕.toFamilyOneJetSec (1, p)) m by      rw [this]      exact 𝓕.is_sol' (1, p) m    exact OneJetSec.isHolonomicAt_iff.mp (h₂ p m)