[GOAL]
F : Type u_1
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₁ : C(X, Y)
f g : Homotopy f₀ f₁
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
F : Type u_1
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₁ : C(X, Y)
g : Homotopy f₀ f₁
toFun✝ : ↑I × X → Y
continuous_toFun✝ : Continuous toFun✝
map_zero_left✝ : ∀ (x : X), ContinuousMap.toFun (ContinuousMap.mk toFun✝) (0, x) = ↑f₀ x
map_one_left✝ : ∀ (x : X), ContinuousMap.toFun (ContinuousMap.mk toFun✝) (1, x) = ↑f₁ x
h :
  (fun f => f.toFun)
      { toContinuousMap := ContinuousMap.mk toFun✝, map_zero_left := map_zero_left✝, map_one_left := map_one_left✝ } =
    (fun f => f.toFun) g
⊢ { toContinuousMap := ContinuousMap.mk toFun✝, map_zero_left := map_zero_left✝, map_one_left := map_one_left✝ } = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
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₁ : C(X, Y)
toFun✝¹ : ↑I × X → Y
continuous_toFun✝¹ : Continuous toFun✝¹
map_zero_left✝¹ : ∀ (x : X), ContinuousMap.toFun (ContinuousMap.mk toFun✝¹) (0, x) = ↑f₀ x
map_one_left✝¹ : ∀ (x : X), ContinuousMap.toFun (ContinuousMap.mk toFun✝¹) (1, x) = ↑f₁ x
toFun✝ : ↑I × X → Y
continuous_toFun✝ : Continuous toFun✝
map_zero_left✝ : ∀ (x : X), ContinuousMap.toFun (ContinuousMap.mk toFun✝) (0, x) = ↑f₀ x
map_one_left✝ : ∀ (x : X), ContinuousMap.toFun (ContinuousMap.mk toFun✝) (1, x) = ↑f₁ x
h :
  (fun f => f.toFun)
      { toContinuousMap := ContinuousMap.mk toFun✝¹, map_zero_left := map_zero_left✝¹,
        map_one_left := map_one_left✝¹ } =
    (fun f => f.toFun)
      { toContinuousMap := ContinuousMap.mk toFun✝, map_zero_left := map_zero_left✝, map_one_left := map_one_left✝ }
⊢ { toContinuousMap := ContinuousMap.mk toFun✝¹, map_zero_left := map_zero_left✝¹, map_one_left := map_one_left✝¹ } =
    { toContinuousMap := ContinuousMap.mk toFun✝, map_zero_left := map_zero_left✝, map_one_left := map_one_left✝ }
