no goals
X✝ : Type ?u.481302
Y : Type ?u.481305
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.481320
γ✝ : Path x y
X : Type ?u.481369
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
⊢ extend γ (min 0 1) = a
simp [zero_le_one, extend_zero]
no goals
X✝ : Type ?u.481302
Y : Type ?u.481305
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.481320
γ✝ : Path x y
X : Type ?u.481369
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
⊢ extend γ 1 = b
simp
case a.h
X✝ : Type ?u.481302
Y : Type ?u.481305
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.481320
γ✝ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
⊢ ↑(truncate γ 0 1) x = ↑(cast γ (_ : extend γ (min 0 1) = a) (_ : extend γ 1 = b)) x
X✝ : Type ?u.481302
Y : Type ?u.481305
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.481320
γ✝ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
⊢ truncate γ 0 1 = cast γ (_ : extend γ (min 0 1) = a) (_ : extend γ 1 = b)
ext x
case a.h
X✝ : Type ?u.481302
Y : Type ?u.481305
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.481320
γ✝ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
⊢ ↑(truncate γ 0 1) x = ↑γ x
case a.h
X✝ : Type ?u.481302
Y : Type ?u.481305
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.481320
γ✝ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
⊢ ↑(truncate γ 0 1) x = ↑(cast γ (_ : extend γ (min 0 1) = a) (_ : extend γ 1 = b)) x
rw [cast_coe]
case a.h
X✝ : Type ?u.481302
Y : Type ?u.481305
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.481320
γ✝ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
this : ↑x ∈ Icc 0 1
⊢ ↑(truncate γ 0 1) x = ↑γ x
case a.h
X✝ : Type ?u.481302
Y : Type ?u.481305
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.481320
γ✝ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
⊢ ↑(truncate γ 0 1) x = ↑γ x
have : ↑x ∈ (Icc 0 1 : Set ℝ) := x.2
no goals
case a.h
X✝ : Type ?u.481302
Y : Type ?u.481305
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.481320
γ✝ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
this : ↑x ∈ Icc 0 1
⊢ ↑(truncate γ 0 1) x = ↑γ x
rw [truncate, coe_mk_mk, max_eq_left this.1, min_eq_left this.2, extend_extends']