no goals
X : Type u_1
Y : Type ?u.226697
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.226712
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
⊢ (if ↑t ≤ 1 / 2 then extend γ (2 * ↑t) else extend γ' (2 * ↑t - 1)) =
    if h : ↑t ≤ 1 / 2 then ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
    else ↑γ' { val := 2 * ↑t - 1, property := (_ : 2 * ↑t - 1 ∈ I) }
split_ifs <;> rw [extend_extends]