awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
h :
  IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
    (CategoryTheory.Functor.map Q f)
i : ι
⊢ IsIso (X := K.homology i) (Y := L.homology i) (HomologicalComplex.homologyMap f i)

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

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', Iff.mp, CategoryTheory.NatIso.isIso_map_iff, HomologicalComplex.homologyMap, HomologicalComplexUpToQuasiIso.homologyFunctorFactors, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
h :
  IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
    (CategoryTheory.Functor.map Q f)
i : ι
mp :
  IsIso (X :=
    Functor.obj (Functor.comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) Q (homologyFunctor C c i))
      K)
    (CategoryTheory.Functor.map
      (Functor.comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) Q (homologyFunctor C c i)) f)
⊢ IsIso (X := K.homology i) (Y := L.homology i) (HomologicalComplex.homologyMap f i)

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

Premises used: Iff.mp, CategoryTheory.NatIso.isIso_map_iff, HomologicalComplexUpToQuasiIso.homologyFunctorFactors
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
h :
  IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
    (CategoryTheory.Functor.map Q f)
i : ι
mp :
  IsIso (X :=
    Functor.obj (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (homologyFunctor C c i)
      (Functor.obj Q K))
    (CategoryTheory.Functor.map (homologyFunctor C c i) (CategoryTheory.Functor.map Q f))
⊢ IsIso (X :=
    Functor.obj (Functor.comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) Q (homologyFunctor C c i))
      K)
    (CategoryTheory.Functor.map
      (Functor.comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) Q (homologyFunctor C c i)) f)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
h :
  IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
    (CategoryTheory.Functor.map Q f)
i : ι
⊢ IsIso (X :=
    Functor.obj (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (homologyFunctor C c i)
      (Functor.obj Q K))
    (CategoryTheory.Functor.map (homologyFunctor C c i) (CategoryTheory.Functor.map Q f))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
h : HomologicalComplex.quasiIso C c f
⊢ IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
    (CategoryTheory.Functor.map Q f)

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

Premises used: HomologicalComplexUpToQuasiIso.Q, HomologicalComplex.quasiIso, CategoryTheory.Localization.inverts
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
h : HomologicalComplex.quasiIso C c f
⊢ IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
    (CategoryTheory.Functor.map Q f)

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

Premises used: HomologicalComplexUpToQuasiIso.Q, HomologicalComplex.quasiIso, CategoryTheory.Localization.inverts
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
⊢ MorphismProperty.IsInvertedBy (C := HomologicalComplex.{v_1, u_1, u_2} C c) (D :=
    HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (HomologicalComplex.homotopyEquivalences C c) Q

Tactic:
MorphismProperty.IsInvertedBy.of_le _ _ _
    (Localization.inverts Q (HomologicalComplex.quasiIso C c))
    (homotopyEquivalences_le_quasiIso C c)

Premises used: homotopyEquivalences_le_quasiIso, HomologicalComplexUpToQuasiIso.Q, HomologicalComplex.quasiIso, CategoryTheory.MorphismProperty.IsInvertedBy.of_le, CategoryTheory.Localization.inverts
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
X Y : HomotopyCategory.{v_1, u_1, u_2} C c
f : X ⟶ Y
⊢ quasiIso C c f ↔
    ∀ (n : ι), IsIso (X := Functor.obj (homologyFunctor C c n) X) (CategoryTheory.Functor.map (homologyFunctor C c n) f)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
⊢ ∀ (i : ι),
    IsIso (X := Functor.obj (quotient C c ⋙ homologyFunctor C c i) K)
        (CategoryTheory.Functor.map (quotient C c ⋙ homologyFunctor C c i) f) ↔
      IsIso (X := Functor.obj (HomologicalComplex.homologyFunctor C c i) K)
        (CategoryTheory.Functor.map (HomologicalComplex.homologyFunctor C c i) f)

Tactic:
have eq := fun (i : ι) => NatIso.isIso_map_iff (homologyFunctorFactors C c i) f
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
eq :
  ∀ (i : ι),
    IsIso (X := Functor.obj (homologyFunctor C c i) (Functor.obj (quotient C c) K))
        (CategoryTheory.Functor.map (homologyFunctor C c i) (CategoryTheory.Functor.map (quotient C c) f)) ↔
      IsIso (X := K.homology i) (Y := L.homology i) (HomologicalComplex.homologyMap f i)
⊢ quasiIso C c (X := Functor.obj (quotient C c) K) (CategoryTheory.Functor.map (quotient C c) f) ↔
    HomologicalComplex.quasiIso C c f

Tactic:
simp only [HomologicalComplex.mem_quasiIso_iff, mem_quasiIso_iff, quasiIso_iff,
    quasiIsoAt_iff_isIso_homologyMap, eq]

Premises used: HomologicalComplex.mem_quasiIso_iff, quasiIso_iff, quasiIsoAt_iff_isIso_homologyMap, HomotopyCategory.mem_quasiIso_iff
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
hP : ∀ (f g : Arrow (HomotopyCategory.{v_1, u_1, u_2} C c)) (x : f ≅ g), quasiIso C c f.hom → quasiIso C c g.hom
⊢ MorphismProperty.RespectsIso (C := HomotopyCategory.{v_1, u_1, u_2} C c) (quasiIso C c)

Tactic:
apply MorphismProperty.RespectsIso.of_respects_arrow_iso

Premises used: CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
f g : Arrow (HomotopyCategory.{v_1, u_1, u_2} C c)
e : f ≅ g
hf : quasiIso C c f.hom
i : ι
⊢ IsIso (X := Functor.obj (homologyFunctor C c i) g.left) (CategoryTheory.Functor.map (homologyFunctor C c i) g.hom)

Tactic:
((MorphismProperty.isomorphisms C).arrow_mk_iso_iff
    ((homologyFunctor C c i).mapArrow.mapIso e)).1 (hf i)

Premises used: CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp, HomotopyCategory.homologyFunctor, CategoryTheory.Functor.mapArrow, CategoryTheory.Functor.mapIso
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
f g : Arrow (HomotopyCategory.{v_1, u_1, u_2} C c)
e : f ≅ g
hf : quasiIso C c f.hom
i : ι
⊢ IsIso (X := Functor.obj (homologyFunctor C c i) g.left) (CategoryTheory.Functor.map (homologyFunctor C c i) g.hom)

Tactic:
exact ((MorphismProperty.isomorphisms C).arrow_mk_iso_iff
    ((homologyFunctor C c i).mapArrow.mapIso e)).1 (hf i)

Premises used: CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp, HomotopyCategory.homologyFunctor, CategoryTheory.Functor.mapArrow, CategoryTheory.Functor.mapIso
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : HomotopyCategory.{v_1, u_1, u_2} C c
⊢ ∀ (n : ι),
    IsIso (X := Functor.obj (homologyFunctor C c n) K) (CategoryTheory.Functor.map (homologyFunctor C c n) (𝟙 K))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
X Y Z : HomotopyCategory.{v_1, u_1, u_2} C c
f : X ⟶ Y
g : Y ⟶ Z
hf : quasiIso C c f
hg : quasiIso C c g
⊢ ∀ (n : ι), IsIso (X := Functor.obj (homologyFunctor C c n) X) (CategoryTheory.Functor.map (homologyFunctor C c n) f)

Tactic:
rw [mem_quasiIso_iff] at hf hg ⊢

Premises used: HomotopyCategory.mem_quasiIso_iff
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
X Y Z : HomotopyCategory.{v_1, u_1, u_2} C c
f : X ⟶ Y
g : Y ⟶ Z
hf : quasiIso C c f
hg : quasiIso C c g
hf₁ :
  ∀ (n : ι), IsIso (X := Functor.obj (homologyFunctor C c n) X) (CategoryTheory.Functor.map (homologyFunctor C c n) f)
⊢ ∀ (n : ι), IsIso (X := Functor.obj (homologyFunctor C c n) Y) (CategoryTheory.Functor.map (homologyFunctor C c n) g)

Tactic:
rw [mem_quasiIso_iff] at hf hg ⊢

Premises used: HomotopyCategory.mem_quasiIso_iff
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
X Y Z : HomotopyCategory.{v_1, u_1, u_2} C c
f : X ⟶ Y
g : Y ⟶ Z
hf :
  ∀ (n : ι), IsIso (X := Functor.obj (homologyFunctor C c n) X) (CategoryTheory.Functor.map (homologyFunctor C c n) f)
hg :
  ∀ (n : ι), IsIso (X := Functor.obj (homologyFunctor C c n) Y) (CategoryTheory.Functor.map (homologyFunctor C c n) g)
simp :
  ∀ (n : ι),
    IsIso (X := Functor.obj (homologyFunctor C c n) X)
      (CategoryTheory.Functor.map (homologyFunctor C c n) f ≫ CategoryTheory.Functor.map (homologyFunctor C c n) g)
⊢ ∀ (n : ι),
    IsIso (X := Functor.obj (homologyFunctor C c n) X) (CategoryTheory.Functor.map (homologyFunctor C c n) (f ≫ g))

Tactic:
simp only [Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
X Y Z : HomotopyCategory.{v_1, u_1, u_2} C c
f : X ⟶ Y
g : Y ⟶ Z
hf :
  ∀ (n : ι), IsIso (X := Functor.obj (homologyFunctor C c n) X) (CategoryTheory.Functor.map (homologyFunctor C c n) f)
hg :
  ∀ (n : ι), IsIso (X := Functor.obj (homologyFunctor C c n) Y) (CategoryTheory.Functor.map (homologyFunctor C c n) g)
⊢ ∀ (n : ι),
    IsIso (X := Functor.obj (homologyFunctor C c n) X)
      (CategoryTheory.Functor.map (homologyFunctor C c n) f ≫ CategoryTheory.Functor.map (homologyFunctor C c n) g)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
i : ι
⊢ MorphismProperty.IsInvertedBy (C := HomotopyCategory.{v_1, u_1, u_2} C c) (quasiIso C c) (homologyFunctor C c i)

Tactic:
fun _ _ _ hf => hf i

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
h :
  ∀ (K L : HomologicalComplex.{v_1, u_1, u_2} C c)
    (f :
      Quiver.Hom (V := HomotopyCategory.{v_1, u_1, u_2} C c) (CategoryTheory.Quotient.mk (r := homotopic C c) K)
        (CategoryTheory.Quotient.mk (r := homotopic C c) L)),
    quasiIso C c f ↔ MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) f
⊢ Eq (α := MorphismProperty (HomotopyCategory.{v_1, u_1, u_2} C c)) (quasiIso C c)
    (MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c))

Tactic:
ext ⟨K⟩ ⟨L⟩ f
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f :
  Quiver.Hom (V := HomotopyCategory.{v_1, u_1, u_2} C c) (CategoryTheory.Quotient.mk (r := homotopic C c) K)
    (CategoryTheory.Quotient.mk (r := homotopic C c) L)
h :
  ∀ (f : K ⟶ L),
    quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
        CategoryTheory.Quotient.mk (r := homotopic C c) L)
        (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L) ↔
      MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) (X :=
        CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y := CategoryTheory.Quotient.mk (r := homotopic C c) L)
        (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
⊢ quasiIso C c f ↔ MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) f

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

