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
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 :=
      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))
have 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
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
⊢ 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))
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.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: simp only [colimit.ι_desc_assoc]
-- 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 :=
      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))
have 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
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
A B : C
inst_1 : HasBinaryProduct.{v₁, u₁} A B
⊢ 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))
have 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 := sorry, inv_hom_id := sorry }) :
    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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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))
⊢ 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))
have 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
Tactic: rw [opProdIsoCoprod, ← op_comp, prod.lift_fst, 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
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
⊢ 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))
have rw₂ : Eq.{v₁ + 1} (α := op A ⟶ coprod.{v₁, u₁} (op A) (op B)) (Quiver.Hom.op (Quiver.Hom.unop coprod.inl)) coprod.inl
Tactic: rw [opProdIsoCoprod, ← op_comp, prod.lift_fst, 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
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
⊢ 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))
have rw₃ : Eq.{v₁ + 1} (α := op A ⟶ coprod.{v₁, u₁} (op A) (op B)) coprod.inl coprod.inl
Tactic: rw [opProdIsoCoprod, ← op_comp, prod.lift_fst, 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
A B : C
inst_1 : HasBinaryProduct.{v₁, u₁} A B
⊢ 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))
have 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 := sorry, inv_hom_id := sorry }) :
    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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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))
⊢ 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))
have 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
Tactic: rw [opProdIsoCoprod, ← op_comp, prod.lift_snd, 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
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
⊢ 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))
have rw₂ : Eq.{v₁ + 1} (α := op B ⟶ coprod.{v₁, u₁} (op A) (op B)) (Quiver.Hom.op (Quiver.Hom.unop coprod.inr)) coprod.inr
Tactic: rw [opProdIsoCoprod, ← op_comp, prod.lift_snd, 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
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
⊢ 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))
have rw₃ : Eq.{v₁ + 1} (α := op B ⟶ coprod.{v₁, u₁} (op A) (op B)) coprod.inr coprod.inr
Tactic: rw [opProdIsoCoprod, ← op_comp, prod.lift_snd, 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
A B : C
inst_1 : HasBinaryProduct.{v₁, u₁} A B
⊢ Eq.{v₁ + 1} (α := op A ⟶ op (prod.{v₁, u₁} A B)) (coprod.inl ≫ Iso.inv (opProdIsoCoprod A B)) (Quiver.Hom.op prod.fst)
have 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))
Tactic: rw [Iso.comp_inv_eq, fst_opProdIsoCoprod_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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))
⊢ Eq.{v₁ + 1} (α := op A ⟶ op (prod.{v₁, u₁} A B)) (coprod.inl ≫ Iso.inv (opProdIsoCoprod A B)) (Quiver.Hom.op prod.fst)
have rw₁ : Eq.{v₁ + 1} (α := op A ⟶ coprod.{v₁, u₁} (op A) (op B)) coprod.inl coprod.inl
Tactic: rw [Iso.comp_inv_eq, fst_opProdIsoCoprod_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
inst_1 : HasBinaryProduct.{v₁, u₁} A B
⊢ Eq.{v₁ + 1} (α := op B ⟶ op (prod.{v₁, u₁} A B)) (coprod.inr ≫ Iso.inv (opProdIsoCoprod A B)) (Quiver.Hom.op prod.snd)
have 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))
Tactic: rw [Iso.comp_inv_eq, snd_opProdIsoCoprod_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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))
⊢ Eq.{v₁ + 1} (α := op B ⟶ op (prod.{v₁, u₁} A B)) (coprod.inr ≫ Iso.inv (opProdIsoCoprod A B)) (Quiver.Hom.op prod.snd)
have rw₁ : Eq.{v₁ + 1} (α := op B ⟶ coprod.{v₁, u₁} (op A) (op B)) coprod.inr coprod.inr
Tactic: rw [Iso.comp_inv_eq, snd_opProdIsoCoprod_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
inst_1 : HasBinaryProduct.{v₁, u₁} A B
⊢ 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
have 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
Tactic: rw [← unop_comp, inl_opProdIsoCoprod_inv, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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
⊢ 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
have rw₁ : Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op A)) (Quiver.Hom.unop (Quiver.Hom.op prod.fst)) prod.fst
Tactic: rw [← unop_comp, inl_opProdIsoCoprod_inv, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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
⊢ 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
have rw₂ : Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op A)) prod.fst prod.fst
Tactic: rw [← unop_comp, inl_opProdIsoCoprod_inv, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
inst_1 : HasBinaryProduct.{v₁, u₁} A B
⊢ 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
have 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
Tactic: rw [← unop_comp, inr_opProdIsoCoprod_inv, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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
⊢ 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
have rw₁ : Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op B)) (Quiver.Hom.unop (Quiver.Hom.op prod.snd)) prod.snd
Tactic: rw [← unop_comp, inr_opProdIsoCoprod_inv, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products (goal)
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
⊢ 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
have rw₂ : Eq.{v₁ + 1} (α := unop (op (prod.{v₁, u₁} A B)) ⟶ unop (op B)) prod.snd prod.snd
Tactic: rw [← unop_comp, inr_opProdIsoCoprod_inv, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasPushouts.{v₁, u₁} C
⊢ HasPullbacks.{v₁, u₁} Cᵒᵖ
have this : HasColimitsOfShape.{0, 0, v₁, u₁} WalkingCospanᵒᵖ C
Tactic: haveI : HasColimitsOfShape WalkingCospanᵒᵖ C :=
    hasColimitsOfShape_of_equivalence walkingCospanOpEquiv.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasPullbacks.{v₁, u₁} C
⊢ HasPushouts.{v₁, u₁} Cᵒᵖ
have this : HasLimitsOfShape.{0, 0, v₁, u₁} WalkingSpanᵒᵖ C
Tactic: haveI : HasLimitsOfShape WalkingSpanᵒᵖ C :=
    hasLimitsOfShape_of_equivalence walkingSpanOpEquiv.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsColimit c ≃ IsLimit c.op
have f₁ : IsColimit c → IsLimit c.op
Tactic: apply equivOfSubsingletonOfSubsingleton
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
f₁ : IsColimit c → IsLimit c.op
⊢ IsColimit c ≃ IsLimit c.op
have g₁ : IsLimit c.op → IsColimit c
Tactic: apply equivOfSubsingletonOfSubsingleton