[PROOFSTEP]
congr
[GOAL]
F✝ : Type u_1
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₁ : C(X, Y)
F : Homotopy f₀ f₁
t : ℝ
ht : t ≤ 0
x : X
⊢ ↑(↑(extend F) t) x = ↑f₀ x
[PROOFSTEP]
rw [← F.apply_zero]
[GOAL]
F✝ : Type u_1
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₁ : C(X, Y)
F : Homotopy f₀ f₁
t : ℝ
ht : t ≤ 0
x : X
⊢ ↑(↑(extend F) t) x = ↑F (0, x)
[PROOFSTEP]
exact ContinuousMap.congr_fun (Set.IccExtend_of_le_left (zero_le_one' ℝ) F.curry ht) x
[GOAL]
F✝ : Type u_1
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₁ : C(X, Y)
F : Homotopy f₀ f₁
t : ℝ
ht : 1 ≤ t
x : X
⊢ ↑(↑(extend F) t) x = ↑f₁ x
[PROOFSTEP]
rw [← F.apply_one]
[GOAL]
F✝ : Type u_1
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₁ : C(X, Y)
F : Homotopy f₀ f₁
t : ℝ
ht : 1 ≤ t
x : X
⊢ ↑(↑(extend F) t) x = ↑F (1, x)
[PROOFSTEP]
exact ContinuousMap.congr_fun (Set.IccExtend_of_right_le (zero_le_one' ℝ) F.curry ht) x
[GOAL]
F✝ : Type u_1
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₁ : C(X, Y)
F : Homotopy f₀ f₁
⊢ ∀ (x : X), ContinuousMap.toFun (ContinuousMap.mk fun x => ↑F (σ x.fst, x.snd)) (0, x) = ↑f₁ x
[PROOFSTEP]
norm_num
[GOAL]
F✝ : Type u_1
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₁ : C(X, Y)
F : Homotopy f₀ f₁
⊢ ∀ (x : X), ContinuousMap.toFun (ContinuousMap.mk fun x => ↑F (σ x.fst, x.snd)) (1, x) = ↑f₀ x
[PROOFSTEP]
norm_num
[GOAL]
F✝ : Type u_1
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₁ : C(X, Y)
F : Homotopy f₀ f₁
⊢ symm (symm F) = F
[PROOFSTEP]
ext
[GOAL]
case h
F✝ : Type u_1
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₁ : C(X, Y)
F : Homotopy f₀ f₁
x✝ : ↑I × X
⊢ ↑(symm (symm F)) x✝ = ↑F x✝
[PROOFSTEP]
simp
[GOAL]
F✝ : Type u_1
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₂
⊢ Continuous fun x =>
    if ↑x.fst ≤ 1 / 2 then ↑(↑(extend F) (2 * ↑x.fst)) x.snd else ↑(↑(extend G) (2 * ↑x.fst - 1)) x.snd
[PROOFSTEP]
refine'
  continuous_if_le (continuous_induced_dom.comp continuous_fst) continuous_const
    (F.continuous.comp (by continuity)).continuousOn (G.continuous.comp (by continuity)).continuousOn _
[GOAL]
F✝ : Type u_1
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₂
⊢ Continuous fun x => (Set.projIcc 0 1 extend.proof_1 (2 * ↑x.fst), x.snd)
[PROOFSTEP]
continuity
[GOAL]
F✝ : Type u_1
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₂
⊢ Continuous fun x => (Set.projIcc 0 1 extend.proof_1 (2 * ↑x.fst - 1), x.snd)
[PROOFSTEP]
continuity
[GOAL]
F✝ : Type u_1
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), ↑x.fst = 1 / 2 → ↑(↑(extend F) (2 * ↑x.fst)) x.snd = ↑(↑(extend G) (2 * ↑x.fst - 1)) x.snd
[PROOFSTEP]
rintro x hx
[GOAL]
F✝ : Type u_1
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
hx : ↑x.fst = 1 / 2
⊢ ↑(↑(extend F) (2 * ↑x.fst)) x.snd = ↑(↑(extend G) (2 * ↑x.fst - 1)) x.snd
[PROOFSTEP]
rw [hx]
[GOAL]
F✝ : Type u_1
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
hx : ↑x.fst = 1 / 2
⊢ ↑(↑(extend F) (2 * (1 / 2))) x.snd = ↑(↑(extend G) (2 * (1 / 2) - 1)) x.snd
[PROOFSTEP]
norm_num
[GOAL]
F✝ : Type u_1
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 : X
⊢ ContinuousMap.toFun
      (ContinuousMap.mk fun x =>
        if ↑x.fst ≤ 1 / 2 then ↑(↑(extend F) (2 * ↑x.fst)) x.snd else ↑(↑(extend G) (2 * ↑x.fst - 1)) x.snd)
      (0, x) =
    ↑f₀ x
[PROOFSTEP]
norm_num
[GOAL]
F✝ : Type u_1
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 : X
⊢ ContinuousMap.toFun
      (ContinuousMap.mk fun x =>
        if ↑x.fst ≤ 1 / 2 then ↑(↑(extend F) (2 * ↑x.fst)) x.snd else ↑(↑(extend G) (2 * ↑x.fst - 1)) x.snd)
      (1, x) =
    ↑f₂ x
[PROOFSTEP]
norm_num
[GOAL]
F✝ : Type u_1
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
⊢ (if ↑x.fst ≤ 1 / 2 then ↑(↑(extend F) (2 * ↑x.fst)) x.snd else ↑(↑(extend G) (2 * ↑x.fst - 1)) x.snd) =
    if h : ↑x.fst ≤ 1 / 2 then ↑F ({ val := 2 * ↑x.fst, property := (_ : 2 * ↑x.fst ∈ I) }, x.snd)
    else ↑G ({ val := 2 * ↑x.fst - 1, property := (_ : 2 * ↑x.fst - 1 ∈ I) }, x.snd)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
F✝ : Type u_1
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 F) (2 * ↑x.fst)) x.snd = ↑F ({ val := 2 * ↑x.fst, property := (_ : 2 * ↑x.fst ∈ I) }, x.snd)
[PROOFSTEP]
rw [extend, ContinuousMap.coe_IccExtend, Set.IccExtend_of_mem]
[GOAL]
case pos
F✝ : Type u_1
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 F) { val := 2 * ↑x.fst, property := ?pos.hx✝ }) x.snd =
    ↑F ({ val := 2 * ↑x.fst, property := (_ : 2 * ↑x.fst ∈ I) }, x.snd)