Premises used: HomotopyCategory.quotient, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
h :
  quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
      CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L) →
    MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) (X :=
      CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y := CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
h₁ :
  MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) (X :=
      CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y := CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L) →
    quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
      CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
⊢ quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
      CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L) ↔
    MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) (X :=
      CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y := CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
hf :
  quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
    CategoryTheory.Quotient.mk (r := homotopic C c) L)
    (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
⊢ HomologicalComplex.quasiIso C c f

Tactic:
rw [quotient_map_mem_quasiIso_iff] at hf

Premises used: HomotopyCategory.quotient_map_mem_quasiIso_iff
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
hf : HomologicalComplex.quasiIso C c f
⊢ MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) (X :=
    CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y := CategoryTheory.Quotient.mk (r := homotopic C c) L)
    (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)

Tactic:
MorphismProperty.map_mem_map _ _ _ hf

Premises used: CategoryTheory.MorphismProperty.map_mem_map
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
hf : HomologicalComplex.quasiIso C c f
⊢ MorphismProperty.map (HomologicalComplex.quasiIso C c) (quotient C c) (X :=
    CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y := CategoryTheory.Quotient.mk (r := homotopic C c) L)
    (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)

Tactic:
exact MorphismProperty.map_mem_map _ _ _ hf

Premises used: CategoryTheory.MorphismProperty.map_mem_map
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
K' L' : HomologicalComplex.{v_1, u_1, u_2} C c
g : K' ⟶ L'
h : HomologicalComplex.quasiIso C c g
e :
  Arrow.mk (X := Functor.obj (quotient C c) K') (CategoryTheory.Functor.map (quotient C c) g) ≅
    Arrow.mk (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
      CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
h₁ :
  ∀ (h : quasiIso C c (X := Functor.obj (quotient C c) K') (CategoryTheory.Functor.map (quotient C c) g))
    (e :
      Arrow.mk (X := Functor.obj (quotient C c) K') (CategoryTheory.Functor.map (quotient C c) g) ≅
        Arrow.mk (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
          CategoryTheory.Quotient.mk (r := homotopic C c) L)
          (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)),
    quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
      CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
⊢ quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
    CategoryTheory.Quotient.mk (r := homotopic C c) L)
    (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)

Tactic:
rw [← quotient_map_mem_quasiIso_iff] at h

Premises used: HomotopyCategory.quotient_map_mem_quasiIso_iff
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
K' L' : HomologicalComplex.{v_1, u_1, u_2} C c
g : K' ⟶ L'
h : quasiIso C c (X := Functor.obj (quotient C c) K') (CategoryTheory.Functor.map (quotient C c) g)
e :
  Arrow.mk (X := Functor.obj (quotient C c) K') (CategoryTheory.Functor.map (quotient C c) g) ≅
    Arrow.mk (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
      CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
⊢ quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
    CategoryTheory.Quotient.mk (r := homotopic C c) L)
    (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)

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

Premises used: HomotopyCategory.quasiIso, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f : K ⟶ L
K' L' : HomologicalComplex.{v_1, u_1, u_2} C c
g : K' ⟶ L'
h : quasiIso C c (X := Functor.obj (quotient C c) K') (CategoryTheory.Functor.map (quotient C c) g)
e :
  Arrow.mk (X := Functor.obj (quotient C c) K') (CategoryTheory.Functor.map (quotient C c) g) ≅
    Arrow.mk (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
      CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)
⊢ quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
    CategoryTheory.Quotient.mk (r := homotopic C c) L)
    (CategoryTheory.Functor.map (quotient C c) f : Functor.obj (quotient C c) K ⟶ Functor.obj (quotient C c) L)

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

Premises used: HomotopyCategory.quasiIso, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp