[GOAL]
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ HEq ((π.map f).map (Quotient.mk (Path.Homotopic.setoid x₀ x₁) p))
    ((π.map g).map (Quotient.mk (Path.Homotopic.setoid x₂ x₃) q))
[PROOFSTEP]
simp only [map_eq, ← Path.Homotopic.map_lift]
[GOAL]
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ HEq (Quotient.mk (Path.Homotopic.setoid (↑f x₀) (↑f x₁)) (Path.map p (_ : Continuous ↑f)))
    (Quotient.mk (Path.Homotopic.setoid (↑g x₂) (↑g x₃)) (Path.map q (_ : Continuous ↑g)))
[PROOFSTEP]
apply Path.Homotopic.hpath_hext
[GOAL]
case hp
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ ∀ (t : ↑I), ↑(Path.map p (_ : Continuous ↑f)) t = ↑(Path.map q (_ : Continuous ↑g)) t
[PROOFSTEP]
exact hfg
[GOAL]
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ ↑f x₀ = ↑g x₂
[PROOFSTEP]
convert hfg 0
[GOAL]
case h.e'_2.h.e'_6
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ x₀ = ↑p 0
[PROOFSTEP]
simp only [Path.source]
[GOAL]
case h.e'_3.h.e'_6
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ x₂ = ↑q 0
[PROOFSTEP]
simp only [Path.source]
[GOAL]
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ ↑f x₁ = ↑g x₃
[PROOFSTEP]
convert hfg 1
[GOAL]
case h.e'_2.h.e'_6
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ x₁ = ↑p 1
[PROOFSTEP]
simp only [Path.target]
[GOAL]
case h.e'_3.h.e'_6
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ x₃ = ↑q 1
[PROOFSTEP]
simp only [Path.target]
[GOAL]
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ (π.map f).map (Quotient.mk (Path.Homotopic.setoid x₀ x₁) p) =
    hcast (_ : ↑f x₀ = ↑g x₂) ≫ (π.map g).map (Quotient.mk (Path.Homotopic.setoid x₂ x₃) q) ≫ hcast (_ : ↑g x₃ = ↑f x₁)
[PROOFSTEP]
rw [Functor.conj_eqToHom_iff_heq ((πₘ f).map ⟦p⟧) ((πₘ g).map ⟦q⟧) (start_path hfg) (end_path hfg)]
[GOAL]
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ HEq ((π.map f).map (Quotient.mk (Path.Homotopic.setoid x₀ x₁) p))
    ((π.map g).map (Quotient.mk (Path.Homotopic.setoid x₂ x₃) q))
