-- Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean
lemma ShortExact.isIso_g_iff  {S : ShortComplex C} (hS : S.ShortExact) [Balanced C] :
    IsIso S.g ↔ IsZero S.X₁

Proof state:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝² : HasZeroObject C
this✝¹ : Mono S.f
this✝ : Epi S.g
hX₁ : IsZero S.X₁
this : Mono S.g
⊢ IsIso S.g

Tactic:
apply isIso_of_mono_of_epi

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
⊢ IsIso S.g ↔ IsZero S.X₁

Tactic:
have := hS.exact.hasZeroObject

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this : HasZeroObject C
⊢ IsIso S.g ↔ IsZero S.X₁

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
⊢ IsIso S.g → IsZero S.X₁

Tactic:
intro hf

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
hf : IsIso S.g
⊢ IsZero S.X₁

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
hf : IsIso S.g
⊢ IsZero S.X₁

Tactic:
simp only [IsZero.iff_id_eq_zero, ← cancel_mono S.f, ← cancel_mono S.g,
  S.zero, zero_comp, assoc, comp_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this : HasZeroObject C
⊢ IsIso S.g ↔ IsZero S.X₁

Tactic:
have := hS.mono_f

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝ : HasZeroObject C
this : Mono S.f
⊢ IsIso S.g ↔ IsZero S.X₁

Proof state:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
hX₁ : IsZero S.X₁
⊢ IsIso S.g

Tactic:
have : Mono S.g := (S.exact_iff_mono (hX₁.eq_of_src _ _)).1 hS.exact

Result:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝² : HasZeroObject C
this✝¹ : Mono S.f
this✝ : Epi S.g
hX₁ : IsZero S.X₁
this : Mono S.g
⊢ IsIso S.g

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝ : HasZeroObject C
this : Mono S.f
⊢ IsIso S.g ↔ IsZero S.X₁

Tactic:
have := hS.epi_g

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
⊢ IsIso S.g ↔ IsZero S.X₁

Proof state:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
⊢ IsZero S.X₁ → IsIso S.g

Tactic:
intro hX₁

Result:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
hX₁ : IsZero S.X₁
⊢ IsIso S.g

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
⊢ IsIso S.g ↔ IsZero S.X₁

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
⊢ IsIso S.g → IsZero S.X₁

case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
⊢ IsZero S.X₁ → IsIso S.g