-- Mathlib/Algebra/Homology/Localization.lean
lemma isIso_Q_map_iff_mem_quasiIso {K L : HomologicalComplex C c} (f : K ⟶ L) :
    IsIso (Q.map f) ↔ HomologicalComplex.quasiIso C c f

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
⊢ IsIso (Q.map f) → HomologicalComplex.quasiIso C c f

Tactic:
intro h

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
⊢ HomologicalComplex.quasiIso C c f

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
i : ι
⊢ QuasiIsoAt f i

Tactic:
rw [quasiIsoAt_iff_isIso_homologyMap]

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
i : ι
⊢ IsIso (HomologicalComplex.homologyMap f i)

Proof state:
case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
⊢ HomologicalComplex.quasiIso C c f → IsIso (Q.map f)

Tactic:
intro h

Result:
case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : HomologicalComplex.quasiIso C c f
⊢ IsIso (Q.map f)

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
i : ι
⊢ IsIso ((homologyFunctor C c i).map (Q.map f))

Tactic:
infer_instance

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
⊢ HomologicalComplex.quasiIso C c f

Tactic:
rw [HomologicalComplex.mem_quasiIso_iff, quasiIso_iff]

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
⊢ ∀ (i : ι), QuasiIsoAt f i

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
i : ι
⊢ IsIso (HomologicalComplex.homologyMap f i)

Tactic:
refine (NatIso.isIso_map_iff (homologyFunctorFactors C c i) f).1 ?_

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
i : ι
⊢ IsIso ((Q ⋙ homologyFunctor C c i).map f)

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
⊢ IsIso (Q.map f) ↔ HomologicalComplex.quasiIso C c f

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
⊢ IsIso (Q.map f) → HomologicalComplex.quasiIso C c f

case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
⊢ HomologicalComplex.quasiIso C c f → IsIso (Q.map f)

Proof state:
case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : HomologicalComplex.quasiIso C c f
⊢ IsIso (Q.map f)

Tactic:
exact Localization.inverts Q (HomologicalComplex.quasiIso C c) _ h

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
i : ι
⊢ IsIso ((Q ⋙ homologyFunctor C c i).map f)

Tactic:
dsimp

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
i : ι
⊢ IsIso ((homologyFunctor C c i).map (Q.map f))

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
⊢ ∀ (i : ι), QuasiIsoAt f i

Tactic:
intro i

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
i : ι
⊢ QuasiIsoAt f i