-- Mathlib/Algebra/Homology/Localization.lean
lemma quasiIso_eq_quasiIso_map_quotient :
    quasiIso C c = (HomologicalComplex.quasiIso C c).map (quotient C c)

Proof state:
case h.mk.mk.intro.mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
⊢ (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f) → quasiIso C c ((quotient C c).map f)

Tactic:
rintro ⟨K', L', g, h, ⟨e⟩⟩

Result:
case h.mk.mk.intro.mpr.intro.intro.intro.intro.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
K' L' : HomologicalComplex C c
g : K' ⟶ L'
h : HomologicalComplex.quasiIso C c g
e : Arrow.mk ((quotient C c).map g) ≅ Arrow.mk ((quotient C c).map f)
⊢ quasiIso C c ((quotient C c).map f)

Proof state:
case h.mk.mk
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : { as := K } ⟶ { as := L }
⊢ quasiIso C c f ↔ (HomologicalComplex.quasiIso C c).map (quotient C c) f

Tactic:
obtain ⟨f, rfl⟩ := (HomotopyCategory.quotient C c).map_surjective f

Result:
case h.mk.mk.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
⊢ quasiIso C c ((quotient C c).map f) ↔ (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
⊢ quasiIso C c = (HomologicalComplex.quasiIso C c).map (quotient C c)

Tactic:
ext ⟨K⟩ ⟨L⟩ f

Result:
case h.mk.mk
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : { as := K } ⟶ { as := L }
⊢ quasiIso C c f ↔ (HomologicalComplex.quasiIso C c).map (quotient C c) f

Proof state:
case h.mk.mk.intro.mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
hf : quasiIso C c ((quotient C c).map f)
⊢ (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f)

Tactic:
rw [quotient_map_mem_quasiIso_iff] at hf

Result:
case h.mk.mk.intro.mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
hf : HomologicalComplex.quasiIso C c f
⊢ (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f)

Proof state:
case h.mk.mk.intro.mpr.intro.intro.intro.intro.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
K' L' : HomologicalComplex C c
g : K' ⟶ L'
h : quasiIso C c ((quotient C c).map g)
e : Arrow.mk ((quotient C c).map g) ≅ Arrow.mk ((quotient C c).map f)
⊢ quasiIso C c ((quotient C c).map f)

Tactic:
exact ((quasiIso C c).arrow_mk_iso_iff e).1 h

Result:
no goals

Proof state:
case h.mk.mk.intro.mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
⊢ quasiIso C c ((quotient C c).map f) → (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f)

Tactic:
intro hf

Result:
case h.mk.mk.intro.mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
hf : quasiIso C c ((quotient C c).map f)
⊢ (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f)

Proof state:
case h.mk.mk.intro.mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
hf : HomologicalComplex.quasiIso C c f
⊢ (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f)

Tactic:
exact MorphismProperty.map_mem_map _ _ _ hf

Result:
no goals

Proof state:
case h.mk.mk.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
⊢ quasiIso C c ((quotient C c).map f) ↔ (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f)

Tactic:
constructor

Result:
case h.mk.mk.intro.mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
⊢ quasiIso C c ((quotient C c).map f) → (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f)

case h.mk.mk.intro.mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
⊢ (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f) → quasiIso C c ((quotient C c).map f)

Proof state:
case h.mk.mk.intro.mpr.intro.intro.intro.intro.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
K' L' : HomologicalComplex C c
g : K' ⟶ L'
h : HomologicalComplex.quasiIso C c g
e : Arrow.mk ((quotient C c).map g) ≅ Arrow.mk ((quotient C c).map f)
⊢ quasiIso C c ((quotient C c).map f)

Tactic:
rw [← quotient_map_mem_quasiIso_iff] at h

Result:
case h.mk.mk.intro.mpr.intro.intro.intro.intro.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
K' L' : HomologicalComplex C c
g : K' ⟶ L'
h : quasiIso C c ((quotient C c).map g)
e : Arrow.mk ((quotient C c).map g) ≅ Arrow.mk ((quotient C c).map f)
⊢ quasiIso C c ((quotient C c).map f)