awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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 : α
⊢ 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 })
have a : ((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop ≫ f.proj j =
  (hf.conePointUniqueUpToIso hf').op.inv.unop ≫ f.π.app { as := j }
Tactic: change _ ≫ f.proj _ = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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 : α
⊢ ((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop ≫ f.proj j =
    (hf.conePointUniqueUpToIso hf').op.inv.unop ≫ f.π.app { as := j }
have a : (opProductIsoCoproduct' hf' hc).inv.unop ≫ (opProductIsoCoproduct' hf hc).hom.unop ≫ f.proj j = 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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 : α
⊢ (opProductIsoCoproduct' hf' hc).inv.unop ≫ (opProductIsoCoproduct' hf hc).hom.unop ≫ f.proj j = f'.π.app { as := j }
have a : ((opProductIsoCoproduct' hf' hc).inv.unop ≫ (opProductIsoCoproduct' hf hc).hom.unop ≫ f.proj j).op =
  Quiver.Hom.op (f'.π.app { as := j })
Tactic: apply Quiver.Hom.op_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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 : α
⊢ ((opProductIsoCoproduct' hf' hc).inv.unop ≫ (opProductIsoCoproduct' hf hc).hom.unop ≫ f.proj j).op =
    Quiver.Hom.op (f'.π.app { as := j })
have a : c.inj j ≫ (opProductIsoCoproduct' hf' hc).inv = Quiver.Hom.op (f'.π.app { as := j })
Tactic: simp only [op_comp, op_unop, Quiver.Hom.op_unop, proj_comp_opProductIsoCoproduct'_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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 : α
⊢ c.inj j ≫ (opProductIsoCoproduct' hf' hc).inv = Quiver.Hom.op (f'.π.app { as := j })
have a : Eq (α := op (Z j) ⟶ op f'.pt)
  (((f'.proj j).op ≫ (opProductIsoCoproduct' hf' hc).hom) ≫ (opProductIsoCoproduct' hf' hc).inv)
  (Quiver.Hom.op (f'.π.app { as := j }))
Tactic: rw [← proj_comp_opProductIsoCoproduct'_hom hf' hc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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 : α
⊢ Eq (α := op (Z j) ⟶ op f'.pt)
    (((f'.proj j).op ≫ (opProductIsoCoproduct' hf' hc).hom) ≫ (opProductIsoCoproduct' hf' hc).inv)
    (Quiver.Hom.op (f'.π.app { as := j }))
have a : (f'.proj j).op = Quiver.Hom.op (f'.π.app { as := j })
Tactic: simp only [Category.assoc, Iso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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
f' : Fan.{u_1, v₁, u₁} Z
⊢ (opProductIsoCoproduct' hf hc).inv ≫ (hf.lift f').op = hc.desc f'.op
have refine : ∀ (x : Discrete α) (j : α),
  Eq (α := op (obj.{u_1, v₁, u_1, u₁} (Discrete.functor Z) { as := j : Discrete α }) ⟶ op (unop (op f'.pt)))
    (Quiver.Hom.op ((hf.lift f').op.unop ≫ f.π.app { as := j }))
    (Quiver.Hom.op
      (Quiver.Hom.unop ((opProductIsoCoproduct' hf hc).hom ≫ hc.desc f'.op) ≫ f.π.app { as := j : Discrete α }))
Tactic: refine (Iso.inv_comp_eq _).mpr (Quiver.Hom.unop_inj (hf.hom_ext (fun ⟨j⟩ ↦ Quiver.Hom.op_inj ?_)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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
f' : Fan.{u_1, v₁, u₁} Z
x : Discrete α
j : α
⊢ Eq (α := op (obj.{u_1, v₁, u_1, u₁} (Discrete.functor Z) { as := j : Discrete α }) ⟶ op (unop (op f'.pt)))
    (Quiver.Hom.op ((hf.lift f').op.unop ≫ f.π.app { as := j }))
    (Quiver.Hom.op
      (Quiver.Hom.unop ((opProductIsoCoproduct' hf hc).hom ≫ hc.desc f'.op) ≫ f.π.app { as := j : Discrete α }))
have simp : Eq (α := op (Z j) ⟶ op f'.pt) (Quiver.Hom.op (f'.π.app { as := j }))
  (Quiver.Hom.op (f.π.app { as := j : Discrete α }) ≫
    (opProductIsoCoproduct' hf hc).hom ≫ hc.desc (Cofan.mk (op f'.pt) fun (a : α) ↦ (f'.proj a).op))
Tactic: simp only [Discrete.functor_obj, unop_op, Quiver.Hom.unop_op, IsLimit.fac, Fan.op, unop_comp,
    Category.assoc, op_comp, op_unop, Quiver.Hom.op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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
f' : Fan.{u_1, v₁, u₁} Z
x : Discrete α
j : α
⊢ Eq (α := op (Z j) ⟶ op f'.pt) (Quiver.Hom.op (f'.π.app { as := j }))
    (Quiver.Hom.op (f.π.app { as := j : Discrete α }) ≫
      (opProductIsoCoproduct' hf hc).hom ≫ hc.desc (Cofan.mk (op f'.pt) fun (a : α) ↦ (f'.proj a).op))
have erw : Eq (α := op (Z j) ⟶ op f'.pt) (Quiver.Hom.op (f'.π.app { as := j }))
  (NatTrans.app (Cocone.ι (Cofan.mk (op f'.pt) fun (a : α) ↦ (f'.proj a).op)) { as := j })
Tactic: erw [← Category.assoc, proj_comp_opProductIsoCoproduct'_hom, IsColimit.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst_1 : HasProduct.{u_1, v₁, u₁} Z
X : C
π : (a : α) → X ⟶ Z a
⊢ Eq (α := (sigmaObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) ⟶ op X)
    (CategoryStruct.comp (Y := op (piObj.{u_1, v₁, u₁} Z)) (Iso.inv (opProductIsoCoproduct Z))
        (Quiver.Hom.op (Pi.lift π)) :
      (sigmaObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) ⟶ op X)
    (Sigma.desc fun (a : α) ↦ (π a).op : (sigmaObj.{u_1, v₁, u₁} fun (a : α) ↦ op (Z a)) ⟶ op X)
have h : ((sigmaObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) ⟶ op X) =
    (Cocone.pt.{u_1, v₁, u_1, u₁} (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ op (Z x))
        (Cofan.mk (sigmaObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) (Sigma.ι fun (x : α) ↦ op (Z x))) ⟶
      op (Fan.mk X π).pt) →
  op (piObj.{u_1, v₁, u₁} Z) = op (Fan.mk (piObj.{u_1, v₁, u₁} Z) (Pi.π Z)).pt →
    op X = op (Fan.mk X π).pt →
      X = (Fan.mk X π).pt →
        piObj.{u_1, v₁, u₁} Z = (Fan.mk (piObj.{u_1, v₁, u₁} Z) (Pi.π Z)).pt →
          Eq (α := X ⟶ piObj.{u_1, v₁, u₁} Z) (Pi.lift π) (IsLimit.lift (productIsProduct Z) (Fan.mk X π))
Tactic: convert!
    opProductIsoCoproduct'_inv_comp_lift (productIsProduct Z) (coproductIsCoproduct (op <| Z ·))
      (Fan.mk _ π)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst_1 : HasProduct.{u_1, v₁, u₁} Z
X : C
π : (a : α) → X ⟶ Z a
h :
  ((sigmaObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) ⟶ op X) =
      (Cocone.pt.{u_1, v₁, u_1, u₁} (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ op (Z x))
          (Cofan.mk (sigmaObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) (Sigma.ι fun (x : α) ↦ op (Z x))) ⟶
        op (Fan.mk X π).pt) →
    op (piObj.{u_1, v₁, u₁} Z) = op (Fan.mk (piObj.{u_1, v₁, u₁} Z) (Pi.π Z)).pt →
      op X = op (Fan.mk X π).pt →
        X = (Fan.mk X π).pt →
          piObj.{u_1, v₁, u₁} Z = (Fan.mk (piObj.{u_1, v₁, u₁} Z) (Pi.π Z)).pt →
            Eq (α := X ⟶ piObj.{u_1, v₁, u₁} Z) (Pi.lift π) (IsLimit.lift (productIsProduct Z) (Fan.mk X π))
⊢ Eq (α := (sigmaObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) ⟶ op X)
    (CategoryStruct.comp (Y := op (piObj.{u_1, v₁, u₁} Z)) (Iso.inv (opProductIsoCoproduct Z))
        (Quiver.Hom.op (Pi.lift π)) :
      (sigmaObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) ⟶ op X)
    (Sigma.desc fun (a : α) ↦ (π a).op : (sigmaObj.{u_1, v₁, u₁} fun (a : α) ↦ op (Z a)) ⟶ op X)
have h₁ : ((sigmaObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) ⟶ op X) =
    (Cocone.pt.{u_1, v₁, u_1, u₁} (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ op (Z x))
        (Cofan.mk (sigmaObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) (Sigma.ι fun (x : α) ↦ op (Z x))) ⟶
      op (Fan.mk X π).pt) →
  Eq (α := (sigmaObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x)) ⟶ op X) (Sigma.desc fun (a : α) ↦ (π a).op)
    (IsColimit.desc (coproductIsCoproduct fun (x : α) ↦ op (Z x)) (Fan.mk X π).op)
Tactic: convert!
    opProductIsoCoproduct'_inv_comp_lift (productIsProduct Z) (coproductIsCoproduct (op <| Z ·))
      (Fan.mk _ π)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst_2 : HasBinaryProduct.{v₁, u₁} A B
⊢ HasBinaryCoproduct.{v₁, u₁} (op A) (op B)
have this : HasProduct.{0, v₁, u₁} (C := C) fun (x : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) x A B
Tactic: have : HasProduct fun x ↦ (WalkingPair.casesOn x A B : C) := ‹_›
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst_2 : HasBinaryProduct.{v₁, u₁} A B
this :
  HasProduct.{0, v₁, u₁} (C := C) fun (x : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) x A B
⊢ HasCoproduct.{0, v₁, u₁} (C := Cᵒᵖ) fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Cᵒᵖ) j (op A) (op B)
have h : ∀ (x : WalkingPair),
  Eq.{u₁ + 1} (α := Cᵒᵖ) (WalkingPair.rec (motive := fun (x : WalkingPair) ↦ Cᵒᵖ) (op A) (op B) x : Cᵒᵖ)
    (op (WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) A B x) : Cᵒᵖ)
Tactic: convert! (inferInstance : HasCoproduct fun x ↦ op (WalkingPair.casesOn x A B : C)) with x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst_2 : HasBinaryProduct.{v₁, u₁} A B
this :
  HasProduct.{0, v₁, u₁} (C := C) fun (x : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) x A B
x : WalkingPair
⊢ Eq.{u₁ + 1} (α := Cᵒᵖ) (WalkingPair.rec (motive := fun (x : WalkingPair) ↦ Cᵒᵖ) (op A) (op B) x : Cᵒᵖ)
    (op (WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) A B x) : Cᵒᵖ)
have h : Eq.{u₁ + 1} (α := Cᵒᵖ) (WalkingPair.rec (motive := fun (x : WalkingPair) ↦ Cᵒᵖ) (op A) (op B) WalkingPair.left : Cᵒᵖ)
  (op (WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) A B WalkingPair.left) : Cᵒᵖ)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst_2 : HasBinaryProduct.{v₁, u₁} A B
this :
  HasProduct.{0, v₁, u₁} (C := C) fun (x : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) x A B
x : WalkingPair
h :
  Eq.{u₁ + 1} (α := Cᵒᵖ) (WalkingPair.rec (motive := fun (x : WalkingPair) ↦ Cᵒᵖ) (op A) (op B) WalkingPair.left : Cᵒᵖ)
    (op (WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) A B WalkingPair.left) : Cᵒᵖ)
⊢ Eq.{u₁ + 1} (α := Cᵒᵖ) (WalkingPair.rec (motive := fun (x : WalkingPair) ↦ Cᵒᵖ) (op A) (op B) x : Cᵒᵖ)
    (op (WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) A B x) : Cᵒᵖ)
have h₁ : Eq.{u₁ + 1} (α := Cᵒᵖ) (WalkingPair.rec (motive := fun (x : WalkingPair) ↦ Cᵒᵖ) (op A) (op B) WalkingPair.right : Cᵒᵖ)
  (op (WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) A B WalkingPair.right) : Cᵒᵖ)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst_2 : HasBinaryProduct.{v₁, u₁} A B
⊢ Eq.{v₁ + 1} (α := op (prod.{v₁, u₁} A B) ⟶ op (prod.{v₁, u₁} A B))
    (CategoryStruct.comp (Y := coprod.{v₁, u₁} (op A) (op B))
      (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))
      (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd)))
    (𝟙 (op (prod.{v₁, u₁} A B)))
have a : Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op (prod.{v₁, u₁} A B)))
  (Quiver.Hom.unop
    (CategoryStruct.comp (Y := coprod.{v₁, u₁} (op A) (op B))
      (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))
      (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))))
  (Quiver.Hom.unop (𝟙 (op (prod.{v₁, u₁} A B))))
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst_2 : HasBinaryProduct.{v₁, u₁} A B
⊢ Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op (prod.{v₁, u₁} A B)))
    (Quiver.Hom.unop
      (CategoryStruct.comp (Y := coprod.{v₁, u₁} (op A) (op B))
        (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))
        (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))))
    (Quiver.Hom.unop (𝟙 (op (prod.{v₁, u₁} A B))))
have a : Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ A)
  (CategoryStruct.comp (Y := prod.{v₁, u₁} A B)
    (Quiver.Hom.unop
        (CategoryStruct.comp (Y := coprod.{v₁, u₁} (op A) (op B))
          (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))
          (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))) :
      unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op (prod.{v₁, u₁} A B)))
    prod.fst)
  (CategoryStruct.comp (Y := prod.{v₁, u₁} A B)
    (Quiver.Hom.unop (𝟙 (op (prod.{v₁, u₁} A B))) : unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op (prod.{v₁, u₁} A B)))
    prod.fst)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst_2 : HasBinaryProduct.{v₁, u₁} A B
a :
  Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ A)
    (CategoryStruct.comp (Y := prod.{v₁, u₁} A B)
      (Quiver.Hom.unop
          (CategoryStruct.comp (Y := coprod.{v₁, u₁} (op A) (op B))
            (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))
            (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))) :
        unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op (prod.{v₁, u₁} A B)))
      prod.fst)
    (CategoryStruct.comp (Y := prod.{v₁, u₁} A B)
      (Quiver.Hom.unop (𝟙 (op (prod.{v₁, u₁} A B))) : unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op (prod.{v₁, u₁} A B)))
      prod.fst)
⊢ Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op (prod.{v₁, u₁} A B)))
    (Quiver.Hom.unop
      (CategoryStruct.comp (Y := coprod.{v₁, u₁} (op A) (op B))
        (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))
        (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))))
    (Quiver.Hom.unop (𝟙 (op (prod.{v₁, u₁} A B))))
have a₁ : Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ B)
  (CategoryStruct.comp (Y := prod.{v₁, u₁} A B)
    (Quiver.Hom.unop
        (CategoryStruct.comp (Y := coprod.{v₁, u₁} (op A) (op B))
          (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))
          (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))) :
      unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op (prod.{v₁, u₁} A B)))
    prod.snd)
  (CategoryStruct.comp (Y := prod.{v₁, u₁} A B)
    (Quiver.Hom.unop (𝟙 (op (prod.{v₁, u₁} A B))) : unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op (prod.{v₁, u₁} A B)))
    prod.snd)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst_2 : HasBinaryProduct.{v₁, u₁} A B
⊢ Eq.{v₁ + 1} (α := prod.{v₁, u₁} A B ⟶ A)
    (CategoryStruct.comp (Y := prod.{v₁, u₁} A B)
        (Quiver.Hom.unop
          (CategoryStruct.comp (Y := coprod.{v₁, u₁} (op A) (op B))
            (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))
            (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))))
        prod.fst :
      prod.{v₁, u₁} A B ⟶ A)
    (CategoryStruct.comp (Y := prod.{v₁, u₁} A B) (Quiver.Hom.unop (𝟙 (op (prod.{v₁, u₁} A B)))) prod.fst :
      prod.{v₁, u₁} A B ⟶ A)
have a : Eq.{v₁ + 1} (α := op A ⟶ op (prod.{v₁, u₁} A B))
  (Quiver.Hom.op
      (CategoryStruct.comp (Y := prod.{v₁, u₁} A B)
        (Quiver.Hom.unop
          (CategoryStruct.comp (Y := coprod.{v₁, u₁} (op A) (op B))
            (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))
            (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))))
        prod.fst) :
    op A ⟶ op (prod.{v₁, u₁} A B))
  (Quiver.Hom.op
      (CategoryStruct.comp (Y := prod.{v₁, u₁} A B) (Quiver.Hom.unop (𝟙 (op (prod.{v₁, u₁} A B)))) prod.fst) :
    op A ⟶ op (prod.{v₁, u₁} A B))
Tactic: apply Quiver.Hom.op_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst_2 : HasBinaryProduct.{v₁, u₁} A B
⊢ Eq.{v₁ + 1} (α := prod.{v₁, u₁} A B ⟶ B)
    (CategoryStruct.comp (Y := prod.{v₁, u₁} A B)
        (Quiver.Hom.unop
          (CategoryStruct.comp (Y := coprod.{v₁, u₁} (op A) (op B))
            (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))
            (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))))
        prod.snd :
      prod.{v₁, u₁} A B ⟶ B)
    (CategoryStruct.comp (Y := prod.{v₁, u₁} A B) (Quiver.Hom.unop (𝟙 (op (prod.{v₁, u₁} A B)))) prod.snd :
      prod.{v₁, u₁} A B ⟶ B)
have a : Eq.{v₁ + 1} (α := op B ⟶ op (prod.{v₁, u₁} A B))
  (Quiver.Hom.op
      (CategoryStruct.comp (Y := prod.{v₁, u₁} A B)
        (Quiver.Hom.unop
          (CategoryStruct.comp (Y := coprod.{v₁, u₁} (op A) (op B))
            (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))
            (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))))
        prod.snd) :
    op B ⟶ op (prod.{v₁, u₁} A B))
  (Quiver.Hom.op
      (CategoryStruct.comp (Y := prod.{v₁, u₁} A B) (Quiver.Hom.unop (𝟙 (op (prod.{v₁, u₁} A B)))) prod.snd) :
    op B ⟶ op (prod.{v₁, u₁} A B))
Tactic: apply Quiver.Hom.op_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst_2 : HasBinaryProduct.{v₁, u₁} A B
⊢ CategoryStruct.comp (Y := op (prod.{v₁, u₁} A B)) (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))
      (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr))) =
    𝟙 (coprod.{v₁, u₁} (op A) (op B))
have h₁ : CategoryStruct.comp (Y := coprod.{v₁, u₁} (op A) (op B)) coprod.inl
    (CategoryStruct.comp (Y := op (prod.{v₁, u₁} A B)) (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))
      (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))) =
  coprod.inl ≫ 𝟙 (coprod.{v₁, u₁} (op A) (op B))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst_2 : HasBinaryProduct.{v₁, u₁} A B
h₁ :
  CategoryStruct.comp (Y := coprod.{v₁, u₁} (op A) (op B)) coprod.inl
      (CategoryStruct.comp (Y := op (prod.{v₁, u₁} A B)) (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))
        (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))) =
    coprod.inl ≫ 𝟙 (coprod.{v₁, u₁} (op A) (op B))
⊢ CategoryStruct.comp (Y := op (prod.{v₁, u₁} A B)) (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))
      (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr))) =
    𝟙 (coprod.{v₁, u₁} (op A) (op B))
have h₂ : CategoryStruct.comp (Y := coprod.{v₁, u₁} (op A) (op B)) coprod.inr
    (CategoryStruct.comp (Y := op (prod.{v₁, u₁} A B)) (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))
      (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))) =
  coprod.inr ≫ 𝟙 (coprod.{v₁, u₁} (op A) (op B))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst_2 : HasBinaryProduct.{v₁, u₁} A B
⊢ CategoryStruct.comp (Y := coprod.{v₁, u₁} (op A) (op B)) coprod.inl
      (CategoryStruct.comp (Y := op (prod.{v₁, u₁} A B)) (coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))
        (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))) =
    coprod.inl ≫ 𝟙 (coprod.{v₁, u₁} (op A) (op B))
have h₁ : CategoryStruct.comp (Y :=
    Cocone.pt.{0, v₁, 0, u₁} (F := pair (op A) (op B))
      (BinaryCofan.mk (P := op (prod.{v₁, u₁} A B)) (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd)))
    (NatTrans.app
        (Cocone.ι (BinaryCofan.mk (P := op (prod.{v₁, u₁} A B)) (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd)))
        { as := WalkingPair.left } :
      obj.{0, v₁, 0, u₁} (pair (op A) (op B)) { as := WalkingPair.left : Discrete WalkingPair } ⟶
        obj.{0, v₁, 0, u₁}
          (obj (const (Discrete WalkingPair))
            (Cocone.pt.{0, v₁, 0, u₁} (F := pair (op A) (op B))
              (BinaryCofan.mk (P := op (prod.{v₁, u₁} A B)) (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd))))
          { as := WalkingPair.left : Discrete WalkingPair })
    (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr))) =
  coprod.inl ≫ 𝟙 (coprod.{v₁, u₁} (op A) (op B))
Tactic: simp only [colimit.ι_desc_assoc]