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 : 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)
inst_4 : ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} c C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f g : K ⟶ L
h : Homotopy f g
⊢ Eq.{u_3 + 1} (α :=
    Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (Functor.obj Q K) (Functor.obj Q L))
    (CategoryTheory.Functor.map Q f) (CategoryTheory.Functor.map Q g)

Tactic:
(ComplexShape.QFactorsThroughHomotopy.areEqualizedByLocalization h).map_eq Q

Premises used: HomologicalComplexUpToQuasiIso.Q, CategoryTheory.AreEqualizedByLocalization.map_eq, ComplexShape.QFactorsThroughHomotopy.areEqualizedByLocalization
-- 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)
inst_4 : ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} c C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f g : K ⟶ L
this :
  ∀ (h : Homotopy f g),
    Eq.{u_3 + 1} (α :=
      Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (Functor.obj Q K) (Functor.obj Q L))
      (CategoryTheory.Functor.map Q f) (CategoryTheory.Functor.map Q g)
⊢ homotopic C c f g →
    Eq.{u_3 + 1} (α :=
      Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (Functor.obj Q K) (Functor.obj Q L))
      (CategoryTheory.Functor.map Q f) (CategoryTheory.Functor.map Q g)

Tactic:
⟨h⟩
-- 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)
inst_4 : ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} c C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f g : K ⟶ L
h : Homotopy f g
⊢ Eq.{u_3 + 1} (α :=
    Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (Functor.obj Q K) (Functor.obj Q L))
    (CategoryTheory.Functor.map Q f) (CategoryTheory.Functor.map Q g)

Tactic:
Q_map_eq_of_homotopy h

Premises used: HomologicalComplexUpToQuasiIso.Q_map_eq_of_homotopy
-- 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)
inst_4 : ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} c C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
f g : K ⟶ L
h : Homotopy f g
⊢ Eq.{u_3 + 1} (α :=
    Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (Functor.obj Q K) (Functor.obj Q L))
    (CategoryTheory.Functor.map Q f) (CategoryTheory.Functor.map Q g)

Tactic:
exact Q_map_eq_of_homotopy h

Premises used: HomologicalComplexUpToQuasiIso.Q_map_eq_of_homotopy
-- 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)
inst_4 : ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} c C
⊢ Iso (C := HomologicalComplex.{v_1, u_1, u_2} C c ⥤ HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c)
    (HomotopyCategory.quotient C c ⋙ Qh) Q

Tactic:
apply Quotient.lift.isLift

Premises used: CategoryTheory.Quotient.lift.isLift
-- 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)
inst_4 : ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} c C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ :
  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)
obtain :
  ∀ (φ : K ⟶ L),
    HomotopyCategory.quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
        CategoryTheory.Quotient.mk (r := homotopic C c) L)
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ :
          Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L) →
      IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X :=
        Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K)) (Y :=
        Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) L))
        (CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ) :
          Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c)
            (Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K))
            (Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) L)))
⊢ HomotopyCategory.quasiIso C c φ →
    IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X :=
      Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K)) (CategoryTheory.Functor.map Qh φ)

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

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
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
inst_4 : ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} c C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
rw :
  IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
      (CategoryTheory.Functor.map Q φ) →
    IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X :=
      Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K)) (Y :=
      Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) L))
      (CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ) :
        Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c)
          (Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K))
          (Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) L)))
⊢ HomotopyCategory.quasiIso C c (X := CategoryTheory.Quotient.mk (r := homotopic C c) K) (Y :=
      CategoryTheory.Quotient.mk (r := homotopic C c) L)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ :
        Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L) →
    IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X :=
      Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K)) (Y :=
      Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) L))
      (CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ) :
        Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c)
          (Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K))
          (Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) L)))

Tactic:
rw [HomotopyCategory.quotient_map_mem_quasiIso_iff φ,
    ← HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso]

Premises used: HomotopyCategory.quotient_map_mem_quasiIso_iff, HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso
-- 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)
inst_4 : ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} c C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
⊢ IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
      (CategoryTheory.Functor.map Q φ) →
    IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X :=
      Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K)) (Y :=
      Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) L))
      (CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ) :
        Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c)
          (Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K))
          (Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) L)))

Tactic:
(NatIso.isIso_map_iff (quotientCompQhIso C c) φ).2

