mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBiproduct.bicone W X).toCocone.ι.app { as := WalkingPair.left } ≫
      (BinaryBiproduct.bicone W X).toCone.π.app { as := WalkingPair.right } ≫
        (mapPair f g).app { as := WalkingPair.right } =
    f ≫
      (BinaryBiproduct.bicone Y Z).toCocone.ι.app { as := WalkingPair.left } ≫
        (BinaryBiproduct.bicone Y Z).toCone.π.app { as := WalkingPair.right }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₁.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBiproduct.bicone W X).toCocone.ι.app { as := WalkingPair.right } ≫
      (BinaryBiproduct.bicone W X).toCone.π.app { as := WalkingPair.left } ≫
        (mapPair f g).app { as := WalkingPair.left } =
    g ≫
      (BinaryBiproduct.bicone Y Z).toCocone.ι.app { as := WalkingPair.right } ≫
        (BinaryBiproduct.bicone Y Z).toCone.π.app { as := WalkingPair.left }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ t.inl ≫ t.toCone.π.app { as := WalkingPair.left } = (BinaryFan.mk (𝟙 X) 0).π.app { as := WalkingPair.left }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ t.inl ≫ t.toCone.π.app { as := WalkingPair.right } = (BinaryFan.mk (𝟙 X) 0).π.app { as := WalkingPair.right }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBiproduct.bicone W X).toCocone.ι.app { as := WalkingPair.right } ≫
      (BinaryBiproduct.bicone W X).toCone.π.app { as := WalkingPair.right } ≫ g =
    g ≫
      (BinaryBiproduct.bicone Y Z).toCocone.ι.app { as := WalkingPair.right } ≫
        (BinaryBiproduct.bicone Y Z).toCone.π.app { as := WalkingPair.right }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ t.inr ≫ t.toCone.π.app { as := WalkingPair.left } = (BinaryFan.mk 0 (𝟙 Y)).π.app { as := WalkingPair.left }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ t.inr ≫ t.toCone.π.app { as := WalkingPair.right } = (BinaryFan.mk 0 (𝟙 Y)).π.app { as := WalkingPair.right }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ (t.fst ≫ t.inl + t.snd ≫ t.inr) ≫ BinaryFan.fst t.toCone = 𝟙 t.pt ≫ BinaryFan.fst t.toCone

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ (t.fst ≫ t.inl + t.snd ≫ t.inr) ≫ BinaryFan.snd t.toCone = 𝟙 t.pt ≫ BinaryFan.snd t.toCone

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : Cone (pair X Y)
ht : IsLimit t
⊢ ((BinaryBicone.ofLimitCone ht).fst ≫ (BinaryBicone.ofLimitCone ht).inl +
        (BinaryBicone.ofLimitCone ht).snd ≫ (BinaryBicone.ofLimitCone ht).inr) ≫
      BinaryFan.fst t =
    𝟙 (BinaryBicone.ofLimitCone ht).pt ≫ BinaryFan.fst t

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : Cone (pair X Y)
ht : IsLimit t
⊢ ((BinaryBicone.ofLimitCone ht).fst ≫ (BinaryBicone.ofLimitCone ht).inl +
        (BinaryBicone.ofLimitCone ht).snd ≫ (BinaryBicone.ofLimitCone ht).inr) ≫
      BinaryFan.snd t =
    𝟙 (BinaryBicone.ofLimitCone ht).pt ≫ BinaryFan.snd t

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ t.toCocone.ι.app { as := WalkingPair.left } ≫ t.fst = (BinaryCofan.mk (𝟙 X) 0).ι.app { as := WalkingPair.left }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ t.toCocone.ι.app { as := WalkingPair.right } ≫ t.fst = (BinaryCofan.mk (𝟙 X) 0).ι.app { as := WalkingPair.right }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case refine_1.left
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inl ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.left } =
    inl ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ t.toCocone.ι.app { as := WalkingPair.left } ≫ t.snd = (BinaryCofan.mk 0 (𝟙 Y)).ι.app { as := WalkingPair.left }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ t.toCocone.ι.app { as := WalkingPair.right } ≫ t.snd = (BinaryCofan.mk 0 (𝟙 Y)).ι.app { as := WalkingPair.right }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case refine_1.right
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inl ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.right } =
    inl ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case refine_2.left
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.left } =
    inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case refine_2.right
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.right } =
    inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ BinaryCofan.inl t.toCocone ≫ (t.fst ≫ t.inl + t.snd ≫ t.inr) = BinaryCofan.inl t.toCocone ≫ 𝟙 t.pt

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ BinaryCofan.inr t.toCocone ≫ (t.fst ≫ t.inl + t.snd ≫ t.inr) = BinaryCofan.inr t.toCocone ≫ 𝟙 t.pt

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : Cocone (pair X Y)
ht : IsColimit t
⊢ t.ι.app { as := WalkingPair.left } ≫ (Iso.refl t.pt).hom =
    (BinaryBicone.ofColimitCocone ht).toCocone.ι.app { as := WalkingPair.left }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : Cocone (pair X Y)
