awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
refine_3 :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S.f))
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S.X₁)))
    ((CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁) ≫
      𝟙 (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S.X₁)))
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S) ≫
      inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S)) ≫
        CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁)
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S.f))
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S.X₁)))
    ((CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁) ≫
      CategoryTheory.Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (𝟙 (Functor.obj Q S.X₁)))
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S) ≫
      inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S)) ≫
        CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁)
have refine_3₁ : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S.f))
    (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S.X₁)))
  (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁)
  (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S) ≫
    inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S)) ≫
      CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁)
Tactic: rw [CategoryTheory.Functor.map_id, comp_id, IsIso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
⊢ Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) (triangleOfSES hS)
have rw : ∃ (X : CochainComplex.{v, u, 0} C ℤ) (Y : CochainComplex.{v, u, 0} C ℤ) (f : X ⟶ Y),
  Nonempty.{w + 1}
    (Iso (C := Triangle (DerivedCategory.{w, v, u} C)) (triangleOfSES hS)
      (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f)))
Tactic: rw [mem_distTriang_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₃ (triangleOfSES h₁))
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Triangle.obj₁ (triangleOfSES h₂))))
    (Triangle.mor₃ (triangleOfSES h₁) ≫
      CategoryTheory.Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
        (CategoryTheory.Functor.map Q f.τ₁))
    (CategoryTheory.Functor.map Q f.τ₃ ≫ Triangle.mor₃ (triangleOfSES h₂))
have dsimp : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q S₁.X₃)
    (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S₂.X₁)))
  ((inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S₁)) ≫
      CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S₁.X₁) ≫
    CategoryTheory.Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
      (CategoryTheory.Functor.map Q f.τ₁))
  (CategoryTheory.Functor.map Q f.τ₃ ≫
    inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S₂)) ≫
      CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S₂.f).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S₂.X₁)
Tactic: dsimp [triangleOfSES, triangleOfSESδ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q S₁.X₃)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S₂.X₁)))
    ((inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S₁)) ≫
        CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S₁.X₁) ≫
      CategoryTheory.Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
        (CategoryTheory.Functor.map Q f.τ₁))
    (CategoryTheory.Functor.map Q f.τ₃ ≫
      inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S₂)) ≫
        CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S₂.f).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S₂.X₁)
have rw : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S₁.f))
    (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S₂.X₁)))
  (CategoryTheory.Functor.map Q
      ((CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
        CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) f.τ₁) ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S₂.X₁)
  (CategoryTheory.Functor.map Q
      (CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ sorry ≫ (CochainComplex.mappingCone.triangle S₂.f).mor₃) ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S₂.X₁)
Tactic: rw [assoc, assoc, IsIso.inv_comp_eq, ← Functor.map_comp_assoc,
      ← CochainComplex.mappingCone.map_descShortComplex,
      Functor.map_comp_assoc, IsIso.hom_inv_id_assoc,
      ← Functor.commShiftIso_hom_naturality,
      ← Functor.map_comp_assoc, ← Functor.map_comp_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S₁.f))
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S₂.X₁)))
    (CategoryTheory.Functor.map Q
        ((CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
          CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) f.τ₁) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S₂.X₁)
    (CategoryTheory.Functor.map Q
        (CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ (CochainComplex.mappingCone.triangle S₂.f).mor₃) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S₂.X₁)
have e_a : (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
    CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) f.τ₁ =
  CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ sorry ≫ (CochainComplex.mappingCone.triangle S₂.f).mor₃
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
e : Iso (C := C ⥤ DerivedCategory.{w, v, u} C)
  (Functor.obj (SingleFunctors.evaluation C (DerivedCategory.{w, v, u} C) 0) (singleFunctors C))
  (Functor.obj (C := SingleFunctors C (DerivedCategory.{w, v, u} C) ℤ)
    (SingleFunctors.evaluation C (DerivedCategory.{w, v, u} C) 0)
    (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q)) :=
  Functor.mapIso (SingleFunctors.evaluation C (DerivedCategory.{w, v, u} C) 0) (singleFunctorsPostcompQIso C)
