Local loops

theorem local_loops [FiniteDimensional ℝ F] {x₀ : E} (hΩ_op : ∃ U ∈ 𝓝 x₀, IsOpen (Ω ∩ fst ⁻¹' U))    (hg : ContinuousAt g x₀) (hb : Continuous b)    (hconv : g x₀ ∈ convexHull ℝ (connectedComponentIn (Prod.mk x₀ ⁻¹' Ω) <| b x₀)) :    ∃ γ : E → ℝ → Loop F, ∃ U ∈ 𝓝 x₀, SurroundingFamilyIn g b γ U Ω := by  have hΩ_op_x₀ : IsOpen (connectedComponentIn (Prod.mk x₀ ⁻¹' Ω) <| b x₀) :=    (isOpen_slice_of_isOpen_over hΩ_op).connectedComponentIn  have b_in : b x₀ ∈ Prod.mk x₀ ⁻¹' Ω :=    connectedComponentIn_nonempty_iff.mp (convexHull_nonempty_iff.mp ⟨g x₀, hconv⟩)  have hΩ_conn : IsConnected (connectedComponentIn (Prod.mk x₀ ⁻¹' Ω) <| b x₀) :=    isConnected_connectedComponentIn_iff.mpr b_in  have hb_in : b x₀ ∈ (connectedComponentIn (Prod.mk x₀ ⁻¹' Ω) <| b x₀) :=    mem_connectedComponentIn b_in  rcases surrounding_loop_of_convexHull hΩ_op_x₀ hΩ_conn hconv hb_in with    ⟨γ, h1γ, h2γ, h3γ, h4γ, h5γ, h6γ⟩  have h5γ : ∀ t s : ℝ, γ t s ∈ mk x₀ ⁻¹' Ω := fun t s ↦ connectedComponentIn_subset _ _ (h5γ t s)  let δ : E → ℝ → Loop F := fun x t ↦ (b x - b x₀) +ᵥ γ t  have hδ : Continuous ↿δ := by    dsimp only [δ, HasUncurry.uncurry, Loop.vadd_apply]    fun_prop  have hδx₀ : ∀ t s, δ x₀ t s = γ t s := by    intro t s    simp only [δ, zero_add, Loop.vadd_apply, sub_self]  have hδs0 : ∀ x t, δ x t 0 = b x := by intro x t; simp [δ, h2γ]  have hδt0 : ∀ x s, δ x 0 s = b x := by intro x s; simp [δ, h3γ]  have hδt1 : ∀ x t s, δ x (projI t) s = δ x t s := by intro x t s; simp [δ, h4γ]  have hδΩ : ∀ᶠ x in 𝓝 x₀, ∀ t ∈ I, ∀ s ∈ I, (x, δ x t s) ∈ Ω := by    rcases hΩ_op with ⟨U, hUx₀, hU⟩    -- todo: this is nicer with `IsCompact.eventually_forall_of_forall_eventually` twice, but then    -- we need the continuity of `δ` with the arguments reassociated differently.    have : ∀ᶠ x : E in 𝓝 x₀, ∀ ts : ℝ × ℝ, ts ∈ I ×ˢ I → (x, δ x ts.1 ts.2) ∈ Ω := by      apply (isCompact_Icc.prod isCompact_Icc).eventually_forall_mem      · fun_prop      · rintro ⟨t, s⟩ _        rw [hδx₀]        change Ω ∈ 𝓝 (x₀, γ t s)        exact mem_nhds_iff.mpr          ⟨_, inter_subset_left, hU, ⟨h5γ t s, show x₀ ∈ U from mem_of_mem_nhds hUx₀⟩⟩    refine this.mono ?_; intro x h t ht s hs; exact h (t, s) ⟨ht, hs⟩  have hδsurr : ∀ᶠ x in 𝓝 x₀, (δ x 1).Surrounds (g x) := by    rcases h6γ with ⟨p, w, h⟩    obtain ⟨W, hW⟩ := smooth_surroundingPts h    let c : E → F × (Fin (d + 1) → F) := fun x ↦ (g x, δ x 1 ∘ p)    have hc : ContinuousAt c x₀ := by fun_prop    have hcx₀ : c x₀ = (g x₀, γ 1 ∘ p) := by      simp [c, δ]    rw [← hcx₀] at hW    filter_upwards [hc.tendsto.eventually hW]    rintro x ⟨_, hx⟩    exact ⟨_, _, hx⟩  exact ⟨δ, _, hδΩ.and hδsurr, ⟨⟨hδs0, hδt0, hδt1, fun x ↦ And.right, hδ⟩, fun x ↦ And.left⟩⟩