awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ⟶ 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)
⊢ 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:
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 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))
⊢ 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)

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

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
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))
⊢ 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:
simp only [colimit.ι_desc_assoc]

Premises used: CategoryTheory.Limits.colimit.ι_desc_assoc
-- 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
h₁ :
  Quiver.Hom.unop
      (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))).unop
⊢ 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:
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
⊢ Quiver.Hom.unop
      (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))).unop

Tactic:
simp
-- 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
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.right } :
        obj.{0, v₁, 0, u₁} (pair (op A) (op B)) { as := WalkingPair.right : 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.right : Discrete WalkingPair })
      (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr))) =
    coprod.inr ≫ 𝟙 (coprod.{v₁, u₁} (op A) (op B))
⊢ 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:
simp only [colimit.ι_desc_assoc]

Premises used: CategoryTheory.Limits.colimit.ι_desc_assoc
-- 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
h₂ :
  Quiver.Hom.unop
      (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.right } :
          obj.{0, v₁, 0, u₁} (pair (op A) (op B)) { as := WalkingPair.right : 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.right : Discrete WalkingPair })
        (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))) =
    (coprod.inr ≫ 𝟙 (coprod.{v₁, u₁} (op A) (op B))).unop
⊢ 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.right } :
        obj.{0, v₁, 0, u₁} (pair (op A) (op B)) { as := WalkingPair.right : 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.right : Discrete WalkingPair })
      (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:
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
⊢ Quiver.Hom.unop
      (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.right } :
          obj.{0, v₁, 0, u₁} (pair (op A) (op B)) { as := WalkingPair.right : 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.right : Discrete WalkingPair })
        (Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)))) =
    (coprod.inr ≫ 𝟙 (coprod.{v₁, u₁} (op A) (op B))).unop

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
inst_1 : HasBinaryProduct.{v₁, u₁} A B
rw :
  Eq.{v₁ + 1} (α := op A ⟶ coprod.{v₁, u₁} (op A) (op B))
    (CategoryStruct.comp (Y := op (prod.{v₁, u₁} A B)) (Quiver.Hom.op prod.fst)
        (Iso.hom
          { hom := Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)),
            inv := coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd), hom_inv_id := ⋯, inv_hom_id := ⋯ }) :
      op A ⟶ coprod.{v₁, u₁} (op A) (op B))
    (coprod.inl : op A ⟶ coprod.{v₁, u₁} (op A) (op B))
rw₁ :
  Eq.{v₁ + 1} (α := op A ⟶ coprod.{v₁, u₁} (op A) (op B))
    (Quiver.Hom.op
      (CategoryStruct.comp (Y := prod.{v₁, u₁} A B)
        (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)) prod.fst))
    coprod.inl
rw₂ : Eq.{v₁ + 1} (α := op A ⟶ coprod.{v₁, u₁} (op A) (op B)) (Quiver.Hom.op (Quiver.Hom.unop coprod.inl)) coprod.inl
rw₃ rw₄ : Eq.{v₁ + 1} (α := op A ⟶ coprod.{v₁, u₁} (op A) (op B)) coprod.inl coprod.inl
⊢ Eq.{v₁ + 1} (α := op A ⟶ coprod.{v₁, u₁} (op A) (op B))
    (CategoryStruct.comp (Y := op (prod.{v₁, u₁} A B)) (Quiver.Hom.op prod.fst) (Iso.hom (opProdIsoCoprod A B)) :
      op A ⟶ coprod.{v₁, u₁} (op A) (op B))
    (coprod.inl : op A ⟶ coprod.{v₁, u₁} (op A) (op B))

Tactic:
rw [opProdIsoCoprod, ← op_comp, prod.lift_fst, Quiver.Hom.op_unop]

Premises used: CategoryTheory.Limits.opProdIsoCoprod, CategoryTheory.op_comp, CategoryTheory.Limits.prod.lift_fst, Quiver.Hom.op_unop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
inst_1 : HasBinaryProduct.{v₁, u₁} A B
rw :
  Eq.{v₁ + 1} (α := op B ⟶ coprod.{v₁, u₁} (op A) (op B))
    (CategoryStruct.comp (Y := op (prod.{v₁, u₁} A B)) (Quiver.Hom.op prod.snd)
        (Iso.hom
          { hom := Quiver.Hom.op (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)),
            inv := coprod.desc (Quiver.Hom.op prod.fst) (Quiver.Hom.op prod.snd), hom_inv_id := ⋯, inv_hom_id := ⋯ }) :
      op B ⟶ coprod.{v₁, u₁} (op A) (op B))
    (coprod.inr : op B ⟶ coprod.{v₁, u₁} (op A) (op B))
rw₁ :
  Eq.{v₁ + 1} (α := op B ⟶ coprod.{v₁, u₁} (op A) (op B))
    (Quiver.Hom.op
      (CategoryStruct.comp (Y := prod.{v₁, u₁} A B)
        (prod.lift (Quiver.Hom.unop coprod.inl) (Quiver.Hom.unop coprod.inr)) prod.snd))
    coprod.inr
rw₂ : Eq.{v₁ + 1} (α := op B ⟶ coprod.{v₁, u₁} (op A) (op B)) (Quiver.Hom.op (Quiver.Hom.unop coprod.inr)) coprod.inr
rw₃ rw₄ : Eq.{v₁ + 1} (α := op B ⟶ coprod.{v₁, u₁} (op A) (op B)) coprod.inr coprod.inr
⊢ Eq.{v₁ + 1} (α := op B ⟶ coprod.{v₁, u₁} (op A) (op B))
    (CategoryStruct.comp (Y := op (prod.{v₁, u₁} A B)) (Quiver.Hom.op prod.snd) (Iso.hom (opProdIsoCoprod A B)) :
      op B ⟶ coprod.{v₁, u₁} (op A) (op B))
    (coprod.inr : op B ⟶ coprod.{v₁, u₁} (op A) (op B))

Tactic:
rw [opProdIsoCoprod, ← op_comp, prod.lift_snd, Quiver.Hom.op_unop]

Premises used: CategoryTheory.Limits.opProdIsoCoprod, CategoryTheory.op_comp, Quiver.Hom.op_unop, CategoryTheory.Limits.prod.lift_snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
inst_1 : HasBinaryProduct.{v₁, u₁} A B
rw :
  Eq.{v₁ + 1} (α := op A ⟶ coprod.{v₁, u₁} (op A) (op B)) (coprod.inl : op A ⟶ coprod.{v₁, u₁} (op A) (op B))
    (CategoryStruct.comp (Y := op (prod.{v₁, u₁} A B)) (Quiver.Hom.op prod.fst) (Iso.hom (opProdIsoCoprod A B)) :
      op A ⟶ coprod.{v₁, u₁} (op A) (op B))
rw₁ rw₂ : Eq.{v₁ + 1} (α := op A ⟶ coprod.{v₁, u₁} (op A) (op B)) coprod.inl coprod.inl
⊢ Eq.{v₁ + 1} (α := op A ⟶ op (prod.{v₁, u₁} A B)) (coprod.inl ≫ Iso.inv (opProdIsoCoprod A B)) (Quiver.Hom.op prod.fst)

Tactic:
rw [Iso.comp_inv_eq, fst_opProdIsoCoprod_hom]

Premises used: CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Limits.fst_opProdIsoCoprod_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
inst_1 : HasBinaryProduct.{v₁, u₁} A B
rw :
  Eq.{v₁ + 1} (α := op B ⟶ coprod.{v₁, u₁} (op A) (op B)) (coprod.inr : op B ⟶ coprod.{v₁, u₁} (op A) (op B))
    (CategoryStruct.comp (Y := op (prod.{v₁, u₁} A B)) (Quiver.Hom.op prod.snd) (Iso.hom (opProdIsoCoprod A B)) :
      op B ⟶ coprod.{v₁, u₁} (op A) (op B))
rw₁ rw₂ : Eq.{v₁ + 1} (α := op B ⟶ coprod.{v₁, u₁} (op A) (op B)) coprod.inr coprod.inr
⊢ Eq.{v₁ + 1} (α := op B ⟶ op (prod.{v₁, u₁} A B)) (coprod.inr ≫ Iso.inv (opProdIsoCoprod A B)) (Quiver.Hom.op prod.snd)

Tactic:
rw [Iso.comp_inv_eq, snd_opProdIsoCoprod_hom]

Premises used: CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Limits.snd_opProdIsoCoprod_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
inst_1 : HasBinaryProduct.{v₁, u₁} A B
⊢ Eq.{v₁ + 1} (α := unop (coprod.{v₁, u₁} (op A) (op B)) ⟶ A)
    (CategoryStruct.comp (Y := unop (op (prod.{v₁, u₁} A B))) (Quiver.Hom.unop (Iso.hom (opProdIsoCoprod A B)))
        prod.fst :
      unop (coprod.{v₁, u₁} (op A) (op B)) ⟶ A)
    (Quiver.Hom.unop coprod.inl : unop (coprod.{v₁, u₁} (op A) (op B)) ⟶ unop (op A))

Tactic:
simp [opProdIsoCoprod]

Premises used: CategoryTheory.Limits.opProdIsoCoprod
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
inst_1 : HasBinaryProduct.{v₁, u₁} A B
⊢ Eq.{v₁ + 1} (α := unop (coprod.{v₁, u₁} (op A) (op B)) ⟶ B)
    (CategoryStruct.comp (Y := unop (op (prod.{v₁, u₁} A B))) (Quiver.Hom.unop (Iso.hom (opProdIsoCoprod A B)))
        prod.snd :
      unop (coprod.{v₁, u₁} (op A) (op B)) ⟶ B)
    (Quiver.Hom.unop coprod.inr : unop (coprod.{v₁, u₁} (op A) (op B)) ⟶ unop (op B))

Tactic:
simp [opProdIsoCoprod]

Premises used: CategoryTheory.Limits.opProdIsoCoprod
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
inst_1 : HasBinaryProduct.{v₁, u₁} A B
rw :
  Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op A))
    (Quiver.Hom.unop (coprod.inl ≫ Iso.inv (opProdIsoCoprod A B))) prod.fst
rw₁ : Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op A)) (Quiver.Hom.unop (Quiver.Hom.op prod.fst)) prod.fst
rw₂ rw₃ : Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op A)) prod.fst prod.fst
⊢ Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op A))
    (Quiver.Hom.unop (Iso.inv (opProdIsoCoprod A B)) ≫ Quiver.Hom.unop coprod.inl) prod.fst

Tactic:
rw [← unop_comp, inl_opProdIsoCoprod_inv, Quiver.Hom.unop_op]

Premises used: Quiver.Hom.unop_op, CategoryTheory.unop_comp, CategoryTheory.Limits.inl_opProdIsoCoprod_inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
inst_1 : HasBinaryProduct.{v₁, u₁} A B
rw :
  Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op B))
    (Quiver.Hom.unop (coprod.inr ≫ Iso.inv (opProdIsoCoprod A B))) prod.snd
rw₁ : Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op B)) (Quiver.Hom.unop (Quiver.Hom.op prod.snd)) prod.snd
rw₂ rw₃ : Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op B)) prod.snd prod.snd
⊢ Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op B))
    (Quiver.Hom.unop (Iso.inv (opProdIsoCoprod A B)) ≫ Quiver.Hom.unop coprod.inr) prod.snd

Tactic:
rw [← unop_comp, inr_opProdIsoCoprod_inv, Quiver.Hom.unop_op]

Premises used: Quiver.Hom.unop_op, CategoryTheory.unop_comp, CategoryTheory.Limits.inr_opProdIsoCoprod_inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasPushouts.{v₁, u₁} C
⊢ HasColimitsOfShape.{0, 0, v₁, u₁} WalkingCospanᵒᵖ C

Tactic:
haveI : HasColimitsOfShape WalkingCospanᵒᵖ C :=
    hasColimitsOfShape_of_equivalence walkingCospanOpEquiv.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasPushouts.{v₁, u₁} C
this : HasColimitsOfShape.{0, 0, v₁, u₁} WalkingCospanᵒᵖ C
⊢ HasPullbacks.{v₁, u₁} Cᵒᵖ

Tactic:
apply hasLimitsOfShape_op_of_hasColimitsOfShape

Premises used: CategoryTheory.Limits.hasLimitsOfShape_op_of_hasColimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasPullbacks.{v₁, u₁} C
⊢ HasLimitsOfShape.{0, 0, v₁, u₁} WalkingSpanᵒᵖ C

Tactic:
haveI : HasLimitsOfShape WalkingSpanᵒᵖ C :=
    hasLimitsOfShape_of_equivalence walkingSpanOpEquiv.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasPullbacks.{v₁, u₁} C
this : HasLimitsOfShape.{0, 0, v₁, u₁} WalkingSpanᵒᵖ C
⊢ HasPushouts.{v₁, u₁} Cᵒᵖ

Tactic:
infer_instance