awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasCoproduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
s : Cocone X
m : (Sigma.cocone X).pt ⟶ s.pt
hm : ∀ (j : Discrete α), (Sigma.cocone X).ι.app j ≫ m = s.ι.app j
b : α
h : Sigma.ι.{w₂, v, u} (C := C) (fun (j : α) ↦ X.obj { as := j : Discrete α }) b ≫ m = s.ι.app { as := b }
⊢ Sigma.ι.{w₂, v, u} (C := C) (fun (j : α) ↦ X.obj { as := j : Discrete α }) b ≫ m =
    CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} fun (j : α) ↦ X.obj { as := j })
      (Sigma.ι.{w₂, v, u} (C := C) (fun (j : α) ↦ X.obj { as := j }) b) (Sigma.desc fun (j : α) ↦ s.ι.app { as := j })

Tactic:
simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]

Premises used: CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasCoproduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
s : Cocone X
m : (Sigma.cocone X).pt ⟶ s.pt
hm : ∀ (j : Discrete α), (Sigma.cocone X).ι.app j ≫ m = s.ι.app j
b : α
⊢ Sigma.ι.{w₂, v, u} (C := C) (fun (j : α) ↦ X.obj { as := j : Discrete α }) b ≫ m = s.ι.app { as := b }

Tactic:
apply hm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasCoproduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
inst_2 : HasColimit X
j : α
⊢ Eq (α := X.obj { as := j : Discrete α } ⟶ colimit X)
    (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} fun (j : α) ↦ X.obj { as := j })
      (ι.{w₂, v, u} (C := C) (fun (j : α) ↦ X.obj { as := j }) j) (Iso.hom (isoColimit X)))
    (colimit.ι X { as := j })

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom (coproductIsCoproduct' X) _ _

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.Discrete.functor, CategoryTheory.Limits.colimit, CategoryTheory.Limits.coproductIsCoproduct', CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasCoproduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
inst_2 : HasColimit X
j : α
⊢ Eq (α := X.obj { as := j : Discrete α } ⟶ sigmaObj.{w₂, v, u} fun (j : α) ↦ X.obj { as := j })
    (CategoryStruct.comp (Y := colimit X) (colimit.ι X { as := j }) (Iso.inv (isoColimit X)))
    (ι.{w₂, v, u} (C := C) (fun (j : α) ↦ X.obj { as := j }) j)

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_inv _ _ _

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.Discrete.functor, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
J : Type u_1
K : Type u_2
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_1 : HasProduct.{u_1, v, u} f
inst_2 : HasProduct.{u_2, v, u} g
k : K
⊢ g ((e : (a : J) → K) ((e.symm : (a : K) → J) k : J)) = g k

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
J : Type u_1
K : Type u_2
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_1 : HasCoproduct.{u_1, v, u} f
inst_2 : HasCoproduct.{u_2, v, u} g
k : K
⊢ g k = g ((e : (a : J) → K) ((e.symm : (a : K) → J) k : J))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
ι : Type u_1
f : ι → Type u_2
g : (i : ι) → f i → C
inst_1 : ∀ (i : ι), HasProduct.{u_2, v, u} (g i)
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (i : ι) ↦ piObj.{u_2, v, u} (g i)
⊢ ∀ (s : Fan (C := C) fun (p : (i : ι) × f i) ↦ g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i)))
    (j : (i : ι) × f i),
    CategoryStruct.comp (Y :=
        Cone.pt (J := Discrete ((i : ι) × f i)) (F :=
          Discrete.functor fun (p : (i : ι) × f i) ↦
            g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i)))
          (Fan.mk (piObj.{u_1, v, u} fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) fun (X : (i : ι) × f i) ↦
            Pi.π (fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) (X.fst (β := fun (i : ι) ↦ f i)) ≫
              Pi.π (g (X.fst (β := fun (i : ι) ↦ f i))) (X.snd (β := fun (i : ι) ↦ f i))))
        ((fun
              (s :
                Fan (C := C) fun (p : (i : ι) × f i) ↦
                  g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i))) ↦
            (Pi.lift fun (b : ι) ↦ Pi.lift fun (c : f b) ↦ s.proj (Sigma.mk (β := fun (i : ι) ↦ f i) b c) :
              s.pt ⟶
                piObj.{u_1, v, u} fun (b : ι) ↦
                  piObj.{u_2, v, u} fun (c : f b) ↦
                    g ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).fst (β := fun (i : ι) ↦ f i))
                      ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).snd (β := fun (i : ι) ↦ f i))))
          s)
        (Fan.proj
          (Fan.mk (piObj.{u_1, v, u} fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) fun (X : (i : ι) × f i) ↦
            Pi.π (fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) (X.fst (β := fun (i : ι) ↦ f i)) ≫
              Pi.π (g (X.fst (β := fun (i : ι) ↦ f i))) (X.snd (β := fun (i : ι) ↦ f i)))
          j) =
      s.proj j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
ι : Type u_1
f : ι → Type u_2
g : (i : ι) → f i → C
inst_1 : ∀ (i : ι), HasProduct.{u_2, v, u} (g i)
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (i : ι) ↦ piObj.{u_2, v, u} (g i)
s : Fan (C := C) fun (p : (i : ι) × f i) ↦ g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i))
_ :
  ∀ (m : s.pt ⟶ piObj.{u_1, v, u} fun (i : ι) ↦ piObj.{u_2, v, u} (g i)),
    (∀ (j : (i : ι) × f i),
        m ≫
            Fan.proj
              (Fan.mk (piObj.{u_1, v, u} fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) fun (X : (i : ι) × f i) ↦
                Pi.π (fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) (X.fst (β := fun (i : ι) ↦ f i)) ≫
                  Pi.π (g (X.fst (β := fun (i : ι) ↦ f i))) (X.snd (β := fun (i : ι) ↦ f i)))
              j =
          s.proj j) →
      m =
        (fun
              (s :
                Fan (C := C) fun (p : (i : ι) × f i) ↦
                  g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i))) ↦
            (Pi.lift fun (b : ι) ↦ Pi.lift fun (c : f b) ↦ s.proj (Sigma.mk (β := fun (i : ι) ↦ f i) b c) :
              s.pt ⟶
                piObj.{u_1, v, u} fun (b : ι) ↦
                  piObj.{u_2, v, u} fun (c : f b) ↦
                    g ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).fst (β := fun (i : ι) ↦ f i))
                      ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).snd (β := fun (i : ι) ↦ f i))))
          s
⊢ ∀
    (m :
      s.pt ⟶
        Cone.pt (J := Discrete ((i : ι) × f i)) (F :=
          Discrete.functor fun (p : (i : ι) × f i) ↦
            g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i)))
          (Fan.mk (piObj.{u_1, v, u} fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) fun (X : (i : ι) × f i) ↦
            Pi.π (fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) (X.fst (β := fun (i : ι) ↦ f i)) ≫
              Pi.π (g (X.fst (β := fun (i : ι) ↦ f i))) (X.snd (β := fun (i : ι) ↦ f i)))),
    (∀ (j : (i : ι) × f i),
        m ≫
            Fan.proj
              (Fan.mk (piObj.{u_1, v, u} fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) fun (X : (i : ι) × f i) ↦
                Pi.π (fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) (X.fst (β := fun (i : ι) ↦ f i)) ≫
                  Pi.π (g (X.fst (β := fun (i : ι) ↦ f i))) (X.snd (β := fun (i : ι) ↦ f i)))
              j =
          s.proj j) →
      m =
        (fun
              (s :
                Fan (C := C) fun (p : (i : ι) × f i) ↦
                  g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i))) ↦
            (Pi.lift fun (b : ι) ↦ Pi.lift fun (c : f b) ↦ s.proj (Sigma.mk (β := fun (i : ι) ↦ f i) b c) :
              s.pt ⟶
                piObj.{u_1, v, u} fun (b : ι) ↦
                  piObj.{u_2, v, u} fun (c : f b) ↦
                    g ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).fst (β := fun (i : ι) ↦ f i))
                      ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).snd (β := fun (i : ι) ↦ f i))))
          s

Tactic:
(m : _ ⟶ (∏ᶜ fun i ↦ ∏ᶜ g i))
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
ι : Type u_1
f : ι → Type u_2
g : (i : ι) → f i → C
inst_1 : ∀ (i : ι), HasProduct.{u_2, v, u} (g i)
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (i : ι) ↦ piObj.{u_2, v, u} (g i)
s : Fan (C := C) fun (p : (i : ι) × f i) ↦ g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i))
m : s.pt ⟶ piObj.{u_1, v, u} fun (i : ι) ↦ piObj.{u_2, v, u} (g i)
w :
  ∀ (j : (i : ι) × f i),
    m ≫
        Fan.proj
          (Fan.mk (piObj.{u_1, v, u} fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) fun (X : (i : ι) × f i) ↦
            Pi.π (fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) (X.fst (β := fun (i : ι) ↦ f i)) ≫
              Pi.π (g (X.fst (β := fun (i : ι) ↦ f i))) (X.snd (β := fun (i : ι) ↦ f i)))
          j =
      s.proj j
⊢ m =
    (fun
          (s :
            Fan (C := C) fun (p : (i : ι) × f i) ↦
              g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i))) ↦
        (Pi.lift fun (b : ι) ↦ Pi.lift fun (c : f b) ↦ s.proj (Sigma.mk (β := fun (i : ι) ↦ f i) b c) :
          s.pt ⟶
            piObj.{u_1, v, u} fun (b : ι) ↦
              piObj.{u_2, v, u} fun (c : f b) ↦
                g ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).fst (β := fun (i : ι) ↦ f i))
                  ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).snd (β := fun (i : ι) ↦ f i))))
      s

Tactic:
aesop (add norm simp Sigma.forall)

Premises used: Sigma.forall
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
ι : Type u_1
f : ι → Type u_2
g : (i : ι) → f i → C
inst_1 : ∀ (i : ι), HasCoproduct.{u_2, v, u} (g i)
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (i : ι) ↦ sigmaObj.{u_2, v, u} (g i)
⊢ ∀ (t : Cofan (C := C) fun (p : (i : ι) × f i) ↦ g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i)))
    (j : (i : ι) × f i),
    CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete ((i : ι) × f i)) (F :=
          Discrete.functor fun (p : (i : ι) × f i) ↦
            g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i)))
          (Cofan.mk (sigmaObj.{u_1, v, u} fun (i : ι) ↦ sigmaObj.{u_2, v, u} (g i)) fun (X : (i : ι) × f i) ↦
            CategoryStruct.comp (Y :=
              sigmaObj.{u_2, v, u} (β := f (X.fst (β := fun (i : ι) ↦ f i))) (g (X.fst (β := fun (i : ι) ↦ f i))))
              (Sigma.ι (g (X.fst (β := fun (i : ι) ↦ f i))) (X.snd (β := fun (i : ι) ↦ f i)))
              (Sigma.ι.{u_1, v, u} (C := C) (fun (i : ι) ↦ sigmaObj.{u_2, v, u} (g i))
                (X.fst (β := fun (i : ι) ↦ f i)))))
        (Cofan.inj (C := C) (f := fun (p : (i : ι) × f i) ↦
          g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i)))
          (Cofan.mk (sigmaObj.{u_1, v, u} fun (i : ι) ↦ sigmaObj.{u_2, v, u} (g i)) fun (X : (i : ι) × f i) ↦
            CategoryStruct.comp (Y :=
              sigmaObj.{u_2, v, u} (β := f (X.fst (β := fun (i : ι) ↦ f i))) (g (X.fst (β := fun (i : ι) ↦ f i))))
              (Sigma.ι (g (X.fst (β := fun (i : ι) ↦ f i))) (X.snd (β := fun (i : ι) ↦ f i)))
              (Sigma.ι.{u_1, v, u} (C := C) (fun (i : ι) ↦ sigmaObj.{u_2, v, u} (g i))
                (X.fst (β := fun (i : ι) ↦ f i))))
          j)
        ((fun
              (s :
                Cofan (C := C) fun (p : (i : ι) × f i) ↦
                  g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i))) ↦
            (Sigma.desc fun (b : ι) ↦ Sigma.desc fun (c : f b) ↦ s.inj (Sigma.mk (β := fun (i : ι) ↦ f i) b c) :
              (sigmaObj.{u_1, v, u} fun (b : ι) ↦
                  sigmaObj.{u_2, v, u} fun (c : f b) ↦
                    g ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).fst (β := fun (i : ι) ↦ f i))
                      ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).snd (β := fun (i : ι) ↦ f i))) ⟶
                s.pt))
          t) =
      t.inj j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : β → C
inst_2 : HasProduct.{w, v, u} f
inst_3 : HasProduct.{w, v₂, u₂} (C := D) fun (b : β) ↦ G.obj (f b)
b : β
⊢ Eq (α := G.obj (piObj.{w, v, u} f) ⟶ G.obj (f b))
    (CategoryStruct.comp (Y := piObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b)) (piComparison G f)
      (Pi.π (fun (b : β) ↦ G.obj (f b)) b))
    (G.map (Pi.π f b))

Tactic:
limit.lift_π _ (Discrete.mk b)

Premises used: CategoryTheory.Limits.piComparison, CategoryTheory.Discrete.mk, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : β → C
inst_2 : HasProduct.{w, v, u} f
inst_3 : HasProduct.{w, v₂, u₂} (C := D) fun (b : β) ↦ G.obj (f b)
P : C
g : (j : β) → P ⟶ f j
h :
  ∀ (j : β),
    CategoryStruct.comp (Y := piObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b))
        (CategoryStruct.comp (Y := G.obj (piObj.{w, v, u} f)) (G.map (Pi.lift g)) (piComparison G f))
        (Pi.π (fun (b : β) ↦ G.obj (f b)) j) =
      CategoryStruct.comp (Y := piObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b)) (Pi.lift fun (j : β) ↦ G.map (g j))
        (Pi.π (fun (b : β) ↦ G.obj (f b)) j)
⊢ Eq (α := G.obj P ⟶ piObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b))
    (CategoryStruct.comp (Y := G.obj (piObj.{w, v, u} f)) (G.map (Pi.lift g)) (piComparison G f))
    (Pi.lift fun (j : β) ↦ G.map (g j))

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : β → C
inst_2 : HasProduct.{w, v, u} f
inst_3 : HasProduct.{w, v₂, u₂} (C := D) fun (b : β) ↦ G.obj (f b)
P : C
g : (j : β) → P ⟶ f j
j : β
⊢ CategoryStruct.comp (Y := piObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b))
      (CategoryStruct.comp (Y := G.obj (piObj.{w, v, u} f)) (G.map (Pi.lift g)) (piComparison G f))
      (Pi.π (fun (b : β) ↦ G.obj (f b)) j) =
    CategoryStruct.comp (Y := piObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b)) (Pi.lift fun (j : β) ↦ G.map (g j))
      (Pi.π (fun (b : β) ↦ G.obj (f b)) j)

Tactic:
simp only [Category.assoc, piComparison_comp_π, ← G.map_comp,
    limit.lift_π, Fan.mk_pt, Fan.mk_π_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.piComparison_comp_π, CategoryTheory.Limits.Fan.mk_pt, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.Fan.mk_π_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : β → C
inst_2 : HasCoproduct.{w, v, u} f
inst_3 : HasCoproduct.{w, v₂, u₂} (C := D) fun (b : β) ↦ G.obj (f b)
b : β
⊢ Eq (α := G.obj (f b) ⟶ G.obj (sigmaObj.{w, v, u} f))
    (CategoryStruct.comp (Y := sigmaObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b))
      (Sigma.ι.{w, v₂, u₂} (C := D) (fun (b : β) ↦ G.obj (f b)) b) (sigmaComparison G f))
    (G.map (Sigma.ι f b))

Tactic:
colimit.ι_desc _ (Discrete.mk b)

Premises used: CategoryTheory.Limits.sigmaComparison, CategoryTheory.Discrete.mk, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.Limits.colimit.desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : β → C
inst_2 : HasCoproduct.{w, v, u} f
inst_3 : HasCoproduct.{w, v₂, u₂} (C := D) fun (b : β) ↦ G.obj (f b)
P : C
g : (j : β) → f j ⟶ P
h :
  ∀ (j : β),
    CategoryStruct.comp (Y := sigmaObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b))
        (Sigma.ι.{w, v₂, u₂} (C := D) (fun (b : β) ↦ G.obj (f b)) j)
        (CategoryStruct.comp (Y := G.obj (sigmaObj.{w, v, u} f)) (sigmaComparison G f) (G.map (Sigma.desc g))) =
      CategoryStruct.comp (Y := sigmaObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b))
        (Sigma.ι.{w, v₂, u₂} (C := D) (fun (b : β) ↦ G.obj (f b)) j) (Sigma.desc fun (j : β) ↦ G.map (g j))
⊢ Eq (α := (sigmaObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b)) ⟶ G.obj P)
    (CategoryStruct.comp (Y := G.obj (sigmaObj.{w, v, u} f)) (sigmaComparison G f) (G.map (Sigma.desc g)))
    (Sigma.desc fun (j : β) ↦ G.map (g j))

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : β → C
inst_2 : HasCoproduct.{w, v, u} f
inst_3 : HasCoproduct.{w, v₂, u₂} (C := D) fun (b : β) ↦ G.obj (f b)
P : C
g : (j : β) → f j ⟶ P
j : β
⊢ CategoryStruct.comp (Y := sigmaObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b))
      (Sigma.ι.{w, v₂, u₂} (C := D) (fun (b : β) ↦ G.obj (f b)) j)
      (CategoryStruct.comp (Y := G.obj (sigmaObj.{w, v, u} f)) (sigmaComparison G f) (G.map (Sigma.desc g))) =
    CategoryStruct.comp (Y := sigmaObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b))
      (Sigma.ι.{w, v₂, u₂} (C := D) (fun (b : β) ↦ G.obj (f b)) j) (Sigma.desc fun (j : β) ↦ G.map (g j))

Tactic:
simp only [ι_comp_sigmaComparison_assoc, ← G.map_comp, colimit.ι_desc,
    Cofan.mk_pt, Cofan.mk_ι_app]

Premises used: CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.ι_comp_sigmaComparison_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts C
⊢ HasProducts.{w, v, u} C

Tactic:
fun J =>
  hasLimitsOfShape_of_equivalence (Discrete.equivalence Equiv.ulift : Discrete (ULift.{w'} J) ≌ _)

Premises used: Equiv.ulift, CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.hasLimitsOfShape_of_equivalence
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts C
⊢ HasCoproducts.{w, v, u} C

Tactic:
fun J =>
  hasColimitsOfShape_of_equivalence (Discrete.equivalence Equiv.ulift : Discrete (ULift.{w'} J) ≌ _)

Premises used: Equiv.ulift, CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{w, v, u} C
⊢ HasProducts.{0, v, u} C

Tactic:
hasProducts_shrink

Premises used: CategoryTheory.Limits.hasProducts_shrink
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
⊢ HasCoproducts.{0, v, u} C

Tactic:
hasCoproducts_shrink

Premises used: CategoryTheory.Limits.hasCoproducts_shrink
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
lf : {J : Type w} → (f : J → C) → Fan.{w, v, u} f
lf_isLimit : {J : Type w} → (f : J → C) → IsLimit (lf f)
⊢ HasProducts.{w, v, u} C

Tactic:
fun _ : Type w =>
  { has_limit := fun F =>
      HasLimit.mk
        ⟨(Cone.postcompose Discrete.natIsoFunctor.inv).obj (lf fun j => F.obj ⟨j⟩),
          (IsLimit.postcomposeInvEquiv _ _).symm (lf_isLimit _)⟩ }

Premises used: CategoryTheory.Limits.IsLimit.postcomposeInvEquiv, CategoryTheory.Limits.HasLimitsOfShape.mk, CategoryTheory.Discrete.natIsoFunctor, CategoryTheory.Discrete.mk, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.mk, Equiv.symm, DFunLike.coe, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj, CategoryTheory.Limits.Cone.postcompose
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
cf : {J : Type w} → (f : J → C) → Cofan.{w, v, u} f
cf_isColimit : {J : Type w} → (f : J → C) → IsColimit (cf f)
⊢ HasCoproducts.{w, v, u} C

Tactic:
fun _ : Type w =>
  { has_colimit := fun F =>
      HasColimit.mk
        ⟨(Cocone.precompose Discrete.natIsoFunctor.hom).obj (cf fun j => F.obj ⟨j⟩),
          (IsColimit.precomposeHomEquiv _ _).symm (cf_isColimit _)⟩ }

Premises used: CategoryTheory.Limits.Cocone.precompose, CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Discrete.natIsoFunctor, CategoryTheory.Discrete.mk, CategoryTheory.Limits.ColimitCocone.mk, Equiv.symm, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeHomEquiv, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{w, v, u} C
J : Type w
⊢ HasProductsOfShape.{w, u, v} J C

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
J : Type w
⊢ HasCoproductsOfShape.{w, u, v} J C

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v, v, u} C
X : C
x x_1 : Cᵒᵖ
x_2 : x ⟶ x_1
a :
  Eq (α :=
    Opposite.unop (Functor.obj.{v, v, u, u} (𝟭 Cᵒᵖ) x_1) ⟶
      Opposite.unop (Functor.obj.{v, v, u, u} (Functor.obj yoneda X ⋙ Functor.rightOp (Functor.obj piConst X)) x))
    (Quiver.Hom.unop
      (Functor.map (Functor.obj yoneda X ⋙ Functor.rightOp (Functor.obj piConst X)) x_2 ≫ Quiver.Hom.op (Pi.lift id)))
    (Quiver.Hom.unop (Quiver.Hom.op (Pi.lift id) ≫ Functor.map (𝟭 Cᵒᵖ) x_2))
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (Functor.obj yoneda X ⋙ Functor.rightOp (Functor.obj piConst X)) x ⟶
      Functor.obj.{v, v, u, u} (𝟭 Cᵒᵖ) x_1)
    (Functor.map (Functor.obj yoneda X ⋙ Functor.rightOp (Functor.obj piConst X)) x_2 ≫ Quiver.Hom.op (Pi.lift id))
    (Quiver.Hom.op (Pi.lift id) ≫ Functor.map (𝟭 Cᵒᵖ) x_2)

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj