[GOAL]
I : Type u
X : I → TopCat
x : (i : I) → ↑(π.obj (X i))
⊢ { obj := fun g => g, map := fun {X_1 Y} p => Path.Homotopic.pi p }.map (𝟙 x) =
    𝟙 ({ obj := fun g => g, map := fun {X_1 Y} p => Path.Homotopic.pi p }.obj x)
[PROOFSTEP]
change (Path.Homotopic.pi fun i => 𝟙 (x i)) = _
[GOAL]
I : Type u
X : I → TopCat
x : (i : I) → ↑(π.obj (X i))
⊢ (Path.Homotopic.pi fun i => 𝟙 (x i)) = 𝟙 ({ obj := fun g => g, map := fun {X_1 Y} p => Path.Homotopic.pi p }.obj x)
[PROOFSTEP]
simp only [FundamentalGroupoid.id_eq_path_refl, Path.Homotopic.pi_lift]
[GOAL]
I : Type u
X : I → TopCat
x : (i : I) → ↑(π.obj (X i))
⊢ Quotient.mk (Path.Homotopic.setoid (fun i => x i) fun i => x i) (Path.pi fun i => Path.refl (x i)) = 𝟙 x
[PROOFSTEP]
rfl
[GOAL]
I : Type u
X : I → TopCat
⊢ piToPiTop X ≫ CategoryTheory.Functor.pi' (proj X) = 𝟙 (CategoryTheory.Grpd.of ((i : I) → ↑(π.obj (X i))))
[PROOFSTEP]
change piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X) = 𝟭 _
[GOAL]
I : Type u
X : I → TopCat
⊢ piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X) = 𝟭 ((i : I) → ↑(π.obj (X i)))
[PROOFSTEP]
apply CategoryTheory.Functor.ext ?_ ?_
[GOAL]
I : Type u
X : I → TopCat
⊢ ∀ (X_1 : (i : I) → ↑(π.obj (X i))),
    (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X_1 = (𝟭 ((i : I) → ↑(π.obj (X i)))).obj X_1
[PROOFSTEP]
intros
[GOAL]
I : Type u
X : I → TopCat
X✝ : (i : I) → ↑(π.obj (X i))
⊢ (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X✝ = (𝟭 ((i : I) → ↑(π.obj (X i)))).obj X✝
[PROOFSTEP]
rfl
[GOAL]
I : Type u
X : I → TopCat
⊢ ∀ (X_1 Y : (i : I) → ↑(π.obj (X i))) (f : X_1 ⟶ Y),
    (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).map f =
      CategoryTheory.eqToHom
          (_ :
            (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X_1 =
              (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X_1) ≫
        (𝟭 ((i : I) → ↑(π.obj (X i)))).map f ≫
          CategoryTheory.eqToHom
            (_ : (𝟭 ((i : I) → ↑(π.obj (X i)))).obj Y = (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj Y)
[PROOFSTEP]
intros
[GOAL]
I : Type u
X : I → TopCat
X✝ Y✝ : (i : I) → ↑(π.obj (X i))
f✝ : X✝ ⟶ Y✝
⊢ (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).map f✝ =
    CategoryTheory.eqToHom
        (_ :
          (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X✝ =
            (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X✝) ≫
      (𝟭 ((i : I) → ↑(π.obj (X i)))).map f✝ ≫
        CategoryTheory.eqToHom
          (_ : (𝟭 ((i : I) → ↑(π.obj (X i)))).obj Y✝ = (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj Y✝)
[PROOFSTEP]
ext
[GOAL]
case w
I : Type u
X : I → TopCat
X✝ Y✝ : (i : I) → ↑(π.obj (X i))
f✝ : X✝ ⟶ Y✝
i✝ : I
⊢ (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).map f✝ i✝ =
    (CategoryTheory.eqToHom
          (_ :
            (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X✝ =
              (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X✝) ≫
        (𝟭 ((i : I) → ↑(π.obj (X i)))).map f✝ ≫
          CategoryTheory.eqToHom
            (_ : (𝟭 ((i : I) → ↑(π.obj (X i)))).obj Y✝ = (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj Y✝))
      i✝
[PROOFSTEP]
simp
[GOAL]
I : Type u
X : I → TopCat
⊢ CategoryTheory.Functor.pi' (proj X) ≫ piToPiTop X = 𝟙 (π.obj (TopCat.of ((i : I) → ↑(X i))))
[PROOFSTEP]
change CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X = 𝟭 _
[GOAL]
I : Type u
X : I → TopCat
⊢ CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X = 𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
[PROOFSTEP]
apply CategoryTheory.Functor.ext
[GOAL]
case h_map
I : Type u
X : I → TopCat
⊢ autoParam
    (∀ (X_1 Y : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))) (f : X_1 ⟶ Y),
      (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).map f =
        CategoryTheory.eqToHom (_ : ?F.obj X_1 = ?G.obj X_1) ≫
          (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).map f ≫
            CategoryTheory.eqToHom
              (_ :
                (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj Y =
                  (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj Y))
    _auto✝
[PROOFSTEP]
intro _ _ f
[GOAL]
case h_map
I : Type u
X : I → TopCat
X✝ Y✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
f : X✝ ⟶ Y✝
⊢ (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).map f =
    CategoryTheory.eqToHom (_ : ?F.obj X✝ = ?G.obj X✝) ≫
      (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).map f ≫
        CategoryTheory.eqToHom
          (_ :
            (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj Y✝ =
              (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj Y✝)
[PROOFSTEP]
suffices Path.Homotopic.pi ((CategoryTheory.Functor.pi' (proj X)).map f) = f by simpa
[GOAL]
I : Type u
X : I → TopCat
X✝ Y✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
f : X✝ ⟶ Y✝
this : Path.Homotopic.pi ((CategoryTheory.Functor.pi' (proj X)).map f) = f
⊢ (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).map f =
    CategoryTheory.eqToHom (_ : ?F.obj X✝ = ?G.obj X✝) ≫
      (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).map f ≫
        CategoryTheory.eqToHom
          (_ :
            (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj Y✝ =
              (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj Y✝)
[PROOFSTEP]
simpa
[GOAL]
case h_map
I : Type u
X : I → TopCat
X✝ Y✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
f : X✝ ⟶ Y✝
⊢ Path.Homotopic.pi ((CategoryTheory.Functor.pi' (proj X)).map f) = f
[PROOFSTEP]
change Path.Homotopic.pi (fun i => (CategoryTheory.Functor.pi' (proj X)).map f i) = _
[GOAL]
case h_map
I : Type u
X : I → TopCat
X✝ Y✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
f : X✝ ⟶ Y✝
⊢ (Path.Homotopic.pi fun i => (CategoryTheory.Functor.pi' (proj X)).map f i) = f
[PROOFSTEP]
simp
[GOAL]
case h_obj
I : Type u
X : I → TopCat
⊢ ∀ (X_1 : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))),
    (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj X_1 = (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj X_1
[PROOFSTEP]
intros
[GOAL]
case h_obj
I : Type u
X : I → TopCat
X✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
⊢ (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj X✝ = (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj X✝
[PROOFSTEP]
rfl
[GOAL]
I : Type u
X : I → TopCat
⊢ Limits.PreservesLimit (Discrete.functor X) π
[PROOFSTEP]
apply Limits.preservesLimitOfPreservesLimitCone (TopCat.piFanIsLimit.{u, u} X)
[GOAL]
I : Type u
X : I → TopCat
⊢ Limits.IsLimit (π.mapCone (TopCat.piFan X))
[PROOFSTEP]
apply (Limits.IsLimit.ofConeEquiv (coneDiscreteComp X)).toFun
[GOAL]
I : Type u
X : I → TopCat
⊢ Limits.IsLimit ((coneDiscreteComp X).functor.obj (π.mapCone (TopCat.piFan X)))
[PROOFSTEP]
simp only [coneDiscreteComp_obj_mapCone]
[GOAL]
I : Type u
X : I → TopCat
⊢ Limits.IsLimit (Limits.Fan.mk (π.obj (TopCat.of ((i : I) → ↑(X i)))) (proj X))
[PROOFSTEP]
apply Limits.IsLimit.ofIsoLimit _ (asIso (piTopToPiCone X)).symm
[GOAL]
I : Type u
X : I → TopCat
⊢ Limits.IsLimit (Grpd.piLimitFan fun i => π.obj (X i))
[PROOFSTEP]
exact Grpd.piLimitFanIsLimit _
[GOAL]
A B : TopCat
⊢ ∀ (X : ↑(π.obj A) × ↑(π.obj B)),
    { obj := fun g => g,
            map := fun {x y} p =>
              match x, y, p with
              | (x₀, x₁), (y₀, y₁), (p₀, p₁) => Path.Homotopic.prod p₀ p₁ }.map
        (𝟙 X) =
      𝟙
        ({ obj := fun g => g,
              map := fun {x y} p =>
                match x, y, p with
                | (x₀, x₁), (y₀, y₁), (p₀, p₁) => Path.Homotopic.prod p₀ p₁ }.obj
          X)
[PROOFSTEP]
rintro ⟨x₀, x₁⟩
[GOAL]
case mk
A B : TopCat
x₀ : ↑(π.obj A)
x₁ : ↑(π.obj B)
⊢ { obj := fun g => g,
          map := fun {x y} p =>
            match x, y, p with
            | (x₀, x₁), (y₀, y₁), (p₀, p₁) => Path.Homotopic.prod p₀ p₁ }.map
      (𝟙 (x₀, x₁)) =
    𝟙
      ({ obj := fun g => g,
            map := fun {x y} p =>
              match x, y, p with
              | (x₀, x₁), (y₀, y₁), (p₀, p₁) => Path.Homotopic.prod p₀ p₁ }.obj
        (x₀, x₁))
[PROOFSTEP]
simp only [CategoryTheory.prod_id, FundamentalGroupoid.id_eq_path_refl]
[GOAL]
case mk
A B : TopCat
x₀ : ↑(π.obj A)
x₁ : ↑(π.obj B)
⊢ Path.Homotopic.prod (𝟙 x₀) (𝟙 x₁) = 𝟙 (x₀, x₁)
[PROOFSTEP]
rfl
[GOAL]
A B : TopCat
⊢ prodToProdTop A B ≫ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) =
    𝟙 (CategoryTheory.Grpd.of (↑(π.obj A) × ↑(π.obj B)))
[PROOFSTEP]
change prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B) = 𝟭 _
[GOAL]
A B : TopCat
⊢ prodToProdTop A B ⋙ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) = 𝟭 (↑(π.obj A) × ↑(π.obj B))
[PROOFSTEP]
apply CategoryTheory.Functor.hext
[GOAL]
case h_obj
A B : TopCat
⊢ ∀ (X : ↑(π.obj A) × ↑(π.obj B)),
    (prodToProdTop A B ⋙ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B)).obj X =
      (𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X
[PROOFSTEP]
intros
[GOAL]
case h_obj
A B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (prodToProdTop A B ⋙ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B)).obj X✝ =
    (𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝
[PROOFSTEP]
ext
[GOAL]
case h_obj.h₁
A B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ ((prodToProdTop A B ⋙ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B)).obj X✝).fst =
    ((𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝).fst
[PROOFSTEP]
simp
[GOAL]
case h_obj.h₂
A B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ ((prodToProdTop A B ⋙ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B)).obj X✝).snd =
    ((𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝).snd
[PROOFSTEP]
simp
[GOAL]
case h_obj.h₁
A B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (projLeft A B).obj X✝ = X✝.fst
[PROOFSTEP]
rfl
[GOAL]
case h_obj.h₂
A B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (projRight A B).obj X✝ = X✝.snd
[PROOFSTEP]
rfl
[GOAL]
case h_map
A B : TopCat
⊢ ∀ (X Y : ↑(π.obj A) × ↑(π.obj B)) (f : X ⟶ Y),
    HEq ((prodToProdTop A B ⋙ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B)).map f)
      ((𝟭 (↑(π.obj A) × ↑(π.obj B))).map f)
[PROOFSTEP]
rintro ⟨x₀, x₁⟩ ⟨y₀, y₁⟩ ⟨f₀, f₁⟩
[GOAL]
case h_map.mk.mk.mk
A B : TopCat
x₀ : ↑(π.obj A)
x₁ : ↑(π.obj B)
y₀ : ↑(π.obj A)
y₁ : ↑(π.obj B)
f₀ : (x₀, x₁).fst ⟶ (y₀, y₁).fst
f₁ : (x₀, x₁).snd ⟶ (y₀, y₁).snd
⊢ HEq ((prodToProdTop A B ⋙ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B)).map (f₀, f₁))
    ((𝟭 (↑(π.obj A) × ↑(π.obj B))).map (f₀, f₁))
[PROOFSTEP]
have :
  Path.Homotopic.projLeft ((prodToProdTop A B).map (f₀, f₁)) = f₀ ∧
    Path.Homotopic.projRight ((prodToProdTop A B).map (f₀, f₁)) = f₁ :=
  And.intro (Path.Homotopic.projLeft_prod f₀ f₁) (Path.Homotopic.projRight_prod f₀ f₁)
[GOAL]
case h_map.mk.mk.mk
A B : TopCat
x₀ : ↑(π.obj A)
x₁ : ↑(π.obj B)
y₀ : ↑(π.obj A)
y₁ : ↑(π.obj B)
f₀ : (x₀, x₁).fst ⟶ (y₀, y₁).fst
f₁ : (x₀, x₁).snd ⟶ (y₀, y₁).snd
this :
  Path.Homotopic.projLeft ((prodToProdTop A B).map (f₀, f₁)) = f₀ ∧
    Path.Homotopic.projRight ((prodToProdTop A B).map (f₀, f₁)) = f₁
⊢ HEq ((prodToProdTop A B ⋙ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B)).map (f₀, f₁))
    ((𝟭 (↑(π.obj A) × ↑(π.obj B))).map (f₀, f₁))
[PROOFSTEP]
simpa
[GOAL]
A B : TopCat
⊢ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ≫ prodToProdTop A B = 𝟙 (π.obj (TopCat.of (↑A × ↑B)))
[PROOFSTEP]
change (projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B = 𝟭 _
[GOAL]
A B : TopCat
⊢ CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ⋙ prodToProdTop A B = 𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))
[PROOFSTEP]
apply CategoryTheory.Functor.hext
[GOAL]
case h_obj
A B : TopCat
⊢ ∀ (X : ↑(π.obj (TopCat.of (↑A × ↑B)))),
    (CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ⋙ prodToProdTop A B).obj X =
      (𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X
[PROOFSTEP]
intros
[GOAL]
case h_obj
A B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ⋙ prodToProdTop A B).obj X✝ =
    (𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝
[PROOFSTEP]
apply Prod.ext
[GOAL]
case h_obj.h₁
A B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ ((CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ⋙ prodToProdTop A B).obj X✝).fst =
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝).fst
[PROOFSTEP]
simp
[GOAL]
case h_obj.h₂
A B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ ((CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ⋙ prodToProdTop A B).obj X✝).snd =
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝).snd
[PROOFSTEP]
simp
[GOAL]
case h_obj.h₁
A B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (projLeft A B).obj X✝ = X✝.fst
[PROOFSTEP]
rfl
[GOAL]
case h_obj.h₂
A B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (projRight A B).obj X✝ = X✝.snd
[PROOFSTEP]
rfl
[GOAL]
case h_map
A B : TopCat
⊢ ∀ (X Y : ↑(π.obj (TopCat.of (↑A × ↑B)))) (f : X ⟶ Y),
    HEq ((CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ⋙ prodToProdTop A B).map f)
      ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).map f)
[PROOFSTEP]
rintro ⟨x₀, x₁⟩ ⟨y₀, y₁⟩ f
[GOAL]
case h_map.mk.mk
A B : TopCat
x₀ : ↑A
x₁ : ↑B
y₀ : ↑A
y₁ : ↑B
f : (x₀, x₁) ⟶ (y₀, y₁)
⊢ HEq ((CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ⋙ prodToProdTop A B).map f)
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).map f)
[PROOFSTEP]
have := Path.Homotopic.prod_projLeft_projRight f
[GOAL]
case h_map.mk.mk
A B : TopCat
x₀ : ↑A
x₁ : ↑B
y₀ : ↑A
y₁ : ↑B
f : (x₀, x₁) ⟶ (y₀, y₁)
this : Path.Homotopic.prod (Path.Homotopic.projLeft f) (Path.Homotopic.projRight f) = f
⊢ HEq ((CategoryTheory.Functor.prod' (projLeft A B) (projRight A B) ⋙ prodToProdTop A B).map f)
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).map f)
[PROOFSTEP]
simp only [CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.prod'_obj, prodToProdTop_obj,
  CategoryTheory.Functor.comp_map, CategoryTheory.Functor.prod'_map, projLeft_map, projRight_map,
  CategoryTheory.Functor.id_obj, CategoryTheory.Functor.id_map, heq_eq_eq]
[GOAL]
case h_map.mk.mk
A B : TopCat
x₀ : ↑A
x₁ : ↑B
y₀ : ↑A
y₁ : ↑B
f : (x₀, x₁) ⟶ (y₀, y₁)
this : Path.Homotopic.prod (Path.Homotopic.projLeft f) (Path.Homotopic.projRight f) = f
⊢ (prodToProdTop A B).map (Path.Homotopic.projLeft f, Path.Homotopic.projRight f) = f
[PROOFSTEP]
apply this
