case inr
F✝ : Type ?u.203878
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
x : ↑I × X
h✝ : ¬↑x.fst ≤ 1 / 2
⊢ ↑(↑(curry G) { val := 2 * ↑x.fst - 1, property := ?inr.hx }) x.snd =
    ↑G ({ val := 2 * ↑x.fst - 1, property := (_ : 2 * ↑x.fst - 1 ∈ I) }, x.snd)

case inr.hx
F✝ : Type ?u.203878
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
x : ↑I × X
h✝ : ¬↑x.fst ≤ 1 / 2
⊢ 2 * ↑x.fst - 1 ∈ Set.Icc 0 1
case inr
F✝ : Type ?u.203878
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
x : ↑I × X
h✝ : ¬↑x.fst ≤ 1 / 2
⊢ ↑(↑(extend G) (2 * ↑x.fst - 1)) x.snd = ↑G ({ val := 2 * ↑x.fst - 1, property := (_ : 2 * ↑x.fst - 1 ∈ I) }, x.snd)
rw [extend, ContinuousMap.coe_IccExtend, Set.IccExtend_of_mem]
no goals
case inr
F✝ : Type ?u.203878
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
x : ↑I × X
h✝ : ¬↑x.fst ≤ 1 / 2
⊢ ↑(↑(curry G) { val := 2 * ↑x.fst - 1, property := ?inr.hx }) x.snd =
    ↑G ({ val := 2 * ↑x.fst - 1, property := (_ : 2 * ↑x.fst - 1 ∈ I) }, x.snd)

case inr.hx
F✝ : Type ?u.203878
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
x : ↑I × X
h✝ : ¬↑x.fst ≤ 1 / 2
⊢ 2 * ↑x.fst - 1 ∈ Set.Icc 0 1
rfl