mathlib-initiative/mathlib-tactics huggingface dataset:
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

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

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 : IsColimit t.toCocone
⊢ BinaryCofan.inl t.toCocone ≫ (t.fst ≫ t.inl + t.snd ≫ t.inr) = BinaryCofan.inl t.toCocone ≫ 𝟙 t.pt

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

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

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

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

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

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

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

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

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

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

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
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 : T ⟶ X
g : T ⟶ Y
⊢ lift f g ≫ fst = (f ≫ inl + g ≫ inr) ≫ fst

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

Tactic:
<;>

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

case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
T : C
f : T ⟶ X
g : T ⟶ Y
⊢ lift f g ≫ snd = (f ≫ inl + g ≫ inr) ≫ snd
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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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
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.π

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

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

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.π
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.π

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

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

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.π
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ (fst.op ≫ (opIso P Q).hom) ≫ fst = inl ≫ fst

pp: case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ (fst.op ≫ (opIso P Q).hom) ≫ snd = inl ≫ snd

Tactic:
<;>

Goal state after:
case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ (fst.op ≫ (opIso P Q).hom) ≫ fst = inl ≫ fst

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ (fst.op ≫ (opIso P Q).hom) ≫ snd = inl ≫ snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ (snd.op ≫ (opIso P Q).hom) ≫ fst = inr ≫ fst

pp: case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ (snd.op ≫ (opIso P Q).hom) ≫ snd = inr ≫ snd

Tactic:
<;>

Goal state after:
case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ (snd.op ≫ (opIso P Q).hom) ≫ fst = inr ≫ fst

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ (snd.op ≫ (opIso P Q).hom) ≫ snd = 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
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ inl ≫ (opIso P Q).inv ≫ inl.op = inl ≫ fst

pp: case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ inr ≫ (opIso P Q).inv ≫ inl.op = inr ≫ fst

Tactic:
<;>

Goal state after:
case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ inl ≫ (opIso P Q).inv ≫ inl.op = inl ≫ fst

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ inr ≫ (opIso P Q).inv ≫ inl.op = inr ≫ fst
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ inl ≫ (opIso P Q).inv ≫ inr.op = inl ≫ snd

pp: case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ inr ≫ (opIso P Q).inv ≫ inr.op = inr ≫ snd

Tactic:
<;>

Goal state after:
case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ inl ≫ (opIso P Q).inv ≫ inr.op = inl ≫ snd

case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ inr ≫ (opIso P Q).inv ≫ inr.op = inr ≫ snd
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
inst✝ : HasBinaryBiproduct X Y
hY : IsZero Y
⊢ (biprod.fst ≫ biprod.inl) ≫ biprod.fst = 𝟙 (X ⊞ Y) ≫ biprod.fst

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
inst✝ : HasBinaryBiproduct X Y
hY : IsZero Y
⊢ (biprod.fst ≫ biprod.inl) ≫ biprod.snd = 𝟙 (X ⊞ Y) ≫ biprod.snd

Tactic:
<;>

Goal state after:
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
inst✝ : HasBinaryBiproduct X Y
hY : IsZero Y
⊢ (biprod.fst ≫ biprod.inl) ≫ biprod.fst = 𝟙 (X ⊞ Y) ≫ biprod.fst

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
inst✝ : HasBinaryBiproduct X Y
hY : IsZero Y
⊢ (biprod.fst ≫ biprod.inl) ≫ biprod.snd = 𝟙 (X ⊞ Y) ≫ biprod.snd
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
inst✝ : HasBinaryBiproduct X Y
hY : IsZero X
⊢ (biprod.snd ≫ biprod.inr) ≫ biprod.fst = 𝟙 (X ⊞ Y) ≫ biprod.fst

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
inst✝ : HasBinaryBiproduct X Y
hY : IsZero X
⊢ (biprod.snd ≫ biprod.inr) ≫ biprod.snd = 𝟙 (X ⊞ Y) ≫ biprod.snd

Tactic:
<;>

Goal state after:
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
inst✝ : HasBinaryBiproduct X Y
hY : IsZero X
⊢ (biprod.snd ≫ biprod.inr) ≫ biprod.fst = 𝟙 (X ⊞ Y) ≫ biprod.fst

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
inst✝ : HasBinaryBiproduct X Y
hY : IsZero X
⊢ (biprod.snd ≫ biprod.inr) ≫ biprod.snd = 𝟙 (X ⊞ Y) ≫ biprod.snd
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
q₁ q₂ : (j : Fin (n + 1)) → α j
hx : ¬x ∈ Icc (q₁ i) (q₂ i)
p : (j : Fin n) → α (i.succAbove j)
⊢ p ∈ i.insertNth x ⁻¹' Icc q₁ q₂ ↔ p ∈ ∅

Tactic:
simp only [mem_preimage, insertNth_mem_Icc, hx, false_and, mem_empty_iff_false]

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_4.x
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
b : Fin (n + 1)
hab : q < b
⊢ q.insertNth x f q < q.insertNth x f b

pp: case refine_4.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
b : Fin (n + 1)
j✝ : Fin n
hab : q.succAbove j✝ < b
⊢ q.insertNth x f (q.succAbove j✝) < q.insertNth x f b

Tactic:
<;>

Goal state after:
case refine_4.x
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
b : Fin (n + 1)
hab : q < b
⊢ q.insertNth x f q < q.insertNth x f b

case refine_4.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
b : Fin (n + 1)
j✝ : Fin n
hab : q.succAbove j✝ < b
⊢ q.insertNth x f (q.succAbove j✝) < q.insertNth x f b
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
f : Fin (n + 1) → α
a : α
⊢ Monotone (vecCons a f) ↔ a ≤ f 0 ∧ Monotone f

Tactic:
by
  simpa only [monotone_iff_forall_lt] using! @liftFun_vecCons α n (· ≤ ·) _ f a

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

Goal state before:
pp: case e'_4
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
h₂ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
⊢ preadditiveHasZeroMorphisms = preadditiveHasZeroMorphisms

pp: case e'_6
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
h₂ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
e_4✝ : (X ⊞ X) = (X ⊞ X)
⊢ preadditiveHasZeroMorphisms = preadditiveHasZeroMorphisms

pp: case e'_7
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
h₂ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
e_4✝ : (X ⊞ X) = (X ⊞ X)
⊢ preadditiveHasZeroMorphisms = preadditiveHasZeroMorphisms

Tactic:
<;>

Goal state after:
case e'_4
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
h₂ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
⊢ preadditiveHasZeroMorphisms = preadditiveHasZeroMorphisms

case e'_6
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
h₂ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
e_4✝ : (X ⊞ X) = (X ⊞ X)
⊢ preadditiveHasZeroMorphisms = preadditiveHasZeroMorphisms

case e'_7
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
h₂ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
e_4✝ : (X ⊞ X) = (X ⊞ X)
⊢ preadditiveHasZeroMorphisms = preadditiveHasZeroMorphisms