awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x₀ x₁ : (↑X : Type u)
p : fromTop x₀ ⟶ fromTop x₁
⊢ hcast ⋯ ≫
      (π.map (TopCat.ofHom H.uliftMap)).map
          (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
            (Prod.mkHom uhpath01 p)) ≫
        hcast ⋯ =
    H.diagonalPath' p

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x₀ x₁ : (↑X : Type u)
p : fromTop x₀ ⟶ fromTop x₁
a :
  ((π.map (TopCat.ofHom H.uliftMap)).map
        (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
          (uhpath01, 𝟙 (fromTop x₀))) ≫
      𝟙
        ((π.map (TopCat.ofHom H.uliftMap)).obj
          (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
            (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
            ({ as := { down := 1 : ULift.{u, 0} (↑I : Type) } : FundamentalGroupoid (ULift.{u, 0} (↑I : Type)) },
              { as := x₀ : FundamentalGroupoid (↑X : Type u) }))) :
    Quiver.Hom (V := (↑(π.obj Y) : Type u)) (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x₀)))
      (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (1, x₀))))
| ((π.map (TopCat.ofHom H.uliftMap)).map
        (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
          (uhpath01, 𝟙 (fromTop x₀))) ≫
      hcast ⋯ ≫ hcast ⋯ :
    Quiver.Hom (V := (↑(π.obj Y) : Type u)) (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x₀)))
      (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (1, x₀))))

Tactic:
rw [eqToHom_trans, eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.eqToHom_trans
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x₀ x₁ : (↑X : Type u)
p : fromTop x₀ ⟶ fromTop x₁
right :
  hcast ⋯ ≫
      CategoryStruct.comp (Y := fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (1, x₀)))
          ((π.map (TopCat.ofHom H.uliftMap)).map
                (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                  (uhpath01, 𝟙 (fromTop x₀))) ≫
              𝟙
                ((π.map (TopCat.ofHom H.uliftMap)).obj
                  (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                    (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                    ({ as := { down := 1 : ULift.{u, 0} (↑I : Type) } :
                        FundamentalGroupoid (ULift.{u, 0} (↑I : Type)) },
                      { as := x₀ : FundamentalGroupoid (↑X : Type u) }))) :
            Quiver.Hom (V := (↑(π.obj Y) : Type u))
              (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x₀)))
              (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (1, x₀))))
          ((π.map (TopCat.ofHom H.uliftMap)).map
              (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                (𝟙 (fromTop { down := 1 }), p)) :
            (π.map (TopCat.ofHom H.uliftMap)).obj
                (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                  (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                  ({ as := { down := 1 : ULift.{u, 0} (↑I : Type) } : FundamentalGroupoid (ULift.{u, 0} (↑I : Type)) },
                    { as := x₀ : FundamentalGroupoid (↑X : Type u) })) ⟶
              (π.map (TopCat.ofHom H.uliftMap)).obj
                (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                  (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X) ({ as := { down := 1 } }, { as := x₁ }))) ≫
        hcast ⋯ =
    H.diagonalPath' p
⊢ (hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
              (uhpath01, 𝟙 (fromTop x₀))) ≫
          hcast ⋯) ≫
      hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
              (𝟙 (fromTop { down := 1 : ULift.{u, 0} (↑I : Type) }), p)) ≫
          hcast ⋯ =
    H.diagonalPath' p

Tactic:
slice_lhs 2 4 => rw [eqToHom_trans, eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.eqToHom_trans
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x₀ x₁ : (↑X : Type u)
p : fromTop x₀ ⟶ fromTop x₁
a :
  ((π.map (TopCat.ofHom H.uliftMap)).map
      (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X) (Prod.mkHom uhpath01 p)) :
    (π.map (TopCat.ofHom H.uliftMap)).obj
        { as := ({ down := 0 : ULift.{u, 0} (↑I : Type) }, x₀) :
          FundamentalGroupoid (ULift.{u, 0} (↑I : Type) × (↑X : Type u)) } ⟶
      (π.map (TopCat.ofHom H.uliftMap)).obj { as := ({ down := 1 }, x₁) })
| ((π.map (TopCat.ofHom H.uliftMap)).map
        (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
          (uhpath01, 𝟙 (fromTop x₀))) ≫
      𝟙
          ((π.map (TopCat.ofHom H.uliftMap)).obj
            (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
              (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
              ({ as := { down := 1 : ULift.{u, 0} (↑I : Type) } : FundamentalGroupoid (ULift.{u, 0} (↑I : Type)) },
                { as := x₀ : FundamentalGroupoid (↑X : Type u) }))) ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
          (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
            (𝟙 (fromTop { down := 1 : ULift.{u, 0} (↑I : Type) }), p)) :
    fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x₀)) ⟶
      (π.map (TopCat.ofHom H.uliftMap)).obj
        (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
          (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
          ({ as := { down := 1 : ULift.{u, 0} (↑I : Type) } : FundamentalGroupoid (ULift.{u, 0} (↑I : Type)) },
            { as := x₁ : FundamentalGroupoid (↑X : Type u) })))

Tactic:
simp [← CategoryTheory.Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x₀ x₁ : (↑X : Type u)
p : fromTop x₀ ⟶ fromTop x₁
right :
  hcast ⋯ ≫
      (π.map (TopCat.ofHom H.uliftMap)).map
          (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
            (Prod.mkHom uhpath01 p)) ≫
        hcast ⋯ =
    H.diagonalPath' p
⊢ hcast ⋯ ≫
      CategoryStruct.comp (Y := fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (1, x₀)))
          ((π.map (TopCat.ofHom H.uliftMap)).map
                (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                  (uhpath01, 𝟙 (fromTop x₀))) ≫
              𝟙
                ((π.map (TopCat.ofHom H.uliftMap)).obj
                  (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                    (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                    ({ as := { down := 1 : ULift.{u, 0} (↑I : Type) } :
                        FundamentalGroupoid (ULift.{u, 0} (↑I : Type)) },
                      { as := x₀ : FundamentalGroupoid (↑X : Type u) }))) :
            Quiver.Hom (V := (↑(π.obj Y) : Type u))
              (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x₀)))
              (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (1, x₀))))
          ((π.map (TopCat.ofHom H.uliftMap)).map
              (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                (𝟙 (fromTop { down := 1 }), p)) :
            (π.map (TopCat.ofHom H.uliftMap)).obj
                (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                  (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                  ({ as := { down := 1 : ULift.{u, 0} (↑I : Type) } : FundamentalGroupoid (ULift.{u, 0} (↑I : Type)) },
                    { as := x₀ : FundamentalGroupoid (↑X : Type u) })) ⟶
              (π.map (TopCat.ofHom H.uliftMap)).obj
                (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                  (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X) ({ as := { down := 1 } }, { as := x₁ }))) ≫
        hcast ⋯ =
    H.diagonalPath' p

Tactic:
slice_lhs 2 4 => simp [← CategoryTheory.Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit
Goal:
x y : Path PUnit.unit PUnit.unit
⊢ x = y

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit
Goal:
x y : FundamentalGroupoid PUnit.{u_1 + 1}
convert_to : Subsingleton.{u_1 + 1} (Path.Homotopic.Quotient PUnit.unit PUnit.unit)
⊢ Subsingleton.{u_1 + 1} (x ⟶ y)

Tactic:
convert_to Subsingleton (Path.Homotopic.Quotient PUnit.unit PUnit.unit)

Premises used: Path.Homotopic.Quotient, Subsingleton, PUnit.unit
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit
Goal:
x y : FundamentalGroupoid PUnit.{u_1 + 1}
⊢ Subsingleton.{u_1 + 1} (Path.Homotopic.Quotient PUnit.unit PUnit.unit)

Tactic:
apply Quotient.instSubsingletonQuotient

Premises used: Quotient.instSubsingletonQuotient
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
i : I
x₀ x₁ : (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)
p : x₀ ⟶ x₁
⊢ (proj X i).map p = Path.Homotopic.proj (X := fun (i : I) ↦ (↑(X i) : Type u)) i p

Tactic:
rfl

Premises used: iInf, Quotient.map, Path.Homotopic.Quotient.map, Quot.map, rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
x : (i : I) → (↑(π.obj (X i)) : Type u)
change :
  Eq.{u + 1} (α :=
    Path.Homotopic.Quotient (X := (i : I) → (↑(X i) : Type u)) (FundamentalGroupoid.as { as := fun (i : I) ↦ (x i).as })
      (FundamentalGroupoid.as { as := fun (i : I) ↦ (x i).as }))
    (Path.Homotopic.pi (X := fun (i : I) ↦ (↑(X i) : Type u)) fun (i : I) ↦
      Path.Homotopic.Quotient.mk (Path.refl (x i).as))
    (𝟙 { as := fun (i : I) ↦ (x i).as })
⊢ Path.Homotopic.pi (X := fun (i : I) ↦ (↑(X i) : Type u)) (𝟙 x) = 𝟙 { as := fun (i : I) ↦ (x i).as }

Tactic:
change (Path.Homotopic.pi fun i => Path.Homotopic.Quotient.mk _) = _

Premises used: Path.Homotopic.pi, Path.Homotopic.Quotient.mk
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
x : (i : I) → (↑(π.obj (X i)) : Type u)
simp :
  Eq.{u + 1} (α :=
    Path.Homotopic.Quotient (X := (i : I) → (↑(X i) : Type u)) (fun (i : I) ↦ (x i).as) fun (i : I) ↦ (x i).as)
    (Path.Homotopic.Quotient.mk (Path.pi (χ := fun (i : I) ↦ (↑(X i) : Type u)) fun (i : I) ↦ Path.refl (x i).as))
    (𝟙 { as := fun (i : I) ↦ (x i).as })
⊢ Eq.{u + 1} (α :=
    Path.Homotopic.Quotient (X := (i : I) → (↑(X i) : Type u)) (FundamentalGroupoid.as { as := fun (i : I) ↦ (x i).as })
      (FundamentalGroupoid.as { as := fun (i : I) ↦ (x i).as }))
    (Path.Homotopic.pi (X := fun (i : I) ↦ (↑(X i) : Type u)) fun (i : I) ↦
      Path.Homotopic.Quotient.mk (Path.refl (x i).as))
    (𝟙 { as := fun (i : I) ↦ (x i).as })

Tactic:
simp only [Path.Homotopic.pi_lift]

Premises used: Path.Homotopic.pi_lift
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
x : (i : I) → (↑(π.obj (X i)) : Type u)
⊢ Eq.{u + 1} (α :=
    Path.Homotopic.Quotient (X := (i : I) → (↑(X i) : Type u)) (fun (i : I) ↦ (x i).as) fun (i : I) ↦ (x i).as)
    (Path.Homotopic.Quotient.mk (Path.pi (χ := fun (i : I) ↦ (↑(X i) : Type u)) fun (i : I) ↦ Path.refl (x i).as))
    (𝟙 { as := fun (i : I) ↦ (x i).as })

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
apply :
  ∀ (X_1 : (i : I) → (↑(π.obj (X i)) : Type u)),
    (piToPiTop X ⋙ CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X)).obj X_1 =
      CategoryTheory.Functor.obj (𝟭 ((i : I) → (↑(π.obj (X i)) : Type u))) X_1
apply₁ :
  ∀ (X_1 Y : (i : I) → (↑(π.obj (X i)) : Type u)) (f : X_1 ⟶ Y),
    (piToPiTop X ⋙ CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X)).map f =
      CategoryTheory.eqToHom ⋯ ≫
        CategoryTheory.Functor.map (𝟭 ((i : I) → (↑(π.obj (X i)) : Type u))) f ≫ CategoryTheory.eqToHom ⋯