[PROOFSTEP]
exact heq_path_of_eq_image hfg
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀) (fromTop x₁)
⊢ (π.map f).map (Quotient.mk (Path.Homotopic.setoid (fromTop x₀) (fromTop x₁)) p') =
    hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
      (π.map (uliftMap H)).map
          (prodToProdTopI (𝟙 (fromTop { down := 0 }))
            (Quotient.mk (Path.Homotopic.setoid (fromTop x₀) (fromTop x₁)) p')) ≫
        hcast (_ : ↑H (0, x₁) = ↑f x₁)
[PROOFSTEP]
apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀) (fromTop x₁)
⊢ ∀ (t : ↑I), ↑f (↑p' t) = ↑(uliftMap H) (↑(Path.prod (Path.refl { down := 0 }) p') t)
[PROOFSTEP]
rw [Path.prod_coe]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀) (fromTop x₁)
⊢ ∀ (t : ↑I), ↑f (↑p' t) = ↑(uliftMap H) ((fun t => (↑(Path.refl { down := 0 }) t, ↑p' t)) t)
[PROOFSTEP]
simp_rw [ulift_apply]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀) (fromTop x₁)
⊢ ∀ (t : ↑I), ↑f (↑p' t) = ↑H ((↑(Path.refl { down := 0 }) t).down, ↑p' t)
[PROOFSTEP]
simp
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀) (fromTop x₁)
⊢ (π.map g).map (Quotient.mk (Path.Homotopic.setoid (fromTop x₀) (fromTop x₁)) p') =
    hcast (_ : ↑g x₀ = ↑H (1, x₀)) ≫
      (π.map (uliftMap H)).map
          (prodToProdTopI (𝟙 (fromTop { down := 1 }))
            (Quotient.mk (Path.Homotopic.setoid (fromTop x₀) (fromTop x₁)) p')) ≫
        hcast (_ : ↑H (1, x₁) = ↑g x₁)
[PROOFSTEP]
apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀) (fromTop x₁)
⊢ ∀ (t : ↑I), ↑g (↑p' t) = ↑(uliftMap H) (↑(Path.prod (Path.refl { down := 1 }) p') t)
[PROOFSTEP]
rw [Path.prod_coe]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀) (fromTop x₁)
⊢ ∀ (t : ↑I), ↑g (↑p' t) = ↑(uliftMap H) ((fun t => (↑(Path.refl { down := 1 }) t, ↑p' t)) t)
[PROOFSTEP]
simp_rw [ulift_apply]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀) (fromTop x₁)
⊢ ∀ (t : ↑I), ↑g (↑p' t) = ↑H ((↑(Path.refl { down := 1 }) t).down, ↑p' t)
[PROOFSTEP]
simp
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
x : ↑X
⊢ Quotient.mk (Path.Homotopic.setoid (fromTop (↑f x)) (fromTop (↑g x))) (evalAt H x) =
    hcast (_ : ↑f x = ↑H (0, x)) ≫
      (π.map (uliftMap H)).map (prodToProdTopI uhpath01 (𝟙 x)) ≫ hcast (_ : ↑H (1, x) = ↑g x)
[PROOFSTEP]
dsimp only [prodToProdTopI, uhpath01, hcast]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
x : ↑X
⊢ Quotient.mk (Path.Homotopic.setoid (fromTop (↑f x)) (fromTop (↑g x))) (evalAt H x) =
    eqToHom (_ : ↑f x = ↑H (0, x)) ≫
      (π.map (uliftMap H)).map
          ((prodToProdTop (TopCat.of (ULift ↑I)) X).map
            (Quotient.mk (Path.Homotopic.setoid (fromTop { down := 0 }) (fromTop { down := 1 })) unitInterval.upath01,
              𝟙 x)) ≫
        eqToHom (_ : ↑H (1, x) = ↑g x)
[PROOFSTEP]
refine' (@Functor.conj_eqToHom_iff_heq (πₓ Y) _ _ _ _ _ _ _ _ (H.apply_one x).symm).mpr _
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
x : ↑X
⊢ HEq (Quotient.mk (Path.Homotopic.setoid (fromTop (↑f x)) (fromTop (↑g x))) (evalAt H x))
    ((π.map (uliftMap H)).map
      ((prodToProdTop (TopCat.of (ULift ↑I)) X).map
        (Quotient.mk (Path.Homotopic.setoid (fromTop { down := 0 }) (fromTop { down := 1 })) unitInterval.upath01,
          𝟙 x)))
[PROOFSTEP]
simp only [id_eq_path_refl, prodToProdTop_map, Path.Homotopic.prod_lift, map_eq, ← Path.Homotopic.map_lift]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
x : ↑X
⊢ HEq (Quotient.mk (Path.Homotopic.setoid (fromTop (↑f x)) (fromTop (↑g x))) (evalAt H x))
    (Path.Homotopic.Quotient.mapFn
      ((prodToProdTop (TopCat.of (ULift ↑I)) X).map
        (Quotient.mk (Path.Homotopic.setoid (fromTop { down := 0 }) (fromTop { down := 1 })) unitInterval.upath01,
          Quotient.mk (Path.Homotopic.setoid x x) (Path.refl x)))
      (uliftMap H))
