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 ℤ
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)
have 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)))
Tactic: refine ⟨Y'.truncLE b, inferInstance, inferInstance,
    inv (X.ιTruncLE b) ≫ CochainComplex.truncLEMap g b,
    inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s 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.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)))
⊢ ∃ (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 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))))
Tactic: refine ⟨Y'.truncLE b, inferInstance, inferInstance,
    inv (X.ιTruncLE b) ≫ CochainComplex.truncLEMap g b,
    inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s 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.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))
    (CategoryTheory.Functor.map Q
      (CategoryStruct.comp (Y := Y.truncLE b) (inv (Y.ιTruncLE b)) (CochainComplex.truncLEMap s b)))
have 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)))
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.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))
⊢ 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))))
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.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))))
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]
-- 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 : 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))
⊢ 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))))
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.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 ≫ s)))))
Tactic: rw [← Functor.map_comp, ← CochainComplex.ιTruncLE_naturality s b,
      Functor.map_comp, IsIso.inv_hom_id_assoc,
      ← Functor.map_comp, CochainComplex.ιTruncLE_naturality g b,
      Functor.map_comp, IsIso.inv_hom_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.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 ≫ s)))))
⊢ 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))))
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.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
          (CategoryStruct.comp (Y := Y'.truncLE b) (CochainComplex.truncLEMap s b) (Y'.ιTruncLE b))))))
Tactic: rw [← Functor.map_comp, ← CochainComplex.ιTruncLE_naturality s b,
      Functor.map_comp, IsIso.inv_hom_id_assoc,
      ← Functor.map_comp, CochainComplex.ιTruncLE_naturality g b,
      Functor.map_comp, IsIso.inv_hom_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 : ℤ
h : a < b
inst_3 : X.IsStrictlyLE a
inst_4 : Y.IsStrictlyGE b
⊢ Subsingleton.{w + 1} (Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y))
have suffices : ∀ (f : Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)), f = 0
Tactic: suffices ∀ (f : Q.obj X ⟶ Q.obj Y), f = 0 from ⟨by simp [this]⟩
-- 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 : ℤ
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)
⊢ f = 0
have 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
Tactic: obtain ⟨X', _, s, _, g, rfl⟩ := right_fac_of_isStrictlyLE f a
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Fractions (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : CochainComplex.{v, u, 0} C ℤ
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
have h₁ : ∀ (i : ℤ), g.f i = HomologicalComplex.Hom.f 0 i
Tactic: ext i
-- 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 : ℤ
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 : ℤ
⊢ g.f i = HomologicalComplex.Hom.f 0 i
have pos : ∀ (hi : a < i), g.f i = HomologicalComplex.Hom.f 0 i
Tactic: by_cases hi : a < i
-- 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 : ℤ
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
⊢ g.f i = HomologicalComplex.Hom.f 0 i
have neg : ∀ (hi : ¬a < i), g.f i = HomologicalComplex.Hom.f 0 i
Tactic: by_cases hi : a < i
-- 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 : ℤ
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
⊢ 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
have this : 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
-- 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 : ℤ
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
⊢ 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
have 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
Tactic: rw [this, Q.map_zero, comp_zero]
-- 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 : ℤ
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
⊢ 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
have 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
Tactic: rw [this, Q.map_zero, comp_zero]
-- 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 : ℤ
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
⊢ 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
have rw₂ : Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q X) (Functor.obj Q Y)) 0 0
Tactic: rw [this, Q.map_zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (hypothesis)
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₂)
⊢ f₁ = f₂
have 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₁
Tactic: have eq₁ := NatIso.naturality_1 (singleFunctorCompHomologyFunctorIso C n) f₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (hypothesis)
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₁
⊢ f₁ = f₂
have 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₂
Tactic: have eq₂ := NatIso.naturality_1 (singleFunctorCompHomologyFunctorIso C n) f₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (goal)
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 (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj (singleFunctor C n) x))
      (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
      (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map (singleFunctor C n) f₁) ≫
        NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1) =
    f₁
eq₂ :
  CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj (singleFunctor C n) x))
      (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
      (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map (singleFunctor C n) f₂) ≫
        NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1) =
    f₂
⊢ f₁ = f₂
have rw : CategoryStruct.comp (Y :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj (singleFunctor C n) x))
    (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
    (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map (singleFunctor C n) f₁) ≫
      NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1) =
  f₂
Tactic: rw [← eq₁, ← eq₂, h]