case a.h
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
⊢ ↑(symm (trans γ γ')) t = ↑(trans (symm γ') (symm γ)) t
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
⊢ symm (trans γ γ') = trans (symm γ') (symm γ)
ext t
case a.h
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
⊢ (if h : ↑(σ t) ≤ 1 / 2 then ↑γ { val := 2 * ↑(σ t), property := (_ : 2 * ↑(σ t) ∈ I) }
    else ↑γ' { val := 2 * ↑(σ t) - 1, property := (_ : 2 * ↑(σ t) - 1 ∈ I) }) =
    if h : ↑t ≤ 1 / 2 then ↑γ' (σ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) })
    else ↑γ (σ { val := 2 * ↑t - 1, property := (_ : 2 * ↑t - 1 ∈ I) })
case a.h
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
⊢ ↑(symm (trans γ γ')) t = ↑(trans (symm γ') (symm γ)) t
simp only [trans_apply, ← one_div, symm_apply, not_le, Function.comp_apply]
case a.h.inl.inl
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
⊢ ↑γ { val := 2 * ↑(σ t), property := (_ : 2 * ↑(σ t) ∈ I) } = ↑γ' (σ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) })

case a.h.inl.inr
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ ↑γ { val := 2 * ↑(σ t), property := (_ : 2 * ↑(σ t) ∈ I) } =
    ↑γ (σ { val := 2 * ↑t - 1, property := (_ : 2 * ↑t - 1 ∈ I) })

case a.h.inr.inl
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ ↑γ' { val := 2 * ↑(σ t) - 1, property := (_ : 2 * ↑(σ t) - 1 ∈ I) } =
    ↑γ' (σ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) })

case a.h.inr.inr
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ ↑γ' { val := 2 * ↑(σ t) - 1, property := (_ : 2 * ↑(σ t) - 1 ∈ I) } =
    ↑γ (σ { val := 2 * ↑t - 1, property := (_ : 2 * ↑t - 1 ∈ I) })
case a.h
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
⊢ (if h : ↑(σ t) ≤ 1 / 2 then ↑γ { val := 2 * ↑(σ t), property := (_ : 2 * ↑(σ t) ∈ I) }
    else ↑γ' { val := 2 * ↑(σ t) - 1, property := (_ : 2 * ↑(σ t) - 1 ∈ I) }) =
    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 with h h₁ h₂ <;> rw [coe_symm_eq] at h
case a.h.inl.inl
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
ht : ↑t = 1 / 2
⊢ ↑γ { val := 2 * ↑(σ t), property := (_ : 2 * ↑(σ t) ∈ I) } = ↑γ' (σ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) })
case a.h.inl.inl
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
⊢ ↑γ { val := 2 * ↑(σ t), property := (_ : 2 * ↑(σ t) ∈ I) } = ↑γ' (σ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) })
have ht : (t : ℝ) = 1 / 2 := by
  refine le_antisymm h₁ ?_
  rw [sub_le_comm] at h
  norm_num at h
  exact h
case a.h.inl.inl
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
ht : ↑t = 1 / 2
⊢ ↑γ { val := 2 * (1 - 1 / 2), property := (_ : (fun x => x ∈ I) (2 * (1 - 1 / 2))) } =
    ↑γ' { val := 1 - 2 * (1 / 2), property := (_ : (fun x => x ∈ I) (1 - 2 * (1 / 2))) }
case a.h.inl.inl
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
ht : ↑t = 1 / 2
⊢ ↑γ { val := 2 * ↑(σ t), property := (_ : 2 * ↑(σ t) ∈ I) } = ↑γ' (σ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) })
simp_rw [unitInterval.symm, ht]
no goals
case a.h.inl.inl
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
ht : ↑t = 1 / 2
⊢ ↑γ { val := 2 * (1 - 1 / 2), property := (_ : (fun x => x ∈ I) (2 * (1 - 1 / 2))) } =
    ↑γ' { val := 1 - 2 * (1 / 2), property := (_ : (fun x => x ∈ I) (1 - 2 * (1 / 2))) }
norm_num
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
⊢ 1 / 2 ≤ ↑t
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
⊢ ↑t = 1 / 2
refine le_antisymm h₁ ?_
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - 1 / 2 ≤ ↑t
h₁ : ↑t ≤ 1 / 2
⊢ 1 / 2 ≤ ↑t
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
⊢ 1 / 2 ≤ ↑t
rw [sub_le_comm] at h
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
h : 1 / 2 ≤ ↑t
⊢ 1 / 2 ≤ ↑t
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - 1 / 2 ≤ ↑t
h₁ : ↑t ≤ 1 / 2
⊢ 1 / 2 ≤ ↑t
norm_num at h
no goals
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
h : 1 / 2 ≤ ↑t
⊢ 1 / 2 ≤ ↑t
exact h
case a.h.inl.inr
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ ↑{ val := 2 * ↑(σ t), property := (_ : 2 * ↑(σ t) ∈ I) } =
    ↑(σ { val := 2 * ↑t - 1, property := (_ : 2 * ↑t - 1 ∈ I) })
case a.h.inl.inr
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ ↑γ { val := 2 * ↑(σ t), property := (_ : 2 * ↑(σ t) ∈ I) } =
    ↑γ (σ { val := 2 * ↑t - 1, property := (_ : 2 * ↑t - 1 ∈ I) })
refine' congr_arg _ (Subtype.ext _)
case a.h.inl.inr
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ 2 * (1 - ↑t) = 1 - (2 * ↑t - 1)
case a.h.inl.inr
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ ↑{ val := 2 * ↑(σ t), property := (_ : 2 * ↑(σ t) ∈ I) } =
    ↑(σ { val := 2 * ↑t - 1, property := (_ : 2 * ↑t - 1 ∈ I) })
norm_num [unitInterval.symm, sub_sub_eq_add_sub, mul_sub]
no goals
case a.h.inl.inr
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ 2 * (1 - ↑t) = 1 - (2 * ↑t - 1)
ring
case a.h.inr.inl
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ ↑{ val := 2 * ↑(σ t) - 1, property := (_ : 2 * ↑(σ t) - 1 ∈ I) } =
    ↑(σ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) })
