awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
s :
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X' ⟶
    CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X
hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) s
g :
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X' ⟶
    CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y
hφ :
  f =
    (MorphismProperty.RightFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) s hs g).map (W :=
      HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯
obtain :
  ∀ (s : X' ⟶ X)
    (hs :
      HomotopyCategory.quasiIso C (ComplexShape.up ℤ) (X :=
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X')
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s))
    (hφ :
      f =
        (MorphismProperty.RightFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
              (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s) hs g).map
          (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯),
    ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (s : X' ⟶ X) (x :
      IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)) (g : X' ⟶ Y),
      f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g
⊢ ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (s : X' ⟶ X) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)) (g : X' ⟶ Y),
    f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g

Tactic:
obtain ⟨s, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective s

Premises used: HomotopyCategory.quotient, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
g :
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X' ⟶
    CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y
s : X' ⟶ X
hs :
  HomotopyCategory.quasiIso C (ComplexShape.up ℤ) (X :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X')
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s)
hφ :
  f =
    (MorphismProperty.RightFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s) hs g).map
      (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯
obtain :
  ∀ (g : X' ⟶ Y)
    (hφ :
      f =
        (MorphismProperty.RightFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
              (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s) hs
              (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) g)).map
          (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯),
    ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (s : X' ⟶ X) (x :
      IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)) (g : X' ⟶ Y),
      f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g
⊢ ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (s : X' ⟶ X) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)) (g : X' ⟶ Y),
    f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g

Tactic:
obtain ⟨g, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective g

Premises used: HomotopyCategory.quotient, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
s : X' ⟶ X
hs :
  HomotopyCategory.quasiIso C (ComplexShape.up ℤ) (X :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X')
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s)
g : X' ⟶ Y
hφ :
  f =
    (MorphismProperty.RightFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s) hs
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) g)).map
      (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯
rw :
  ∀
    (hs_1 :
      IsIso (C := DerivedCategory.{w, v, u} C) (X :=
        Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X'))
        (CategoryTheory.Functor.map Qh
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s)))
    (g : X' ⟶ Y)
    (hφ :
      f =
        (MorphismProperty.RightFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
              (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s) hs
              (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) g)).map
          (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯),
    ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (s : X' ⟶ X) (x :
      IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)) (g : X' ⟶ Y),
      f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g
⊢ ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (s : X' ⟶ X) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)) (g : X' ⟶ Y),
    f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g

Tactic:
rw [← isIso_Qh_map_iff] at hs

Premises used: DerivedCategory.isIso_Qh_map_iff
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
s : X' ⟶ X
hs_1 :
  HomotopyCategory.quasiIso C (ComplexShape.up ℤ) (X :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X')
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s)
hs :
  IsIso (C := DerivedCategory.{w, v, u} C) (X :=
    Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X'))
    (CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s))
g : X' ⟶ Y
hφ :
  f =
    (MorphismProperty.RightFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s) hs_1
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) g)).map
      (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯
⊢ ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (s : X' ⟶ X) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)) (g : X' ⟶ Y),
    f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g

Tactic:
⟨X', s, hs, g, hφ⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
s : X' ⟶ X
hs_1 :
  HomotopyCategory.quasiIso C (ComplexShape.up ℤ) (X :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X')
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s)
hs :
  IsIso (C := DerivedCategory.{w, v, u} C) (X :=
    Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X'))
    (CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s))
g : X' ⟶ Y
hφ :
  f =
    (MorphismProperty.RightFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s) hs_1
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) g)).map
      (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯
⊢ ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (s : X' ⟶ X) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)) (g : X' ⟶ Y),
    f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g

Tactic:
exact ⟨X', s, hs, g, hφ⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
have :
  ∀
    (φ :
      MorphismProperty.LeftFraction (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
        (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)
        (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y))
    (hφ : f = φ.map (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯),
    ∃ (Y' : CochainComplex.{v, u, 0} C ℤ) (g : X ⟶ Y') (s : Y ⟶ Y') (x :
      IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)),
      f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)
⊢ ∃ (Y' : CochainComplex.{v, u, 0} C ℤ) (g : X ⟶ Y') (s : Y ⟶ Y') (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)),
    f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)

Tactic:
have ⟨φ, hφ⟩ := Localization.exists_leftFraction Qh (HomotopyCategory.quasiIso C _) f
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
φ :
  MorphismProperty.LeftFraction (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
    (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)
    (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)
hφ : f = φ.map (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯
obtain :
  ∀ (X' : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (g : CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X ⟶ X')
    (s : CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y ⟶ X')
    (hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) s)
    (hφ :
      f =
        (MorphismProperty.LeftFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) g s hs).map (W :=
          HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯),
    ∃ (Y' : CochainComplex.{v, u, 0} C ℤ) (g : X ⟶ Y') (s : Y ⟶ Y') (x :
      IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)),
      f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)
⊢ ∃ (Y' : CochainComplex.{v, u, 0} C ℤ) (g : X ⟶ Y') (s : Y ⟶ Y') (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)),
    f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)

Tactic:
obtain ⟨X', g, s, hs, rfl⟩ := φ.cases

Premises used: CategoryTheory.MorphismProperty.LeftFraction.cases, rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
g : CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X ⟶ X'
s : CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y ⟶ X'
hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) s
hφ :
  f =
    (MorphismProperty.LeftFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) g s hs).map (W :=
      HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯
obtain :
  ∀ (X' : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
    (g :
      CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X')
    (s :
      CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X')
    (hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) s)
    (hφ :
      f =
        (MorphismProperty.LeftFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) g s hs).map (W :=
          HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯),
    ∃ (Y' : CochainComplex.{v, u, 0} C ℤ) (g : X ⟶ Y') (s : Y ⟶ Y') (x :
      IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)),
      f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)
⊢ ∃ (Y' : CochainComplex.{v, u, 0} C ℤ) (g : X ⟶ Y') (s : Y ⟶ Y') (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)),
    f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)

Tactic:
obtain ⟨X', rfl⟩ := HomotopyCategory.quotient_obj_surjective X'

Premises used: HomotopyCategory.quotient_obj_surjective, rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
g :
  CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X'
s :
  CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X'
hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) s
hφ :
  f =
    (MorphismProperty.LeftFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) g s hs).map (W :=
      HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯
obtain :
  ∀ (s : Y ⟶ X')
    (hs :
      HomotopyCategory.quasiIso C (ComplexShape.up ℤ) (X :=
        CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y) (Y :=
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X')
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s))
    (hφ :
      f =
        (MorphismProperty.LeftFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) g
              (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s) hs).map
          (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯),
    ∃ (Y' : CochainComplex.{v, u, 0} C ℤ) (g : X ⟶ Y') (s : Y ⟶ Y') (x :
      IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)),
      f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)