[PROOFSTEP]
apply Path.Homotopic.hpath_hext
[GOAL]
case hp
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
x : ↑X
⊢ ∀ (t : ↑I),
    ↑(evalAt H x) t =
      ↑((fun q => Path.map q (_ : Continuous ↑(uliftMap H))) (Path.prod unitInterval.upath01 (Path.refl x))) t
[PROOFSTEP]
intro
[GOAL]
case hp
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
x : ↑X
t✝ : ↑I
⊢ ↑(evalAt H x) t✝ =
    ↑((fun q => Path.map q (_ : Continuous ↑(uliftMap H))) (Path.prod unitInterval.upath01 (Path.refl x))) t✝
[PROOFSTEP]
rfl
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (π.map f).map p ≫ Quotient.mk (Path.Homotopic.setoid ((π.map f).obj (fromTop x₁)) (↑g x₁)) (evalAt H x₁) =
      diagonalPath' H p ∧
    Quotient.mk (Path.Homotopic.setoid (fromTop (↑f x₀)) (↑g x₀)) (evalAt H x₀) ≫ (π.map g).map p = diagonalPath' H p
[PROOFSTEP]
rw [H.apply_zero_path, H.apply_one_path, H.evalAt_eq]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
          (π.map (uliftMap H)).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) p) ≫ hcast (_ : ↑H (0, x₁) = ↑f x₁)) ≫
        Quotient.mk (Path.Homotopic.setoid ((π.map f).obj (fromTop x₁)) (↑g x₁)) (evalAt H x₁) =
      diagonalPath' H p ∧
    (hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
          (π.map (uliftMap H)).map (prodToProdTopI uhpath01 (𝟙 x₀)) ≫ hcast (_ : ↑H (1, x₀) = ↑g x₀)) ≫
        hcast (_ : ↑g x₀ = ↑H (1, x₀)) ≫
          (π.map (uliftMap H)).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) p) ≫ hcast (_ : ↑H (1, x₁) = ↑g x₁) =
      diagonalPath' H p
[PROOFSTEP]
erw [H.evalAt_eq]
  -- Porting note: `rw` didn't work, so using `erw`
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
          (π.map (uliftMap H)).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) p) ≫ hcast (_ : ↑H (0, x₁) = ↑f x₁)) ≫
        hcast (_ : ↑f (fromTop x₁) = ↑H (0, fromTop x₁)) ≫
          (π.map (uliftMap H)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x₁))) ≫
            hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁)) =
      diagonalPath' H p ∧
    (hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
          (π.map (uliftMap H)).map (prodToProdTopI uhpath01 (𝟙 x₀)) ≫ hcast (_ : ↑H (1, x₀) = ↑g x₀)) ≫
        hcast (_ : ↑g x₀ = ↑H (1, x₀)) ≫
          (π.map (uliftMap H)).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) p) ≫ hcast (_ : ↑H (1, x₁) = ↑g x₁) =
      diagonalPath' H p
[PROOFSTEP]
dsimp only [prodToProdTopI]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
          (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
            hcast (_ : ↑H (0, x₁) = ↑f x₁)) ≫
        hcast (_ : ↑f (fromTop x₁) = ↑H (0, fromTop x₁)) ≫
          (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁))) ≫
            hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁)) =
      diagonalPath' H p ∧
    (hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
          (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
            hcast (_ : ↑H (1, x₀) = ↑g x₀)) ≫
        hcast (_ : ↑g x₀ = ↑H (1, x₀)) ≫
          (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p)) ≫
            hcast (_ : ↑H (1, x₁) = ↑g x₁) =
      diagonalPath' H p
[PROOFSTEP]
constructor
[GOAL]
case left
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
        (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
          hcast (_ : ↑H (0, x₁) = ↑f x₁)) ≫
      hcast (_ : ↑f (fromTop x₁) = ↑H (0, fromTop x₁)) ≫
        (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁))) ≫
          hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁)) =
    diagonalPath' H p
[PROOFSTEP]
slice_lhs 2 4 =>
  rw [eqToHom_trans, eqToHom_refl]
    -- Porting note: this ↓ `simp` didn't do this
