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 : 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:
exact ⟨X', g, s, hs, 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)
n : ℤ
inst_3 : X.IsStrictlyLE n
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)
⊢ ∃ (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

Tactic:
obtain ⟨X', s, hs, g, rfl⟩ := right_fac f

Premises used: DerivedCategory.right_fac, 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 ℤ
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
rw : ∀ i ≤ n, QuasiIsoAt s i
⊢ 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))

Tactic:
rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncLEMap_iff]

Premises used: CochainComplex.quasiIso_truncLEMap_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 ℤ
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
rw : ∀ (hs : QuasiIso s) (g : X' ⟶ Y), ∀ i ≤ n, QuasiIsoAt s i
⊢ ∀ i ≤ n, QuasiIsoAt s i

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 ℤ
n : ℤ
inst_3 : X.IsStrictlyLE n
X' : CochainComplex.{v, u, 0} C ℤ
s : X' ⟶ X
hs : QuasiIso s
g : X' ⟶ Y
⊢ ∀ i ≤ n, 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 ℤ
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))

Tactic:
have : IsIso (Q.map (CochainComplex.truncLEMap s n)) := by
    rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncLEMap_iff]
    rw [isIso_Q_map_iff_quasiIso] at hs
    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 ℤ
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
this :
  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))
⊢ ∃ (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:
⟨X'.truncLE n, inferInstance, CochainComplex.truncLEMap s n ≫ X.ιTruncLE n, ?_,
      CochainComplex.truncLEMap g n ≫ Y.ιTruncLE n, ?_⟩

Premises used: CochainComplex.truncLEMap, CochainComplex.truncLE, inferInstance, CochainComplex.ιTruncLE, Exists.intro, CategoryTheory.CategoryStruct.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 : 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
this :
  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))
refine_1 :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncLE n))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := X.truncLE n) (CochainComplex.truncLEMap s n) (X.ιTruncLE n)))
refine_2 :
  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)
    (CategoryStruct.comp (Y := Functor.obj Q (X'.truncLE n))
      (inv
        (CategoryTheory.Functor.map Q
          (CategoryStruct.comp (Y := X.truncLE n) (CochainComplex.truncLEMap s n) (X.ιTruncLE n))))
      (CategoryTheory.Functor.map Q
        (CategoryStruct.comp (Y := Y.truncLE n) (CochainComplex.truncLEMap g n) (Y.ιTruncLE n))))
⊢ ∃ (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:
refine ⟨X'.truncLE n, inferInstance, CochainComplex.truncLEMap s n ≫ X.ιTruncLE n, ?_,
      CochainComplex.truncLEMap g n ≫ Y.ιTruncLE n, ?_⟩
-- 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 : 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
this :
  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))
refine_1 :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncLE n))
    (CategoryStruct.comp (Y := Functor.obj Q (X.truncLE n))
      (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s n)) (CategoryTheory.Functor.map Q (X.ιTruncLE n)))
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncLE n))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := X.truncLE n) (CochainComplex.truncLEMap s n) (X.ιTruncLE n)))

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 ℤ
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
this :
  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))
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (X'.truncLE n))
    (CategoryStruct.comp (Y := Functor.obj Q (X.truncLE n))
      (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s n)) (CategoryTheory.Functor.map Q (X.ιTruncLE n)))

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 ℤ
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
this :
  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))
⊢ 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)
    (CategoryStruct.comp (Y := Functor.obj Q (X'.truncLE n))
      (inv
        (CategoryTheory.Functor.map Q
          (CategoryStruct.comp (Y := X.truncLE n) (CochainComplex.truncLEMap s n) (X.ιTruncLE n))))
      (CategoryTheory.Functor.map Q
        (CategoryStruct.comp (Y := Y.truncLE n) (CochainComplex.truncLEMap g n) (Y.ιTruncLE n))))

Tactic:
simp
-- 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)
n : ℤ
inst_3 : Y.IsStrictlyGE n
obtain :
  ∀ (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)),
    ∃ (Y'_1 : CochainComplex.{v, u, 0} C ℤ) (_ : Y'_1.IsStrictlyGE n) (g_1 : X ⟶ Y'_1) (s_1 : Y ⟶ Y'_1) (x :
      IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s_1)),
      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))
        (CategoryTheory.Functor.map Q g_1 ≫ inv (CategoryTheory.Functor.map Q s_1))
⊢ ∃ (Y' : CochainComplex.{v, u, 0} C ℤ) (_ : Y'.IsStrictlyGE n) (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', g, s, hs, rfl⟩ := left_fac f

Premises used: rfl, DerivedCategory.left_fac
-- 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)
rw : ∀ (i : ℤ), n ≤ i → QuasiIsoAt s i
⊢ 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))

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 ℤ
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)
⊢ QuasiIso s

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 ℤ
n : ℤ
inst_3 : Y.IsStrictlyGE n
Y' : CochainComplex.{v, u, 0} C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : QuasiIso s
⊢ ∀ (i : ℤ), n ≤ 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 ℤ
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)
⊢ 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))

Tactic:
have : IsIso (Q.map (CochainComplex.truncGEMap s n)) := by
    rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncGEMap_iff]
    rw [isIso_Q_map_iff_quasiIso] at hs
    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 ℤ
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))
⊢ ∃ (Y'_1 : CochainComplex.{v, u, 0} C ℤ) (_ : Y'_1.IsStrictlyGE n) (g_1 : X ⟶ Y'_1) (s_1 : Y ⟶ Y'_1) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s_1)),
    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))
      (CategoryTheory.Functor.map Q g_1 ≫ inv (CategoryTheory.Functor.map Q s_1))

Tactic:
⟨Y'.truncGE n, inferInstance, X.πTruncGE n ≫ CochainComplex.truncGEMap g n,
    Y.πTruncGE n ≫ CochainComplex.truncGEMap s n, ?_, ?_⟩

Premises used: CochainComplex.truncGEMap, inferInstance, CochainComplex.truncGE, Exists.intro, CategoryTheory.CategoryStruct.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))
refine_1 :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))
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 ≫ 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)))))
⊢ ∃ (Y'_1 : CochainComplex.{v, u, 0} C ℤ) (_ : Y'_1.IsStrictlyGE n) (g_1 : X ⟶ Y'_1) (s_1 : Y ⟶ Y'_1) (x :
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s_1)),
    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))
      (CategoryTheory.Functor.map Q g_1 ≫ inv (CategoryTheory.Functor.map Q s_1))

Tactic:
refine ⟨Y'.truncGE n, inferInstance, X.πTruncGE n ≫ CochainComplex.truncGEMap g n,
    Y.πTruncGE n ≫ CochainComplex.truncGEMap s n, ?_, ?_⟩
-- 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))
refine_1 :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (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)))
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (Y := Functor.obj Q (Y'.truncGE n))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := Y.truncGE n) (Y.πTruncGE n) (CochainComplex.truncGEMap s n)))

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 ℤ
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))
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (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)))

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 ℤ
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.{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))

Tactic:
have eq := Q.congr_map (CochainComplex.πTruncGE_naturality s n)
-- 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.{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))

Tactic:
have eq' := Q.congr_map (CochainComplex.πTruncGE_naturality g n)