⊢ piToPiTop X ⋙ CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X) =
    𝟭 ((i : I) → (↑(π.obj (X i)) : Type u))

Tactic:
apply CategoryTheory.Functor.ext ?_ ?_

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
X_1 : (i : I) → (↑(π.obj (X i)) : Type u)
⊢ (piToPiTop X ⋙ CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X)).obj X_1 =
    CategoryTheory.Functor.obj (𝟭 ((i : I) → (↑(π.obj (X i)) : Type u))) X_1

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
X_1 Y : (i : I) → (↑(π.obj (X i)) : Type u)
f : X_1 ⟶ Y
w :
  ∀ (i : I),
    (piToPiTop X ⋙ CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X)).map f i =
      (CategoryTheory.eqToHom ⋯ ≫
          CategoryTheory.Functor.map (𝟭 ((i : I) → (↑(π.obj (X i)) : Type u))) f ≫ CategoryTheory.eqToHom ⋯)
        i
⊢ (piToPiTop X ⋙ CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X)).map f =
    CategoryTheory.eqToHom ⋯ ≫
      CategoryTheory.Functor.map (𝟭 ((i : I) → (↑(π.obj (X i)) : Type u))) f ≫ CategoryTheory.eqToHom ⋯

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
X_1 Y : (i : I) → (↑(π.obj (X i)) : Type u)
f : X_1 ⟶ Y
i : I
⊢ (piToPiTop X ⋙ CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X)).map f i =
    (CategoryTheory.eqToHom ⋯ ≫
        CategoryTheory.Functor.map (𝟭 ((i : I) → (↑(π.obj (X i)) : Type u))) f ≫ CategoryTheory.eqToHom ⋯)
      i

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
h_map :
  autoParam
    (∀ (X_1 Y : (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)) (f : X_1 ⟶ Y),
      (CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X) ⋙ piToPiTop X).map f =
        CategoryTheory.eqToHom ⋯ ≫
          CategoryTheory.Functor.map (𝟭 (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)) f ≫
            CategoryTheory.eqToHom ⋯)
    CategoryTheory.Functor.ext._auto_1
h_obj :
  ∀ (X_1 : (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)),
    (CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X) ⋙ piToPiTop X).obj X_1 =
      CategoryTheory.Functor.obj (𝟭 (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)) X_1
⊢ CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X) ⋙ piToPiTop X =
    𝟭 (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)

Tactic:
apply CategoryTheory.Functor.ext

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
X_1 : (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)
h_map :
  ∀ (Y : (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)) (f : X_1 ⟶ Y),
    (CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X) ⋙ piToPiTop X).map f =
      CategoryTheory.eqToHom ⋯ ≫
        CategoryTheory.Functor.map (𝟭 (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)) f ≫
          CategoryTheory.eqToHom ⋯
⊢ ∀ (Y : (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)) (f : X_1 ⟶ Y),
    (CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X) ⋙ piToPiTop X).map f =
      CategoryTheory.eqToHom ⋯ ≫
        CategoryTheory.Functor.map (𝟭 (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)) f ≫
          CategoryTheory.eqToHom ⋯

Tactic:
_
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
X_1 Y : (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)
f : X_1 ⟶ Y
this :
  Path.Homotopic.pi (X := fun (i : I) ↦ (↑(X i) : Type u))
      ((CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X)).map f) =
    f
⊢ (CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X) ⋙ piToPiTop X).map f =
    CategoryTheory.eqToHom ⋯ ≫
      CategoryTheory.Functor.map (𝟭 (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)) f ≫
        CategoryTheory.eqToHom ⋯

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
X_1 Y : (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)
f : X_1 ⟶ Y
h_map :
  Path.Homotopic.pi (X := fun (i : I) ↦ (↑(X i) : Type u))
      ((CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X)).map f) =
    f
⊢ (CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X) ⋙ piToPiTop X).map f =
    CategoryTheory.eqToHom ⋯ ≫
      CategoryTheory.Functor.map (𝟭 (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)) f ≫
        CategoryTheory.eqToHom ⋯

Tactic:
suffices Path.Homotopic.pi ((CategoryTheory.Functor.pi' (proj X)).map f) = f by simpa
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
X_1 Y : (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)
f : X_1 ⟶ Y
⊢ (Path.Homotopic.pi (X := fun (i : I) ↦ (↑(X i) : Type u)) fun (i : I) ↦
      (CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X)).map f i) =
    f

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
X_1 : (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)
⊢ (CategoryTheory.Functor.pi' (C := fun (i : I) ↦ (↑(π.obj (X i)) : Type u)) (proj X) ⋙ piToPiTop X).obj X_1 =
    CategoryTheory.Functor.obj (𝟭 (↑(π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) : Type u)) X_1

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
⊢ (coneDiscreteComp X).functor.obj (π.mapCone (TopCat.piFan X)) =
    Limits.Fan.mk (π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) (proj X)

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Limits.Fan.mk, CategoryTheory.Functor.comp, Quotient.map, Path.Homotopic.Quotient.map, CategoryTheory.Discrete.natTrans, FundamentalGroupoid.map, Quot.map, FundamentalGroupoidFunctor.proj, rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
⊢ IsIso (piTopToPiCone X)

Tactic:
haveI : IsIso (piTopToPiCone X).hom := (inferInstance : IsIso (piIso X).inv)
  Limits.Cone.cone_iso_of_hom_iso (piTopToPiCone X)

Premises used: CategoryTheory.Limits.Cone.cone_iso_of_hom_iso, FundamentalGroupoidFunctor.piTopToPiCone
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
apply : Limits.IsLimit (π.mapCone (TopCat.piFan X))
⊢ Limits.PreservesLimit (Discrete.functor X) π

Tactic:
apply Limits.preservesLimit_of_preserves_limit_cone (TopCat.piFanIsLimit X)

Premises used: TopCat.piFanIsLimit, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
apply : Limits.IsLimit ((coneDiscreteComp X).functor.obj (π.mapCone (TopCat.piFan X)))
⊢ Limits.IsLimit (π.mapCone (TopCat.piFan X))

Tactic:
apply (Limits.IsLimit.ofConeEquiv (coneDiscreteComp X)).toFun

Premises used: Equiv.toFun, CategoryTheory.Limits.IsLimit.ofConeEquiv, FundamentalGroupoidFunctor.coneDiscreteComp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
simp : Limits.IsLimit (Limits.Fan.mk (π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) (proj X))
⊢ Limits.IsLimit ((coneDiscreteComp X).functor.obj (π.mapCone (TopCat.piFan X)))

Tactic:
simp only [coneDiscreteComp_obj_mapCone]

Premises used: FundamentalGroupoidFunctor.coneDiscreteComp_obj_mapCone
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
I : Type u
X : I → TopCat
apply :
  Limits.IsLimit (J := Discrete I) (F := Discrete.functor fun (i : I) ↦ π.obj (X i))
    (Grpd.piLimitFan fun (i : I) ↦ π.obj (X i))
⊢ Limits.IsLimit (Limits.Fan.mk (π.obj (TopCat.of ((i : I) → (↑(X i) : Type u)))) (proj X))

Tactic:
apply Limits.IsLimit.ofIsoLimit _ (asIso (piTopToPiCone X)).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.asIso, FundamentalGroupoidFunctor.piTopToPiCone
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
x₀ x₁ : (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v))
p : x₀ ⟶ x₁
⊢ (projLeft A B).map p = Path.Homotopic.projLeft p

Tactic:
rfl

Premises used: Quotient.map, Path.Homotopic.Quotient.map, Quot.map, rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
x₀ x₁ : (↑(π.obj (TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v)))) : Type (max u v))
p : x₀ ⟶ x₁
⊢ (projRight A B).map p = Path.Homotopic.projRight p

Tactic:
rfl

Premises used: Quotient.map, Path.Homotopic.Quotient.map, Quot.map, rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
x₀ : (↑(π.obj A) : Type u)
x₁ : (↑(π.obj B) : Type v)
simp : Path.Homotopic.prod (𝟙 x₀) (𝟙 x₁) = 𝟙 { as := (x₀.as, x₁.as) }
⊢ Eq (α :=
    { as := ((x₀, x₁).1.as, (x₀, x₁).2.as) :
        FundamentalGroupoid (↑(TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v))) : Type (max v u)) } ⟶
      { as := ((x₀, x₁).1.as, (x₀, x₁).2.as) })
    (match (motive :=
        (x y : Prod.{u, v} (↑(π.obj A) : Type u) (↑(π.obj B) : Type v)) →
          (x ⟶ y) →
            ({ as := (x.1.as, x.2.as) :
                FundamentalGroupoid (↑(TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v))) : Type (max v u)) } ⟶
              { as := (y.1.as, y.2.as) }))
        (x₀, x₁), (x₀, x₁), 𝟙 (x₀, x₁) with
      | (fst, snd), (fst_1, snd_1), (p₀, p₁) => Path.Homotopic.prod p₀ p₁ :
      { as := ((x₀, x₁).1.as, (x₀, x₁).2.as) :
          FundamentalGroupoid (↑(TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v))) : Type (max v u)) } ⟶
        { as := ((x₀, x₁).1.as, (x₀, x₁).2.as) })
    (𝟙 { as := ((x₀, x₁).1.as, (x₀, x₁).2.as) } :
      { as := ((x₀, x₁).1.as, (x₀, x₁).2.as) :
          FundamentalGroupoid (↑(TopCat.of (Prod.{u, v} (↑A : Type u) (↑B : Type v))) : Type (max v u)) } ⟶
        { as := ((x₀, x₁).1.as, (x₀, x₁).2.as) })

Tactic:
simp only
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
x₀ : (↑(π.obj A) : Type u)
x₁ : (↑(π.obj B) : Type v)
⊢ Path.Homotopic.prod (𝟙 x₀) (𝟙 x₁) = 𝟙 { as := (x₀.as, x₁.as) }

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
Goal:
A : TopCat
B : TopCat
x₀ x₁ : (↑(π.obj A) : Type u)
y₀ y₁ : (↑(π.obj B) : Type v)
p₀ : x₀ ⟶ x₁
p₁ : y₀ ⟶ y₁
⊢ (prodToProdTop A B).map (p₀, p₁) = Path.Homotopic.prod p₀ p₁

Tactic:
rfl

Premises used: Path.Homotopic.prod, Quotient.map₂, rfl