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
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
⊢ Eq (α := Y ⟶ obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) { as := WalkingPair.right }))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
      (desc b.inl b.inr ≫ 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 Q X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
rw :
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y)
      (Iso.hom (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) (desc b.inl b.inr) =
    𝟙 b.pt
rw₁ :
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y)
      (Iso.hom (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)))
      (Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) =
    𝟙 b.pt
rw₂ rw₃ : Eq.{uC' + 1} (α := b.pt ⟶ b.pt) (𝟙 b.pt) (𝟙 b.pt)
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (lift b.fst b.snd) (desc b.inl b.inr) = 𝟙 b.pt

Tactic:
rw [← biprod.conePointUniqueUpToIso_hom X Y hb, ←
      biprod.conePointUniqueUpToIso_inv X Y hb, Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Limits.biprod.conePointUniqueUpToIso_hom, CategoryTheory.Limits.biprod.conePointUniqueUpToIso_inv
-- 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 Q X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
rw :
  desc b.inl b.inr ≫ Iso.hom (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)) =
    𝟙 (biprod.{uC', uC} X Y)
rw₁ :
  Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)) ≫
      Iso.hom (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)) =
    𝟙 (biprod.{uC', uC} X Y)
rw₂ rw₃ :
  Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ biprod.{uC', uC} X Y) (𝟙 (biprod.{uC', uC} X Y)) (𝟙 (biprod.{uC', uC} X Y))
⊢ desc b.inl b.inr ≫ lift b.fst b.snd = 𝟙 (biprod.{uC', uC} X Y)

Tactic:
rw [← biprod.conePointUniqueUpToIso_hom X Y hb, ←
      biprod.conePointUniqueUpToIso_inv X Y hb, Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Limits.biprod.conePointUniqueUpToIso_hom, CategoryTheory.Limits.biprod.conePointUniqueUpToIso_inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
mp : IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl → 𝟙 (biprod.{uC', uC} X Y) = fst ≫ inl
mpr : 𝟙 (biprod.{uC', uC} X Y) = fst ≫ inl → IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl
⊢ IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl ↔ 𝟙 (biprod.{uC', uC} X Y) = fst ≫ inl

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
h : IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ X) (inv inl ≫ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl fst)
    (inv inl ≫ 𝟙 X)

Tactic:
have := (cancel_epi (inv biprod.inl : X ⊞ Y ⟶ X)).2 <| @biprod.inl_fst _ _ _ X Y _
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
h : IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl
this :
  Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ X) (inv inl ≫ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl fst)
    (inv inl ≫ 𝟙 X)
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ X) fst (inv inl)

Tactic:
rw [IsIso.inv_hom_id_assoc, Category.comp_id] at this

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.IsIso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
h : IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl
this : Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ X) fst (inv inl)
mp : 𝟙 (biprod.{uC', uC} X Y) = inv inl ≫ inl
mp₁ mp₂ :
  Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ biprod.{uC', uC} X Y) (𝟙 (biprod.{uC', uC} X Y)) (𝟙 (biprod.{uC', uC} X Y))
⊢ 𝟙 (biprod.{uC', uC} X Y) = fst ≫ inl

Tactic:
rw [this, IsIso.inv_hom_id]

Premises used: CategoryTheory.IsIso.inv_hom_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
h : 𝟙 (biprod.{uC', uC} X Y) = fst ≫ inl
⊢ IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl

Tactic:
⟨⟨biprod.fst, biprod.inl_fst, h.symm⟩⟩

Premises used: CategoryTheory.Limits.biprod.inl_fst, CategoryTheory.Limits.biprod.fst, And.intro, Exists.intro, Eq.symm, CategoryTheory.IsIso.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
h : 𝟙 (biprod.{uC', uC} X Y) = fst ≫ inl
⊢ IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl

Tactic:
exact ⟨⟨biprod.fst, biprod.inl_fst, h.symm⟩⟩
-- 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 Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_4 : Epi f
inst_5 : Epi g
inst_6 : HasBinaryBiproduct.{uC', uC} W X
inst_7 : HasBinaryBiproduct.{uC', uC} Y Z
⊢ Eq (α := biprod.{uC', uC} W X ⟶ biprod.{uC', uC} Y Z) (map f g)
    (Iso.hom (isoCoprod W X) ≫ coprod.map f g ≫ Iso.inv (isoCoprod Y Z))

Tactic:
aesop
-- 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 Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_4 : Epi f
inst_5 : Epi g
inst_6 : HasBinaryBiproduct.{uC', uC} W X
inst_7 : HasBinaryBiproduct.{uC', uC} Y Z
rw :
  Epi (X := biprod.{uC', uC} W X) (Y := biprod.{uC', uC} Y Z)
    (Iso.hom (isoCoprod W X) ≫ coprod.map f g ≫ Iso.inv (isoCoprod Y Z))
⊢ Epi (X := biprod.{uC', uC} W X) (Y := biprod.{uC', uC} Y Z) (map f g)

Tactic:
rw [show biprod.map f g =
    (biprod.isoCoprod _ _).hom ≫ coprod.map f g ≫ (biprod.isoCoprod _ _).inv by aesop]
-- 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 Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_4 : Epi f
inst_5 : Epi g
inst_6 : HasBinaryBiproduct.{uC', uC} W X
inst_7 : HasBinaryBiproduct.{uC', uC} Y Z
⊢ Epi (X := biprod.{uC', uC} W X) (Y := biprod.{uC', uC} Y Z)
    (Iso.hom (isoCoprod W X) ≫ coprod.map f g ≫ Iso.inv (isoCoprod Y Z))

Tactic:
infer_instance
-- 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 Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_4 : Epi f
inst_5 : Epi g
inst_6 : HasBinaryBiproduct.{uC', uC} W X
inst_7 : HasBinaryBiproduct.{uC', uC} Y Z
⊢ Eq (α := prod.{uC', uC} W X ⟶ prod.{uC', uC} Y Z) (map f g : prod.{uC', uC} W X ⟶ prod.{uC', uC} Y Z)
    (CategoryStruct.comp (Y := biprod.{uC', uC} W X) (Iso.inv (biprod.isoProd W X))
        (CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (biprod.map f g) (Iso.hom (biprod.isoProd Y Z))) :
      prod.{uC', uC} W X ⟶ prod.{uC', uC} Y Z)

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 Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_4 : Epi f
inst_5 : Epi g
inst_6 : HasBinaryBiproduct.{uC', uC} W X
inst_7 : HasBinaryBiproduct.{uC', uC} Y Z
rw :
  Epi (X := prod.{uC', uC} W X) (Y := prod.{uC', uC} Y Z)
    (CategoryStruct.comp (Y := biprod.{uC', uC} W X) (Iso.inv (biprod.isoProd W X))
        (CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (biprod.map f g) (Iso.hom (biprod.isoProd Y Z))) :
      prod.{uC', uC} W X ⟶ prod.{uC', uC} Y Z)
⊢ Epi (X := prod.{uC', uC} W X) (Y := prod.{uC', uC} Y Z) (map f g)

Tactic:
rw [show prod.map f g = (biprod.isoProd _ _).inv ≫ biprod.map f g ≫
    (biprod.isoProd _ _).hom by 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 Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_4 : Epi f
inst_5 : Epi g
inst_6 : HasBinaryBiproduct.{uC', uC} W X
inst_7 : HasBinaryBiproduct.{uC', uC} Y Z
⊢ Epi (X := prod.{uC', uC} W X) (Y := prod.{uC', uC} Y Z)
    (CategoryStruct.comp (Y := biprod.{uC', uC} W X) (Iso.inv (biprod.isoProd W X))
        (CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (biprod.map f g) (Iso.hom (biprod.isoProd Y Z))) :
      prod.{uC', uC} W X ⟶ prod.{uC', uC} Y Z)

Tactic:
infer_instance
-- 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 Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_4 : Mono f
inst_5 : Mono g
inst_6 : HasBinaryBiproduct.{uC', uC} W X
inst_7 : HasBinaryBiproduct.{uC', uC} Y Z
⊢ Eq (α := biprod.{uC', uC} W X ⟶ biprod.{uC', uC} Y Z) (map f g)
    (Iso.hom (isoProd W X) ≫ prod.map f g ≫ Iso.inv (isoProd Y Z))

Tactic:
aesop
-- 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 Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_4 : Mono f
inst_5 : Mono g
inst_6 : HasBinaryBiproduct.{uC', uC} W X
inst_7 : HasBinaryBiproduct.{uC', uC} Y Z
rw :
  Mono (X := biprod.{uC', uC} W X) (Y := biprod.{uC', uC} Y Z)
    (Iso.hom (isoProd W X) ≫ prod.map f g ≫ Iso.inv (isoProd Y Z))
⊢ Mono (X := biprod.{uC', uC} W X) (Y := biprod.{uC', uC} Y Z) (map f g)

Tactic:
rw [show biprod.map f g = (biprod.isoProd _ _).hom ≫ prod.map f g ≫
    (biprod.isoProd _ _).inv by aesop]
-- 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 Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_4 : Mono f
inst_5 : Mono g
inst_6 : HasBinaryBiproduct.{uC', uC} W X
inst_7 : HasBinaryBiproduct.{uC', uC} Y Z
⊢ Mono (X := biprod.{uC', uC} W X) (Y := biprod.{uC', uC} Y Z)
    (Iso.hom (isoProd W X) ≫ prod.map f g ≫ Iso.inv (isoProd Y Z))

Tactic:
infer_instance
-- 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 Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_4 : Mono f
inst_5 : Mono g
inst_6 : HasBinaryBiproduct.{uC', uC} W X
inst_7 : HasBinaryBiproduct.{uC', uC} Y Z
⊢ Eq (α := coprod.{uC', uC} W X ⟶ coprod.{uC', uC} Y Z) (map f g : coprod.{uC', uC} W X ⟶ coprod.{uC', uC} Y Z)
    (CategoryStruct.comp (Y := biprod.{uC', uC} W X) (Iso.inv (biprod.isoCoprod W X))
        (CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (biprod.map f g) (Iso.hom (biprod.isoCoprod Y Z))) :
      coprod.{uC', uC} W X ⟶ coprod.{uC', uC} Y Z)

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 Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_4 : Mono f
inst_5 : Mono g
inst_6 : HasBinaryBiproduct.{uC', uC} W X
inst_7 : HasBinaryBiproduct.{uC', uC} Y Z
rw :
  Mono (X := coprod.{uC', uC} W X) (Y := coprod.{uC', uC} Y Z)
    (CategoryStruct.comp (Y := biprod.{uC', uC} W X) (Iso.inv (biprod.isoCoprod W X))
        (CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (biprod.map f g) (Iso.hom (biprod.isoCoprod Y Z))) :
      coprod.{uC', uC} W X ⟶ coprod.{uC', uC} Y Z)
⊢ Mono (X := coprod.{uC', uC} W X) (Y := coprod.{uC', uC} Y Z) (map f g)

Tactic:
rw [show coprod.map f g = (biprod.isoCoprod _ _).inv ≫ biprod.map f g ≫
    (biprod.isoCoprod _ _).hom by 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 Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_4 : Mono f
inst_5 : Mono g
inst_6 : HasBinaryBiproduct.{uC', uC} W X
inst_7 : HasBinaryBiproduct.{uC', uC} Y Z
⊢ Mono (X := coprod.{uC', uC} W X) (Y := coprod.{uC', uC} Y Z)
    (CategoryStruct.comp (Y := biprod.{uC', uC} W X) (Iso.inv (biprod.isoCoprod W X))
        (CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (biprod.map f g) (Iso.hom (biprod.isoCoprod Y Z))) :
      coprod.{uC', uC} W X ⟶ coprod.{uC', uC} Y Z)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
c : BinaryBicone.{uC', uC} X Y
⊢ Fork.ι c.fstKernelFork = c.inr

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ι, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
c : BinaryBicone.{uC', uC} X Y
⊢ Fork.ι c.sndKernelFork = c.inl

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ι, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
c : BinaryBicone.{uC', uC} X Y
⊢ Cofork.π c.inlCokernelCofork = c.snd

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
c : BinaryBicone.{uC', uC} X Y
⊢ Cofork.π c.inrCokernelCofork = c.fst

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.Cofork.π
-- 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 Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsLimit c.toCone
s : Fork c.fst 0
h₁ : ((s.ι ≫ c.snd) ≫ Fork.ι c.fstKernelFork) ≫ BinaryFan.fst c.toCone = s.ι ≫ BinaryFan.fst c.toCone
h₂ : ((s.ι ≫ c.snd) ≫ Fork.ι c.fstKernelFork) ≫ BinaryFan.snd c.toCone = s.ι ≫ BinaryFan.snd c.toCone
⊢ (s.ι ≫ c.snd) ≫ Fork.ι c.fstKernelFork = s.ι

Tactic:
apply BinaryFan.IsLimit.hom_ext i

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext
-- 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 Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsLimit c.toCone
s : Fork c.fst 0
⊢ ((s.ι ≫ c.snd) ≫ Fork.ι c.fstKernelFork) ≫ BinaryFan.fst c.toCone = s.ι ≫ BinaryFan.fst c.toCone

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 Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsLimit c.toCone
s : Fork c.fst 0
⊢ ((s.ι ≫ c.snd) ≫ Fork.ι c.fstKernelFork) ≫ BinaryFan.snd c.toCone = s.ι ≫ BinaryFan.snd c.toCone

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 Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsLimit c.toCone
s : Fork c.fst 0
m : s.pt ⟶ c.fstKernelFork.pt
hm : m ≫ Fork.ι c.fstKernelFork = s.ι
⊢ m = s.ι ≫ c.snd

Tactic:
simp [← hm]
-- 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 Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsLimit c.toCone
s : Fork c.snd 0
h₁ : ((s.ι ≫ c.fst) ≫ Fork.ι c.sndKernelFork) ≫ BinaryFan.fst c.toCone = s.ι ≫ BinaryFan.fst c.toCone
h₂ : ((s.ι ≫ c.fst) ≫ Fork.ι c.sndKernelFork) ≫ BinaryFan.snd c.toCone = s.ι ≫ BinaryFan.snd c.toCone
⊢ (s.ι ≫ c.fst) ≫ Fork.ι c.sndKernelFork = s.ι

Tactic:
apply BinaryFan.IsLimit.hom_ext i

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext
-- 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 Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsLimit c.toCone
s : Fork c.snd 0
⊢ ((s.ι ≫ c.fst) ≫ Fork.ι c.sndKernelFork) ≫ BinaryFan.fst c.toCone = s.ι ≫ BinaryFan.fst c.toCone

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 Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsLimit c.toCone
s : Fork c.snd 0
⊢ ((s.ι ≫ c.fst) ≫ Fork.ι c.sndKernelFork) ≫ BinaryFan.snd c.toCone = s.ι ≫ BinaryFan.snd c.toCone

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 Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsLimit c.toCone
s : Fork c.snd 0
m : s.pt ⟶ c.sndKernelFork.pt
hm : m ≫ Fork.ι c.sndKernelFork = s.ι
⊢ m = s.ι ≫ c.fst

Tactic:
simp [← hm]
-- 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 Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsColimit c.toCocone
s : Cofork c.inl 0
h₁ : BinaryCofan.inl c.toCocone ≫ Cofork.π c.inlCokernelCofork ≫ c.inr ≫ s.π = BinaryCofan.inl c.toCocone ≫ s.π
h₂ : BinaryCofan.inr c.toCocone ≫ Cofork.π c.inlCokernelCofork ≫ c.inr ≫ s.π = BinaryCofan.inr c.toCocone ≫ s.π
⊢ Cofork.π c.inlCokernelCofork ≫ c.inr ≫ s.π = s.π

Tactic:
apply BinaryCofan.IsColimit.hom_ext i

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext
-- 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 Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsColimit c.toCocone
s : Cofork c.inl 0
⊢ BinaryCofan.inl c.toCocone ≫ Cofork.π c.inlCokernelCofork ≫ c.inr ≫ s.π = BinaryCofan.inl c.toCocone ≫ s.π

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 Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsColimit c.toCocone
s : Cofork c.inl 0
⊢ BinaryCofan.inr c.toCocone ≫ Cofork.π c.inlCokernelCofork ≫ c.inr ≫ s.π = BinaryCofan.inr c.toCocone ≫ s.π

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 Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsColimit c.toCocone
s : Cofork c.inl 0
m : c.inlCokernelCofork.pt ⟶ s.pt
hm : Cofork.π c.inlCokernelCofork ≫ m = s.π
⊢ m = c.inr ≫ s.π

Tactic:
simp [← hm]
-- 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 Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsColimit c.toCocone
s : Cofork c.inr 0
h₁ : BinaryCofan.inl c.toCocone ≫ Cofork.π c.inrCokernelCofork ≫ c.inl ≫ s.π = BinaryCofan.inl c.toCocone ≫ s.π
h₂ : BinaryCofan.inr c.toCocone ≫ Cofork.π c.inrCokernelCofork ≫ c.inl ≫ s.π = BinaryCofan.inr c.toCocone ≫ s.π
⊢ Cofork.π c.inrCokernelCofork ≫ c.inl ≫ s.π = s.π

Tactic:
apply BinaryCofan.IsColimit.hom_ext i

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext
-- 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 Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsColimit c.toCocone
s : Cofork c.inr 0
⊢ BinaryCofan.inl c.toCocone ≫ Cofork.π c.inrCokernelCofork ≫ c.inl ≫ s.π = BinaryCofan.inl c.toCocone ≫ s.π

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 Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsColimit c.toCocone
s : Cofork c.inr 0
⊢ BinaryCofan.inr c.toCocone ≫ Cofork.π c.inrCokernelCofork ≫ c.inl ≫ s.π = BinaryCofan.inr c.toCocone ≫ s.π

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 Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsColimit c.toCocone
s : Cofork c.inr 0
m : c.inrCokernelCofork.pt ⟶ s.pt
hm : Cofork.π c.inrCokernelCofork ≫ m = s.π
⊢ m = c.inl ≫ s.π

Tactic:
simp [← hm]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
⊢ Eq.{uC' + 1} (α :=
    Cone.pt.{0, uC', 0, uC} (F := parallelPair (X := biprod.{uC', uC} X Y) fst 0) (fstKernelFork X Y) ⟶
      biprod.{uC', uC} X Y)
    (Fork.ι (fstKernelFork X Y)) inr

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ι, rfl