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

Goal state before:
pp: case left
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 P' Q Q' X Y : C
b : BinaryBicone X Y
x✝ : Discrete WalkingPair
⊢ b.toBicone.toCone.π.app { as := WalkingPair.left } =
    (Iso.refl b.toBicone.toCone.pt).hom ≫ b.toCone.π.app { as := WalkingPair.left }

pp: case right
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 P' Q Q' X Y : C
b : BinaryBicone X Y
x✝ : Discrete WalkingPair
⊢ b.toBicone.toCone.π.app { as := WalkingPair.right } =
    (Iso.refl b.toBicone.toCone.pt).hom ≫ b.toCone.π.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
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 P' Q Q' X Y : C
b : BinaryBicone X Y
x✝ : Discrete WalkingPair
⊢ b.toBicone.toCone.π.app { as := WalkingPair.left } =
    (Iso.refl b.toBicone.toCone.pt).hom ≫ b.toCone.π.app { as := WalkingPair.left }

case right
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 P' Q Q' X Y : C
b : BinaryBicone X Y
x✝ : Discrete WalkingPair
⊢ b.toBicone.toCone.π.app { as := WalkingPair.right } =
    (Iso.refl b.toBicone.toCone.pt).hom ≫ b.toCone.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case left
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 P' Q Q' X Y : C
b : BinaryBicone X Y
x✝ : Discrete WalkingPair
⊢ b.toBicone.toCocone.ι.app { as := WalkingPair.left } ≫ (Iso.refl b.toBicone.toCocone.pt).hom =
    b.toCocone.ι.app { as := WalkingPair.left }

pp: case right
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 P' Q Q' X Y : C
b : BinaryBicone X Y
x✝ : Discrete WalkingPair
⊢ b.toBicone.toCocone.ι.app { as := WalkingPair.right } ≫ (Iso.refl b.toBicone.toCocone.pt).hom =
    b.toCocone.ι.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
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 P' Q Q' X Y : C
b : BinaryBicone X Y
x✝ : Discrete WalkingPair
⊢ b.toBicone.toCocone.ι.app { as := WalkingPair.left } ≫ (Iso.refl b.toBicone.toCocone.pt).hom =
    b.toCocone.ι.app { as := WalkingPair.left }

case right
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 P' Q Q' X Y : C
b : BinaryBicone X Y
x✝ : Discrete WalkingPair
⊢ b.toBicone.toCocone.ι.app { as := WalkingPair.right } ≫ (Iso.refl b.toBicone.toCocone.pt).hom =
    b.toCocone.ι.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type u_1
inst✝¹ : Finite J
f : J → C
inst✝ : HasProduct f
⊢ HasBiproduct f

Tactic:
by
  cases nonempty_fintype J
  exact HasBiproduct.mk
    { bicone := _
      isBilimit := biconeIsBilimitOfLimitConeOfIsLimit (limit.isLimit _) }

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

Goal state before:
pp: case left
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
X Y : C
b : Bicone (pairFunction X Y)
⊢ b.toBinaryBicone.toCone.π.app { as := WalkingPair.left } =
    (Iso.refl b.toBinaryBicone.toCone.pt).hom ≫ b.toCone.π.app { as := WalkingPair.left }

pp: case right
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
X Y : C
b : Bicone (pairFunction X Y)
⊢ b.toBinaryBicone.toCone.π.app { as := WalkingPair.right } =
    (Iso.refl b.toBinaryBicone.toCone.pt).hom ≫ b.toCone.π.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
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
X Y : C
b : Bicone (pairFunction X Y)
⊢ b.toBinaryBicone.toCone.π.app { as := WalkingPair.left } =
    (Iso.refl b.toBinaryBicone.toCone.pt).hom ≫ b.toCone.π.app { as := WalkingPair.left }

case right
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
X Y : C
b : Bicone (pairFunction X Y)
⊢ b.toBinaryBicone.toCone.π.app { as := WalkingPair.right } =
    (Iso.refl b.toBinaryBicone.toCone.pt).hom ≫ b.toCone.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case left
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
X Y : C
b : Bicone (pairFunction X Y)
⊢ b.toBinaryBicone.toCocone.ι.app { as := WalkingPair.left } ≫ (Iso.refl b.toBinaryBicone.toCocone.pt).hom =
    b.toCocone.ι.app { as := WalkingPair.left }