⊢ Iso (C := Triangle (DerivedCategory.{w, v, u} C)) hS.singleTriangle
    (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯)
have refine_1 : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₁ hS.singleTriangle)
    (Triangle.obj₂ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) sorry)))
  (Triangle.mor₁ hS.singleTriangle ≫ Iso.hom (e.app S.X₂))
  (Iso.hom (e.app S.X₁) ≫
    Triangle.mor₁ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) sorry))
Tactic: refine Triangle.isoMk _ _ (e.app S.X₁) (e.app S.X₂) (e.app S.X₃) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
e : Iso (C := C ⥤ DerivedCategory.{w, v, u} C)
  (Functor.obj (SingleFunctors.evaluation C (DerivedCategory.{w, v, u} C) 0) (singleFunctors C))
  (Functor.obj (C := SingleFunctors C (DerivedCategory.{w, v, u} C) ℤ)
    (SingleFunctors.evaluation C (DerivedCategory.{w, v, u} C) 0)
    (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q)) :=
  Functor.mapIso (SingleFunctors.evaluation C (DerivedCategory.{w, v, u} C) 0) (singleFunctorsPostcompQIso C)
refine_1 :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₁ hS.singleTriangle)
      (Triangle.obj₂ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯)))
    (Triangle.mor₁ hS.singleTriangle ≫ Iso.hom (e.app S.X₂))
    (Iso.hom (e.app S.X₁) ≫
      Triangle.mor₁ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯))
⊢ Iso (C := Triangle (DerivedCategory.{w, v, u} C)) hS.singleTriangle
    (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯)
have refine_2 : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₂ hS.singleTriangle)
    (Triangle.obj₃ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) sorry)))
  (Triangle.mor₂ hS.singleTriangle ≫ Iso.hom (e.app S.X₃))
  (Iso.hom (e.app S.X₂) ≫
    Triangle.mor₂ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) sorry))
Tactic: refine Triangle.isoMk _ _ (e.app S.X₁) (e.app S.X₂) (e.app S.X₃) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
e : Iso (C := C ⥤ DerivedCategory.{w, v, u} C)
  (Functor.obj (SingleFunctors.evaluation C (DerivedCategory.{w, v, u} C) 0) (singleFunctors C))
  (Functor.obj (C := SingleFunctors C (DerivedCategory.{w, v, u} C) ℤ)
    (SingleFunctors.evaluation C (DerivedCategory.{w, v, u} C) 0)
    (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q)) :=
  Functor.mapIso (SingleFunctors.evaluation C (DerivedCategory.{w, v, u} C) 0) (singleFunctorsPostcompQIso C)
refine_1 :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₁ hS.singleTriangle)
      (Triangle.obj₂ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯)))
    (Triangle.mor₁ hS.singleTriangle ≫ Iso.hom (e.app S.X₂))
    (Iso.hom (e.app S.X₁) ≫
      Triangle.mor₁ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯))
refine_2 :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₂ hS.singleTriangle)
      (Triangle.obj₃ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯)))
    (Triangle.mor₂ hS.singleTriangle ≫ Iso.hom (e.app S.X₃))
    (Iso.hom (e.app S.X₂) ≫
      Triangle.mor₂ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯))
⊢ Iso (C := Triangle (DerivedCategory.{w, v, u} C)) hS.singleTriangle
    (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯)
have refine_3 : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₃ hS.singleTriangle)
    (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
      (Triangle.obj₁ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) sorry))))
  (Triangle.mor₃ hS.singleTriangle ≫
    Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Iso.hom (e.app S.X₁)))
  (Iso.hom (e.app S.X₃) ≫
    Triangle.mor₃ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) sorry))
Tactic: refine Triangle.isoMk _ _ (e.app S.X₁) (e.app S.X₂) (e.app S.X₃) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
S₁ S₂ : ShortComplex.{v, u} C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₃ h₁.singleTriangle)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Triangle.obj₁ h₂.singleTriangle)))
    (Triangle.mor₃ h₁.singleTriangle ≫
      Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.map (singleFunctor C 0) f.τ₁))
    (Functor.map (singleFunctor C 0) f.τ₃ ≫ Triangle.mor₃ h₂.singleTriangle)
