-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
@[simp]
lemma biprod_isZero_iff (A B : C) [HasBinaryBiproduct A B] :
    IsZero (biprod A B) ↔ IsZero A ∧ IsZero B

Proof state:
case mpr.intro
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
hA : IsZero A
hB : IsZero B
⊢ 𝟙 (A ⊞ B) = 0

Tactic:
apply biprod.hom_ext

Result:
case mpr.intro.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
hA : IsZero A
hB : IsZero B
⊢ 𝟙 (A ⊞ B) ≫ biprod.fst = 0 ≫ biprod.fst

case mpr.intro.h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
hA : IsZero A
hB : IsZero B
⊢ 𝟙 (A ⊞ B) ≫ biprod.snd = 0 ≫ biprod.snd

Proof state:
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
h : 𝟙 (A ⊞ B) = 0
⊢ 𝟙 B = biprod.inr ≫ 𝟙 (A ⊞ B) ≫ biprod.snd

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro.h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
hA : IsZero A
hB : IsZero B
⊢ 𝟙 (A ⊞ B) ≫ biprod.snd = 0 ≫ biprod.snd

Tactic:
apply hB.eq_of_tgt

Result:
no goals

Proof state:
case mpr.intro
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
hA : IsZero A
hB : IsZero B
⊢ IsZero (A ⊞ B)

Tactic:
rw [IsZero.iff_id_eq_zero]

Result:
case mpr.intro
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
hA : IsZero A
hB : IsZero B
⊢ 𝟙 (A ⊞ B) = 0

Proof state:
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
h : 𝟙 (A ⊞ B) = 0
⊢ 𝟙 A = biprod.inl ≫ 𝟙 (A ⊞ B) ≫ biprod.fst

Tactic:
simp

Result:
no goals

Proof state:
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
⊢ IsZero (A ⊞ B) ↔ IsZero A ∧ IsZero B

Tactic:
constructor

Result:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
⊢ IsZero (A ⊞ B) → IsZero A ∧ IsZero B

case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
⊢ IsZero A ∧ IsZero B → IsZero (A ⊞ B)

Proof state:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
h : IsZero (A ⊞ B)
⊢ IsZero A ∧ IsZero B

Tactic:
simp only [IsZero.iff_id_eq_zero] at h ⊢

Result:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
h : 𝟙 (A ⊞ B) = 0
⊢ 𝟙 A = 0 ∧ 𝟙 B = 0

Proof state:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
⊢ IsZero (A ⊞ B) → IsZero A ∧ IsZero B

Tactic:
intro h

Result:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
h : IsZero (A ⊞ B)
⊢ IsZero A ∧ IsZero B

Proof state:
case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
⊢ IsZero A ∧ IsZero B → IsZero (A ⊞ B)

Tactic:
rintro ⟨hA, hB⟩

Result:
case mpr.intro
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
hA : IsZero A
hB : IsZero B
⊢ IsZero (A ⊞ B)

Proof state:
case mpr.intro.h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
hA : IsZero A
hB : IsZero B
⊢ 𝟙 (A ⊞ B) ≫ biprod.fst = 0 ≫ biprod.fst

Tactic:
apply hA.eq_of_tgt

Result:
no goals

Proof state:
case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
h : 𝟙 (A ⊞ B) = 0
⊢ 𝟙 A = 0 ∧ 𝟙 B = 0

Tactic:
simp only [show 𝟙 A = biprod.inl ≫ 𝟙 (A ⊞ B) ≫ biprod.fst by simp,
  show 𝟙 B = biprod.inr ≫ 𝟙 (A ⊞ B) ≫ biprod.snd by simp, h, zero_comp, comp_zero,
  and_self]

Result:
no goals