Extend loops

theorem extend_loops {U₀ U₁ K₀ K₁ : Set E} (hU₀ : IsOpen U₀) (hU₁ : IsOpen U₁) (hK₀ : IsClosed K₀)    (hK₁ : IsClosed K₁) (hKU₀ : K₀ ⊆ U₀) (hKU₁ : K₁ ⊆ U₁) {γ₀ γ₁ : E → ℝ → Loop F}    (h₀ : SurroundingFamilyIn g b γ₀ U₀ Ω) (h₁ : SurroundingFamilyIn g b γ₁ U₁ Ω) :    ∃ U ∈ 𝓝ˢ (K₀ ∪ K₁),      ∃ γ : E → ℝ → Loop F,        SurroundingFamilyIn g b γ U Ω ∧          (∀ᶠ x in 𝓝ˢ K₀, γ x = γ₀ x) ∧ ∀ᶠ x in 𝓝ˢ (U₁ᶜ), γ x = γ₀ x := by  obtain ⟨V₀, hV₀, hKV₀, hVU₀⟩ := normal_exists_closure_subset hK₀ hU₀ hKU₀  let L₁ := K₁ \ U₀  have hL₁ : IsClosed L₁ := hK₁.sdiff hU₀  have hV₀L₁ : Disjoint (closure V₀) L₁ := disjoint_sdiff_self_right.mono hVU₀ Subset.rfl  obtain ⟨V₂, hV₂, hLV₂, h2V₂⟩ :=    normal_exists_closure_subset hL₁ (isClosed_closure.isOpen_compl.inter hU₁)      (subset_inter (subset_compl_iff_disjoint_left.mpr hV₀L₁) <| sdiff_subset.trans hKU₁)  obtain ⟨V₁, hV₁, hLV₁, hV₁₂⟩ := normal_exists_closure_subset hL₁ hV₂ hLV₂  rw [subset_inter_iff, subset_compl_iff_disjoint_left] at h2V₂  rcases h2V₂ with ⟨hV₀₂, hV₂U₁⟩  have hVU₁ : V₁ ⊆ U₁ := subset_closure.trans (hV₁₂.trans <| subset_closure.trans hV₂U₁)  have hdisj : Disjoint (closure V₀ ∪ V₂ᶜ) (closure V₁) := by    refine Disjoint.union_left (hV₀₂.mono_right (hV₁₂.trans subset_closure)) ?_    rw [← subset_compl_iff_disjoint_left, compl_compl]; exact hV₁₂  refine ⟨V₀ ∪ U₁ ∩ U₀ ∪ V₁, ((hV₀.union <| hU₁.inter hU₀).union hV₁).mem_nhdsSet.mpr ?_, ?_⟩  · refine union_subset (hKV₀.trans <| subset_union_left.trans <| subset_union_left) ?_    rw [← inter_union_sdiff K₁];    exact union_subset_union ((inter_subset_inter_left _ hKU₁).trans <| subset_union_right) hLV₁  obtain ⟨ρ, h0ρ, h1ρ, -⟩ :=    exists_continuous_zero_one_of_isClosed (isClosed_closure.union hV₂.isClosed_compl)      isClosed_closure hdisj  let h₀' : SurroundingFamilyIn g b γ₀ (U₁ ∩ U₀) Ω := h₀.mono inter_subset_right  let h₁' : SurroundingFamilyIn g b γ₁ (U₁ ∩ U₀) Ω := h₁.mono inter_subset_left  let γ := sfHomotopy h₀'.to_sf h₁'.to_sf  have hγ : ∀ τ, SurroundingFamilyIn g b (γ τ) (U₁ ∩ U₀) Ω := surroundingFamilyIn_sfHomotopy h₀' h₁'  have heq1 : ∀ x ∈ closure V₀ ∪ V₂ᶜ, γ (ρ x) x = γ₀ x := by    intro x hx    simp_rw [γ, h0ρ hx, Pi.zero_apply, sfHomotopy_zero]  have heq2 : ∀ x ∈ V₀, γ (ρ x) x = γ₀ x := fun x hx ↦    heq1 x (subset_closure.trans subset_union_left hx)  refine ⟨fun x t ↦ γ (ρ x) x t, ?_, ?_, ?_⟩  · refine ⟨⟨fun x ↦ (hγ <| ρ x).base x, fun x ↦ (hγ <| ρ x).t₀ x, fun x ↦ (hγ <| ρ x).projI x,      ?_, ?_⟩, ?_⟩    · rintro x ((hx | hx) | hx)      · simp_rw [heq2 x hx, h₀.surrounds x (hVU₀ <| subset_closure hx)]      · simp_rw [γ]        exact (hγ <| ρ x).surrounds x hx      · simp_rw [γ, h1ρ (subset_closure hx), Pi.one_apply, sfHomotopy_one, h₁.surrounds x (hVU₁ hx)]    · fun_prop    · intro x hx t ht s _; refine sfHomotopy_in' _ _ _ id _ hx ht ?_ ?_      · intro x hx t _ht s hρx; refine h₀.val_in ?_; rcases hx with ((hx | ⟨-, hx⟩) | hx)        · exact (subset_closure.trans hVU₀) hx        · exact hx        · exact (hρx <| h1ρ <| subset_closure hx).elim      · intro x hx t _ht s hρx; refine h₁.val_in ?_; rcases hx with ((hx | ⟨hx, -⟩) | hx)        · exact (hρx <| h0ρ <| subset_closure.trans subset_union_left hx).elim        · exact hx        · exact hVU₁ hx  · exact eventually_of_mem (hV₀.mem_nhdsSet.mpr hKV₀) heq2  · exact eventually_of_mem      (isClosed_closure.isOpen_compl.mem_nhdsSet.mpr <| compl_subset_compl.mpr hV₂U₁)      fun x hx ↦ heq1 x <| mem_union_right _ <| compl_subset_compl.mpr subset_closure hx