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 ℤ
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)
hs₁ : QuasiIso s
⊢ f = CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q 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 ℤ
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)
rw : ∀ i ≤ b, QuasiIsoAt s i
⊢ 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:
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 ℤ
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)
⊢ ∀ i ≤ b, 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.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))

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
-- 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)
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))
⊢ ∃ (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:
⟨Y'.truncLE b, inferInstance, inferInstance,
    inv (X.ιTruncLE b) ≫ CochainComplex.truncLEMap g b,
    inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s b, ?_, ?_⟩

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

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

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

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_comp, DerivedCategory.Q, CategoryTheory.IsIso.inv_inv, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.Functor.map_inv, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map, 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 : ℤ
h : a < b
inst_3 : X.IsStrictlyLE a
inst_4 : Y.IsStrictlyGE b
this : ∀ (f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)), f = 0
⊢ ∀ (a b : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)), a = b

Tactic:
simp [this]
-- 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 : ℤ
h : a < b
inst_3 : X.IsStrictlyLE a
inst_4 : Y.IsStrictlyGE b
suffices : ∀ (f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)), f = 0
⊢ Subsingleton.{w + 1} (Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))

Tactic:
suffices ∀ (f : Q.obj X ⟶ Q.obj Y), f = 0 from ⟨by simp [this]⟩
-- 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 : ℤ
h : a < b
inst_3 : X.IsStrictlyLE a
inst_4 : Y.IsStrictlyGE b
f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)
obtain :
  ∀ (X' : CochainComplex.{v, u, 0} C ℤ),
    X'.IsStrictlyLE a →
      ∀ (s : X' ⟶ X)
        (w : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s))
        (g : X' ⟶ 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) 0
⊢ f = 0

Tactic:
obtain ⟨X', _, s, _, g, rfl⟩ := right_fac_of_isStrictlyLE f a

Premises used: DerivedCategory.right_fac_of_isStrictlyLE, 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 ℤ
a b : ℤ
h : a < b
inst_3 : X.IsStrictlyLE a
inst_4 : Y.IsStrictlyGE b
X' : CochainComplex.{v, u, 0} C ℤ
w : X'.IsStrictlyLE a
s : X' ⟶ X
w_1 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
h₁ : ∀ (i : ℤ), g.f i = HomologicalComplex.Hom.f 0 i
⊢ g = 0

Tactic:
ext i
-- 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 : ℤ
h : a < b
inst_3 : X.IsStrictlyLE a
inst_4 : Y.IsStrictlyGE b
X' : CochainComplex.{v, u, 0} C ℤ
w : X'.IsStrictlyLE a
s : X' ⟶ X
w_1 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
i : ℤ
pos : ∀ (hi : a < i), g.f i = HomologicalComplex.Hom.f 0 i
neg : ∀ (hi : ¬a < i), g.f i = HomologicalComplex.Hom.f 0 i
⊢ g.f i = HomologicalComplex.Hom.f 0 i

Tactic:
by_cases hi : a < i
-- 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 : ℤ
h : a < b
inst_3 : X.IsStrictlyLE a
inst_4 : Y.IsStrictlyGE b
X' : CochainComplex.{v, u, 0} C ℤ
w : X'.IsStrictlyLE a
s : X' ⟶ X
w_1 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
i : ℤ
hi : a < i
⊢ g.f i = HomologicalComplex.Hom.f 0 i

Tactic:
apply (X'.isZero_of_isStrictlyLE a i hi).eq_of_src

Premises used: CochainComplex.isZero_of_isStrictlyLE, CategoryTheory.Limits.IsZero.eq_of_src
-- 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 : ℤ
h : a < b
inst_3 : X.IsStrictlyLE a
inst_4 : Y.IsStrictlyGE b
X' : CochainComplex.{v, u, 0} C ℤ
w : X'.IsStrictlyLE a
s : X' ⟶ X
w_1 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
i : ℤ
hi : ¬a < i
⊢ i < b

Tactic:
lia
-- 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 : ℤ
h : a < b
inst_3 : X.IsStrictlyLE a
inst_4 : Y.IsStrictlyGE b
X' : CochainComplex.{v, u, 0} C ℤ
w : X'.IsStrictlyLE a
s : X' ⟶ X
w_1 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
i : ℤ
hi : ¬a < i
⊢ g.f i = HomologicalComplex.Hom.f 0 i

Tactic:
apply (Y.isZero_of_isStrictlyGE b i (by lia)).eq_of_tgt

Premises used: CochainComplex.isZero_of_isStrictlyGE, CategoryTheory.Limits.IsZero.eq_of_tgt
-- 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 : ℤ
h : a < b
inst_3 : X.IsStrictlyLE a
inst_4 : Y.IsStrictlyGE b
X' : CochainComplex.{v, u, 0} C ℤ
w : X'.IsStrictlyLE a
s : X' ⟶ X
w_1 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
⊢ g = 0

Tactic:
have : g = 0 := by
    ext i
    by_cases hi : a < i
    · apply (X'.isZero_of_isStrictlyLE a i hi).eq_of_src
    · apply (Y.isZero_of_isStrictlyGE b i (by lia)).eq_of_tgt
-- 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 : ℤ
h : a < b
inst_3 : X.IsStrictlyLE a
inst_4 : Y.IsStrictlyGE b
X' : CochainComplex.{v, u, 0} C ℤ
w : X'.IsStrictlyLE a
s : X' ⟶ X
w_1 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X') (CategoryTheory.Functor.map Q s)
g : X' ⟶ Y
this : g = 0
rw :
  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 0) 0
rw₁ :
  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) ≫ 0) 0
rw₂ rw₃ : Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)) 0 0
⊢ 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) 0

