Sf Homotopy in

theorem sfHomotopy_in' {ι} (h₀ : SurroundingFamily g b γ₀ U) (h₁ : SurroundingFamily g b γ₁ U)    (τ : ι → ℝ) (x : ι → E) (i : ι) {V : Set E} (hx : x i ∈ V) {t : ℝ} (ht : t ∈ I) {s : ℝ}    (h_in₀ : ∀ i, x i ∈ V → ∀ t ∈ I, ∀ (s : ℝ), τ i ≠ 1 → (x i, γ₀ (x i) t s) ∈ Ω)    (h_in₁ : ∀ i, x i ∈ V → ∀ t ∈ I, ∀ (s : ℝ), τ i ≠ 0 → (x i, γ₁ (x i) t s) ∈ Ω) :    (x i, sfHomotopy h₀ h₁ (τ i) (x i) t s) ∈ Ω := by  by_cases hτ0 : τ i = 0  · simp only [hτ0, sfHomotopy_zero]; exact h_in₀ i hx t ht s (by norm_num [hτ0])  by_cases hτ1 : τ i = 1  · simp only [hτ1, sfHomotopy_one]; exact h_in₁ i hx t ht s (by norm_num [hτ1])  generalize hy : sfHomotopy h₀ h₁ (τ i) (x i) t s = y  have h2y : y ∈ range (sfHomotopy h₀ h₁ (τ i) (x i) t) := by rw [← hy]; exact mem_range_self _  rw [sfHomotopy, Loop.range_ofPath, projI_eq_self.mpr ht] at h2y  replace h2y := range_strans_subset h2y  rcases h2y with (⟨s', rfl⟩ | ⟨s', rfl⟩)  · exact h_in₀ _ hx _ (unitInterval.mul_mem ρ_mem_I ht) _ hτ1  · exact h_in₁ _ hx _ (unitInterval.mul_mem ρ_mem_I ht) _ hτ0