X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x : X
f g : Path x x
⊢ Path.Homotopic f g → GenLoop.Homotopic (↑genLoopOneEquivPathSelf.symm f) (↑genLoopOneEquivPathSelf.symm g)
X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x : X
f g : Path x x
⊢ GenLoop.Homotopic (↑genLoopOneEquivPathSelf.symm f) (↑genLoopOneEquivPathSelf.symm g) ↔ Path.Homotopic f g
refine ⟨GenLoop.Homotopic.diagonal, ?_⟩
case intro
X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x : X
f g : Path x x
H : Path.Homotopy f g
⊢ GenLoop.Homotopic (↑genLoopOneEquivPathSelf.symm f) (↑genLoopOneEquivPathSelf.symm g)
X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x : X
f g : Path x x
⊢ Path.Homotopic f g → GenLoop.Homotopic (↑genLoopOneEquivPathSelf.symm f) (↑genLoopOneEquivPathSelf.symm g)
rintro ⟨H⟩
case intro
X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x : X
f g : Path x x
H : Path.Homotopy f g
⊢ ∀ (t : ↑I) (x_1 : I^ 1),
    x_1 ∈ Cube.boundary 1 →
      ↑(ContinuousMap.mk fun x_2 =>
                ContinuousMap.toFun
                  (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.eval 0)).toContinuousMap
                  (t, x_2))
            x_1 =
          ↑(↑genLoopOneEquivPathSelf.symm f).toContinuousMap x_1 ∧
        ↑(ContinuousMap.mk fun x_2 =>
                ContinuousMap.toFun
                  (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.eval 0)).toContinuousMap
                  (t, x_2))
            x_1 =
          ↑(↑genLoopOneEquivPathSelf.symm g).toContinuousMap x_1
case intro
X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x : X
f g : Path x x
H : Path.Homotopy f g
⊢ GenLoop.Homotopic (↑genLoopOneEquivPathSelf.symm f) (↑genLoopOneEquivPathSelf.symm g)
refine ⟨H.1.compContinuousMap _, ?_⟩
case intro
X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x : X
f g : Path x x
H : Path.Homotopy f g
⊢ ∀ (t : ↑I) (x_1 : I^ 1),
    x_1 ∈ {0, 1} →
      ↑(ContinuousMap.mk fun x_2 =>
                ContinuousMap.toFun
                  (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.eval 0)).toContinuousMap
                  (t, x_2))
            x_1 =
          ↑(↑genLoopOneEquivPathSelf.symm f).toContinuousMap x_1 ∧
        ↑(ContinuousMap.mk fun x_2 =>
                ContinuousMap.toFun
                  (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.eval 0)).toContinuousMap
                  (t, x_2))
            x_1 =
          ↑(↑genLoopOneEquivPathSelf.symm g).toContinuousMap x_1
case intro
X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x : X
f g : Path x x
H : Path.Homotopy f g
⊢ ∀ (t : ↑I) (x_1 : I^ 1),
    x_1 ∈ Cube.boundary 1 →
      ↑(ContinuousMap.mk fun x_2 =>
                ContinuousMap.toFun
                  (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.eval 0)).toContinuousMap
                  (t, x_2))
            x_1 =
          ↑(↑genLoopOneEquivPathSelf.symm f).toContinuousMap x_1 ∧
        ↑(ContinuousMap.mk fun x_2 =>
                ContinuousMap.toFun
                  (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.eval 0)).toContinuousMap
                  (t, x_2))
            x_1 =
          ↑(↑genLoopOneEquivPathSelf.symm g).toContinuousMap x_1
rw [Cube.boundary_one]
case intro.inl
X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x : X
f g : Path x x
H : Path.Homotopy f g
t : ↑I
⊢ ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.eval 0)).toContinuousMap (t, x_1))
        0 =
      ↑(↑genLoopOneEquivPathSelf.symm f).toContinuousMap 0 ∧
    ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.eval 0)).toContinuousMap (t, x_1))
        0 =
      ↑(↑genLoopOneEquivPathSelf.symm g).toContinuousMap 0

case intro.inr
X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x : X
f g : Path x x
H : Path.Homotopy f g
t : ↑I
⊢ ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.eval 0)).toContinuousMap (t, x_1))
        1 =
      ↑(↑genLoopOneEquivPathSelf.symm f).toContinuousMap 1 ∧
    ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.eval 0)).toContinuousMap (t, x_1))
        1 =
      ↑(↑genLoopOneEquivPathSelf.symm g).toContinuousMap 1
case intro
X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x : X
f g : Path x x
H : Path.Homotopy f g
⊢ ∀ (t : ↑I) (x_1 : I^ 1),
    x_1 ∈ {0, 1} →
      ↑(ContinuousMap.mk fun x_2 =>
                ContinuousMap.toFun
                  (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.eval 0)).toContinuousMap
                  (t, x_2))
            x_1 =
          ↑(↑genLoopOneEquivPathSelf.symm f).toContinuousMap x_1 ∧
        ↑(ContinuousMap.mk fun x_2 =>
                ContinuousMap.toFun
                  (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.eval 0)).toContinuousMap
                  (t, x_2))
            x_1 =
          ↑(↑genLoopOneEquivPathSelf.symm g).toContinuousMap x_1
rintro t _ (rfl | rfl)
no goals
case intro.inl
X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x : X
f g : Path x x
H : Path.Homotopy f g
t : ↑I
⊢ ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.eval 0)).toContinuousMap (t, x_1))
        0 =
      ↑(↑genLoopOneEquivPathSelf.symm f).toContinuousMap 0 ∧
    ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.eval 0)).toContinuousMap (t, x_1))
        0 =
      ↑(↑genLoopOneEquivPathSelf.symm g).toContinuousMap 0
exact H.prop' _ _ (.inl rfl)
no goals
case intro.inr
X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x : X
f g : Path x x
H : Path.Homotopy f g
t : ↑I
⊢ ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.eval 0)).toContinuousMap (t, x_1))
        1 =
      ↑(↑genLoopOneEquivPathSelf.symm f).toContinuousMap 1 ∧
    ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.eval 0)).toContinuousMap (t, x_1))
        1 =
      ↑(↑genLoopOneEquivPathSelf.symm g).toContinuousMap 1
exact H.prop' _ _ (.inr rfl)