case h.mk
F✝ : Type ?u.209823
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✝)
F✝ : Type ?u.209823
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)
ext ⟨t, _⟩
case h.mk
F✝ : Type ?u.209823
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)
case h.mk
F✝ : Type ?u.209823
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✝)
rw [trans_apply, symm_apply, trans_apply]
case h.mk
F✝ : Type ?u.209823
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✝)
case h.mk
F✝ : Type ?u.209823
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)
simp only [coe_symm_eq, symm_apply]
case h.mk.inl.inl
F✝ : Type ?u.209823
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✝)

case h.mk.inl.inr
F✝ : Type ?u.209823
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✝)

case h.mk.inr.inl
F✝ : Type ?u.209823
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✝)

case h.mk.inr.inr
F✝ : Type ?u.209823
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✝)
case h.mk
F✝ : Type ?u.209823
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✝)
split_ifs with h₁ h₂ h₂
case h.mk.inl.inl
F✝ : Type ?u.209823
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✝)
case h.mk.inl.inl
F✝ : Type ?u.209823
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✝)
have ht : (t : ℝ) = 1 / 2 := by linarith
case h.mk.inl.inl
F✝ : Type ?u.209823
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✝)
case h.mk.inl.inl
F✝ : Type ?u.209823
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✝)
simp only [ht]
no goals
case h.mk.inl.inl
F✝ : Type ?u.209823
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✝)
norm_num
no goals
F✝ : Type ?u.209823
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
linarith
case h.mk.inl.inr.h.e_6.h.e_fst
F✝ : Type ?u.209823
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) }
case h.mk.inl.inr
F✝ : Type ?u.209823
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✝)
congr 2
case h.mk.inl.inr.h.e_6.h.e_fst.a
F✝ : Type ?u.209823
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) })
case h.mk.inl.inr.h.e_6.h.e_fst
F✝ : Type ?u.209823
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) }
apply Subtype.ext
case h.mk.inl.inr.h.e_6.h.e_fst.a
F✝ : Type ?u.209823
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)
case h.mk.inl.inr.h.e_6.h.e_fst.a
F✝ : Type ?u.209823
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) })
simp only [coe_symm_eq]
no goals
case h.mk.inl.inr.h.e_6.h.e_fst.a
F✝ : Type ?u.209823
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)
linarith
case h.mk.inr.inl.h.e_6.h.e_fst
F✝ : Type ?u.209823
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) }
case h.mk.inr.inl
F✝ : Type ?u.209823
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✝)
congr 2
case h.mk.inr.inl.h.e_6.h.e_fst.a
F✝ : Type ?u.209823
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) })
case h.mk.inr.inl.h.e_6.h.e_fst
F✝ : Type ?u.209823
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) }
apply Subtype.ext
case h.mk.inr.inl.h.e_6.h.e_fst.a
F✝ : Type ?u.209823
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
case h.mk.inr.inl.h.e_6.h.e_fst.a
F✝ : Type ?u.209823
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) })
simp only [coe_symm_eq]
no goals
case h.mk.inr.inl.h.e_6.h.e_fst.a
F✝ : Type ?u.209823
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
linarith
case h.mk.inr.inr.h
F✝ : Type ?u.209823
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
case h.mk.inr.inr
F✝ : Type ?u.209823
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✝)
exfalso
no goals
case h.mk.inr.inr.h
F✝ : Type ?u.209823
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
linarith