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
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 : c.inj j ≫ (opProductIsoCoproduct' hf' hc).inv = Quiver.Hom.op (f'.π.app { as := j })
⊢ ((opProductIsoCoproduct' hf' hc).inv.unop ≫ (opProductIsoCoproduct' hf hc).hom.unop ≫ f.proj j).op =
    Quiver.Hom.op (f'.π.app { as := j })

Tactic:
simp only [op_comp, op_unop, Quiver.Hom.op_unop, proj_comp_opProductIsoCoproduct'_hom]

Premises used: CategoryTheory.op_comp, Opposite.op_unop, Quiver.Hom.op_unop, CategoryTheory.Limits.proj_comp_opProductIsoCoproduct'_hom
-- 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 :
  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 }))
⊢ c.inj j ≫ (opProductIsoCoproduct' hf' hc).inv = Quiver.Hom.op (f'.π.app { as := j })

Tactic:
rw [← proj_comp_opProductIsoCoproduct'_hom hf' hc]

Premises used: CategoryTheory.Limits.proj_comp_opProductIsoCoproduct'_hom
-- 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 : (f'.proj j).op = Quiver.Hom.op (f'.π.app { as := 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 }))

Tactic:
simp only [Category.assoc, Iso.hom_inv_id, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id
-- 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 : α
⊢ (f'.proj j).op = Quiver.Hom.op (f'.π.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 : HasProduct.{u_1, v₁, u₁} Z
b : α
⊢ Eq.{v₁ + 1} (α := op (Z b) ⟶ sigmaObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x))
    (CategoryStruct.comp (Y := op (piObj.{u_1, v₁, u₁} Z)) (Quiver.Hom.op (Pi.π Z b))
        (Iso.hom (opProductIsoCoproduct Z)) :
      op (Z b) ⟶ sigmaObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x))
    (Sigma.ι.{u_1, v₁, u₁} (C := Cᵒᵖ) (fun (x : α) ↦ op (Z x)) b :
      op (Z b) ⟶ sigmaObj.{u_1, v₁, u₁} fun (x : α) ↦ op (Z x))

Tactic:
proj_comp_opProductIsoCoproduct'_hom _ _ b

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.colimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.proj_comp_opProductIsoCoproduct'_hom, CategoryTheory.Limits.colimit.ι
-- 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
f' : Fan.{u_1, v₁, u₁} Z
⊢ (opProductIsoCoproduct' hf hc).inv ≫ (hf.lift f').op = hc.desc f'.op

Tactic:
(Iso.inv_comp_eq _).mpr (Quiver.Hom.unop_inj (hf.hom_ext (fun ⟨j⟩ ↦ Quiver.Hom.op_inj ?_)))

Premises used: Iff.mpr, CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.Fan.op, Quiver.Hom.op, Quiver.Hom.op_inj, CategoryTheory.Iso.inv_comp_eq, Quiver.Hom.unop, CategoryTheory.Limits.opProductIsoCoproduct', CategoryTheory.Limits.IsLimit.hom_ext, Quiver.Hom.unop_inj, CategoryTheory.Limits.IsColimit.desc, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.Cofan.IsColimit.op.match_1, CategoryTheory.Iso.hom, Eq, 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
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
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 α }))
⊢ (opProductIsoCoproduct' hf hc).inv ≫ (hf.lift f').op = hc.desc f'.op

Tactic:
refine (Iso.inv_comp_eq _).mpr (Quiver.Hom.unop_inj (hf.hom_ext (fun ⟨j⟩ ↦ Quiver.Hom.op_inj ?_)))

Premises used: Iff.mpr, CategoryTheory.Iso.inv_comp_eq
-- 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
f' : Fan.{u_1, v₁, u₁} Z
x : Discrete α
j : α
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))
⊢ 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:
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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, Quiver.Hom.unop_op, CategoryTheory.Discrete.functor_obj, CategoryTheory.Limits.Fan.op, Opposite.op_unop, Quiver.Hom.op_unop, CategoryTheory.unop_comp, Opposite.unop_op, 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
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 : α
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 })
⊢ 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:
erw [← Category.assoc, proj_comp_opProductIsoCoproduct'_hom, IsColimit.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Category.assoc, CategoryTheory.Limits.proj_comp_opProductIsoCoproduct'_hom
-- 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
f' : Fan.{u_1, v₁, u₁} Z
x : Discrete α
j : α
⊢ 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:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
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 (α :=
    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)
    (CategoryStruct.comp (Y := op (Fan.mk (piObj.{u_1, v₁, u₁} Z) (Pi.π Z)).pt)
      (Iso.inv (opProductIsoCoproduct' (productIsProduct Z) (coproductIsCoproduct fun (x : α) ↦ op (Z x))))
      (Quiver.Hom.op (IsLimit.lift (productIsProduct Z) (Fan.mk X π))))
    (IsColimit.desc (coproductIsCoproduct fun (x : α) ↦ op (Z x)) (Fan.mk X π).op)

Tactic:
opProductIsoCoproduct'_inv_comp_lift (productIsProduct Z) (coproductIsCoproduct (op <| Z ·))
      (Fan.mk _ π)

Premises used: CategoryTheory.Limits.Fan.mk, CategoryTheory.Limits.productIsProduct, CategoryTheory.Limits.coproductIsCoproduct, Opposite.op, CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
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 π))
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)
⊢ 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)

Tactic:
convert!
    opProductIsoCoproduct'_inv_comp_lift (productIsProduct Z) (coproductIsCoproduct (op <| Z ·))
      (Fan.mk _ π)

Premises used: CategoryTheory.Limits.Fan.mk, CategoryTheory.Limits.productIsProduct, CategoryTheory.Limits.coproductIsCoproduct, Opposite.op, CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
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
e_1 :
  ((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)
e_4 : op (piObj.{u_1, v₁, u₁} Z) = op (Fan.mk (piObj.{u_1, v₁, u₁} Z) (Pi.π Z)).pt
e_5 : op X = op (Fan.mk X π).pt
e_3 : X = (Fan.mk X π).pt
e_4_1 : 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:
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
α : Type u_1
Z : α → C
inst_1 : HasProduct.{u_1, v₁, u₁} Z
X : C
π : (a : α) → X ⟶ Z a
e_1 :
  ((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:
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
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst_2 : HasBinaryProduct.{v₁, u₁} A B
⊢ 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) := ‹_›
-- 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₂
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 (x : WalkingPair) ↦
    op (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) x A B)

Tactic:
(inferInstance : HasCoproduct fun x ↦ op (WalkingPair.casesOn x A B : C))

Premises used: inferInstance
-- 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₂
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
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ᵒᵖ)
⊢ HasCoproduct.{0, v₁, u₁} (C := Cᵒᵖ) fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Cᵒᵖ) j (op A) (op B)

Tactic:
convert! (inferInstance : HasCoproduct fun x ↦ op (WalkingPair.casesOn x A B : C)) with x

Premises used: inferInstance
-- 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₂
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ᵒᵖ)
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ᵒᵖ)
⊢ 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:
cases x
-- 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₂
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
⊢ 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:
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₂
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
⊢ 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:
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₂
A B : C
inst_2 : HasBinaryProduct.{v₁, u₁} A B
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))))
⊢ 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)))

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
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)
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)
⊢ 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:
ext
-- 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₂
A B : C
inst_2 : HasBinaryProduct.{v₁, u₁} A B
a :
  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)
⊢ 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:
simp only
-- 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₂
A B : C
inst_2 : HasBinaryProduct.{v₁, u₁} A B
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))
⊢ 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)

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
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 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:
simp