[GOAL]
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
    hcast (_ : ↑H (0, x₁) = ↑f x₁) ≫ hcast (_ : ↑f (fromTop x₁) = ↑H (0, fromTop x₁))
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁))
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
rw [eqToHom_trans, eqToHom_refl]
    -- Porting note: this ↓ `simp` didn't do this
[GOAL]
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
    hcast (_ : ↑H (0, x₁) = ↑f x₁) ≫ hcast (_ : ↑f (fromTop x₁) = ↑H (0, fromTop x₁))
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁))
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
rw [eqToHom_trans, eqToHom_refl]
    -- Porting note: this ↓ `simp` didn't do this
[GOAL]
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
    hcast (_ : ↑H (0, x₁) = ↑f x₁) ≫ hcast (_ : ↑f (fromTop x₁) = ↑H (0, fromTop x₁))
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁))
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
rw [eqToHom_trans, eqToHom_refl]
  -- Porting note: this ↓ `simp` didn't do this
[GOAL]
case left
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
      (((π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
            𝟙 ((π.map (uliftMap H)).obj ((prodToProdTop (TopCat.of (ULift ↑I)) X).obj ({ down := 0 }, x₁)))) ≫
          (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))) ≫
        hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁)) =
    diagonalPath' H p
[PROOFSTEP]
slice_lhs 2 4 => simp [← CategoryTheory.Functor.map_comp]
[GOAL]
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
    𝟙 ((π.map (uliftMap H)).obj ((prodToProdTop (TopCat.of (ULift ↑I)) X).obj ({ down := 0 }, x₁))) ≫
      (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁))
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
simp [← CategoryTheory.Functor.map_comp]
[GOAL]
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
    𝟙 ((π.map (uliftMap H)).obj ((prodToProdTop (TopCat.of (ULift ↑I)) X).obj ({ down := 0 }, x₁))) ≫
      (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁))
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
simp [← CategoryTheory.Functor.map_comp]
[GOAL]
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
    𝟙 ((π.map (uliftMap H)).obj ((prodToProdTop (TopCat.of (ULift ↑I)) X).obj ({ down := 0 }, x₁))) ≫
      (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁))
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
simp [← CategoryTheory.Functor.map_comp]
[GOAL]
case right
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
        (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
          hcast (_ : ↑H (1, x₀) = ↑g x₀)) ≫
      hcast (_ : ↑g x₀ = ↑H (1, x₀)) ≫
        (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p)) ≫
          hcast (_ : ↑H (1, x₁) = ↑g x₁) =
    diagonalPath' H p
[PROOFSTEP]
slice_lhs 2 4 =>
  rw [eqToHom_trans, eqToHom_refl]
    -- Porting note: this ↓ `simp` didn't do this
[GOAL]
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
    hcast (_ : ↑H (1, x₀) = ↑g x₀) ≫ hcast (_ : ↑g x₀ = ↑H (1, x₀))
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, x₁) = ↑g x₁)
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
rw [eqToHom_trans, eqToHom_refl]
    -- Porting note: this ↓ `simp` didn't do this
[GOAL]
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
    hcast (_ : ↑H (1, x₀) = ↑g x₀) ≫ hcast (_ : ↑g x₀ = ↑H (1, x₀))
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, x₁) = ↑g x₁)
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
rw [eqToHom_trans, eqToHom_refl]
    -- Porting note: this ↓ `simp` didn't do this
[GOAL]
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
    hcast (_ : ↑H (1, x₀) = ↑g x₀) ≫ hcast (_ : ↑g x₀ = ↑H (1, x₀))
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, x₁) = ↑g x₁)
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
rw [eqToHom_trans, eqToHom_refl]
  -- Porting note: this ↓ `simp` didn't do this
[GOAL]
case right
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
      (((π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
            𝟙 ((π.map (uliftMap H)).obj ((prodToProdTop (TopCat.of (ULift ↑I)) X).obj ({ down := 1 }, x₀)))) ≫
          (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))) ≫
        hcast (_ : ↑H (1, x₁) = ↑g x₁) =
    diagonalPath' H p