ht : IsColimit t
⊢ t.ι.app { as := WalkingPair.right } ≫ (Iso.refl t.pt).hom =
    (BinaryBicone.ofColimitCocone ht).toCocone.ι.app { as := WalkingPair.right }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case h₀.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (inl ≫ (fst ≫ inl + snd ≫ inr)) ≫ fst = (inl ≫ 𝟙 (X ⊞ Y)) ≫ fst

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (inl ≫ (fst ≫ inl + snd ≫ inr)) ≫ snd = (inl ≫ 𝟙 (X ⊞ Y)) ≫ snd

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case h₁.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (inr ≫ (fst ≫ inl + snd ≫ inr)) ≫ fst = (inr ≫ 𝟙 (X ⊞ Y)) ≫ fst

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (inr ≫ (fst ≫ inl + snd ≫ inr)) ≫ snd = (inr ≫ 𝟙 (X ⊞ Y)) ≫ snd

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
T : C
f : X ⟶ T
g : Y ⟶ T
⊢ inl ≫ desc f g = inl ≫ (fst ≫ f + snd ≫ g)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
T : C
f : X ⟶ T
g : Y ⟶ T
⊢ inr ≫ desc f g = inr ≫ (fst ≫ f + snd ≫ g)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case h₀.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ (inl ≫ map f g) ≫ fst = (inl ≫ (fst ≫ f ≫ inl + snd ≫ g ≫ inr)) ≫ fst

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ (inl ≫ map f g) ≫ snd = (inl ≫ (fst ≫ f ≫ inl + snd ≫ g ≫ inr)) ≫ snd

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case h₁.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ fst = (inr ≫ (fst ≫ f ≫ inl + snd ≫ g ≫ inr)) ≫ fst

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ snd = (inr ≫ (fst ≫ f ≫ inl + snd ≫ g ≫ inr)) ≫ snd

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝⁷ : Category.{uC', uC} C
inst✝⁶ : HasZeroMorphisms C
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
P Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
⊢ map f g = (biprod.isoProd W X).inv ≫ biprod.map f g ≫ (biprod.isoProd Y Z).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case pos
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W' : C
g' : W' ⟶ ⨁ f
w : g' ≫ biproduct.toSubtype f p = 0
j : K
h : (p j)ᶜ
⊢ g' ≫ biproduct.π f j ≫ 𝟙 (f j) = g' ≫ biproduct.π f j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ (𝟙 Y - (𝟙 Y - retraction f ≫ f)) ≫ Cofork.π c = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
c' : CokernelCofork (𝟙 Y - (𝟙 Y - retraction f ≫ f)) := CokernelCofork.ofπ (Cofork.π c) ⋯
⊢ 𝟙 Y - (𝟙 Y - retraction f ≫ f) = retraction f ≫ f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
c' : CokernelCofork (𝟙 Y - (𝟙 Y - retraction f ≫ f)) := CokernelCofork.ofπ (Cofork.π c) ⋯
i' : IsColimit c' := isCokernelEpiComp i (retraction f) ⋯
i'' : IsColimit (coforkOfCokernelCofork c') := isColimitCoforkOfCokernelCofork i'
⊢ (𝟙 Y - retraction f ≫ f) ≫ (𝟙 Y - retraction f ≫ f) = 𝟙 Y - retraction f ≫ f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ f ≫ retraction f = 𝟙 X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ f ≫ Cofork.π c = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝⁷ : Category.{uC', uC} C
inst✝⁶ : HasZeroMorphisms C
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
P Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
⊢ map f g = (biprod.isoCoprod W X).inv ≫ biprod.map f g ≫ (biprod.isoCoprod Y Z).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₁
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P Q X Y : C
c : BinaryBicone 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

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₂
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P Q X Y : C
c : BinaryBicone 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

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T✝ : C
f : T✝ ⟶ X
g : T✝ ⟶ Y
⊢ (f ≫ b.inl + g ≫ b.inr) ≫ BinaryFan.fst b.toCone = f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T✝ : C
f : T✝ ⟶ X
g : T✝ ⟶ Y
⊢ (f ≫ b.inl + g ≫ b.inr) ≫ BinaryFan.snd b.toCone = g

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₁
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P Q X Y : C
c : BinaryBicone 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

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₂
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P Q X Y : C
c : BinaryBicone 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

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case pos
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W : C
g' : ⨁ f ⟶ W
w : biproduct.fromSubtype f p ≫ g' = 0
j : K
h : (p j)ᶜ
⊢ 𝟙 (f j) ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₁
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P Q X Y : C
c : BinaryBicone 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

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₂
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P Q X Y : C
c : BinaryBicone 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

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₁
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P Q X Y : C
c : BinaryBicone 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

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₂
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P Q X Y : C
c : BinaryBicone 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

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
x : ↑M
⊢ (ConcreteCategory.hom (𝟙 M)) x = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N O : ModuleCat R
f : M ⟶ N
g : N ⟶ O
x : ↑M
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
e : M ≅ N
x : ↑M
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
e : M ≅ N
x : ↑N
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) 0 = (Hom.hom default) 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.fstKernelFork
T✝ : C
f : T✝ ⟶ X
g : T✝ ⟶ Y
⊢ (f ≫ b.inl + g ≫ b.inr) ≫ BinaryFan.fst b.toCone = f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.fstKernelFork
T✝ : C
f : T✝ ⟶ X
g : T✝ ⟶ Y
⊢ (f ≫ b.inl + g ≫ b.inr) ≫ BinaryFan.snd b.toCone = g

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case refine_1
J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasFiniteBiproducts C
X : C
a : ⨁ Empty.elim ⟶ X
⊢ ∀ (j : Empty), biproduct.ι Empty.elim j ≫ a = biproduct.ι Empty.elim j ≫ default

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case refine_2
J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasFiniteBiproducts C
X : C
a : X ⟶ ⨁ Empty.elim
⊢ ∀ (j : Empty), a ≫ biproduct.π Empty.elim j = default ≫ biproduct.π Empty.elim j

Tactic:
simp

Goal state after: