awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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.RightFraction (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 ⋯
⊢ ∃ (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
have obtain : ∀ (X' : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
  (s : X' ⟶ CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)
  (hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) s)
  (g : 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 sorry),
  ∃ (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 ⟨X', s, hs, g, rfl⟩ := φ.cases
Cleared hypotheses: φ, hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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 ℤ)
s : X' ⟶ CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X
hs : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) s
g : 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 ⋯
⊢ ∃ (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
have obtain : ∀ (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 sorry),
  ∃ (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 ⟨X', rfl⟩ := HomotopyCategory.quotient_obj_surjective X'
Cleared hypotheses: X', s, hs, g, hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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 ⋯
⊢ ∃ (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
have 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 sorry),
  ∃ (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
Cleared hypotheses: s, hs, hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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 ⋯
⊢ ∃ (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
have 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 sorry),
  ∃ (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
Cleared hypotheses: g, hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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 ⋯
⊢ ∃ (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
have 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 sorry),
  ∃ (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
Cleared hypotheses: g, hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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)
⊢ ∃ (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)
have 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 sorry),
  ∃ (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
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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 ⋯
⊢ ∃ (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)
have 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 sorry),
  ∃ (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
Cleared hypotheses: φ, hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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 ⋯
⊢ ∃ (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)
have 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 sorry),
  ∃ (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'
Cleared hypotheses: X', g, s, hs, hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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 ⋯
⊢ ∃ (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)
have 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 sorry),
  ∃ (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
Cleared hypotheses: s, hs, hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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 ⋯
⊢ ∃ (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)
have 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 sorry),
  ∃ (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
Cleared hypotheses: g, hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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 ⋯
⊢ ∃ (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)
have 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 sorry),
  ∃ (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
Cleared hypotheses: g, hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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)
n : ℤ
inst_3 : X.IsStrictlyLE n
⊢ ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (_ : X'.IsStrictlyLE n) (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
have obtain : ∀ (X' : CochainComplex.{v, u, 0} C ℤ) (s : X' ⟶ X)
  (hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)) (g : X' ⟶ Y),
  ∃ (X'_1 : CochainComplex.{v, u, 0} C ℤ) (_ : X'_1.IsStrictlyLE n) (s_1 : X'_1 ⟶ X) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X'_1) (CategoryTheory.Functor.map Q s_1)) (g_1 :
    X'_1 ⟶ Y),
    Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))
      (inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g)
      (inv (CategoryTheory.Functor.map Q s_1) ≫ CategoryTheory.Functor.map Q g_1)
Tactic: obtain ⟨X', s, hs, g, rfl⟩ := right_fac f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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 ℤ
n : ℤ
inst_3 : X.IsStrictlyLE n
X' : CochainComplex.{v, u, 0} C ℤ
s : X' ⟶ X
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncLE n)) (Y := Functor.obj Q (X.truncLE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s n))
have rw : ∀ i ≤ n, QuasiIsoAt s i
Tactic: rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncLEMap_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
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 ℤ
n : ℤ
inst_3 : X.IsStrictlyLE n
X' : CochainComplex.{v, u, 0} C ℤ
s : X' ⟶ X
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
⊢ ∀ i ≤ n, QuasiIsoAt s i
have rw : ∀ (hs : QuasiIso s) (g : X' ⟶ Y), ∀ i ≤ n, QuasiIsoAt s i
Tactic: rw [isIso_Q_map_iff_quasiIso] at hs
Cleared hypotheses: hs, g