[PROOFSTEP]
slice_lhs 2 4 => simp [← CategoryTheory.Functor.map_comp]
[GOAL]
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
    𝟙 ((π.map (uliftMap H)).obj ((prodToProdTop (TopCat.of (ULift ↑I)) X).obj ({ down := 1 }, x₀))) ≫
      (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, x₁) = ↑g x₁)
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
simp [← CategoryTheory.Functor.map_comp]
[GOAL]
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
    𝟙 ((π.map (uliftMap H)).obj ((prodToProdTop (TopCat.of (ULift ↑I)) X).obj ({ down := 1 }, x₀))) ≫
      (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, x₁) = ↑g x₁)
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
simp [← CategoryTheory.Functor.map_comp]
[GOAL]
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
    𝟙 ((π.map (uliftMap H)).obj ((prodToProdTop (TopCat.of (ULift ↑I)) X).obj ({ down := 1 }, x₀))) ≫
      (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, x₁) = ↑g x₁)
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
simp [← CategoryTheory.Functor.map_comp]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
x y : ↑(π.obj X)
p : x ⟶ y
⊢ (π.map f).map p ≫
      (fun x =>
          Quotient.mk (Path.Homotopic.setoid ((π.map f).obj x) ((π.map g).obj x)) (ContinuousMap.Homotopy.evalAt H x))
        y =
    (fun x =>
          Quotient.mk (Path.Homotopic.setoid ((π.map f).obj x) ((π.map g).obj x)) (ContinuousMap.Homotopy.evalAt H x))
        x ≫
      (π.map g).map p
[PROOFSTEP]
erw [(H.eq_diag_path p).1, (H.eq_diag_path p).2]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
⊢ IsIso (homotopicMapsNatIso H)
[PROOFSTEP]
apply NatIso.isIso_of_isIso_app
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ ↑(π.obj X) ≌ ↑(π.obj Y)
[PROOFSTEP]
apply CategoryTheory.Equivalence.mk (πₘ hequiv.toFun : πₓ X ⥤ πₓ Y) (πₘ hequiv.invFun : πₓ Y ⥤ πₓ X)
[GOAL]
case η
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ 𝟭 ↑(π.obj X) ≅ π.map hequiv.toFun ⋙ π.map hequiv.invFun
[PROOFSTEP]
simp only [Grpd.hom_to_functor, Grpd.id_to_functor]
[GOAL]
case ε
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ π.map hequiv.invFun ⋙ π.map hequiv.toFun ≅ 𝟭 ↑(π.obj Y)
[PROOFSTEP]
simp only [Grpd.hom_to_functor, Grpd.id_to_functor]
[GOAL]
case η
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ 𝟙 (π.obj X) ≅ π.map hequiv.toFun ⋙ π.map hequiv.invFun
[PROOFSTEP]
convert (asIso (homotopicMapsNatIso hequiv.left_inv.some)).symm
[GOAL]
case h.e'_3
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ 𝟙 (π.obj X) = π.map (ContinuousMap.id ↑X)
case h.e'_4
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ π.map hequiv.toFun ⋙ π.map hequiv.invFun = π.map (ContinuousMap.comp hequiv.invFun hequiv.toFun)
[PROOFSTEP]
exacts [((π).map_id X).symm, ((π).map_comp _ _).symm]
[GOAL]
case ε
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ π.map hequiv.invFun ⋙ π.map hequiv.toFun ≅ 𝟙 (π.obj Y)
[PROOFSTEP]
convert asIso (homotopicMapsNatIso hequiv.right_inv.some)
[GOAL]
case h.e'_3
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ π.map hequiv.invFun ⋙ π.map hequiv.toFun = π.map (ContinuousMap.comp hequiv.toFun hequiv.invFun)
case h.e'_4
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ 𝟙 (π.obj Y) = π.map (ContinuousMap.id ↑Y)
[PROOFSTEP]
exacts [((π).map_comp _ _).symm, ((π).map_id Y).symm]