⊢ ∃ (Y' : CochainComplex.{v, u, 0} C ℤ) (g : X ⟶ Y') (s : Y ⟶ Y') (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)),
    f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)

Tactic:
obtain ⟨s, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective s

Premises used: HomotopyCategory.quotient, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
g :
  CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X'
s : Y ⟶ X'
hs :
  HomotopyCategory.quasiIso C (ComplexShape.up ℤ) (X :=
    CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y) (Y :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X')
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s)
hφ :
  f =
    (MorphismProperty.LeftFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) g
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s) hs).map
      (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯
obtain :
  ∀ (g : X ⟶ X')
    (hφ :
      f =
        (MorphismProperty.LeftFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
              (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) g)
              (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s) hs).map
          (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯),
    ∃ (Y' : CochainComplex.{v, u, 0} C ℤ) (g : X ⟶ Y') (s : Y ⟶ Y') (x :
      IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)),
      f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)
⊢ ∃ (Y' : CochainComplex.{v, u, 0} C ℤ) (g : X ⟶ Y') (s : Y ⟶ Y') (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)),
    f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)

Tactic:
obtain ⟨g, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective g

Premises used: HomotopyCategory.quotient, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
s : Y ⟶ X'
hs :
  HomotopyCategory.quasiIso C (ComplexShape.up ℤ) (X :=
    CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y) (Y :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X')
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s)
g : X ⟶ X'
hφ :
  f =
    (MorphismProperty.LeftFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) g)
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s) hs).map
      (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯
rw :
  ∀
    (hs_1 :
      IsIso (C := DerivedCategory.{w, v, u} C) (X :=
        Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)) (Y :=
        Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X'))
        (CategoryTheory.Functor.map Qh
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s)))
    (g : X ⟶ X')
    (hφ :
      f =
        (MorphismProperty.LeftFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
              (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) g)
              (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s) hs).map
          (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯),
    ∃ (Y' : CochainComplex.{v, u, 0} C ℤ) (g : X ⟶ Y') (s : Y ⟶ Y') (x :
      IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)),
      f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)
⊢ ∃ (Y' : CochainComplex.{v, u, 0} C ℤ) (g : X ⟶ Y') (s : Y ⟶ Y') (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)),
    f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)

Tactic:
rw [← isIso_Qh_map_iff] at hs

Premises used: DerivedCategory.isIso_Qh_map_iff
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
s : Y ⟶ X'
hs_1 :
  HomotopyCategory.quasiIso C (ComplexShape.up ℤ) (X :=
    CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y) (Y :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X')
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s)
hs :
  IsIso (C := DerivedCategory.{w, v, u} C) (X :=
    Functor.obj Qh (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)) (Y :=
    Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) X'))
    (CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s))
g : X ⟶ X'
hφ :
  f =
    (MorphismProperty.LeftFraction.mk (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) g)
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) s) hs_1).map
      (W := HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) Qh ⋯
⊢ ∃ (Y' : CochainComplex.{v, u, 0} C ℤ) (g : X ⟶ Y') (s : Y ⟶ Y') (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)),
    f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)

Tactic:
⟨X', g, s, hs, hφ⟩

Premises used: Exists.intro