no goals
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : Homotopy p₀ q₀
G : Homotopy p₁ q₁
x : ↑I × ↑I
⊢ (if ↑x.snd ≤ 1 / 2 then extend (eval F x.fst) (2 * ↑x.snd) else extend (eval G x.fst) (2 * ↑x.snd - 1)) =
    if h : ↑x.snd ≤ 1 / 2 then ↑(eval F x.fst) { val := 2 * ↑x.snd, property := (_ : 2 * ↑x.snd ∈ I) }
    else ↑(eval G x.fst) { val := 2 * ↑x.snd - 1, property := (_ : 2 * ↑x.snd - 1 ∈ I) }
split_ifs <;> exact Path.extend_extends _ _