awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
c : BinaryBicone.{uC', uC} P Q
⊢ c.toCocone.ι.app { as := WalkingPair.left } = c.inl

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
c : BinaryBicone.{uC', uC} P Q
⊢ c.toCocone.ι.app { as := WalkingPair.right } = c.inr

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
c : BinaryBicone.{uC', uC} P Q
⊢ BinaryCofan.inl c.toCocone = c.inl

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
c : BinaryBicone.{uC', uC} P Q
⊢ BinaryCofan.inr c.toCocone = c.inr

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' : C
c : BinaryBicone.{uC', uC} P Q
⊢ IsSplitMono c.inl

Tactic:
c.retract_left.instIsSplitMonoI

Premises used: CategoryTheory.Limits.BinaryBicone.retract_left, CategoryTheory.Retract.instIsSplitMonoI
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' : C
c : BinaryBicone.{uC', uC} P Q
⊢ IsSplitMono c.inr

Tactic:
c.retract_right.instIsSplitMonoI

Premises used: CategoryTheory.Limits.BinaryBicone.retract_right, CategoryTheory.Retract.instIsSplitMonoI
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' : C
c : BinaryBicone.{uC', uC} P Q
⊢ IsSplitEpi c.fst

Tactic:
c.retract_left.instIsSplitEpiR

Premises used: CategoryTheory.Limits.BinaryBicone.retract_left, CategoryTheory.Retract.instIsSplitEpiR
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' : C
c : BinaryBicone.{uC', uC} P Q
⊢ IsSplitEpi c.snd

Tactic:
c.retract_right.instIsSplitEpiR

Premises used: CategoryTheory.Limits.BinaryBicone.retract_right, CategoryTheory.Retract.instIsSplitEpiR
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
j j' : WalkingPair
left :
  Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.left b.inl b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) j' b.fst b.snd) :
      pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
    (if h : WalkingPair.left = j' then eqToHom ⋯ else 0 : pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
right :
  Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.right ⟶ pairFunction X Y j')
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.right b.inl
          b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) j' b.fst b.snd) :
      pairFunction X Y WalkingPair.right ⟶ pairFunction X Y j')
    (if h : WalkingPair.right = j' then eqToHom ⋯ else 0 : pairFunction X Y WalkingPair.right ⟶ pairFunction X Y j')
⊢ Eq.{uC' + 1} (α := pairFunction X Y j ⟶ pairFunction X Y j')
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) j b.inl b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) j' b.fst b.snd) :
      pairFunction X Y j ⟶ pairFunction X Y j')
    (if h : j = j' then eqToHom ⋯ else 0 : pairFunction X Y j ⟶ pairFunction X Y j')

Tactic:
rcases j with ⟨⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
j' : WalkingPair
left :
  Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.left)
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.left b.inl b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) WalkingPair.left b.fst
          b.snd) :
      pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.left)
    (if h : WalkingPair.left = WalkingPair.left then eqToHom ⋯ else 0 :
      pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.left)
left₁ :
  Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.right)
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.left b.inl b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) WalkingPair.right b.fst
          b.snd) :
      pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.right)
    (if h : WalkingPair.left = WalkingPair.right then eqToHom ⋯ else 0 :
      pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.right)
⊢ Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.left b.inl b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) j' b.fst b.snd) :
      pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
    (if h : WalkingPair.left = j' then eqToHom ⋯ else 0 : pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')

Tactic:
rcases j' with ⟨⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
j' : WalkingPair
right :
  Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.left)
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.right b.inl
          b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) WalkingPair.left b.fst
          b.snd) :
      pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.left)
    (if h : WalkingPair.right = WalkingPair.left then eqToHom ⋯ else 0 :
      pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.left)
right₁ :
  Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.right)
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.right b.inl
          b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) WalkingPair.right b.fst
          b.snd) :
      pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.right)
    (if h : WalkingPair.right = WalkingPair.right then eqToHom ⋯ else 0 :
      pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.right)
⊢ Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.right ⟶ pairFunction X Y j')
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.right b.inl
          b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) j' b.fst b.snd) :
      pairFunction X Y WalkingPair.right ⟶ pairFunction X Y j')
    (if h : WalkingPair.right = j' then eqToHom ⋯ else 0 : pairFunction X Y WalkingPair.right ⟶ pairFunction X Y j')

Tactic:
rcases j' with ⟨⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
⊢ Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.left)
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.left b.inl b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) WalkingPair.left b.fst
          b.snd) :
      pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.left)
    (if h : WalkingPair.left = WalkingPair.left then eqToHom ⋯ else 0 :
      pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.left)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
⊢ Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.right)
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.left b.inl b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) WalkingPair.right b.fst
          b.snd) :
      pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.right)
    (if h : WalkingPair.left = WalkingPair.right then eqToHom ⋯ else 0 :
      pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.right)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
⊢ Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.left)
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.right b.inl
          b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) WalkingPair.left b.fst
          b.snd) :
      pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.left)
    (if h : WalkingPair.right = WalkingPair.left then eqToHom ⋯ else 0 :
      pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.left)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
⊢ Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.right)
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.right b.inl
          b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) WalkingPair.right b.fst
          b.snd) :
      pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.right)
    (if h : WalkingPair.right = WalkingPair.right then eqToHom ⋯ else 0 :
      pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.right)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
x : Discrete WalkingPair
as : WalkingPair
left :
  Eq (α :=
    obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBicone.toCone.pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := WalkingPair.left : Discrete WalkingPair })
    (b.toBicone.toCone.π.app { as := WalkingPair.left })
    (Iso.hom (Iso.refl b.toBicone.toCone.pt) ≫ b.toCone.π.app { as := WalkingPair.left })