Tactic:
rw [this, Q.map_zero, comp_zero]

Premises used: DerivedCategory.Q, CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_zero
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
x x_1 : C
f₁ f₂ : x ⟶ x_1
h :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C n) x)
      (Functor.obj (singleFunctor C n) x_1))
    (CategoryTheory.Functor.map (singleFunctor C n) f₁) (CategoryTheory.Functor.map (singleFunctor C n) f₂)
⊢ CategoryStruct.comp (Y :=
      Functor.obj.{v, v, u, u}
        (Functor.comp (D := DerivedCategory.{w, v, u} C) (singleFunctor C n) (homologyFunctor C n)) x)
      (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
      (CategoryTheory.Functor.map
          (Functor.comp (D := DerivedCategory.{w, v, u} C) (singleFunctor C n) (homologyFunctor C n)) f₁ ≫
        NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1) =
    CategoryTheory.Functor.map (𝟭 C) f₁

Tactic:
have eq₁ := NatIso.naturality_1 (singleFunctorCompHomologyFunctorIso C n) f₁
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
x x_1 : C
f₁ f₂ : x ⟶ x_1
h :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C n) x)
      (Functor.obj (singleFunctor C n) x_1))
    (CategoryTheory.Functor.map (singleFunctor C n) f₁) (CategoryTheory.Functor.map (singleFunctor C n) f₂)
eq₁ :
  CategoryStruct.comp (Y :=
      Functor.obj.{v, v, u, u}
        (Functor.comp (D := DerivedCategory.{w, v, u} C) (singleFunctor C n) (homologyFunctor C n)) x)
      (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
      (CategoryTheory.Functor.map
          (Functor.comp (D := DerivedCategory.{w, v, u} C) (singleFunctor C n) (homologyFunctor C n)) f₁ ≫
        NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1) =
    CategoryTheory.Functor.map (𝟭 C) f₁
⊢ CategoryStruct.comp (Y :=
      Functor.obj.{v, v, u, u}
        (Functor.comp (D := DerivedCategory.{w, v, u} C) (singleFunctor C n) (homologyFunctor C n)) x)
      (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
      (CategoryTheory.Functor.map
          (Functor.comp (D := DerivedCategory.{w, v, u} C) (singleFunctor C n) (homologyFunctor C n)) f₂ ≫
        NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1) =
    CategoryTheory.Functor.map (𝟭 C) f₂

Tactic:
have eq₂ := NatIso.naturality_1 (singleFunctorCompHomologyFunctorIso C n) f₂
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
f :
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C n) A) (Functor.obj (singleFunctor C n) B)
change :
  ∀
    (f :
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A))
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) B))),
    ∃ (a : A ⟶ B), CategoryTheory.Functor.map (singleFunctor C n) a = f
⊢ ∃ (a : A ⟶ B), CategoryTheory.Functor.map (singleFunctor C n) a = f

Tactic:
change Q.obj ((CochainComplex.singleFunctor C n).obj A) ⟶
      Q.obj ((CochainComplex.singleFunctor C n).obj B) at f

Premises used: CochainComplex.singleFunctor, DerivedCategory.Q, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
f :
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A))
    (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) B))
this :
  ∃ (f' :
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (CochainComplex.singleFunctor C n) A)
      (Functor.obj (CochainComplex.singleFunctor C n) B)),
    f = CategoryTheory.Functor.map Q f'
obtain :
  ∀
    (f' :
      Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (CochainComplex.singleFunctor C n) A)
        (Functor.obj (CochainComplex.singleFunctor C n) B)),
    ∃ (a : A ⟶ B),
      Eq.{w + 1} (α :=
        Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C n) A)
          (Functor.obj (singleFunctor C n) B))
        (CategoryTheory.Functor.map (singleFunctor C n) a) (CategoryTheory.Functor.map Q f')
⊢ ∃ (a : A ⟶ B), CategoryTheory.Functor.map (singleFunctor C n) a = f

Tactic:
obtain ⟨f', rfl⟩ := this

Premises used: rfl