case pos.hx
F✝ : Type u_1
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 ∈ Set.Icc 0 1
[PROOFSTEP]
rfl
[GOAL]
case neg
F✝ : Type u_1
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)
[PROOFSTEP]
rw [extend, ContinuousMap.coe_IccExtend, Set.IccExtend_of_mem]
[GOAL]
case neg
F✝ : Type u_1
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 := ?neg.hx✝ }) x.snd =
    ↑G ({ val := 2 * ↑x.fst - 1, property := (_ : 2 * ↑x.fst - 1 ∈ I) }, x.snd)
case neg.hx
F✝ : Type u_1
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
[PROOFSTEP]
rfl
[GOAL]
F✝ : Type u_1
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₂
⊢ symm (trans F G) = trans (symm G) (symm F)
[PROOFSTEP]
ext ⟨t, _⟩
[GOAL]
case h.mk
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
⊢ ↑(symm (trans F G)) (t, snd✝) = ↑(trans (symm G) (symm F)) (t, snd✝)
[PROOFSTEP]
rw [trans_apply, symm_apply, trans_apply]
[GOAL]
case h.mk
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
⊢ (if h : ↑(σ (t, snd✝).fst, (t, snd✝).snd).fst ≤ 1 / 2 then
      ↑F
        ({ val := 2 * ↑(σ (t, snd✝).fst, (t, snd✝).snd).fst,
            property := (_ : 2 * ↑(σ (t, snd✝).fst, (t, snd✝).snd).fst ∈ I) },
          (σ (t, snd✝).fst, (t, snd✝).snd).snd)
    else
      ↑G
        ({ val := 2 * ↑(σ (t, snd✝).fst, (t, snd✝).snd).fst - 1,
            property := (_ : 2 * ↑(σ (t, snd✝).fst, (t, snd✝).snd).fst - 1 ∈ I) },
          (σ (t, snd✝).fst, (t, snd✝).snd).snd)) =
    if h : ↑(t, snd✝).fst ≤ 1 / 2 then
      ↑(symm G) ({ val := 2 * ↑(t, snd✝).fst, property := (_ : 2 * ↑(t, snd✝).fst ∈ I) }, (t, snd✝).snd)
    else ↑(symm F) ({ val := 2 * ↑(t, snd✝).fst - 1, property := (_ : 2 * ↑(t, snd✝).fst - 1 ∈ I) }, (t, snd✝).snd)
