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 ℤ
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))
    (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)))))
have 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)))
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]
-- 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 ℤ
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 ℤ) (_ : 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
have 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
Tactic: obtain ⟨X', hX', s, hs, g, fac⟩ := right_fac_of_isStrictlyLE f b
-- 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 ℤ
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))
have 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))
Tactic: rw [isIso_Q_map_iff_quasiIso] at hs
Cleared hypotheses: g, fac
-- 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 ℤ
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
⊢ 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))
have rw : ∀ (i : ℤ), a ≤ i → QuasiIsoAt s i
Tactic: rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncGEMap_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (hypothesis)
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
⊢ ∃ (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
have 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))
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
-- 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 ℤ
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
have 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))))
Tactic: refine ⟨X'.truncGE a, inferInstance, inferInstance,
    CochainComplex.truncGEMap s a ≫ inv (X.πTruncGE a), ?_,
      CochainComplex.truncGEMap g a ≫ inv (Y.πTruncGE a), ?_⟩
-- 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 ℤ
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))))
⊢ ∃ (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
have 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))))
Tactic: refine ⟨X'.truncGE a, inferInstance, inferInstance,
    CochainComplex.truncGEMap s a ≫ inv (X.πTruncGE a), ?_,
      CochainComplex.truncGEMap g a ≫ inv (Y.πTruncGE a), ?_⟩
-- 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 ℤ
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))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := X.truncGE a) (CochainComplex.truncGEMap s a) (inv (X.πTruncGE a))))
have 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))))
Tactic: rw [Q.map_comp]
-- 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 ℤ
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))
⊢ 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))))
have 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))))))
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]
-- 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 ℤ
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))
⊢ 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))))))
have 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)
  (CategoryStruct.comp (Y := Functor.obj Q (X.truncGE a)) (CategoryTheory.Functor.map Q (s ≫ 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))))))
Tactic: rw [← Functor.map_comp_assoc, ← CochainComplex.πTruncGE_naturality s a,
      Functor.map_comp, assoc, IsIso.hom_inv_id_assoc,
      ← Functor.map_comp_assoc, CochainComplex.πTruncGE_naturality g a,
      Functor.map_comp, assoc, IsIso.hom_inv_id, comp_id]
-- 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 ℤ
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)
    (CategoryStruct.comp (Y := Functor.obj Q (X.truncGE a)) (CategoryTheory.Functor.map Q (s ≫ 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))))))
⊢ 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))))))
have 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)
  (CategoryStruct.comp (Y := Functor.obj Q (X.truncGE a))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := X'.truncGE a) (X'.πTruncGE a) (CochainComplex.truncGEMap s 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))))))
Tactic: rw [← Functor.map_comp_assoc, ← CochainComplex.πTruncGE_naturality s a,
      Functor.map_comp, assoc, IsIso.hom_inv_id_assoc,
      ← Functor.map_comp_assoc, CochainComplex.πTruncGE_naturality g a,
      Functor.map_comp, assoc, IsIso.hom_inv_id, comp_id]
-- 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 ℤ
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 ℤ) (_ : 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)
have 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)
Tactic: obtain ⟨Y', hY', g, s, hs, fac⟩ := left_fac_of_isStrictlyGE f a
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (hypothesis)
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)
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncLE b)) (Y := Functor.obj Q (Y'.truncLE b))
    (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s b))
have hs₁ : QuasiIso s
Tactic: rw [isIso_Q_map_iff_quasiIso] at hs
Cleared hypotheses: fac
-- 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 ℤ
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_1 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q Y) (CategoryTheory.Functor.map Q s)
hs : QuasiIso s
fac : f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q s)
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncLE b)) (Y := Functor.obj Q (Y'.truncLE b))
    (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s b))
have rw : ∀ i ≤ b, QuasiIsoAt s i
Tactic: rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncLEMap_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (hypothesis)
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)
⊢ ∃ (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)
have this : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Y.truncLE b)) (Y := Functor.obj Q (Y'.truncLE b))
  (CategoryTheory.Functor.map Q (CochainComplex.truncLEMap s b))
Tactic: have : IsIso (Q.map (CochainComplex.truncLEMap s b)) := by
    rw [isIso_Q_map_iff_quasiIso] at hs
    rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncLEMap_iff]
    infer_instance