X✝ : Type ?u.458739
Y : Type ?u.458742
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.458757
γ✝ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ range ↑(truncate γ t₀ t₁) ⊆ range (extend γ)
X✝ : Type ?u.458739
Y : Type ?u.458742
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.458757
γ✝ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ range ↑(truncate γ t₀ t₁) ⊆ range ↑γ
rw [← γ.extend_range]
X✝ : Type ?u.458739
Y : Type ?u.458742
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.458757
γ✝ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ ∀ (x : ℝ) (h : x ∈ I), ↑(truncate γ t₀ t₁) { val := x, property := h } ∈ range (extend γ)
X✝ : Type ?u.458739
Y : Type ?u.458742
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.458757
γ✝ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ range ↑(truncate γ t₀ t₁) ⊆ range (extend γ)
simp only [range_subset_iff, SetCoe.exists, SetCoe.forall]
X✝ : Type ?u.458739
Y : Type ?u.458742
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.458757
γ✝ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ x : ℝ
_hx : x ∈ I
⊢ ↑(truncate γ t₀ t₁) { val := x, property := _hx } ∈ range (extend γ)
X✝ : Type ?u.458739
Y : Type ?u.458742
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.458757
γ✝ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ ∀ (x : ℝ) (h : x ∈ I), ↑(truncate γ t₀ t₁) { val := x, property := h } ∈ range (extend γ)
intro x _hx
no goals
X✝ : Type ?u.458739
Y : Type ?u.458742
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.458757
γ✝ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ x : ℝ
_hx : x ∈ I
⊢ ↑(truncate γ t₀ t₁) { val := x, property := _hx } ∈ range (extend γ)
simp only [FunLike.coe, Path.truncate, mem_range_self]