right :
  Eq (α :=
    obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBicone.toCone.pt)
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := WalkingPair.right : Discrete WalkingPair })
    (b.toBicone.toCone.π.app { as := WalkingPair.right })
    (Iso.hom (Iso.refl b.toBicone.toCone.pt) ≫ b.toCone.π.app { as := WalkingPair.right })
⊢ Eq (α :=
    obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBicone.toCone.pt) { as := as : Discrete WalkingPair } ⟶
      obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := as : Discrete WalkingPair })
    (b.toBicone.toCone.π.app { as := as }) (Iso.hom (Iso.refl b.toBicone.toCone.pt) ≫ b.toCone.π.app { as := as })

Tactic:
cases as
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
x : Discrete WalkingPair
⊢ Eq (α :=
    obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBicone.toCone.pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := WalkingPair.left : Discrete WalkingPair })
    (b.toBicone.toCone.π.app { as := WalkingPair.left })
    (Iso.hom (Iso.refl b.toBicone.toCone.pt) ≫ b.toCone.π.app { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
x : Discrete WalkingPair
⊢ Eq (α :=
    obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBicone.toCone.pt)
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := WalkingPair.right : Discrete WalkingPair })
    (b.toBicone.toCone.π.app { as := WalkingPair.right })
    (Iso.hom (Iso.refl b.toBicone.toCone.pt) ≫ b.toCone.π.app { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
x : Discrete WalkingPair
as : WalkingPair
left :
  Eq (α :=
    obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      b.toCocone.pt)
    (b.toBicone.toCocone.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
      Iso.hom (Iso.refl b.toBicone.toCocone.pt))
    (b.toCocone.ι.app { as := WalkingPair.left })
right :
  Eq (α :=
    obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      b.toCocone.pt)
    (b.toBicone.toCocone.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫
      Iso.hom (Iso.refl b.toBicone.toCocone.pt))
    (b.toCocone.ι.app { as := WalkingPair.right })
⊢ Eq (α :=
    obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := as : Discrete WalkingPair } ⟶ b.toCocone.pt)
    (b.toBicone.toCocone.ι.app { as := as : Discrete WalkingPair } ≫ Iso.hom (Iso.refl b.toBicone.toCocone.pt))
    (b.toCocone.ι.app { as := as })

Tactic:
cases as
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
x : Discrete WalkingPair
⊢ Eq (α :=
    obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      b.toCocone.pt)
    (b.toBicone.toCocone.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
      Iso.hom (Iso.refl b.toBicone.toCocone.pt))
    (b.toCocone.ι.app { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
x : Discrete WalkingPair
⊢ Eq (α :=
    obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      b.toCocone.pt)
    (b.toBicone.toCocone.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫
      Iso.hom (Iso.refl b.toBicone.toCocone.pt))
    (b.toCocone.ι.app { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
⊢ b.ι WalkingPair.left ≫ b.π WalkingPair.left = 𝟙 X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
⊢ b.ι WalkingPair.left ≫ b.π WalkingPair.right = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
⊢ b.ι WalkingPair.right ≫ b.π WalkingPair.left = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
⊢ b.ι WalkingPair.right ≫ b.π WalkingPair.right = 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
j : Discrete WalkingPair
left :
  Eq (α :=
    obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBinaryBicone.toCone.pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (b.toBinaryBicone.toCone.π.app { as := WalkingPair.left })
    (Iso.hom (Iso.refl b.toBinaryBicone.toCone.pt) ≫ b.toCone.π.app { as := WalkingPair.left })
right :
  Eq (α :=
    obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBinaryBicone.toCone.pt)
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (b.toBinaryBicone.toCone.π.app { as := WalkingPair.right })
    (Iso.hom (Iso.refl b.toBinaryBicone.toCone.pt) ≫ b.toCone.π.app { as := WalkingPair.right })
⊢ b.toBinaryBicone.toCone.π.app j = Iso.hom (Iso.refl b.toBinaryBicone.toCone.pt) ≫ b.toCone.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
⊢ Eq (α :=
    obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBinaryBicone.toCone.pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (b.toBinaryBicone.toCone.π.app { as := WalkingPair.left })
    (Iso.hom (Iso.refl b.toBinaryBicone.toCone.pt) ≫ b.toCone.π.app { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
⊢ Eq (α :=
    obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBinaryBicone.toCone.pt)
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (b.toBinaryBicone.toCone.π.app { as := WalkingPair.right })
    (Iso.hom (Iso.refl b.toBinaryBicone.toCone.pt) ≫ b.toCone.π.app { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
j : Discrete WalkingPair
left :
  Eq (α := obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶ b.toCocone.pt)
    (b.toBinaryBicone.toCocone.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
      Iso.hom (Iso.refl b.toBinaryBicone.toCocone.pt))
    (b.toCocone.ι.app { as := WalkingPair.left })
right :
  Eq (α := obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶ b.toCocone.pt)
    (b.toBinaryBicone.toCocone.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫
      Iso.hom (Iso.refl b.toBinaryBicone.toCocone.pt))
    (b.toCocone.ι.app { as := WalkingPair.right })
⊢ b.toBinaryBicone.toCocone.ι.app j ≫ Iso.hom (Iso.refl b.toBinaryBicone.toCocone.pt) = b.toCocone.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
⊢ Eq (α := obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶ b.toCocone.pt)
    (b.toBinaryBicone.toCocone.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
      Iso.hom (Iso.refl b.toBinaryBicone.toCocone.pt))
    (b.toCocone.ι.app { as := WalkingPair.left })

Tactic:
simp