-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem Biprod.column_nonzero_of_iso {W X Y Z : C} (f : W ⊞ X ⟶ Y ⊞ Z) [IsIso f] :
    𝟙 W = 0 ∨ biprod.inl ≫ f ≫ biprod.fst ≠ 0 ∨ biprod.inl ≫ f ≫ biprod.snd ≠ 0

Proof state:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ False

Tactic:
have h₀ : x = 0 := by
  dsimp [x]
  rw [← Category.id_comp (inv f), Category.assoc, ← biprod.total]
  conv_lhs =>
    slice 2 3
    rw [comp_add]
  simp only [Category.assoc]
  rw [comp_add_assoc, add_comp]
  conv_lhs =>
    congr
    next => skip
    slice 1 3
    rw [a₂]
  simp only [zero_comp, add_zero]
  conv_lhs =>
    slice 1 3
    rw [a₁]
  simp only [zero_comp]

Result:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
h₀ : x = 0
⊢ False

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
⊢ x = 𝟙 W

Tactic:
simp [x]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ biprod.inl ≫ f ≫ (biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst = 0

Tactic:
conv_lhs =>
  slice 2 3
  rw [comp_add]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ biprod.inl ≫ ((f ≫ biprod.fst ≫ biprod.inl + f ≫ biprod.snd ≫ biprod.inr) ≫ inv f) ≫ biprod.fst = 0

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst + ((0 ≫ biprod.inr) ≫ inv f) ≫ biprod.fst = 0

Tactic:
simp only [zero_comp, add_zero]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst = 0

Proof state:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
h₀ : x = 0
⊢ False

Tactic:
exact nz (h₁.symm.trans h₀)

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ ((0 ≫ biprod.inl) ≫ inv f) ≫ biprod.fst = 0

Tactic:
simp only [zero_comp]

Result:
no goals