[PROOFSTEP]
simp only [coe_symm_eq, symm_apply]
[GOAL]
case h.mk
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
⊢ (if h : 1 - ↑t ≤ 1 / 2 then ↑F ({ val := 2 * (1 - ↑t), property := (_ : (fun x => x ∈ I) (2 * (1 - ↑t))) }, snd✝)
    else ↑G ({ val := 2 * (1 - ↑t) - 1, property := (_ : (fun x => x ∈ I) (2 * (1 - ↑t) - 1)) }, snd✝)) =
    if h : ↑t ≤ 1 / 2 then ↑G (σ { val := 2 * ↑t, property := (_ : 2 * ↑(t, snd✝).fst ∈ I) }, snd✝)
    else ↑F (σ { val := 2 * ↑t - 1, property := (_ : 2 * ↑(t, snd✝).fst - 1 ∈ I) }, snd✝)
[PROOFSTEP]
split_ifs with h₁ h₂ h₂
[GOAL]
case pos
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ ↑F ({ val := 2 * (1 - ↑t), property := (_ : (fun x => x ∈ I) (2 * (1 - ↑t))) }, snd✝) =
    ↑G (σ { val := 2 * ↑t, property := (_ : 2 * ↑(t, snd✝).fst ∈ I) }, snd✝)
[PROOFSTEP]
have ht : (t : ℝ) = 1 / 2 := by linarith
[GOAL]
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ ↑t = 1 / 2
[PROOFSTEP]
linarith
[GOAL]
case pos
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
ht : ↑t = 1 / 2
⊢ ↑F ({ val := 2 * (1 - ↑t), property := (_ : (fun x => x ∈ I) (2 * (1 - ↑t))) }, snd✝) =
    ↑G (σ { val := 2 * ↑t, property := (_ : 2 * ↑(t, snd✝).fst ∈ I) }, snd✝)
[PROOFSTEP]
simp only [ht]
[GOAL]
case pos
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
ht : ↑t = 1 / 2
⊢ ↑F ({ val := 2 * (1 - 1 / 2), property := (_ : (fun x => x ∈ I) (2 * (1 - 1 / 2))) }, snd✝) =
    ↑G (σ { val := 2 * (1 / 2), property := (_ : (fun x => x ∈ I) (2 * (1 / 2))) }, snd✝)
[PROOFSTEP]
norm_num
[GOAL]
case neg
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ ↑F ({ val := 2 * (1 - ↑t), property := (_ : (fun x => x ∈ I) (2 * (1 - ↑t))) }, snd✝) =
    ↑F (σ { val := 2 * ↑t - 1, property := (_ : 2 * ↑(t, snd✝).fst - 1 ∈ I) }, snd✝)
[PROOFSTEP]
congr 2
[GOAL]
case neg.h.e_6.h.e_fst
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ { val := 2 * (1 - ↑t), property := (_ : (fun x => x ∈ I) (2 * (1 - ↑t))) } =
    σ { val := 2 * ↑t - 1, property := (_ : 2 * ↑(t, snd✝).fst - 1 ∈ I) }
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case neg.h.e_6.h.e_fst.a
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ ↑{ val := 2 * (1 - ↑t), property := (_ : (fun x => x ∈ I) (2 * (1 - ↑t))) } =
    ↑(σ { val := 2 * ↑t - 1, property := (_ : 2 * ↑(t, snd✝).fst - 1 ∈ I) })
[PROOFSTEP]
simp only [coe_symm_eq]
[GOAL]
case neg.h.e_6.h.e_fst.a
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ 2 * (1 - ↑t) = 1 - (2 * ↑t - 1)
[PROOFSTEP]
linarith
[GOAL]
case pos
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ ↑G ({ val := 2 * (1 - ↑t) - 1, property := (_ : (fun x => x ∈ I) (2 * (1 - ↑t) - 1)) }, snd✝) =
    ↑G (σ { val := 2 * ↑t, property := (_ : 2 * ↑(t, snd✝).fst ∈ I) }, snd✝)
