-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma quasiIsoAt_iff_exactAt' (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i]
    (hL : L.ExactAt i) :
    QuasiIsoAt f i ↔ K.ExactAt i

Proof state:
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hL : IsZero (L.sc i).homology
⊢ IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f)) ↔ IsZero (K.sc i).homology

Tactic:
constructor

Result:
case mp
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hL : IsZero (L.sc i).homology
⊢ IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f)) → IsZero (K.sc i).homology

case mpr
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hL : IsZero (L.sc i).homology
⊢ IsZero (K.sc i).homology → IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f))

Proof state:
case mpr
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hL : IsZero (L.sc i).homology
hK : IsZero (K.sc i).homology
⊢ IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f))

Tactic:
exact ⟨⟨0, IsZero.eq_of_src hK _ _, IsZero.eq_of_tgt hL _ _⟩⟩

Result:
no goals

Proof state:
case mpr
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hL : IsZero (L.sc i).homology
⊢ IsZero (K.sc i).homology → IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f))

Tactic:
intro hK

Result:
case mpr
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hL : IsZero (L.sc i).homology
hK : IsZero (K.sc i).homology
⊢ IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f))

Proof state:
case mp
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hL : IsZero (L.sc i).homology
h : IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f))
⊢ IsZero (K.sc i).homology

Tactic:
exact IsZero.of_iso hL (@asIso _ _ _ _ _ h)

Result:
no goals

Proof state:
case mp
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hL : IsZero (L.sc i).homology
⊢ IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f)) → IsZero (K.sc i).homology

Tactic:
intro h

Result:
case mp
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hL : IsZero (L.sc i).homology
h : IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f))
⊢ IsZero (K.sc i).homology

Proof state:
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hL : L.ExactAt i
⊢ QuasiIsoAt f i ↔ K.ExactAt i

Tactic:
simp only [quasiIsoAt_iff, ShortComplex.quasiIso_iff, exactAt_iff,
  ShortComplex.exact_iff_isZero_homology] at hL ⊢

Result:
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hL : IsZero (L.sc i).homology
⊢ IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f)) ↔ IsZero (K.sc i).homology