case a.h.inr.inl
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ ↑γ' { val := 2 * ↑(σ t) - 1, property := (_ : 2 * ↑(σ t) - 1 ∈ I) } =
    ↑γ' (σ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) })
refine' congr_arg _ (Subtype.ext _)
case a.h.inr.inl
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ 2 * (1 - ↑t) - 1 = 1 - 2 * ↑t
case a.h.inr.inl
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ ↑{ val := 2 * ↑(σ t) - 1, property := (_ : 2 * ↑(σ t) - 1 ∈ I) } =
    ↑(σ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) })
norm_num [mul_sub, h]
no goals
case a.h.inr.inl
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ 2 * (1 - ↑t) - 1 = 1 - 2 * ↑t
ring
case a.h.inr.inr.h
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ False
case a.h.inr.inr
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ ↑γ' { val := 2 * ↑(σ t) - 1, property := (_ : 2 * ↑(σ t) - 1 ∈ I) } =
    ↑γ (σ { val := 2 * ↑t - 1, property := (_ : 2 * ↑t - 1 ∈ I) })
exfalso
case a.h.inr.inr.h
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - 1 / 2 ≤ ↑t
h₂ : ¬↑t ≤ 1 / 2
⊢ False
case a.h.inr.inr.h
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ False
rw [sub_le_comm] at h
case a.h.inr.inr.h
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ↑t < 1 / 2
h₂ : 1 / 2 < ↑t
⊢ False
case a.h.inr.inr.h
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - 1 / 2 ≤ ↑t
h₂ : ¬↑t ≤ 1 / 2
⊢ False
norm_num at h h₂
no goals
case a.h.inr.inr.h
X : Type u_1
Y : Type ?u.237548
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.237563
γ✝ γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ↑t < 1 / 2
h₂ : 1 / 2 < ↑t
⊢ False
exact (h.trans h₂).ne rfl