have dsimp : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₁.X₃)
    (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁)))
  ((NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₁.X₃ ≫
      triangleOfSESδ sorry ≫
        Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
          (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₁.X₁)) ≫
    Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.map (singleFunctor C 0) f.τ₁))
  (Functor.map (singleFunctor C 0) f.τ₃ ≫
    NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₂.X₃ ≫
      triangleOfSESδ sorry ≫
        Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
          (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
Tactic: dsimp [singleδ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
S₁ S₂ : ShortComplex.{v, u} C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₁.X₃)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁)))
    ((NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₁.X₃ ≫
        triangleOfSESδ ⋯ ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₁.X₁)) ≫
      Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.map (singleFunctor C 0) f.τ₁))
    (Functor.map (singleFunctor C 0) f.τ₃ ≫
      NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₂.X₃ ≫
        triangleOfSESδ ⋯ ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
have rw : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₁.X₃)
    (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁)))
  (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₁.X₃ ≫
    triangleOfSESδ sorry ≫
      Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
          (Functor.map (SingleFunctors.functor (CochainComplex.singleFunctors C) 0 ⋙ Q) f.τ₁) ≫
        Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
          (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
  (Functor.map (singleFunctor C 0) f.τ₃ ≫
    NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₂.X₃ ≫
      triangleOfSESδ sorry ≫
        Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
          (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
Tactic: rw [assoc, assoc, ← Functor.map_comp, ← NatTrans.naturality, Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
S₁ S₂ : ShortComplex.{v, u} C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₁.X₃)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁)))
    (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₁.X₃ ≫
      triangleOfSESδ ⋯ ≫
        Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (Functor.map (SingleFunctors.functor (CochainComplex.singleFunctors C) 0 ⋙ Q) f.τ₁) ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
    (Functor.map (singleFunctor C 0) f.τ₃ ≫
      NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₂.X₃ ≫
        triangleOfSESδ ⋯ ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
have dsimp : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₁.X₃)
    (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁)))
  (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₁.X₃ ≫
    triangleOfSESδ sorry ≫
      Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
          (Functor.map Q (Functor.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0) f.τ₁)) ≫
        Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
          (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
  (Functor.map (singleFunctor C 0) f.τ₃ ≫
    NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₂.X₃ ≫
      triangleOfSESδ sorry ≫
        Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
          (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
Tactic: dsimp [CochainComplex.singleFunctors]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
⊢ Eq.{w + 1} (α := SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n)
    ((fun (y : Cocycle K L n) ↦
        (SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
            ((AddEquiv.symm Cocycle.equivHomShift :
                (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
              y) :
          SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n))
      y₁)
    ((fun (y : Cocycle K L n) ↦
        (SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
            ((AddEquiv.symm Cocycle.equivHomShift :
                (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
              y) :
          SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n))
      y₂)
have refine : Eq (α := ShiftedHom (C := DerivedCategory C) (Functor.obj DerivedCategory.Q K) (Functor.obj DerivedCategory.Q L) n)
  ((SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q :
      (a : SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) →
        ShiftedHom (DerivedCategory.Q.obj K) (DerivedCategory.Q.obj L) n)
    ((fun (y : Cocycle K L n) ↦
        (SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
            ((AddEquiv.symm Cocycle.equivHomShift :
                (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
              y) :
          SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n))
      y₁))
  ((SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q :
      (a : SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) →
        ShiftedHom (DerivedCategory.Q.obj K) (DerivedCategory.Q.obj L) n)
    ((fun (y : Cocycle K L n) ↦
        (SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
            ((AddEquiv.symm Cocycle.equivHomShift :
                (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
              y) :
          SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n))
      y₂))
Tactic: refine (SmallShiftedHom.equiv _ DerivedCategory.Q).injective ?_