Premises used: Iff.mpr, HomologicalComplexUpToQuasiIso.quotientCompQhIso, CategoryTheory.NatIso.isIso_map_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
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
inst_4 : ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} c C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
⊢ IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X := Functor.obj Q K)
      (CategoryTheory.Functor.map Q φ) →
    IsIso (C := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (X :=
      Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K)) (Y :=
      Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) L))
      (CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ) :
        Quiver.Hom (V := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c)
          (Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) K))
          (Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C c) L)))

Tactic:
exact (NatIso.isIso_map_iff (quotientCompQhIso C c) φ).2

Premises used: Iff.mpr, HomologicalComplexUpToQuasiIso.quotientCompQhIso, CategoryTheory.NatIso.isIso_map_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
inst_3 :
  MorphismProperty.HasLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomologicalComplex.quasiIso C c)
inst_4 : ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} c C
⊢ Functor.IsLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (D :=
    HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) (HomotopyCategory.quotient C c ⋙ Qh)
    (HomologicalComplex.quasiIso C c)

Tactic:
Functor.IsLocalization.of_iso _ (quotientCompQhIso C c).symm

Premises used: CategoryTheory.Functor.IsLocalization.of_iso, HomologicalComplexUpToQuasiIso.quotientCompQhIso, CategoryTheory.Iso.symm
-- 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)
inst_4 : ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} c C
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) Qh (homologyFunctor C c i))
        (Functor.obj (Quotient.functor (homotopic C c)) K) ⟶
      Functor.obj (HomotopyCategory.homologyFunctor C c i) (Functor.obj (Quotient.functor (homotopic C c)) K))
    (NatTrans.app
      (Iso.hom
        (Iso.symm (Functor.associator (Quotient.functor (homotopic C c)) Qh (homologyFunctor C c i)) ≪≫
          Functor.isoWhiskerRight (quotientCompQhIso C c) (homologyFunctor C c i) ≪≫
            homologyFunctorFactors C c i ≪≫ Iso.symm (HomotopyCategory.homologyFunctorFactors C c i)))
      K)
    (CategoryTheory.Functor.map (homologyFunctor C c i) (NatTrans.app (Iso.hom (quotientCompQhIso C c)) K) ≫
      NatTrans.app (Iso.hom (homologyFunctorFactors C c i)) K ≫
        NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors C c i)) K)

Tactic:
simp
-- 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)
inst_4 : ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} c C
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.homologyFunctor C c i) (Functor.obj (Quotient.functor (homotopic C c)) K) ⟶
      Functor.obj
        (Functor.comp (D := HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) Qh (homologyFunctor C c i))
        (Functor.obj (Quotient.functor (homotopic C c)) K))
    (NatTrans.app
      (Iso.inv
        (Iso.symm (Functor.associator (Quotient.functor (homotopic C c)) Qh (homologyFunctor C c i)) ≪≫
          Functor.isoWhiskerRight (quotientCompQhIso C c) (homologyFunctor C c i) ≪≫
            homologyFunctorFactors C c i ≪≫ Iso.symm (HomotopyCategory.homologyFunctorFactors C c i)))
      K)
    (NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors C c i)) K ≫
      NatTrans.app (Iso.inv (homologyFunctorFactors C c i)) K ≫
        CategoryTheory.Functor.map (homologyFunctor C c i) (NatTrans.app (Iso.inv (quotientCompQhIso C c)) K))

Tactic:
simp
-- 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)
inst_4 : ComplexShape.QFactorsThroughHomotopy.{u_2, v_1, u_1} c C
inst_5 :
  Functor.IsLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C c) (HomotopyCategory.quotient C c)
    (HomologicalComplex.homotopyEquivalences C c)
⊢ Functor.IsLocalization (C := HomotopyCategory.{v_1, u_1, u_2} C c) (D :=
    HomologicalComplexUpToQuasiIso.{v_1, u_1, u_2, u_3} C c) Qh (HomotopyCategory.quasiIso C c)

Tactic:
Functor.IsLocalization.of_comp (HomotopyCategory.quotient C c)
    Qh (HomologicalComplex.homotopyEquivalences C c)
    (HomotopyCategory.quasiIso C c) (HomologicalComplex.quasiIso C c)
    (homotopyEquivalences_le_quasiIso C c)
    (HomotopyCategory.quasiIso_eq_quasiIso_map_quotient C c)

Premises used: homotopyEquivalences_le_quasiIso, HomologicalComplex.homotopyEquivalences, HomologicalComplex.quasiIso, CategoryTheory.Functor.IsLocalization.of_comp, HomotopyCategory.quasiIso_eq_quasiIso_map_quotient, HomotopyCategory.quasiIso, HomologicalComplexUpToQuasiIso.Qh, HomotopyCategory.quotient
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Preadditive.{v_1, u_2} C
inst_2 : HasBinaryBiproducts.{v_1, u_2} C
E : Type u_3
inst_3 : Category.{v_2, u_3} E
F : HomologicalComplex.{v_1, u_2, u_1} C c ⥤ E
hF : MorphismProperty.IsInvertedBy (HomologicalComplex.homotopyEquivalences C c) F
K L : HomologicalComplex.{v_1, u_2, u_1} C c
f g : K ⟶ L
this : ∀ (h : Homotopy f g), F.map f = F.map g
⊢ homotopic C c f g → F.map f = F.map g

Tactic:
⟨h⟩
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Preadditive.{v_1, u_2} C
inst_2 : HasBinaryBiproducts.{v_1, u_2} C
E : Type u_3
inst_3 : Category.{v_2, u_3} E
F : HomologicalComplex.{v_1, u_2, u_1} C c ⥤ E
hF : MorphismProperty.IsInvertedBy (HomologicalComplex.homotopyEquivalences C c) F
K L : HomologicalComplex.{v_1, u_2, u_1} C c
f g : K ⟶ L
h : Homotopy f g
⊢ DecidableRel c.Rel

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Preadditive.{v_1, u_2} C
inst_2 : HasBinaryBiproducts.{v_1, u_2} C
E : Type u_3
inst_3 : Category.{v_2, u_3} E
F : HomologicalComplex.{v_1, u_2, u_1} C c ⥤ E
hF : MorphismProperty.IsInvertedBy (HomologicalComplex.homotopyEquivalences C c) F
K L : HomologicalComplex.{v_1, u_2, u_1} C c
f g : K ⟶ L
h : Homotopy f g
⊢ DecidableRel c.Rel

Tactic:
classical infer_instance
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Preadditive.{v_1, u_2} C
inst_2 : HasBinaryBiproducts.{v_1, u_2} C
E : Type u_3
inst_3 : Category.{v_2, u_3} E
F : HomologicalComplex.{v_1, u_2, u_1} C c ⥤ E
hF : MorphismProperty.IsInvertedBy (HomologicalComplex.homotopyEquivalences C c) F
K L : HomologicalComplex.{v_1, u_2, u_1} C c
f g : K ⟶ L
h : Homotopy f g
have : ∀ (this : DecidableRel c.Rel), F.map f = F.map g
⊢ F.map f = F.map g

Tactic:
have : DecidableRel c.Rel := by classical infer_instance
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Preadditive.{v_1, u_2} C
inst_2 : HasBinaryBiproducts.{v_1, u_2} C
E : Type u_3
inst_3 : Category.{v_2, u_3} E
F : HomologicalComplex.{v_1, u_2, u_1} C c ⥤ E
hF : MorphismProperty.IsInvertedBy (HomologicalComplex.homotopyEquivalences C c) F
K L : HomologicalComplex.{v_1, u_2, u_1} C c
f g : K ⟶ L
h : Homotopy f g
this : DecidableRel c.Rel
⊢ F.map f = F.map g

Tactic:
h.map_eq_of_inverts_homotopyEquivalences hc F hF

Premises used: Homotopy.map_eq_of_inverts_homotopyEquivalences
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Preadditive.{v_1, u_2} C
inst_2 : HasBinaryBiproducts.{v_1, u_2} C
E : Type u_3
inst_3 : Category.{v_2, u_3} E
F : HomologicalComplex.{v_1, u_2, u_1} C c ⥤ E
hF : MorphismProperty.IsInvertedBy (HomologicalComplex.homotopyEquivalences C c) F
K L : HomologicalComplex.{v_1, u_2, u_1} C c
f g : K ⟶ L
h : Homotopy f g
this : DecidableRel c.Rel
⊢ F.map f = F.map g

Tactic:
exact h.map_eq_of_inverts_homotopyEquivalences hc F hF

Premises used: Homotopy.map_eq_of_inverts_homotopyEquivalences
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Preadditive.{v_1, u_2} C
inst_2 : HasBinaryBiproducts.{v_1, u_2} C
h₁ :
  Localization.StrictUniversalPropertyFixedTarget (C := HomologicalComplex.{v_1, u_2, u_1} C c)
    (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c) (HomotopyCategory.{v_1, u_2, u_1} C c)
h₂ :
  Localization.StrictUniversalPropertyFixedTarget (C := HomologicalComplex.{v_1, u_2, u_1} C c)
    (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c)
    (MorphismProperty.Localization (C := HomologicalComplex.{v_1, u_2, u_1} C c)
      (HomologicalComplex.homotopyEquivalences C c))
⊢ Functor.IsLocalization (C := HomologicalComplex.{v_1, u_2, u_1} C c) (HomotopyCategory.quotient C c)
    (HomologicalComplex.homotopyEquivalences C c)

Tactic:
apply Functor.IsLocalization.mk'

Premises used: CategoryTheory.Functor.IsLocalization.mk'
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Preadditive.{v_1, u_2} C
inst_2 : HasBinaryBiproducts.{v_1, u_2} C
⊢ Localization.StrictUniversalPropertyFixedTarget (C := HomologicalComplex.{v_1, u_2, u_1} C c)
    (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c) (HomotopyCategory.{v_1, u_2, u_1} C c)

Tactic:
apply c.strictUniversalPropertyFixedTargetQuotient hc

Premises used: ComplexShape.strictUniversalPropertyFixedTargetQuotient
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Preadditive.{v_1, u_2} C
inst_2 : HasBinaryBiproducts.{v_1, u_2} C
⊢ Localization.StrictUniversalPropertyFixedTarget (C := HomologicalComplex.{v_1, u_2, u_1} C c)
    (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c)
    (MorphismProperty.Localization (C := HomologicalComplex.{v_1, u_2, u_1} C c)
      (HomologicalComplex.homotopyEquivalences C c))

Tactic:
apply c.strictUniversalPropertyFixedTargetQuotient hc

Premises used: ComplexShape.strictUniversalPropertyFixedTargetQuotient
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Preadditive.{v_1, u_2} C
inst_2 : HasBinaryBiproducts.{v_1, u_2} C
inst_3 : CategoryWithHomology.{v_1, u_2} C
K L : HomologicalComplex.{v_1, u_2, u_1} C c
f g : K ⟶ L
h : Homotopy f g
⊢ AreEqualizedByLocalization (HomologicalComplex.quasiIso C c) f g

Tactic:
h.map_eq_of_inverts_homotopyEquivalences hc _
      (MorphismProperty.IsInvertedBy.of_le _ _ _
        (Localization.inverts _ (HomologicalComplex.quasiIso C _))
        (homotopyEquivalences_le_quasiIso C _))

Premises used: homotopyEquivalences_le_quasiIso, HomologicalComplex.quasiIso, CategoryTheory.MorphismProperty.IsInvertedBy.of_le, CategoryTheory.AreEqualizedByLocalization, Homotopy.map_eq_of_inverts_homotopyEquivalences, CategoryTheory.Localization.inverts
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Preadditive.{v_1, u_2} C
inst_2 : HasBinaryBiproducts.{v_1, u_2} C
inst_3 : CategoryWithHomology.{v_1, u_2} C
K L : HomologicalComplex.{v_1, u_2, u_1} C c
f g : K ⟶ L
h : Homotopy f g
⊢ AreEqualizedByLocalization (HomologicalComplex.quasiIso C c) f g

Tactic:
exact h.map_eq_of_inverts_homotopyEquivalences hc _
      (MorphismProperty.IsInvertedBy.of_le _ _ _
        (Localization.inverts _ (HomologicalComplex.quasiIso C _))
        (homotopyEquivalences_le_quasiIso C _))

Premises used: homotopyEquivalences_le_quasiIso, HomologicalComplex.quasiIso, CategoryTheory.MorphismProperty.IsInvertedBy.of_le, Homotopy.map_eq_of_inverts_homotopyEquivalences, CategoryTheory.Localization.inverts
-- Module: Mathlib.Algebra.Homology.Localization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : AddRightCancelSemigroup ι
inst_3 : One ι
inst_4 : HasBinaryBiproducts.{v_1, u_1} C
⊢ Functor.IsLocalization (C := HomologicalComplex.{v_1, u_1, u_2} C (ComplexShape.down ι))
    (HomotopyCategory.quotient C (ComplexShape.down ι))
    (HomologicalComplex.homotopyEquivalences C (ComplexShape.down ι))

Tactic:
(ComplexShape.down ι).quotient_isLocalization (fun _ => ⟨_, rfl⟩) C

Premises used: HAdd.hAdd, Exists.intro, ComplexShape.quotient_isLocalization, ComplexShape.down, OfNat.ofNat, rfl