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 ℤ
n : ℤ
inst_3 : Y.IsStrictlyGE n
Y' : CochainComplex.{v, u, 0} C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncGE n)) (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n))
eq :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q Y) (Functor.obj Q (Y'.truncGE n)))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))
    (CategoryTheory.Functor.map Q (s ≫ Y'.πTruncGE n))
eq' :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q (Y'.truncGE n)))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := X.truncGE n) (X.πTruncGE n) (CochainComplex.truncGEMap g n)))
    (CategoryTheory.Functor.map Q (g ≫ Y'.πTruncGE n))
⊢ Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q Y) (Functor.obj Q (Y'.truncGE n)))
    (CategoryStruct.comp (Y := Functor.obj Q (Y.truncGE n)) (CategoryTheory.Functor.map Q (Y.πTruncGE n))
      (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n)))
    (CategoryTheory.Functor.map Q s ≫ CategoryTheory.Functor.map Q (Y'.πTruncGE n))

Tactic:
simp only [Functor.map_comp] at eq eq'

Premises used: CategoryTheory.Functor.map_comp
-- 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 ℤ
n : ℤ
inst_3 : Y.IsStrictlyGE n
Y' : CochainComplex.{v, u, 0} C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncGE n)) (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n))
eq :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q Y) (Functor.obj Q (Y'.truncGE n)))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))
    (CategoryTheory.Functor.map Q (s ≫ Y'.πTruncGE n))
eq' :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q (Y'.truncGE n)))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := X.truncGE n) (X.πTruncGE n) (CochainComplex.truncGEMap g n)))
    (CategoryTheory.Functor.map Q (g ≫ Y'.πTruncGE n))
eq₁ :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q Y) (Functor.obj Q (Y'.truncGE n)))
    (CategoryStruct.comp (Y := Functor.obj Q (Y.truncGE n)) (CategoryTheory.Functor.map Q (Y.πTruncGE n))
      (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n)))
    (CategoryTheory.Functor.map Q s ≫ CategoryTheory.Functor.map Q (Y'.πTruncGE n))
⊢ Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q (Y'.truncGE n)))
    (CategoryStruct.comp (Y := Functor.obj Q (X.truncGE n)) (CategoryTheory.Functor.map Q (X.πTruncGE n))
      (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap g n)))
    (CategoryTheory.Functor.map Q g ≫ CategoryTheory.Functor.map Q (Y'.πTruncGE n))

Tactic:
simp only [Functor.map_comp] at eq eq'

Premises used: CategoryTheory.Functor.map_comp
-- 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 ℤ
n : ℤ
inst_3 : Y.IsStrictlyGE n
Y' : CochainComplex.{v, u, 0} C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncGE n)) (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n))
eq :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q Y) (Functor.obj Q (Y'.truncGE n)))
    (CategoryStruct.comp (Y := Functor.obj Q (Y.truncGE n)) (CategoryTheory.Functor.map Q (Y.πTruncGE n))
      (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n)))
    (CategoryTheory.Functor.map Q s ≫ CategoryTheory.Functor.map Q (Y'.πTruncGE n))
eq' :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q (Y'.truncGE n)))
    (CategoryStruct.comp (Y := Functor.obj Q (X.truncGE n)) (CategoryTheory.Functor.map Q (X.πTruncGE n))
      (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap g n)))
    (CategoryTheory.Functor.map Q g ≫ CategoryTheory.Functor.map Q (Y'.πTruncGE n))
refine_2 :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q (Y'.truncGE n)))
    (CategoryTheory.Functor.map Q g ≫
      inv (CategoryTheory.Functor.map Q s) ≫
        CategoryStruct.comp (Y := Functor.obj Q (Y.truncGE n)) (CategoryTheory.Functor.map Q (Y.πTruncGE n))
          (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n)))
    (CategoryStruct.comp (Y := Functor.obj Q (X.truncGE n)) (CategoryTheory.Functor.map Q (X.πTruncGE n))
      (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap g n)))
⊢ Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))
    (CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s))
    (CategoryStruct.comp (Y := Functor.obj Q (Y'.truncGE n))
      (CategoryTheory.Functor.map Q
        (CategoryStruct.comp (Y := X.truncGE n) (X.πTruncGE n) (CochainComplex.truncGEMap g n)))
      (inv
        (CategoryTheory.Functor.map Q
          (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))))

Tactic:
simp only [Functor.map_comp, ← cancel_mono (Q.map (CochainComplex.πTruncGE Y n)
      ≫ Q.map (CochainComplex.truncGEMap s n)), assoc, IsIso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CochainComplex.truncGEMap, DerivedCategory.Q, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp, CochainComplex.πTruncGE
-- 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 ℤ
n : ℤ
inst_3 : Y.IsStrictlyGE n
Y' : CochainComplex.{v, u, 0} C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncGE n)) (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n))
eq :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q Y) (Functor.obj Q (Y'.truncGE n)))
    (CategoryStruct.comp (Y := Functor.obj Q (Y.truncGE n)) (CategoryTheory.Functor.map Q (Y.πTruncGE n))
      (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n)))
    (CategoryTheory.Functor.map Q s ≫ CategoryTheory.Functor.map Q (Y'.πTruncGE n))
eq' :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q (Y'.truncGE n)))
    (CategoryStruct.comp (Y := Functor.obj Q (X.truncGE n)) (CategoryTheory.Functor.map Q (X.πTruncGE n))
      (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap g n)))
    (CategoryTheory.Functor.map Q g ≫ CategoryTheory.Functor.map Q (Y'.πTruncGE n))
⊢ Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q (Y'.truncGE n)))
    (CategoryTheory.Functor.map Q g ≫
      inv (CategoryTheory.Functor.map Q s) ≫
        CategoryStruct.comp (Y := Functor.obj Q (Y.truncGE n)) (CategoryTheory.Functor.map Q (Y.πTruncGE n))
          (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s n)))
    (CategoryStruct.comp (Y := Functor.obj Q (X.truncGE n)) (CategoryTheory.Functor.map Q (X.πTruncGE n))
      (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap g n)))

Tactic:
simp only [eq, IsIso.inv_hom_id_assoc, eq']

Premises used: CategoryTheory.IsIso.inv_hom_id_assoc
-- 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 ℤ
a b : ℤ
inst_3 : X.IsStrictlyGE a
inst_4 : X.IsStrictlyLE b
inst_5 : Y.IsStrictlyGE a
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
obtain :
  ∀ (X' : CochainComplex.{v, u, 0} C ℤ) (hX' : X'.IsStrictlyLE b) (s : X' ⟶ X)
    (hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s))
    (g : X' ⟶ Y) (fac : f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g),
    ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (_ : X'.IsStrictlyGE a) (_ : X'.IsStrictlyLE b) (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 ℤ) (_ : X'.IsStrictlyGE a) (_ : X'.IsStrictlyLE b) (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', hX', s, hs, g, fac⟩ := right_fac_of_isStrictlyLE f b

Premises used: DerivedCategory.right_fac_of_isStrictlyLE
-- 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 ℤ
a b : ℤ
inst_3 : X.IsStrictlyGE a
inst_4 : X.IsStrictlyLE b
inst_5 : Y.IsStrictlyGE a
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : CochainComplex.{v, u, 0} C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
fac : f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g
rw :
  ∀ (hs_1 : QuasiIso s) (g : X' ⟶ Y) (fac : f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g),
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncGE a)) (Y := Functor.obj Q (X.truncGE a))
      (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a))
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncGE a)) (Y := Functor.obj Q (X.truncGE a))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a))

Tactic:
rw [isIso_Q_map_iff_quasiIso] at hs

Premises used: DerivedCategory.isIso_Q_map_iff_quasiIso
-- 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 ℤ
a b : ℤ
inst_3 : X.IsStrictlyGE a
inst_4 : X.IsStrictlyLE b
inst_5 : Y.IsStrictlyGE a
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : CochainComplex.{v, u, 0} C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs_1 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
hs : QuasiIso s
g : X' ⟶ Y
fac : f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g
rw : ∀ (i : ℤ), a ≤ i → QuasiIsoAt s i
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncGE a)) (Y := Functor.obj Q (X.truncGE a))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a))

