-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma exact_iff_mono [HasZeroObject C] (hf : S.f = 0) :
    S.Exact ↔ Mono S.g

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
this✝ : S.HasHomology
h : IsZero S.homology
this : IsIso S.pOpcycles
⊢ Mono S.g

Tactic:
have := mono_of_isZero_kernel' _ S.homologyIsKernel h

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
this✝¹ : S.HasHomology
h : IsZero S.homology
this✝ : IsIso S.pOpcycles
this : Mono S.fromOpcycles
⊢ Mono S.g

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
h : S.Exact
⊢ Mono S.g

Tactic:
have := h.hasHomology

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
h : S.Exact
this : S.HasHomology
⊢ Mono S.g

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
⊢ S.Exact ↔ Mono S.g

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
⊢ S.Exact → Mono S.g

case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
⊢ Mono S.g → S.Exact

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
h : S.Exact
this : S.HasHomology
⊢ Mono S.g

Tactic:
simp only [exact_iff_isZero_homology] at h

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
this : S.HasHomology
h : IsZero S.homology
⊢ Mono S.g

Proof state:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
⊢ Mono S.g → S.Exact

Tactic:
intro

Result:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
a✝ : Mono S.g
⊢ S.Exact

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
this : S.HasHomology
h : IsZero S.homology
⊢ Mono S.g

Tactic:
have := S.isIso_pOpcycles hf

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
this✝ : S.HasHomology
h : IsZero S.homology
this : IsIso S.pOpcycles
⊢ Mono S.g

Proof state:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
a✝ : Mono S.g
⊢ S.Exact

Tactic:
rw [(HomologyData.ofIsLimitKernelFork S hf _
  (KernelFork.IsLimit.ofMonoOfIsZero (KernelFork.ofι (0 : 0 ⟶ S.X₂) zero_comp)
    inferInstance (isZero_zero C))).exact_iff]

Result:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
a✝ : Mono S.g
⊢ IsZero
    (HomologyData.ofIsLimitKernelFork S hf (KernelFork.ofι 0 ⋯)
          (KernelFork.IsLimit.ofMonoOfIsZero (KernelFork.ofι 0 ⋯) ⋯ ⋯)).left.H

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
this✝¹ : S.HasHomology
h : IsZero S.homology
this✝ : IsIso S.pOpcycles
this : Mono S.fromOpcycles
⊢ Mono (S.pOpcycles ≫ S.fromOpcycles)

Tactic:
apply mono_comp

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
⊢ S.Exact → Mono S.g

Tactic:
intro h

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
h : S.Exact
⊢ Mono S.g

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
this✝¹ : S.HasHomology
h : IsZero S.homology
this✝ : IsIso S.pOpcycles
this : Mono S.fromOpcycles
⊢ Mono S.g

Tactic:
rw [← S.p_fromOpcycles]

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
this✝¹ : S.HasHomology
h : IsZero S.homology
this✝ : IsIso S.pOpcycles
this : Mono S.fromOpcycles
⊢ Mono (S.pOpcycles ≫ S.fromOpcycles)

Proof state:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
a✝ : Mono S.g
⊢ IsZero
    (HomologyData.ofIsLimitKernelFork S hf (KernelFork.ofι 0 ⋯)
          (KernelFork.IsLimit.ofMonoOfIsZero (KernelFork.ofι 0 ⋯) ⋯ ⋯)).left.H

Tactic:
exact isZero_zero C

Result:
no goals