-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
/-- Given a morphism of short complexes `φ : S₁ ⟶ S₂` in an abelian category, if `S₁.f`
and `S₁.g` are zero (e.g. when `S₁` is of the form `0 ⟶ S₁.X₂ ⟶ 0`) and `S₂.f = 0`
(e.g when `S₂` is of the form `0 ⟶ S₂.X₂ ⟶ S₂.X₃`), then `φ` is a quasi-isomorphism iff
the obvious short complex `S₁.X₂ ⟶ S₂.X₂ ⟶ S₂.X₃` is exact and `φ.τ₂` is a mono). -/
lemma quasiIso_iff_of_zeros {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂)
    (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) :
    QuasiIso φ ↔
      (ShortComplex.mk φ.τ₂ S₂.g (by rw [φ.comm₂₃, hg₁, zero_comp])).Exact ∧ Mono φ.τ₂

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
⊢ (mk φ.τ₂ S₂.g ⋯).Exact

Tactic:
apply exact_of_f_is_kernel

Result:
case mp.hS
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
⊢ IsLimit (KernelFork.ofι (mk φ.τ₂ S₂.g ⋯).f ⋯)

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
⊢ (mk φ.τ₂ S₂.g ⋯).Exact ∧ Mono φ.τ₂

Tactic:
have : Mono φ.τ₂ := by
  rw [← S₂.liftCycles_i φ.τ₂ w]
  apply mono_comp

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
⊢ (mk φ.τ₂ S₂.g ⋯).Exact ∧ Mono φ.τ₂

Proof state:
case mp.hS
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
⊢ IsLimit (KernelFork.ofι (mk φ.τ₂ S₂.g ⋯).f ⋯)

Tactic:
exact IsLimit.ofIsoLimit S₂.cyclesIsKernel
  (Fork.ext (asIso (S₂.liftCycles φ.τ₂ w)).symm (by simp))

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ QuasiIso φ ↔ (mk φ.τ₂ S₂.g ⋯).Exact ∧ Mono φ.τ₂

Tactic:
have w : φ.τ₂ ≫ S₂.g = 0 := by rw [φ.comm₂₃, hg₁, zero_comp]

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
⊢ QuasiIso φ ↔ (mk φ.τ₂ S₂.g ⋯).Exact ∧ Mono φ.τ₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
⊢ QuasiIso φ ↔ (mk φ.τ₂ S₂.g ⋯).Exact ∧ Mono φ.τ₂

Tactic:
rw [quasiIso_iff_isIso_liftCycles φ hf₁ hg₁ hf₂]

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
⊢ IsIso (S₂.liftCycles φ.τ₂ ⋯) ↔ (mk φ.τ₂ S₂.g ⋯).Exact ∧ Mono φ.τ₂

Proof state:
case mpr.intro.refine_1
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : (mk φ.τ₂ S₂.g ⋯).Exact
h₂ : Mono φ.τ₂
⊢ S₂.liftCycles φ.τ₂ ⋯ ≫ h₁.lift S₂.iCycles ⋯ = 𝟙 S₁.X₂

Tactic:
rw [← cancel_mono φ.τ₂, assoc, h₁.lift_f, liftCycles_i, id_comp]

Result:
no goals

Proof state:
case mpr.intro
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : (mk φ.τ₂ S₂.g ⋯).Exact
h₂ : Mono φ.τ₂
⊢ IsIso (S₂.liftCycles φ.τ₂ ⋯)

Tactic:
refine ⟨⟨h₁.lift S₂.iCycles (by simp), ?_, ?_⟩⟩

Result:
case mpr.intro.refine_1
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : (mk φ.τ₂ S₂.g ⋯).Exact
h₂ : Mono φ.τ₂
⊢ S₂.liftCycles φ.τ₂ ⋯ ≫ h₁.lift S₂.iCycles ⋯ = 𝟙 S₁.X₂

case mpr.intro.refine_2
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : (mk φ.τ₂ S₂.g ⋯).Exact
h₂ : Mono φ.τ₂
⊢ h₁.lift S₂.iCycles ⋯ ≫ S₂.liftCycles φ.τ₂ ⋯ = 𝟙 S₂.cycles

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ φ.τ₂ ≫ S₂.g = 0

Tactic:
rw [φ.comm₂₃, hg₁, zero_comp]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.160614, u_1} C
inst✝¹ : Category.{?u.160618, u_2} D
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ φ.τ₂ ≫ S₂.g = 0

Tactic:
rw [φ.comm₂₃, hg₁, zero_comp]

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
⊢ IsIso (S₂.liftCycles φ.τ₂ ⋯) → (mk φ.τ₂ S₂.g ⋯).Exact ∧ Mono φ.τ₂

Tactic:
intro h

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
⊢ (mk φ.τ₂ S₂.g ⋯).Exact ∧ Mono φ.τ₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
⊢ Mono (S₂.liftCycles φ.τ₂ w ≫ S₂.iCycles)

Tactic:
apply mono_comp

Result:
no goals

Proof state:
case mpr.intro.refine_2
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : (mk φ.τ₂ S₂.g ⋯).Exact
h₂ : Mono φ.τ₂
⊢ h₁.lift S₂.iCycles ⋯ ≫ S₂.liftCycles φ.τ₂ ⋯ = 𝟙 S₂.cycles

Tactic:
rw [← cancel_mono S₂.iCycles, assoc, liftCycles_i, h₁.lift_f, id_comp]

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
⊢ (mk φ.τ₂ S₂.g ⋯).Exact ∧ Mono φ.τ₂ → IsIso (S₂.liftCycles φ.τ₂ ⋯)

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case mpr.intro
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : (mk φ.τ₂ S₂.g ⋯).Exact
h₂ : Mono φ.τ₂
⊢ IsIso (S₂.liftCycles φ.τ₂ ⋯)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
⊢ IsIso (S₂.liftCycles φ.τ₂ ⋯) ↔ (mk φ.τ₂ S₂.g ⋯).Exact ∧ Mono φ.τ₂

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
⊢ IsIso (S₂.liftCycles φ.τ₂ ⋯) → (mk φ.τ₂ S₂.g ⋯).Exact ∧ Mono φ.τ₂

case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
⊢ (mk φ.τ₂ S₂.g ⋯).Exact ∧ Mono φ.τ₂ → IsIso (S₂.liftCycles φ.τ₂ ⋯)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
⊢ (asIso (S₂.liftCycles φ.τ₂ w)).symm.hom ≫ Fork.ι (KernelFork.ofι (mk φ.τ₂ S₂.g ⋯).f ⋯) =
    Fork.ι (KernelFork.ofι S₂.iCycles ⋯)

Tactic:
simp

Result:
no goals