awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.HomologySequence (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 : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
f : X ⟶ Y
hf : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Qh X) (CategoryTheory.Functor.map Qh f)
n : ℤ
⊢ IsIso (X := Functor.obj (Functor.comp (D := DerivedCategory.{w, v, u} C) Qh (homologyFunctor C n)) X)
    (CategoryTheory.Functor.map (Functor.comp (D := DerivedCategory.{w, v, u} C) Qh (homologyFunctor C n)) f)
have mp : IsIso (X := Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj Qh X))
  (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map Qh f))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.HomologySequence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
f : K ⟶ Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L
a a' : ℤ
h : n + a = a'
⊢ Eq (α :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (Functor.shift (homologyFunctor C 0) a) (Functor.obj Q K) ⟶
      Functor.obj (C := DerivedCategory.{w, v, u} C) (Functor.shift (homologyFunctor C 0) a') (Functor.obj Q L))
    (Functor.shiftMap (homologyFunctor C 0) (ShiftedHom.map f Q) a a' h)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C a)) K ≫
      Functor.shiftMap (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0) f a a' h ≫
        NatTrans.app (Iso.inv (homologyFunctorFactors C a')) L)
have rw : Eq (α :=
  Functor.obj (C := DerivedCategory.{w, v, u} C) (Functor.shift (homologyFunctor C 0) a) (Functor.obj Q K) ⟶
    Functor.obj (C := DerivedCategory.{w, v, u} C) (Functor.shift (homologyFunctor C 0) a') (Functor.obj Q L))
  (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C 0) a) (NatTrans.app (Iso.inv (quotientCompQhIso C)) K) ≫
    ((CategoryTheory.Functor.map (homologyFunctor C a) (NatTrans.app (Iso.hom (quotientCompQhIso C)) K) ≫
          NatTrans.app (Iso.hom (homologyFunctorFactors C a)) K ≫
            NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a)) K) ≫
        (NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a)) K ≫
            Functor.shiftMap (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0) f a a' sorry ≫
              NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a')) L) ≫
          NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a')) L ≫
            NatTrans.app (Iso.inv (homologyFunctorFactors C a')) L ≫
              CategoryTheory.Functor.map (homologyFunctor C a') (NatTrans.app (Iso.inv (quotientCompQhIso C)) L)) ≫
      CategoryTheory.Functor.map (Functor.shift (homologyFunctor C 0) a')
        (NatTrans.app (Iso.hom (quotientCompQhIso C)) L))
  (NatTrans.app (Iso.hom (homologyFunctorFactors C a)) K ≫
    Functor.shiftMap (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0) f a a' h ≫
      NatTrans.app (Iso.inv (homologyFunctorFactors C a')) L)
Tactic: rw [← ShiftedHom.map_naturality_1 f (quotientCompQhIso C),
    ShiftedHom.mk₀_comp, ShiftedHom.comp_mk₀,
    Functor.shiftMap_comp', Functor.shiftMap_comp,
    ShiftedHom.comp_map, shiftMap_homologyFunctor_map_Qh ..,
    homologyFunctorFactorsh_hom_app_quotient_obj,
    homologyFunctorFactorsh_inv_app_quotient_obj,
    HomotopyCategory.homologyFunctor_shiftMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.HomologySequence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (DerivedCategory.{w, v, u} C)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
rw : n₀ + 1 = n₁
⊢ 1 + n₀ = n₁
have rw₁ : n₁ = n₁
Tactic: rw [add_comm 1, h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.HomologySequence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n₀))
        T.obj₃ ⟶
      homology T.obj₁ n₁)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ homologyδOfTriangle T n₀ n₁ h)
    (DerivedCategory.HomologySequence.δ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T) n₀ n₁ h ≫
      NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₁)
have dsimp : Eq (α :=
  Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
      (Functor.obj DerivedCategory.Q T.obj₃) ⟶
    homology T.obj₁ n₁)
  (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ homologyδOfTriangle T n₀ n₁ h)
  (CategoryStruct.comp (Y :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
      (Functor.obj DerivedCategory.Q T.obj₁))
    (Functor.shiftMap (DerivedCategory.homologyFunctor C 0)
      (CategoryTheory.Functor.map DerivedCategory.Q T.mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso DerivedCategory.Q 1)) T.obj₁)
      n₀ n₁ sorry)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₁))
Tactic: dsimp [DerivedCategory.HomologySequence.δ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.HomologySequence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ Eq (α :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
        (Functor.obj DerivedCategory.Q T.obj₃) ⟶
      homology T.obj₁ n₁)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ homologyδOfTriangle T n₀ n₁ h)
    (CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
        (Functor.obj DerivedCategory.Q T.obj₁))
      (Functor.shiftMap (DerivedCategory.homologyFunctor C 0)
        (CategoryTheory.Functor.map DerivedCategory.Q T.mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso DerivedCategory.Q 1)) T.obj₁)
        n₀ n₁ ⋯)
      (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₁))
have rw : Eq (α :=
  Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
      (Functor.obj DerivedCategory.Q T.obj₃) ⟶
    homology T.obj₁ n₁)
  (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ homologyδOfTriangle T n₀ n₁ h)
  (CategoryStruct.comp (Y :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
      (Functor.obj DerivedCategory.Q T.obj₁))
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫
      Functor.shiftMap (homologyFunctor C (ComplexShape.up ℤ) 0) T.mor₃ n₀ n₁ sorry ≫
        NatTrans.app (Iso.inv (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₁)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₁))
Tactic: rw [dsimp% [ShiftedHom.map]
      DerivedCategory.shiftMap_homologyFunctor_map_Q T.mor₃ n₀ n₁ (by lia)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.HomologySequence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n : ℤ
⊢ Eq (α := homology T.obj₁ n ⟶ homology T.obj₃ n)
    (CategoryStruct.comp (Y := homology T.obj₂ n) (homologyMap T.mor₁ n) (homologyMap T.mor₂ n)) 0
have rw : Eq (α :=
  Functor.obj (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
      T.obj₁ ⟶
    homology T.obj₃ n)
  (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫
    CategoryStruct.comp (Y := homology T.obj₂ n) (homologyMap T.mor₁ n) (homologyMap T.mor₂ n))
  (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
Tactic: rw [← cancel_epi ((DerivedCategory.homologyFunctorFactors _ _).hom.app _),
    ← DerivedCategory.homologyFunctorFactors_hom_naturality_assoc,
    ← DerivedCategory.homologyFunctorFactors_hom_naturality,
    ← Functor.map_comp_assoc, dsimp% comp_distTriang_mor_zero₁₂ _ hT, Functor.map_zero,
    Limits.zero_comp, Limits.comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.HomologySequence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n : ℤ
rw :
  Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
        T.obj₁ ⟶
      homology T.obj₃ n)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫
      CategoryStruct.comp (Y := homology T.obj₂ n) (homologyMap T.mor₁ n) (homologyMap T.mor₂ n))
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
⊢ Eq (α := homology T.obj₁ n ⟶ homology T.obj₃ n)
    (CategoryStruct.comp (Y := homology T.obj₂ n) (homologyMap T.mor₁ n) (homologyMap T.mor₂ n)) 0
have rw₁ : Eq (α :=
  Functor.obj (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
      T.obj₁ ⟶
    homology T.obj₃ n)
  (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
      (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁) ≫
    NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₂ ≫ homologyMap T.mor₂ n)
  (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
Tactic: rw [← cancel_epi ((DerivedCategory.homologyFunctorFactors _ _).hom.app _),
    ← DerivedCategory.homologyFunctorFactors_hom_naturality_assoc,
    ← DerivedCategory.homologyFunctorFactors_hom_naturality,
    ← Functor.map_comp_assoc, dsimp% comp_distTriang_mor_zero₁₂ _ hT, Functor.map_zero,
    Limits.zero_comp, Limits.comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.HomologySequence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n : ℤ
rw :
  Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
        T.obj₁ ⟶
      homology T.obj₃ n)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫
      CategoryStruct.comp (Y := homology T.obj₂ n) (homologyMap T.mor₁ n) (homologyMap T.mor₂ n))
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
rw₁ :
  Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
        T.obj₁ ⟶
      homology T.obj₃ n)
    (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
        (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁) ≫
      NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₂ ≫ homologyMap T.mor₂ n)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
⊢ Eq (α := homology T.obj₁ n ⟶ homology T.obj₃ n)
    (CategoryStruct.comp (Y := homology T.obj₂ n) (homologyMap T.mor₁ n) (homologyMap T.mor₂ n)) 0
have rw₂ : Eq (α :=
  Functor.obj (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
      T.obj₁ ⟶
    homology T.obj₃ n)
  (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
      (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁) ≫
    CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
        (CategoryTheory.Functor.map DerivedCategory.Q T.mor₂) ≫
      NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₃)
  (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
Tactic: rw [← cancel_epi ((DerivedCategory.homologyFunctorFactors _ _).hom.app _),
    ← DerivedCategory.homologyFunctorFactors_hom_naturality_assoc,
    ← DerivedCategory.homologyFunctorFactors_hom_naturality,
    ← Functor.map_comp_assoc, dsimp% comp_distTriang_mor_zero₁₂ _ hT, Functor.map_zero,
    Limits.zero_comp, Limits.comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.HomologySequence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n : ℤ
rw :
  Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
        T.obj₁ ⟶
      homology T.obj₃ n)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫
      CategoryStruct.comp (Y := homology T.obj₂ n) (homologyMap T.mor₁ n) (homologyMap T.mor₂ n))
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
rw₁ :
  Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
        T.obj₁ ⟶
      homology T.obj₃ n)
    (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
        (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁) ≫
      NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₂ ≫ homologyMap T.mor₂ n)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
rw₂ :
  Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
        T.obj₁ ⟶
      homology T.obj₃ n)
    (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
        (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁) ≫
      CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
          (CategoryTheory.Functor.map DerivedCategory.Q T.mor₂) ≫
        NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₃)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
⊢ Eq (α := homology T.obj₁ n ⟶ homology T.obj₃ n)
    (CategoryStruct.comp (Y := homology T.obj₂ n) (homologyMap T.mor₁ n) (homologyMap T.mor₂ n)) 0
have rw₃ : Eq (α :=
  Functor.obj (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n))
      T.obj₁ ⟶
    homology T.obj₃ n)
  (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
      (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁ ≫ CategoryTheory.Functor.map DerivedCategory.Q T.mor₂) ≫
    NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₃)
  (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n)) T.obj₁ ≫ 0)
Tactic: rw [← cancel_epi ((DerivedCategory.homologyFunctorFactors _ _).hom.app _),
    ← DerivedCategory.homologyFunctorFactors_hom_naturality_assoc,
    ← DerivedCategory.homologyFunctorFactors_hom_naturality,
    ← Functor.map_comp_assoc, dsimp% comp_distTriang_mor_zero₁₂ _ hT, Functor.map_zero,
    Limits.zero_comp, Limits.comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.HomologySequence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ Eq (α := homology T.obj₃ n₀ ⟶ homology T.obj₂ n₁) (homologyδOfTriangle T n₀ n₁ h ≫ homologyMap T.mor₁ n₁) 0
have rw : Eq (α :=
  Functor.obj (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n₀))
      T.obj₃ ⟶
    homology T.obj₂ n₁)
  (CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
        (Triangle.obj₁ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)))
      (DerivedCategory.HomologySequence.δ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T) n₀ n₁ sorry)
      (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n₁)
          (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁) ≫
        NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₂) :
    Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
        (Functor.obj DerivedCategory.Q T.obj₃) ⟶
      homology T.obj₂ n₁)
  (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ 0 :
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n₀))
        T.obj₃ ⟶
      homology T.obj₂ n₁)
Tactic: rw [← cancel_epi ((DerivedCategory.homologyFunctorFactors _ _).hom.app _),
    homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc ..,
    ← DerivedCategory.homologyFunctorFactors_hom_naturality]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.HomologySequence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n₀))
        T.obj₃ ⟶
      homology T.obj₂ n₁)
    (CategoryStruct.comp (Y :=
        Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
          (Triangle.obj₁ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)))
        (DerivedCategory.HomologySequence.δ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T) n₀ n₁ ⋯)
        (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n₁)
            (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁) ≫
          NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₂) :
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
          (Functor.obj DerivedCategory.Q T.obj₃) ⟶
        homology T.obj₂ n₁)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ 0 :
      Functor.obj
          (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n₀))
          T.obj₃ ⟶
        homology T.obj₂ n₁)
have dsimp : Eq (α :=
  Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
      (Functor.obj DerivedCategory.Q T.obj₃) ⟶
    homology T.obj₂ n₁)
  (CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
        (Functor.obj DerivedCategory.Q T.obj₁))
      (DerivedCategory.HomologySequence.δ
        (Triangle.mk (X := Functor.obj DerivedCategory.Q T.obj₁) (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁)
          (CategoryTheory.Functor.map DerivedCategory.Q T.mor₂)
          (CategoryTheory.Functor.map DerivedCategory.Q T.mor₃ ≫
            NatTrans.app (Iso.hom (Functor.commShiftIso DerivedCategory.Q 1)) T.obj₁))
        n₀ n₁ sorry)
      (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n₁)
          (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁) ≫
        NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₂) :
    Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
        (Functor.obj DerivedCategory.Q T.obj₃) ⟶
      homology T.obj₂ n₁)
  (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ 0 :
    Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
        (Functor.obj DerivedCategory.Q T.obj₃) ⟶
      homology T.obj₂ n₁)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.HomologySequence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ Eq (α :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
        (Functor.obj DerivedCategory.Q T.obj₃) ⟶
      homology T.obj₂ n₁)
    (CategoryStruct.comp (Y :=
        Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
          (Functor.obj DerivedCategory.Q T.obj₁))
        (DerivedCategory.HomologySequence.δ
          (Triangle.mk (X := Functor.obj DerivedCategory.Q T.obj₁) (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁)
            (CategoryTheory.Functor.map DerivedCategory.Q T.mor₂)
            (CategoryTheory.Functor.map DerivedCategory.Q T.mor₃ ≫
              NatTrans.app (Iso.hom (Functor.commShiftIso DerivedCategory.Q 1)) T.obj₁))
          n₀ n₁ ⋯)
        (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n₁)
            (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁) ≫
          NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₂) :
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
          (Functor.obj DerivedCategory.Q T.obj₃) ⟶
        homology T.obj₂ n₁)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ 0 :
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
          (Functor.obj DerivedCategory.Q T.obj₃) ⟶
        homology T.obj₂ n₁)
have rw : Eq (α :=
  Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
      (Functor.obj DerivedCategory.Q T.obj₃) ⟶
    homology T.obj₂ n₁)
  (CategoryStruct.comp (Y :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
      (Functor.obj DerivedCategory.Q T.obj₂))
    0 (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₂))
  (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ 0)
Tactic: rw [reassoc_of% dsimp% DerivedCategory.HomologySequence.δ_comp _ hT n₀ n₁ h]