Tactic:
rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncGEMap_iff]

Premises used: CochainComplex.quasiIso_truncGEMap_iff, DerivedCategory.isIso_Q_map_iff_quasiIso
-- 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 ℤ
a b : ℤ
inst_3 : X.IsStrictlyGE a
inst_4 : X.IsStrictlyLE b
inst_5 : Y.IsStrictlyGE a
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : CochainComplex.{v, u, 0} C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs_1 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
hs : QuasiIso s
g : X' ⟶ Y
fac : f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g
⊢ ∀ (i : ℤ), a ≤ i → QuasiIsoAt s i

Tactic:
infer_instance
-- 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 ℤ
a b : ℤ
inst_3 : X.IsStrictlyGE a
inst_4 : X.IsStrictlyLE b
inst_5 : Y.IsStrictlyGE a
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : CochainComplex.{v, u, 0} C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
fac : f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncGE a)) (Y := Functor.obj Q (X.truncGE a))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a))

Tactic:
have : IsIso (Q.map (CochainComplex.truncGEMap s a)) := by
    rw [isIso_Q_map_iff_quasiIso] at hs
    rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncGEMap_iff]
    infer_instance
-- 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 ℤ
a b : ℤ
inst_3 : X.IsStrictlyGE a
inst_4 : X.IsStrictlyLE b
inst_5 : Y.IsStrictlyGE a
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : CochainComplex.{v, u, 0} C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
fac : f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncGE a)) (Y := Functor.obj Q (X.truncGE a))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a))
⊢ ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (_ : X'.IsStrictlyGE a) (_ : X'.IsStrictlyLE b) (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'.truncGE a, inferInstance, inferInstance,
    CochainComplex.truncGEMap s a ≫ inv (X.πTruncGE a), ?_,
      CochainComplex.truncGEMap g a ≫ inv (Y.πTruncGE a), ?_⟩

Premises used: CochainComplex.truncGEMap, inferInstance, CochainComplex.truncGE, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, CochainComplex.πTruncGE
-- 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 ℤ
a b : ℤ
inst_3 : X.IsStrictlyGE a
inst_4 : X.IsStrictlyLE b
inst_5 : Y.IsStrictlyGE a
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : CochainComplex.{v, u, 0} C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
fac : f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncGE a)) (Y := Functor.obj Q (X.truncGE a))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a))
refine_1 :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncGE a))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := X.truncGE a) (CochainComplex.truncGEMap s a) (inv (X.πTruncGE a))))
refine_2 :
  f =
    CategoryStruct.comp (Y := Functor.obj Q (X'.truncGE a))
      (inv
        (CategoryTheory.Functor.map Q
          (CategoryStruct.comp (Y := X.truncGE a) (CochainComplex.truncGEMap s a) (inv (X.πTruncGE a)))))
      (CategoryTheory.Functor.map Q
        (CategoryStruct.comp (Y := Y.truncGE a) (CochainComplex.truncGEMap g a) (inv (Y.πTruncGE a))))
⊢ ∃ (X' : CochainComplex.{v, u, 0} C ℤ) (_ : X'.IsStrictlyGE a) (_ : X'.IsStrictlyLE b) (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:
refine ⟨X'.truncGE a, inferInstance, inferInstance,
    CochainComplex.truncGEMap s a ≫ inv (X.πTruncGE a), ?_,
      CochainComplex.truncGEMap g a ≫ inv (Y.πTruncGE a), ?_⟩
-- 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 ℤ
a b : ℤ
inst_3 : X.IsStrictlyGE a
inst_4 : X.IsStrictlyLE b
inst_5 : Y.IsStrictlyGE a
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : CochainComplex.{v, u, 0} C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
fac : f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncGE a)) (Y := Functor.obj Q (X.truncGE a))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a))
refine_1 :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncGE a))
    (CategoryStruct.comp (Y := Functor.obj Q (X.truncGE a))
      (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a))
      (CategoryTheory.Functor.map Q (inv (X.πTruncGE a))))
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncGE a))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := X.truncGE a) (CochainComplex.truncGEMap s a) (inv (X.πTruncGE a))))

Tactic:
rw [Q.map_comp]

Premises used: DerivedCategory.Q, CategoryTheory.Functor.map_comp
-- 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 ℤ
a b : ℤ
inst_3 : X.IsStrictlyGE a
inst_4 : X.IsStrictlyLE b
inst_5 : Y.IsStrictlyGE a
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : CochainComplex.{v, u, 0} C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
fac : f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncGE a)) (Y := Functor.obj Q (X.truncGE a))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a))
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncGE a))
    (CategoryStruct.comp (Y := Functor.obj Q (X.truncGE a))
      (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a))
      (CategoryTheory.Functor.map Q (inv (X.πTruncGE a))))

Tactic:
infer_instance
-- 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 ℤ
a b : ℤ
inst_3 : X.IsStrictlyGE a
inst_4 : X.IsStrictlyLE b
inst_5 : Y.IsStrictlyGE a
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
X' : CochainComplex.{v, u, 0} C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
fac : f = inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncGE a)) (Y := Functor.obj Q (X.truncGE a))
    (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a))
refine_2 :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X') (Functor.obj Q Y))
    (CategoryTheory.Functor.map Q g)
    (CategoryTheory.Functor.map Q s ≫
      CategoryStruct.comp (Y := Functor.obj Q (X.truncGE a)) (CategoryTheory.Functor.map Q (X.πTruncGE a))
        (CategoryStruct.comp (Y := Functor.obj Q (X'.truncGE a))
          (inv (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap s a)))
          (CategoryStruct.comp (Y := Functor.obj Q (Y.truncGE a))
            (CategoryTheory.Functor.map Q (CochainComplex.truncGEMap g a))
            (inv (CategoryTheory.Functor.map Q (Y.πTruncGE a))))))
⊢ f =
    CategoryStruct.comp (Y := Functor.obj Q (X'.truncGE a))
      (inv
        (CategoryTheory.Functor.map Q
          (CategoryStruct.comp (Y := X.truncGE a) (CochainComplex.truncGEMap s a) (inv (X.πTruncGE a)))))
      (CategoryTheory.Functor.map Q
        (CategoryStruct.comp (Y := Y.truncGE a) (CochainComplex.truncGEMap g a) (inv (Y.πTruncGE a))))

Tactic:
simp only [Functor.map_comp, Functor.map_inv, IsIso.inv_comp, IsIso.inv_inv, assoc, fac,
      ← cancel_epi (Q.map s), IsIso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_comp, DerivedCategory.Q, CategoryTheory.IsIso.inv_inv, CategoryTheory.Functor.map_inv, CategoryTheory.Functor.map, CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi
-- 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 ℤ
a b : ℤ
inst_3 : X.IsStrictlyLE b
inst_4 : Y.IsStrictlyGE a
inst_5 : Y.IsStrictlyLE b
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
obtain :
  ∀ (Y' : CochainComplex.{v, u, 0} C ℤ) (hY' : Y'.IsStrictlyGE a) (g : X ⟶ Y') (s : Y ⟶ Y')
    (hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s))
    (fac : f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)),
    ∃ (Y' : CochainComplex.{v, u, 0} C ℤ) (_ : Y'.IsStrictlyGE a) (_ : Y'.IsStrictlyLE b) (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 ℤ) (_ : Y'.IsStrictlyGE a) (_ : Y'.IsStrictlyLE b) (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 ⟨Y', hY', g, s, hs, fac⟩ := left_fac_of_isStrictlyGE f a

Premises used: DerivedCategory.left_fac_of_isStrictlyGE
-- 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 ℤ
a b : ℤ
inst_3 : X.IsStrictlyLE b
inst_4 : Y.IsStrictlyGE a
inst_5 : Y.IsStrictlyLE b
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
Y' : CochainComplex.{v, u, 0} C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
fac : f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)
⊢ QuasiIso s

Tactic:
rw [isIso_Q_map_iff_quasiIso] at hs

Premises used: DerivedCategory.isIso_Q_map_iff_quasiIso