pp: case right
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
X Y : C
b : Bicone (pairFunction X Y)
⊢ b.toBinaryBicone.toCocone.ι.app { as := WalkingPair.right } ≫ (Iso.refl b.toBinaryBicone.toCocone.pt).hom =
    b.toCocone.ι.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
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
X Y : C
b : Bicone (pairFunction X Y)
⊢ b.toBinaryBicone.toCocone.ι.app { as := WalkingPair.left } ≫ (Iso.refl b.toBinaryBicone.toCocone.pt).hom =
    b.toCocone.ι.app { as := WalkingPair.left }

case right
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
X Y : C
b : Bicone (pairFunction X Y)
⊢ b.toBinaryBicone.toCocone.ι.app { as := WalkingPair.right } ≫ (Iso.refl b.toBinaryBicone.toCocone.pt).hom =
    b.toCocone.ι.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
val✝ : Fintype β
g g' : γ
h : g' = g
⊢ ι f g' ≫ ((lift fun b ↦ π f (ε b)) ≫ desc fun b ↦ ι f (ε b)) ≫ π f g = ι f g' ≫ 𝟙 (⨁ f) ≫ π f g

pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
val✝ : Fintype β
g g' : γ
h : ¬g' = g
⊢ ι f g' ≫ ((lift fun b ↦ π f (ε b)) ≫ desc fun b ↦ ι f (ε b)) ≫ π f g = ι f g' ≫ 𝟙 (⨁ f) ≫ π f g

Tactic:
<;>

Goal state after:
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
val✝ : Fintype β
g g' : γ
h : g' = g
⊢ ι f g' ≫ ((lift fun b ↦ π f (ε b)) ≫ desc fun b ↦ ι f (ε b)) ≫ π f g = ι f g' ≫ 𝟙 (⨁ f) ≫ π f g

case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
val✝ : Fintype β
g g' : γ
h : ¬g' = g
⊢ ι f g' ≫ ((lift fun b ↦ π f (ε b)) ≫ desc fun b ↦ ι f (ε b)) ≫ π f g = ι f g' ≫ 𝟙 (⨁ f) ≫ π f g
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
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone (pair X Y)
⊢ (BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.left } =
    s.π.app { as := WalkingPair.left }

pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone (pair X Y)
⊢ (BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.right } =
    s.π.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone (pair X Y)
⊢ (BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.left } =
    s.π.app { as := WalkingPair.left }

case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone (pair X Y)
⊢ (BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.right } =
    s.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₁.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ inl ≫ (isoProd X Y).hom ≫ prod.fst = inl ≫ prod.lift fst snd ≫ prod.fst

pp: case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ inr ≫ (isoProd X Y).hom ≫ prod.fst = inr ≫ prod.lift fst snd ≫ prod.fst

pp: case h₂.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ inl ≫ (isoProd X Y).hom ≫ prod.snd = inl ≫ prod.lift fst snd ≫ prod.snd

pp: case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ inr ≫ (isoProd X Y).hom ≫ prod.snd = inr ≫ prod.lift fst snd ≫ prod.snd

Tactic:
<;>

Goal state after:
case h₁.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ inl ≫ (isoProd X Y).hom ≫ prod.fst = inl ≫ prod.lift fst snd ≫ prod.fst

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ inr ≫ (isoProd X Y).hom ≫ prod.fst = inr ≫ prod.lift fst snd ≫ prod.fst

case h₂.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ inl ≫ (isoProd X Y).hom ≫ prod.snd = inl ≫ prod.lift fst snd ≫ prod.snd

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ inr ≫ (isoProd X Y).hom ≫ prod.snd = inr ≫ prod.lift fst snd ≫ prod.snd
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
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone (pair X Y)
⊢ b.toCocone.ι.app { as := WalkingPair.left } ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s) =
    s.ι.app { as := WalkingPair.left }

pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone (pair X Y)
⊢ b.toCocone.ι.app { as := WalkingPair.right } ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s) =
    s.ι.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone (pair X Y)
⊢ b.toCocone.ι.app { as := WalkingPair.left } ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s) =
    s.ι.app { as := WalkingPair.left }