[PROOFSTEP]
congr 2
[GOAL]
case pos.h.e_6.h.e_fst
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ { val := 2 * (1 - ↑t) - 1, property := (_ : (fun x => x ∈ I) (2 * (1 - ↑t) - 1)) } =
    σ { val := 2 * ↑t, property := (_ : 2 * ↑(t, snd✝).fst ∈ I) }
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case pos.h.e_6.h.e_fst.a
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ ↑{ val := 2 * (1 - ↑t) - 1, property := (_ : (fun x => x ∈ I) (2 * (1 - ↑t) - 1)) } =
    ↑(σ { val := 2 * ↑t, property := (_ : 2 * ↑(t, snd✝).fst ∈ I) })
[PROOFSTEP]
simp only [coe_symm_eq]
[GOAL]
case pos.h.e_6.h.e_fst.a
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ 2 * (1 - ↑t) - 1 = 1 - 2 * ↑t
[PROOFSTEP]
linarith
[GOAL]
case neg
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ ↑G ({ val := 2 * (1 - ↑t) - 1, property := (_ : (fun x => x ∈ I) (2 * (1 - ↑t) - 1)) }, snd✝) =
    ↑F (σ { val := 2 * ↑t - 1, property := (_ : 2 * ↑(t, snd✝).fst - 1 ∈ I) }, snd✝)
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
F✝ : Type u_1
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₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
F✝ : Type u_1
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₁ g₀ g₁ : C(X, Y)
F : Homotopy f₀ f₁
h₀ : f₀ = g₀
h₁ : f₁ = g₁
⊢ ∀ (x : X), ContinuousMap.toFun (ContinuousMap.mk ↑F) (0, x) = ↑g₀ x
[PROOFSTEP]
simp [← h₀]
[GOAL]
F✝ : Type u_1
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₁ g₀ g₁ : C(X, Y)
F : Homotopy f₀ f₁
h₀ : f₀ = g₀
h₁ : f₁ = g₁
⊢ ∀ (x : X), ContinuousMap.toFun (ContinuousMap.mk ↑F) (1, x) = ↑g₁ x
[PROOFSTEP]
simp [← h₁]
[GOAL]
F✝ : Type u_1
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₁ : C(X, Y)
g₀ g₁ : C(Y, Z)
F : Homotopy f₀ f₁
G : Homotopy g₀ g₁
⊢ ∀ (x : X), ContinuousMap.toFun (ContinuousMap.mk fun x => ↑G (x.fst, ↑F x)) (0, x) = ↑(comp g₀ f₀) x
[PROOFSTEP]
simp
[GOAL]
F✝ : Type u_1
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₁ : C(X, Y)
g₀ g₁ : C(Y, Z)
F : Homotopy f₀ f₁
G : Homotopy g₀ g₁
⊢ ∀ (x : X), ContinuousMap.toFun (ContinuousMap.mk fun x => ↑G (x.fst, ↑F x)) (1, x) = ↑(comp g₁ f₁) x
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
⊢ ∀ {x y : C(X, Y)}, Homotopic x y → Homotopic y x
[PROOFSTEP]
apply symm
[GOAL]
F : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
⊢ ∀ {x y z : C(X, Y)}, Homotopic x y → Homotopic y z → Homotopic x z
[PROOFSTEP]
apply trans
[GOAL]
F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : HomotopyWith f₀ f₁ P
G : HomotopyWith f₁ f₂ P
src✝ : Homotopy f₀ f₂ := Homotopy.trans F.toHomotopy G.toHomotopy
t : ↑I
⊢ P
    (ContinuousMap.mk fun x =>
      ContinuousMap.toFun
        { toContinuousMap := src✝.toContinuousMap,
            map_zero_left := (_ : ∀ (x : X), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑f₀ x),
            map_one_left := (_ : ∀ (x : X), ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑f₂ x) }.toContinuousMap
        (t, x))
[PROOFSTEP]
simp only [Homotopy.trans]
[GOAL]
F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : HomotopyWith f₀ f₁ P
G : HomotopyWith f₁ f₂ P
src✝ : Homotopy f₀ f₂ := Homotopy.trans F.toHomotopy G.toHomotopy
t : ↑I
⊢ P
    (ContinuousMap.mk fun x =>
      if ↑t ≤ 1 / 2 then ↑(↑(Homotopy.extend F.toHomotopy) (2 * ↑t)) x
      else ↑(↑(Homotopy.extend G.toHomotopy) (2 * ↑t - 1)) x)
[PROOFSTEP]
change P ⟨fun _ => ite ((t : ℝ) ≤ _) _ _, _⟩
[GOAL]
F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : HomotopyWith f₀ f₁ P
G : HomotopyWith f₁ f₂ P
src✝ : Homotopy f₀ f₂ := Homotopy.trans F.toHomotopy G.toHomotopy
t : ↑I
⊢ P
    (ContinuousMap.mk fun x =>
      if ↑t ≤ 1 / 2 then ↑(↑(Homotopy.extend F.toHomotopy) (2 * ↑t)) x
      else ↑(↑(Homotopy.extend G.toHomotopy) (2 * ↑t - 1)) x)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : HomotopyWith f₀ f₁ P
G : HomotopyWith f₁ f₂ P
src✝ : Homotopy f₀ f₂ := Homotopy.trans F.toHomotopy G.toHomotopy
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ P (ContinuousMap.mk fun x => ↑(↑(Homotopy.extend F.toHomotopy) (2 * ↑t)) x)
[PROOFSTEP]
exact F.extendProp _
[GOAL]
case neg
F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : HomotopyWith f₀ f₁ P
G : HomotopyWith f₁ f₂ P
src✝ : Homotopy f₀ f₂ := Homotopy.trans F.toHomotopy G.toHomotopy
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ P (ContinuousMap.mk fun x => ↑(↑(Homotopy.extend G.toHomotopy) (2 * ↑t - 1)) x)
[PROOFSTEP]
exact G.extendProp _
[GOAL]
F✝ : Type u_1
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)
S : Set X
F : HomotopyRel f₀ f₁ S
G : HomotopyRel f₁ f₂ S
src✝ : Homotopy f₀ f₂ := Homotopy.trans F.toHomotopy G.toHomotopy
t : ↑I
x : X
hx : x ∈ S
⊢ ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left := (_ : ∀ (x : X), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑f₀ x),
                  map_one_left :=
                    (_ : ∀ (x : X), ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑f₂ x) }.toContinuousMap
              (t, x))
        x =
      ↑f₀ x ∧
    ↑(mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := src✝.toContinuousMap,
                  map_zero_left := (_ : ∀ (x : X), ContinuousMap.toFun src✝.toContinuousMap (0, x) = ↑f₀ x),
                  map_one_left :=
                    (_ : ∀ (x : X), ContinuousMap.toFun src✝.toContinuousMap (1, x) = ↑f₂ x) }.toContinuousMap
              (t, x))
        x =
      ↑f₂ x
[PROOFSTEP]
simp only [Homotopy.trans]
[GOAL]
F✝ : Type u_1
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)
S : Set X
F : HomotopyRel f₀ f₁ S
G : HomotopyRel f₁ f₂ S
src✝ : Homotopy f₀ f₂ := Homotopy.trans F.toHomotopy G.toHomotopy
t : ↑I
x : X
hx : x ∈ S
⊢ ↑(mk fun x =>
            if ↑t ≤ 1 / 2 then ↑(↑(Homotopy.extend F.toHomotopy) (2 * ↑t)) x
            else ↑(↑(Homotopy.extend G.toHomotopy) (2 * ↑t - 1)) x)
        x =
      ↑f₀ x ∧
    ↑(mk fun x =>
            if ↑t ≤ 1 / 2 then ↑(↑(Homotopy.extend F.toHomotopy) (2 * ↑t)) x
            else ↑(↑(Homotopy.extend G.toHomotopy) (2 * ↑t - 1)) x)
        x =
      ↑f₂ x
[PROOFSTEP]
change (⟨fun _ => ite ((t : ℝ) ≤ _) _ _, _⟩ : C(X, Y)) _ = _ ∧ _ = _
[GOAL]
F✝ : Type u_1
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)
S : Set X
F : HomotopyRel f₀ f₁ S
G : HomotopyRel f₁ f₂ S
src✝ : Homotopy f₀ f₂ := Homotopy.trans F.toHomotopy G.toHomotopy
t : ↑I
x : X
hx : x ∈ S
⊢ ↑(mk fun x =>
            if ↑t ≤ 1 / 2 then ↑(↑(Homotopy.extend F.toHomotopy) (2 * ↑t)) x
            else ↑(↑(Homotopy.extend G.toHomotopy) (2 * ↑t - 1)) x)
        x =
      ↑f₀ x ∧
    ↑(mk fun x =>
            if ↑t ≤ 1 / 2 then ↑(↑(Homotopy.extend F.toHomotopy) (2 * ↑t)) x
            else ↑(↑(Homotopy.extend G.toHomotopy) (2 * ↑t - 1)) x)
        x =
      ↑f₂ x
[PROOFSTEP]
split_ifs
[GOAL]
case pos
F✝ : Type u_1
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)
S : Set X
F : HomotopyRel f₀ f₁ S
G : HomotopyRel f₁ f₂ S
src✝ : Homotopy f₀ f₂ := Homotopy.trans F.toHomotopy G.toHomotopy
t : ↑I
x : X
hx : x ∈ S
h✝ : ↑t ≤ 1 / 2
⊢ ↑(mk fun x => ↑(↑(Homotopy.extend F.toHomotopy) (2 * ↑t)) x) x = ↑f₀ x ∧
    ↑(mk fun x => ↑(↑(Homotopy.extend F.toHomotopy) (2 * ↑t)) x) x = ↑f₂ x
[PROOFSTEP]
simp [(HomotopyWith.extendProp F (2 * t) x hx).1, F.fst_eq_snd hx, G.fst_eq_snd hx]
[GOAL]
case neg
F✝ : Type u_1
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)
S : Set X
F : HomotopyRel f₀ f₁ S
G : HomotopyRel f₁ f₂ S
src✝ : Homotopy f₀ f₂ := Homotopy.trans F.toHomotopy G.toHomotopy
t : ↑I
x : X
hx : x ∈ S
h✝ : ¬↑t ≤ 1 / 2
⊢ ↑(mk fun x => ↑(↑(Homotopy.extend G.toHomotopy) (2 * ↑t - 1)) x) x = ↑f₀ x ∧
    ↑(mk fun x => ↑(↑(Homotopy.extend G.toHomotopy) (2 * ↑t - 1)) x) x = ↑f₂ x
[PROOFSTEP]
simp [(HomotopyWith.extendProp G (2 * t - 1) x hx).1, F.fst_eq_snd hx, G.fst_eq_snd hx]
[GOAL]
F✝ : Type u_1
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)
S : Set X
f₀ f₁ g₀ g₁ : C(X, Y)
F : HomotopyRel f₀ f₁ S
h₀ : f₀ = g₀
h₁ : f₁ = g₁
t : ↑I
x : X
hx : x ∈ S
⊢ ↑(mk fun x => ContinuousMap.toFun (Homotopy.cast F.toHomotopy h₀ h₁).toContinuousMap (t, x)) x = ↑g₀ x ∧
    ↑(mk fun x => ContinuousMap.toFun (Homotopy.cast F.toHomotopy h₀ h₁).toContinuousMap (t, x)) x = ↑g₁ x
[PROOFSTEP]
simpa only [← h₀, ← h₁] using F.prop t x hx
[GOAL]
F : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
S : Set X
⊢ ∀ {x y : C(X, Y)}, HomotopicRel x y S → HomotopicRel y x S
[PROOFSTEP]
apply symm
[GOAL]
F : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
S : Set X
⊢ ∀ {x y z : C(X, Y)}, HomotopicRel x y S → HomotopicRel y z S → HomotopicRel x z S
[PROOFSTEP]
apply trans