awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
a :
  ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
    (hc.coconePointUniqueUpToIso hc').op.inv.unop
⊢ (opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv = (hc.coconePointUniqueUpToIso hc').op.inv

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
a :
  ∀ (j : Discrete α),
    c'.ι.app j ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
      c'.ι.app j ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop
⊢ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
    (hc.coconePointUniqueUpToIso hc').op.inv.unop

Tactic:
apply hc'.hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
a :
  c'.inj j ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
    c'.ι.app { as := j } ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop
⊢ Eq (α := obj.{u_1, v₁, u_1, u₁} (Discrete.functor Z) { as := j : Discrete α } ⟶ unop (op c.pt))
    (c'.ι.app { as := j } ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop)
    (c'.ι.app { as := j } ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop)

Tactic:
change c'.inj _ ≫ _ = _

Premises used: CategoryTheory.Limits.Cofan.inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
a : c'.inj j ≫ (opCoproductIsoProduct' hc' hf).inv.unop ≫ (opCoproductIsoProduct' hc hf).hom.unop = c.ι.app { as := j }
⊢ c'.inj j ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
    c'.ι.app { as := j } ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop

Tactic:
simp only [unop_op, unop_comp, Discrete.functor_obj, const_obj_obj, Iso.op_inv,
    Quiver.Hom.unop_op, IsColimit.comp_coconePointUniqueUpToIso_inv]

Premises used: Quiver.Hom.unop_op, CategoryTheory.Discrete.functor_obj, CategoryTheory.Iso.op_inv, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.unop_comp, Opposite.unop_op, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
a :
  (c'.inj j ≫ (opCoproductIsoProduct' hc' hf).inv.unop ≫ (opCoproductIsoProduct' hc hf).hom.unop).op =
    Quiver.Hom.op (c.ι.app { as := j })
⊢ c'.inj j ≫ (opCoproductIsoProduct' hc' hf).inv.unop ≫ (opCoproductIsoProduct' hc hf).hom.unop = c.ι.app { as := j }

Tactic:
apply Quiver.Hom.op_inj

Premises used: Quiver.Hom.op_inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
a : (opCoproductIsoProduct' hc hf).hom ≫ f.proj j = Quiver.Hom.op (c.ι.app { as := j })
⊢ (c'.inj j ≫ (opCoproductIsoProduct' hc' hf).inv.unop ≫ (opCoproductIsoProduct' hc hf).hom.unop).op =
    Quiver.Hom.op (c.ι.app { as := j })

Tactic:
simp only [op_comp, op_unop, Quiver.Hom.op_unop, Category.assoc,
    opCoproductIsoProduct'_inv_comp_inj]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, Opposite.op_unop, Quiver.Hom.op_unop, CategoryTheory.Limits.opCoproductIsoProduct'_inv_comp_inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
a :
  (opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc hf).inv ≫ (c.inj j).op =
    Quiver.Hom.op (c.ι.app { as := j })
⊢ (opCoproductIsoProduct' hc hf).hom ≫ f.proj j = Quiver.Hom.op (c.ι.app { as := j })

Tactic:
rw [← opCoproductIsoProduct'_inv_comp_inj hc hf]

Premises used: CategoryTheory.Limits.opCoproductIsoProduct'_inv_comp_inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
a : (c.inj j).op = Quiver.Hom.op (c.ι.app { as := j })
⊢ (opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc hf).inv ≫ (c.inj j).op =
    Quiver.Hom.op (c.ι.app { as := j })

Tactic:
simp only [Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (c.inj j).op = Quiver.Hom.op (c.ι.app { as := j })

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst_1 : HasCoproduct.{u_1, v₁, u₁} Z
b : α
⊢ Eq.{v₁ + 1} (α := (piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) ⟶ op (Z b))
    (CategoryStruct.comp (Y := op (sigmaObj.{u_1, v₁, u₁} Z)) (Iso.inv (opCoproductIsoProduct Z))
        (Quiver.Hom.op (Sigma.ι Z b)) :
      (piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) ⟶ op (Z b))
    (Pi.π (fun (x : α) ↦ op (Z x)) b : (piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) ⟶ op (Z b))

Tactic:
opCoproductIsoProduct'_inv_comp_inj _ _ b

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.opCoproductIsoProduct'_inv_comp_inj, CategoryTheory.Limits.colimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hf : IsLimit f
c' : Cofan.{u_1, v₁, u₁} Z
⊢ Eq (α := op c'.pt ⟶ f.pt) ((hc.desc c').op ≫ (opCoproductIsoProduct' hc hf).hom : op c'.pt ⟶ f.pt)
    (hf.lift c'.op : c'.op.pt ⟶ f.pt)

Tactic:
(Iso.eq_comp_inv _).mp (Quiver.Hom.unop_inj (hc.hom_ext (fun ⟨j⟩ ↦ Quiver.Hom.op_inj ?_)))

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, Quiver.Hom.op, CategoryTheory.Iso.eq_comp_inv, Quiver.Hom.op_inj, Quiver.Hom.unop, CategoryTheory.Limits.opCoproductIsoProduct', CategoryTheory.Limits.Cocone.ι, Quiver.Hom.unop_inj, CategoryTheory.Limits.IsColimit.desc, CategoryTheory.CategoryStruct.comp, Iff.mp, CategoryTheory.Limits.Cofan.IsColimit.op.match_1, Eq, CategoryTheory.Iso.inv, CategoryTheory.Limits.Cofan.op, CategoryTheory.NatTrans.app, CategoryTheory.Limits.IsLimit.lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hf : IsLimit f
c' : Cofan.{u_1, v₁, u₁} Z
refine :
  ∀ (x : Discrete α) (j : α),
    Eq (α := op (unop (op c'.pt)) ⟶ op (obj.{u_1, v₁, u_1, u₁} (Discrete.functor Z) { as := j : Discrete α }))
      (Quiver.Hom.op (c.ι.app { as := j } ≫ (hc.desc c').op.unop))
      (Quiver.Hom.op
        (c.ι.app { as := j : Discrete α } ≫ Quiver.Hom.unop (hf.lift c'.op ≫ (opCoproductIsoProduct' hc hf).inv)))
⊢ Eq (α := op c'.pt ⟶ f.pt) ((hc.desc c').op ≫ (opCoproductIsoProduct' hc hf).hom : op c'.pt ⟶ f.pt)
    (hf.lift c'.op : c'.op.pt ⟶ f.pt)

Tactic:
refine (Iso.eq_comp_inv _).mp (Quiver.Hom.unop_inj (hc.hom_ext (fun ⟨j⟩ ↦ Quiver.Hom.op_inj ?_)))

Premises used: CategoryTheory.Iso.eq_comp_inv, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hf : IsLimit f
c' : Cofan.{u_1, v₁, u₁} Z
x : Discrete α
j : α
simp :
  Eq (α := op c'.pt ⟶ op (Z j)) (Quiver.Hom.op (c'.ι.app { as := j }))
    (hf.lift (Fan.mk (op c'.pt) fun (a : α) ↦ (c'.inj a).op) ≫
      (opCoproductIsoProduct' hc hf).inv ≫ Quiver.Hom.op (c.ι.app { as := j : Discrete α }))
⊢ Eq (α := op (unop (op c'.pt)) ⟶ op (obj.{u_1, v₁, u_1, u₁} (Discrete.functor Z) { as := j : Discrete α }))
    (Quiver.Hom.op (c.ι.app { as := j } ≫ (hc.desc c').op.unop))
    (Quiver.Hom.op
      (c.ι.app { as := j : Discrete α } ≫ Quiver.Hom.unop (hf.lift c'.op ≫ (opCoproductIsoProduct' hc hf).inv)))

Tactic:
simp only [unop_op, Discrete.functor_obj, const_obj_obj, Quiver.Hom.unop_op, IsColimit.fac,
    Cofan.op, unop_comp, op_comp, op_unop, Quiver.Hom.op_unop, Category.assoc]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Category.assoc, CategoryTheory.op_comp, Quiver.Hom.unop_op, CategoryTheory.Discrete.functor_obj, Opposite.op_unop, Quiver.Hom.op_unop, CategoryTheory.unop_comp, Opposite.unop_op, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Limits.Cofan.op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hf : IsLimit f
c' : Cofan.{u_1, v₁, u₁} Z
x : Discrete α
j : α
erw :
  Eq (α := op c'.pt ⟶ op (Z j)) (Quiver.Hom.op (c'.ι.app { as := j }))
    (NatTrans.app (Cone.π (Fan.mk (op c'.pt) fun (a : α) ↦ (c'.inj a).op)) { as := j })
⊢ Eq (α := op c'.pt ⟶ op (Z j)) (Quiver.Hom.op (c'.ι.app { as := j }))
    (hf.lift (Fan.mk (op c'.pt) fun (a : α) ↦ (c'.inj a).op) ≫
      (opCoproductIsoProduct' hc hf).inv ≫ Quiver.Hom.op (c.ι.app { as := j : Discrete α }))

Tactic:
erw [opCoproductIsoProduct'_inv_comp_inj, IsLimit.fac]

Premises used: CategoryTheory.Limits.opCoproductIsoProduct'_inv_comp_inj, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hc : IsColimit c
hf : IsLimit f
c' : Cofan.{u_1, v₁, u₁} Z
x : Discrete α
j : α
⊢ Eq (α := op c'.pt ⟶ op (Z j)) (Quiver.Hom.op (c'.ι.app { as := j }))
    (NatTrans.app (Cone.π (Fan.mk (op c'.pt) fun (a : α) ↦ (c'.inj a).op)) { as := j })

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst_1 : HasCoproduct.{u_1, v₁, u₁} Z
X : C
π : (a : α) → Z a ⟶ X
⊢ Eq (α :=
    op (Cofan.mk X π).pt ⟶
      Cone.pt.{u_1, v₁, u_1, u₁} (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ op (Z x))
        (Fan.mk (piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) (Pi.π fun (x : α) ↦ op (Z x))))
    (CategoryStruct.comp (Y := op (Cofan.mk (sigmaObj.{u_1, v₁, u₁} Z) (Sigma.ι Z)).pt)
      (Quiver.Hom.op (IsColimit.desc (coproductIsCoproduct Z) (Cofan.mk X π)))
      (Iso.hom (opCoproductIsoProduct' (coproductIsCoproduct Z) (productIsProduct fun (x : α) ↦ op (Z x)))))
    (IsLimit.lift (productIsProduct fun (x : α) ↦ op (Z x)) (Cofan.mk X π).op)

Tactic:
desc_op_comp_opCoproductIsoProduct'_hom (coproductIsCoproduct Z) (productIsProduct (op <| Z ·))
      (Cofan.mk _ π)

Premises used: CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom, CategoryTheory.Limits.productIsProduct, CategoryTheory.Limits.coproductIsCoproduct, Opposite.op, CategoryTheory.Limits.Cofan.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst_1 : HasCoproduct.{u_1, v₁, u₁} Z
X : C
π : (a : α) → Z a ⟶ X
h :
  (op X ⟶ piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) =
      (op (Cofan.mk X π).pt ⟶
        Cone.pt.{u_1, v₁, u_1, u₁} (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ op (Z x))
          (Fan.mk (piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) (Pi.π fun (x : α) ↦ op (Z x)))) →
    op X = op (Cofan.mk X π).pt →
      op (sigmaObj.{u_1, v₁, u₁} Z) = op (Cofan.mk (sigmaObj.{u_1, v₁, u₁} Z) (Sigma.ι Z)).pt →
        sigmaObj.{u_1, v₁, u₁} Z = (Cofan.mk (sigmaObj.{u_1, v₁, u₁} Z) (Sigma.ι Z)).pt →
          X = (Cofan.mk X π).pt →
            Eq (α := sigmaObj.{u_1, v₁, u₁} Z ⟶ X) (Sigma.desc π)
              (IsColimit.desc (coproductIsCoproduct Z) (Cofan.mk X π))
h₁ :
  (op X ⟶ piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) =
      (op (Cofan.mk X π).pt ⟶
        Cone.pt.{u_1, v₁, u_1, u₁} (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ op (Z x))
          (Fan.mk (piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) (Pi.π fun (x : α) ↦ op (Z x)))) →
    Eq (α := op X ⟶ piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) (Pi.lift fun (a : α) ↦ (π a).op)
      (IsLimit.lift (productIsProduct fun (x : α) ↦ op (Z x)) (Cofan.mk X π).op)
⊢ Eq.{v₁ + 1} (α := op X ⟶ piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x))
    (CategoryStruct.comp (Y := op (sigmaObj.{u_1, v₁, u₁} Z)) (Quiver.Hom.op (Sigma.desc π))
        (Iso.hom (opCoproductIsoProduct Z)) :
      op X ⟶ piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x))
    (Pi.lift fun (a : α) ↦ (π a).op : op X ⟶ piObj.{u_1, v₁, u₁} fun (a : α) ↦ op (Z a))

Tactic:
convert!
    desc_op_comp_opCoproductIsoProduct'_hom (coproductIsCoproduct Z) (productIsProduct (op <| Z ·))
      (Cofan.mk _ π)

Premises used: CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom, CategoryTheory.Limits.productIsProduct, CategoryTheory.Limits.coproductIsCoproduct, Opposite.op, CategoryTheory.Limits.Cofan.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst_1 : HasCoproduct.{u_1, v₁, u₁} Z
X : C
π : (a : α) → Z a ⟶ X
e_1 :
  (op X ⟶ piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) =
    (op (Cofan.mk X π).pt ⟶
      Cone.pt.{u_1, v₁, u_1, u₁} (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ op (Z x))
        (Fan.mk (piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) (Pi.π fun (x : α) ↦ op (Z x))))
e_3 : op X = op (Cofan.mk X π).pt
e_4 : op (sigmaObj.{u_1, v₁, u₁} Z) = op (Cofan.mk (sigmaObj.{u_1, v₁, u₁} Z) (Sigma.ι Z)).pt
e_3_1 : sigmaObj.{u_1, v₁, u₁} Z = (Cofan.mk (sigmaObj.{u_1, v₁, u₁} Z) (Sigma.ι Z)).pt
e_4_1 : X = (Cofan.mk X π).pt
⊢ Eq (α := sigmaObj.{u_1, v₁, u₁} Z ⟶ X) (Sigma.desc π) (IsColimit.desc (coproductIsCoproduct Z) (Cofan.mk X π))

Tactic:
simp [Sigma.desc, coproductIsCoproduct]

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.Limits.Sigma.desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst_1 : HasCoproduct.{u_1, v₁, u₁} Z
X : C
π : (a : α) → Z a ⟶ X
e_1 :
  (op X ⟶ piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) =
    (op (Cofan.mk X π).pt ⟶
      Cone.pt.{u_1, v₁, u_1, u₁} (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ op (Z x))
        (Fan.mk (piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) (Pi.π fun (x : α) ↦ op (Z x))))
⊢ Eq (α := op X ⟶ piObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) (Pi.lift fun (a : α) ↦ (π a).op)
    (IsLimit.lift (productIsProduct fun (x : α) ↦ op (Z x)) (Cofan.mk X π).op)

Tactic:
simp [Pi.lift, productIsProduct]

Premises used: CategoryTheory.Limits.productIsProduct, CategoryTheory.Limits.Pi.lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst_2 : HasProduct.{u_1, v₁, u₁} Z
⊢ HasColimit.{u_1, u_1, v₁, u₁} (Functor.op (Discrete.functor Z))

Tactic:
hasColimit_op_of_hasLimit (Discrete.functor Z)

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.hasColimit_op_of_hasLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst_2 : HasProduct.{u_1, v₁, u₁} Z
⊢ HasColimit.{u_1, u_1, v₁, u₁} ((Discrete.opposite α).inverse ⋙ Functor.op (Discrete.functor Z))

Tactic:
hasColimit_equivalence_comp (Discrete.opposite α).symm

Premises used: CategoryTheory.Limits.hasColimit_equivalence_comp, CategoryTheory.Discrete.functor, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst_2 : HasProduct.{u_1, v₁, u₁} Z
x : Discrete α
⊢ obj.{u_1, v₁, u_1, u₁}
      (Discrete.functor
        (obj.{u_1, v₁, u_1, u₁} ((Discrete.opposite α).inverse ⋙ Functor.op (Discrete.functor Z)) ∘ Discrete.mk))
      x ≅
    obj.{u_1, v₁, u_1, u₁}
      (Discrete.functor
        (obj.{u_1, v₁, u_1, u₁} ((Discrete.opposite α).inverse ⋙ Functor.op (Discrete.functor Z)) ∘ Discrete.mk))
      x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst_2 : HasProduct.{u_1, v₁, u₁} Z
f : Fan.{u_1, v₁, u₁} Z
hf : IsLimit f
e : Iso (C := Functor.{u_1, v₁, u_1, u₁} (Discrete α) Cᵒᵖ) (Discrete.functor fun (x : α) ↦ Opposite.op (Z x))
  ((Discrete.opposite α).inverse ⋙ Functor.op (Discrete.functor Z)) :=
  Discrete.natIso fun (x : Discrete α) ↦
    Iso.refl (obj.{u_1, v₁, u_1, u₁} (Discrete.functor fun (x : α) ↦ Opposite.op (Z x)) x)
refine :
  ∀ (x : Discrete α) (a : α),
    Eq (α :=
      obj.{u_1, v₁, u_1, u₁} (Discrete.functor fun (x : α) ↦ Opposite.op (Z x)) { as := a : Discrete α } ⟶ f.op.pt)
      (((Cocone.precompose e.hom).obj (Cocone.whisker (Discrete.opposite α).symm.functor (Cone.op f))).ι.app
          { as := a : Discrete α } ≫
        Iso.hom
          (Iso.refl ((Cocone.precompose e.hom).obj (Cocone.whisker (Discrete.opposite α).symm.functor (Cone.op f))).pt))
      (f.op.ι.app { as := a })
⊢ IsColimit f.op

Tactic:
refine IsColimit.ofIsoColimit ((IsColimit.precomposeHomEquiv e _).2
    (IsColimit.whiskerEquivalence hf.op (Discrete.opposite α).symm))
    (Cocone.ext (Iso.refl _) (fun ⟨a⟩ ↦ ?_))

Premises used: CategoryTheory.Limits.Cocone.precompose, CategoryTheory.Limits.IsLimit.op, CategoryTheory.Limits.IsColimit.whiskerEquivalence, CategoryTheory.Limits.Cocone.ext, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Limits.Cocone.whisker, CategoryTheory.Iso.refl, CategoryTheory.Equivalence.functor, CategoryTheory.Limits.Cocone.ι, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.Cofan.IsColimit.op.match_1, CategoryTheory.Discrete.opposite, CategoryTheory.Limits.Cone.op, CategoryTheory.Iso.hom, Eq, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.IsColimit.precomposeHomEquiv, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, Equiv.invFun, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f : Fan.{u_1, v₁, u₁} Z
c : Cofan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hf : IsLimit f
hc : IsColimit c
b : α
⊢ (f.proj b).op ≫ (opProductIsoCoproduct' hf hc).hom = c.inj b

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom (Fan.IsLimit.op hf) hc ⟨b⟩

Premises used: Quiver.Hom.op, CategoryTheory.Discrete.mk, CategoryTheory.Limits.Cofan.inj, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.Fan.IsLimit.op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f f' : Fan.{u_1, v₁, u₁} Z
c : Cofan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
a :
  ((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop =
    (hf.conePointUniqueUpToIso hf').op.inv.unop
⊢ (opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv = (hf.conePointUniqueUpToIso hf').op.inv

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f f' : Fan.{u_1, v₁, u₁} Z
c : Cofan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
a :
  ∀ (j : Discrete α),
    ((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop ≫ f.π.app j =
      (hf.conePointUniqueUpToIso hf').op.inv.unop ≫ f.π.app j
⊢ ((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop =
    (hf.conePointUniqueUpToIso hf').op.inv.unop

Tactic:
apply hf.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f f' : Fan.{u_1, v₁, u₁} Z
c : Cofan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
j : α
a :
  ((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop ≫ f.proj j =
    (hf.conePointUniqueUpToIso hf').op.inv.unop ≫ f.π.app { as := j }
⊢ Eq (α := unop (op f'.pt) ⟶ obj.{u_1, v₁, u_1, u₁} (Discrete.functor Z) { as := j : Discrete α })
    (((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop ≫ f.π.app { as := j })
    ((hf.conePointUniqueUpToIso hf').op.inv.unop ≫ f.π.app { as := j })

Tactic:
change _ ≫ f.proj _ = _

Premises used: CategoryTheory.Limits.Fan.proj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f f' : Fan.{u_1, v₁, u₁} Z
c : Cofan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
j : α
a : (opProductIsoCoproduct' hf' hc).inv.unop ≫ (opProductIsoCoproduct' hf hc).hom.unop ≫ f.proj j = f'.π.app { as := j }
⊢ ((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop ≫ f.proj j =
    (hf.conePointUniqueUpToIso hf').op.inv.unop ≫ f.π.app { as := j }

Tactic:
simp only [unop_op, unop_comp, Category.assoc, Discrete.functor_obj, Iso.op_inv,
    Quiver.Hom.unop_op, IsLimit.conePointUniqueUpToIso_inv_comp]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.unop_op, CategoryTheory.Discrete.functor_obj, CategoryTheory.Iso.op_inv, CategoryTheory.unop_comp, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, Opposite.unop_op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f f' : Fan.{u_1, v₁, u₁} Z
c : Cofan.{u_1, v₁, u₁} (C := Cᵒᵖ) fun (x : α) ↦ op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
j : α
a :
  ((opProductIsoCoproduct' hf' hc).inv.unop ≫ (opProductIsoCoproduct' hf hc).hom.unop ≫ f.proj j).op =
    Quiver.Hom.op (f'.π.app { as := j })
⊢ (opProductIsoCoproduct' hf' hc).inv.unop ≫ (opProductIsoCoproduct' hf hc).hom.unop ≫ f.proj j = f'.π.app { as := j }

Tactic:
apply Quiver.Hom.op_inj

Premises used: Quiver.Hom.op_inj