case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone (pair X Y)
⊢ b.toCocone.ι.app { as := WalkingPair.right } ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s) =
    s.ι.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoProd X Y).inv ≫ fst = lift prod.fst prod.snd ≫ fst

pp: case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoProd X Y).inv ≫ snd = lift prod.fst prod.snd ≫ snd

Tactic:
<;>

Goal state after:
case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoProd X Y).inv ≫ fst = lift prod.fst prod.snd ≫ fst

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoProd X Y).inv ≫ snd = lift prod.fst prod.snd ≫ snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₁.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (coprod.inl ≫ (isoCoprod X Y).inv) ≫ fst = (coprod.inl ≫ coprod.desc inl inr) ≫ fst

pp: case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (coprod.inl ≫ (isoCoprod X Y).inv) ≫ snd = (coprod.inl ≫ coprod.desc inl inr) ≫ snd

pp: case h₂.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (coprod.inr ≫ (isoCoprod X Y).inv) ≫ fst = (coprod.inr ≫ coprod.desc inl inr) ≫ fst

pp: case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (coprod.inr ≫ (isoCoprod X Y).inv) ≫ snd = (coprod.inr ≫ coprod.desc inl inr) ≫ snd

Tactic:
<;>

Goal state after:
case h₁.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (coprod.inl ≫ (isoCoprod X Y).inv) ≫ fst = (coprod.inl ≫ coprod.desc inl inr) ≫ fst

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (coprod.inl ≫ (isoCoprod X Y).inv) ≫ snd = (coprod.inl ≫ coprod.desc inl inr) ≫ snd

case h₂.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (coprod.inr ≫ (isoCoprod X Y).inv) ≫ fst = (coprod.inr ≫ coprod.desc inl inr) ≫ fst

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (coprod.inr ≫ (isoCoprod X Y).inv) ≫ snd = (coprod.inr ≫ coprod.desc inl inr) ≫ snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ biprod.inl ≫ (biprod.isoCoprod X Y).hom = biprod.inl ≫ biprod.desc coprod.inl coprod.inr

pp: case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ biprod.inr ≫ (biprod.isoCoprod X Y).hom = biprod.inr ≫ biprod.desc coprod.inl coprod.inr

Tactic:
<;>

Goal state after:
case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ biprod.inl ≫ (biprod.isoCoprod X Y).hom = biprod.inl ≫ biprod.desc coprod.inl coprod.inr

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ biprod.inr ≫ (biprod.isoCoprod X Y).hom = biprod.inr ≫ biprod.desc coprod.inl coprod.inr
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
b : BinaryBicone X Y
i : b.IsBilimit
⊢ (b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.left } =
    𝟙 b.pt ≫ b.toCone.π.app { as := WalkingPair.left }

pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
i : b.IsBilimit
⊢ (b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.right } =
    𝟙 b.pt ≫ b.toCone.π.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
i : b.IsBilimit
⊢ (b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.left } =
    𝟙 b.pt ≫ b.toCone.π.app { as := WalkingPair.left }

case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
i : b.IsBilimit
⊢ (b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.right } =
    𝟙 b.pt ≫ b.toCone.π.app { as := WalkingPair.right }
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 }

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:
<;>

Goal state after:
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 }

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 }
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 }

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:
<;>

Goal state after:
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 }

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 }
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

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:
<;>

Goal state after:
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

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
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 }

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:
<;>

Goal state after:
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 }

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 }
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

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
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
j : Subtype p
k : Subtype pᶜ
⊢ biproduct.ι (Subtype.restrict pᶜ f) k ≫
      (biproduct.fromSubtype f pᶜ ≫ biproduct.toSubtype f p) ≫ biproduct.π (Subtype.restrict p f) j =
    biproduct.ι (Subtype.restrict pᶜ f) k ≫ 0 ≫ biproduct.π (Subtype.restrict p f) j

Tactic:
simp only [Category.assoc, biproduct.ι_fromSubtype_assoc, biproduct.ι_toSubtype_assoc,
          comp_zero, zero_comp]

Goal state after:
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
j : Subtype p
k : Subtype pᶜ
⊢ (if h : p ↑k then biproduct.ι (Subtype.restrict p f) ⟨↑k, h⟩ else 0) ≫ biproduct.π (Subtype.restrict p f) j = 0
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 }

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:
<;>

Goal state after:
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 }

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 }