case h
X : Type u_1
Y : Type ?u.114634
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.114649
γ✝ : Path x✝ y
a b : X
γ : Path a b
x : X
⊢ x ∈ range ↑(symm γ) ↔ x ∈ range ↑γ
X : Type u_1
Y : Type ?u.114634
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.114649
γ✝ : Path x y
a b : X
γ : Path a b
⊢ range ↑(symm γ) = range ↑γ
ext x
case h
X : Type u_1
Y : Type ?u.114634
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.114649
γ✝ : Path x✝ y
a b : X
γ : Path a b
x : X
⊢ (∃ x_1 h,
      ContinuousMap.toFun γ.toContinuousMap
          { val := 1 - x_1, property := (_ : 1 - ↑{ val := x_1, property := (_ : x_1 ∈ I) } ∈ I) } =
        x) ↔
    ∃ x_1 h, ContinuousMap.toFun γ.toContinuousMap { val := x_1, property := h } = x
case h
X : Type u_1
Y : Type ?u.114634
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.114649
γ✝ : Path x✝ y
a b : X
γ : Path a b
x : X
⊢ x ∈ range ↑(symm γ) ↔ x ∈ range ↑γ
simp only [mem_range, Path.symm, FunLike.coe, unitInterval.symm, SetCoe.exists, comp_apply,
  Subtype.coe_mk]
case h.e'_2.h.e'_6.h.e'_3
X : Type u_1
Y : Type ?u.114634
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.114649
γ✝ : Path x✝ y✝
a b : X
γ : Path a b
x : X
y : ℝ
hy : y ∈ I
hxy : ContinuousMap.toFun γ.toContinuousMap { val := y, property := hy } = x
⊢ 1 - (1 - y) = y
case h
X : Type u_1
Y : Type ?u.114634
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.114649
γ✝ : Path x✝ y
a b : X
γ : Path a b
x : X
⊢ (∃ x_1 h,
      ContinuousMap.toFun γ.toContinuousMap
          { val := 1 - x_1, property := (_ : 1 - ↑{ val := x_1, property := (_ : x_1 ∈ I) } ∈ I) } =
        x) ↔
    ∃ x_1 h, ContinuousMap.toFun γ.toContinuousMap { val := x_1, property := h } = x
constructor <;> rintro ⟨y, hy, hxy⟩ <;> refine' ⟨1 - y, mem_iff_one_sub_mem.mp hy, _⟩ <;>
  convert hxy
no goals
case h.e'_2.h.e'_6.h.e'_3
X : Type u_1
Y : Type ?u.114634
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.114649
γ✝ : Path x✝ y✝
a b : X
γ : Path a b
x : X
y : ℝ
hy : y ∈ I
hxy : ContinuousMap.toFun γ.toContinuousMap { val := y, property := hy } = x
⊢ 1 - (1 - y) = y
simp