case intro
X : Type u
inst✝¹ : TopologicalSpace X
n : ℕ
x : X
f g h : GenLoop n x
inst✝ : NeZero n
H : ContinuousMap.HomotopyRel f.toContinuousMap g.toContinuousMap (Cube.boundary n)
⊢ Path.Homotopic (diagonal f) (diagonal g)
X : Type u
inst✝¹ : TopologicalSpace X
n : ℕ
x : X
f g h : GenLoop n x
inst✝ : NeZero n
H : Homotopic f g
⊢ Path.Homotopic (diagonal f) (diagonal g)
rcases H with ⟨H⟩
case intro
X : Type u
inst✝¹ : TopologicalSpace X
n : ℕ
x : X
f g h : GenLoop n x
inst✝ : NeZero n
H : ContinuousMap.HomotopyRel f.toContinuousMap g.toContinuousMap (Cube.boundary n)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      ↑(ContinuousMap.mk fun x_2 =>
                ContinuousMap.toFun
                  (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy
                      (ContinuousMap.constPi (Fin n))).toContinuousMap
                  (t, x_2))
            x_1 =
          ↑(diagonal f).toContinuousMap x_1 ∧
        ↑(ContinuousMap.mk fun x_2 =>
                ContinuousMap.toFun
                  (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy
                      (ContinuousMap.constPi (Fin n))).toContinuousMap
                  (t, x_2))
            x_1 =
          ↑(diagonal g).toContinuousMap x_1
case intro
X : Type u
inst✝¹ : TopologicalSpace X
n : ℕ
x : X
f g h : GenLoop n x
inst✝ : NeZero n
H : ContinuousMap.HomotopyRel f.toContinuousMap g.toContinuousMap (Cube.boundary n)
⊢ Path.Homotopic (diagonal f) (diagonal g)
refine ⟨H.compContinuousMap _, ?_⟩
case intro.inl
X : Type u
inst✝¹ : TopologicalSpace X
n : ℕ
x : X
f g h : GenLoop n x
inst✝ : NeZero n
H : ContinuousMap.HomotopyRel f.toContinuousMap g.toContinuousMap (Cube.boundary n)
t : ↑I
⊢ ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.constPi (Fin n))).toContinuousMap
              (t, x_1))
        0 =
      ↑(diagonal f).toContinuousMap 0 ∧
    ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.constPi (Fin n))).toContinuousMap
              (t, x_1))
        0 =
      ↑(diagonal g).toContinuousMap 0

case intro.inr
X : Type u
inst✝¹ : TopologicalSpace X
n : ℕ
x : X
f g h : GenLoop n x
inst✝ : NeZero n
H : ContinuousMap.HomotopyRel f.toContinuousMap g.toContinuousMap (Cube.boundary n)
t : ↑I
⊢ ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.constPi (Fin n))).toContinuousMap
              (t, x_1))
        1 =
      ↑(diagonal f).toContinuousMap 1 ∧
    ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.constPi (Fin n))).toContinuousMap
              (t, x_1))
        1 =
      ↑(diagonal g).toContinuousMap 1
case intro
X : Type u
inst✝¹ : TopologicalSpace X
n : ℕ
x : X
f g h : GenLoop n x
inst✝ : NeZero n
H : ContinuousMap.HomotopyRel f.toContinuousMap g.toContinuousMap (Cube.boundary n)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      ↑(ContinuousMap.mk fun x_2 =>
                ContinuousMap.toFun
                  (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy
                      (ContinuousMap.constPi (Fin n))).toContinuousMap
                  (t, x_2))
            x_1 =
          ↑(diagonal f).toContinuousMap x_1 ∧
        ↑(ContinuousMap.mk fun x_2 =>
                ContinuousMap.toFun
                  (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy
                      (ContinuousMap.constPi (Fin n))).toContinuousMap
                  (t, x_2))
            x_1 =
          ↑(diagonal g).toContinuousMap x_1
rintro t _ (rfl | rfl)
no goals
case intro.inl
X : Type u
inst✝¹ : TopologicalSpace X
n : ℕ
x : X
f g h : GenLoop n x
inst✝ : NeZero n
H : ContinuousMap.HomotopyRel f.toContinuousMap g.toContinuousMap (Cube.boundary n)
t : ↑I
⊢ ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.constPi (Fin n))).toContinuousMap
              (t, x_1))
        0 =
      ↑(diagonal f).toContinuousMap 0 ∧
    ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.constPi (Fin n))).toContinuousMap
              (t, x_1))
        0 =
      ↑(diagonal g).toContinuousMap 0
exact H.prop' _ _ Cube.zero_mem_boundary
no goals
case intro.inr
X : Type u
inst✝¹ : TopologicalSpace X
n : ℕ
x : X
f g h : GenLoop n x
inst✝ : NeZero n
H : ContinuousMap.HomotopyRel f.toContinuousMap g.toContinuousMap (Cube.boundary n)
t : ↑I
⊢ ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.constPi (Fin n))).toContinuousMap
              (t, x_1))
        1 =
      ↑(diagonal f).toContinuousMap 1 ∧
    ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              (ContinuousMap.Homotopy.compContinuousMap H.toHomotopy (ContinuousMap.constPi (Fin n))).toContinuousMap
              (t, x_1))
        1 =
      ↑(diagonal g).toContinuousMap 1
exact H.prop' _ _ Cube.one_mem_boundary