no goals
X✝ : Type ?u.471660
Y : Type ?u.471663
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.471678
γ✝ : Path x y
X : Type ?u.471727
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
⊢ extend γ (min t t) = extend γ t
rw [min_self]
case a.h
X✝ : Type ?u.471660
Y : Type ?u.471663
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.471678
γ✝ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
⊢ ↑(truncate γ t t) x =
    ↑(cast (refl (extend γ t)) (_ : extend γ (min t t) = extend γ t) (_ : extend γ t = extend γ t)) x
X✝ : Type ?u.471660
Y : Type ?u.471663
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.471678
γ✝ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
⊢ truncate γ t t = cast (refl (extend γ t)) (_ : extend γ (min t t) = extend γ t) (_ : extend γ t = extend γ t)
ext x
case a.h
X✝ : Type ?u.471660
Y : Type ?u.471663
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.471678
γ✝ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
⊢ ↑(truncate γ t t) x = ↑(refl (extend γ t)) x
case a.h
X✝ : Type ?u.471660
Y : Type ?u.471663
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.471678
γ✝ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
⊢ ↑(truncate γ t t) x =
    ↑(cast (refl (extend γ t)) (_ : extend γ (min t t) = extend γ t) (_ : extend γ t = extend γ t)) x
rw [cast_coe]
case a.h
X✝ : Type ?u.471660
Y : Type ?u.471663
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.471678
γ✝ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
⊢ extend γ (if (if ↑x ≤ t then t else ↑x) ≤ t then if ↑x ≤ t then t else ↑x else t) = extend γ t
case a.h
X✝ : Type ?u.471660
Y : Type ?u.471663
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.471678
γ✝ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
⊢ ↑(truncate γ t t) x = ↑(refl (extend γ t)) x
simp only [truncate, FunLike.coe, refl, min_def, max_def]
no goals
case a.h
X✝ : Type ?u.471660
Y : Type ?u.471663
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.471678
γ✝ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
⊢ extend γ (if (if ↑x ≤ t then t else ↑x) ≤ t then if ↑x ≤ t then t else ↑x else t) = extend γ t
split_ifs with h₁ h₂ <;> congr