awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n : ℤ
φ : (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
⊢ IsIso (X := HomologicalComplex.homology (mappingCone S.f) n) (Y := HomologicalComplex.homology S.X₃ n)
    (HomologicalComplex.homologyMap (descShortComplex S) n)
have this : IsIso (X := Functor.obj (quotient C (up ℤ) ⋙ homologyFunctor C (up ℤ) n) (mappingCone S.f)) (Y :=
  HomologicalComplex.homology S.X₃ n)
  (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (mappingCone S.f) ≫
    HomologicalComplex.homologyMap (descShortComplex S) n)
Tactic: have : IsIso ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫
        HomologicalComplex.homologyMap (descShortComplex S) n) := by
      apply Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono
        ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅_exact _
          (mappingCone_triangleh_distinguished S.f) n _ rfl).δlast
        (composableArrows₅_exact hS n _ rfl).δlast φ
      all_goals dsimp [φ]; infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
f : S₁ ⟶ S₂
⊢ map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂ = descShortComplex S₁ ≫ f.τ₃
have h : ∀ (n : ℤ),
  HomologicalComplex.Hom.f (map S₁.f S₂.f f.τ₁ f.τ₂ sorry ≫ descShortComplex S₂) n = (descShortComplex S₁ ≫ f.τ₃).f n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
f : S₁ ⟶ S₂
n : ℤ
⊢ HomologicalComplex.Hom.f (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂) n = (descShortComplex S₁ ≫ f.τ₃).f n
have h : CategoryStruct.comp (Y := (mappingCone S₁.f).X n)
    (HomComplex.Cochain.v (inl S₁.f) (n + 1) n sorry : S₁.X₁.X (n + 1) ⟶ (mappingCone S₁.f).X n)
    (HomologicalComplex.Hom.f (map S₁.f S₂.f f.τ₁ f.τ₂ sorry ≫ descShortComplex S₂) n :
      (mappingCone S₁.f).X n ⟶ S₂.X₃.X n) =
  HomComplex.Cochain.v (inl S₁.f) (n + 1) n sorry ≫ (descShortComplex S₁ ≫ f.τ₃).f n
Tactic: apply ext_from _ (n + 1) n rfl
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
f : S₁ ⟶ S₂
n : ℤ
h :
  CategoryStruct.comp (Y := (mappingCone S₁.f).X n)
      (HomComplex.Cochain.v (inl S₁.f) (n + 1) n ⋯ : S₁.X₁.X (n + 1) ⟶ (mappingCone S₁.f).X n)
      (HomologicalComplex.Hom.f (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂) n :
        (mappingCone S₁.f).X n ⟶ S₂.X₃.X n) =
    HomComplex.Cochain.v (inl S₁.f) (n + 1) n ⋯ ≫ (descShortComplex S₁ ≫ f.τ₃).f n
⊢ HomologicalComplex.Hom.f (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂) n = (descShortComplex S₁ ≫ f.τ₃).f n
have h₁ : CategoryStruct.comp (Y := (mappingCone S₁.f).X n)
    (HomologicalComplex.Hom.f (inr S₁.f) n : S₁.X₂.X n ⟶ (mappingCone S₁.f).X n)
    (HomologicalComplex.Hom.f (map S₁.f S₂.f f.τ₁ f.τ₂ sorry ≫ descShortComplex S₂) n :
      (mappingCone S₁.f).X n ⟶ S₂.X₃.X n) =
  HomologicalComplex.Hom.f (inr S₁.f) n ≫ (descShortComplex S₁ ≫ f.τ₃).f n
Tactic: apply ext_from _ (n + 1) n rfl
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a a' : ℤ
ha' : n + a = a'
X : C
i : ℤ
⊢ HomologicalComplex.X.{v, u, 0}
      (Functor.obj (single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) X)
      i =
    HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) X) i
have obtain : ∀ (ha' : n + a = a + n),
  HomologicalComplex.X.{v, u, 0}
      (Functor.obj (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
        X)
      i =
    HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) X) i
Tactic: obtain rfl : a' = a + n := by lia
Cleared hypotheses: a', ha'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
⊢ HomologicalComplex.X.{v, u, 0}
      (Functor.obj (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
        X)
      i =
    HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) X) i
have pos : ∀ (h : i = a),
  HomologicalComplex.X.{v, u, 0}
      (Functor.obj (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
        X)
      i =
    HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) X) i
Tactic: by_cases h : i = a
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
pos :
  ∀ (h : i = a),
    HomologicalComplex.X.{v, u, 0}
        (Functor.obj
          (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) X)
        i =
      HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) X) i
⊢ HomologicalComplex.X.{v, u, 0}
      (Functor.obj (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
        X)
      i =
    HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) X) i
have neg : ∀ (h : ¬i = a),
  HomologicalComplex.X.{v, u, 0}
      (Functor.obj (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
        X)
      i =
    HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) X) i
Tactic: by_cases h : i = a
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
h : i = a
⊢ HomologicalComplex.X.{v, u, 0}
      (Functor.obj (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
        X)
      i =
    HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) X) i
have pos : ∀ (ha' : n + i = i + n),
  HomologicalComplex.X.{v, u, 0}
      (Functor.obj (single C (ComplexShape.up ℤ) (i + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
        X)
      i =
    HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) X) i
Tactic: subst h
Cleared hypotheses: a, ha', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
h : ¬i = a
⊢ HomologicalComplex.X.{v, u, 0}
      (Functor.obj (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
        X)
      i =
    HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) X) i
have neg : (if i + n = a + n then X else 0) = if i = a then X else 0
Tactic: dsimp [single]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
h : ¬i = a
⊢ (if i + n = a + n then X else 0) = if i = a then X else 0
have neg : (if i + n = a + n then X else 0) = 0
Tactic: rw [if_neg h, if_neg (fun h' => h (by lia))]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
h : ¬i = a
neg : (if i + n = a + n then X else 0) = 0
⊢ (if i + n = a + n then X else 0) = if i = a then X else 0
have neg₁ : Eq.{u + 1} (α := C) 0 0
Tactic: rw [if_neg h, if_neg (fun h' => h (by lia))]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a a' : ℤ
ha' : n + a = a'
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ)
      (Functor.obj (single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) X)
      (Functor.obj (single C (ComplexShape.up ℤ) a) Y))
    (CategoryTheory.Functor.map
        (single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) f ≫
      Iso.hom
        ((fun (X : C) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯ :
              Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                (Functor.obj
                  (single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) X)
                (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
          Y))
    (Iso.hom
        ((fun (X : C) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯ :
              Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                (Functor.obj
                  (single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) X)
                (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
          X) ≫
      CategoryTheory.Functor.map (single C (ComplexShape.up ℤ) a) f)
have obtain : ∀ (ha' : n + a = a + n),
  Eq (α :=
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ)
      (Functor.obj (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
        X)
      (Functor.obj (single C (ComplexShape.up ℤ) a) Y))
    (CategoryTheory.Functor.map
        (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) f ≫
      Iso.hom
        ((fun (X : C) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso sorry) sorry :
              Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                (Functor.obj
                  (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                  X)
                (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
          Y))
    (Iso.hom
        ((fun (X : C) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso sorry) sorry :
              Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                (Functor.obj
                  (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                  X)
                (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
          X) ≫
      CategoryTheory.Functor.map (single C (ComplexShape.up ℤ) a) f)
Tactic: obtain rfl : a' = a + n := by lia
Cleared hypotheses: a', ha'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a : ℤ
X Y : C
f : X ⟶ Y
ha' : n + a = a + n
⊢ Eq (α :=
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ)
      (Functor.obj (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
        X)
      (Functor.obj (single C (ComplexShape.up ℤ) a) Y))
    (CategoryTheory.Functor.map
        (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) f ≫
      Iso.hom
        ((fun (X : C) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯ :
              Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                (Functor.obj
                  (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                  X)
                (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
          Y))
    (Iso.hom
        ((fun (X : C) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯ :
              Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                (Functor.obj
                  (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                  X)
                (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
          X) ≫
      CategoryTheory.Functor.map (single C (ComplexShape.up ℤ) a) f)
have hfg : Eq (α :=
  HomologicalComplex.X.{v, u, 0}
      (Functor.obj (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
        X)
      a ⟶
    HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) Y) a)
  (Hom.f
    (CategoryTheory.Functor.map
        (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) f ≫
      Iso.hom
        ((fun (X : C) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso sorry) sorry :
              Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                (Functor.obj
                  (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                  X)
                (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
          Y))
    a)
  (Hom.f
    (Iso.hom
        ((fun (X : C) ↦
            (Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso sorry) sorry :
              Iso (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                (Functor.obj
                  (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                  X)
                (Functor.obj (single C (ComplexShape.up ℤ) a) X)))
          X) ≫
      CategoryTheory.Functor.map (single C (ComplexShape.up ℤ) a) f)
    a)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
a : ℤ
⊢ Eq (α :=
    Iso (C := C ⥤ CochainComplex.{v, u, 0} C ℤ)
      (single C (ComplexShape.up ℤ) a ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 0)
      (single C (ComplexShape.up ℤ) a))
    (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯)
    (Functor.isoWhiskerLeft (single C (ComplexShape.up ℤ) a) (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ))
have w : ∀ (x : C),
  Eq.{v + 1} (α :=
    X.{v, u, 0}
        (Functor.obj
          (single C (ComplexShape.up ℤ) a ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 0) x)
        a ⟶
      X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) a)
    (Hom.f
      (NatTrans.app (Iso.hom (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso sorry) sorry) sorry)) x)
      a)
    (Hom.f
      (NatTrans.app
        (Iso.hom
          (Functor.isoWhiskerLeft (single C (ComplexShape.up ℤ) a) (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ)))
        x)
      a)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
a : ℤ
x : C
⊢ Eq.{v + 1} (α :=
    X.{v, u, 0}
        (Functor.obj
          (single C (ComplexShape.up ℤ) a ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 0) x)
        a ⟶
      X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) a)
    (Hom.f
      (NatTrans.app (Iso.hom (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯)) x)
      a)
    (Hom.f
      (NatTrans.app
        (Iso.hom
          (Functor.isoWhiskerLeft (single C (ComplexShape.up ℤ) a) (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ)))
        x)
      a)
have w : Eq.{v + 1} (α :=
  X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) (a + 0) ⟶
    X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) a)
  (eqToHom sorry)
  (Hom.f
    (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ))
      (Functor.obj (single C (ComplexShape.up ℤ) a) x))
    a)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
⊢ Eq (α :=
    Iso (C := C ⥤ CochainComplex.{v, u, 0} C ℤ)
      (single C (ComplexShape.up ℤ) a'' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (m + n))
      (single C (ComplexShape.up ℤ) a))
    (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯)
    (Functor.isoWhiskerLeft (single C (ComplexShape.up ℤ) a'') (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) m n) ≪≫
      Iso.symm
          (Functor.associator (single C (ComplexShape.up ℤ) a'')
            (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) m)
            (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)) ≪≫
        Iso.trans (Y := single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
          (Functor.isoWhiskerRight
            (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯)
            (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n))
          (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯))
have w : ∀ (x : C),
  Eq.{v + 1} (α :=
    X.{v, u, 0}
        (Functor.obj
          (single C (ComplexShape.up ℤ) a'' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (m + n)) x)
        a ⟶
      X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) a)
    (Hom.f
      (NatTrans.app (Iso.hom (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso sorry) sorry) sorry)) x)
      a)
    (Hom.f
      (NatTrans.app
        (Iso.hom
          (Functor.isoWhiskerLeft (single C (ComplexShape.up ℤ) a'')
              (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) m n) ≪≫
            Iso.symm
                (Functor.associator (single C (ComplexShape.up ℤ) a'')
                  (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) m)
                  (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)) ≪≫
              Iso.trans (Y :=
                single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                (Functor.isoWhiskerRight
                  (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso sorry) sorry) sorry)
                  (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n))
                (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso sorry) sorry) sorry)))
        x)
      a)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x : C
⊢ Eq.{v + 1} (α :=
    X.{v, u, 0}
        (Functor.obj
          (single C (ComplexShape.up ℤ) a'' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (m + n)) x)
        a ⟶
      X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) a)
    (Hom.f
      (NatTrans.app (Iso.hom (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯)) x)
      a)
    (Hom.f
      (NatTrans.app
        (Iso.hom
          (Functor.isoWhiskerLeft (single C (ComplexShape.up ℤ) a'')
              (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) m n) ≪≫
            Iso.symm
                (Functor.associator (single C (ComplexShape.up ℤ) a'')
                  (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) m)
                  (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)) ≪≫
              Iso.trans (Y :=
                single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
                (Functor.isoWhiskerRight
                  (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯)
                  (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n))
                (NatIso.ofComponents (fun (X : C) ↦ Hom.isoOfComponents (fun (i : ℤ) ↦ eqToIso ⋯) ⋯) ⋯)))
        x)
      a)
have w : Eq.{v + 1} (α :=
  X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a'') x) (a + (m + n)) ⟶
    X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) x) a)
  (eqToHom sorry)
  (Hom.f
      (NatTrans.app (Iso.hom (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) m n))
        (Functor.obj (single C (ComplexShape.up ℤ) a'') x))
      a ≫
    𝟙 (X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a'') x) (a + n + m)) ≫ eqToHom sorry ≫ eqToHom sorry)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
R : Type u_1
inst_3 : Ring R
n : ℤ
inst_4 : Linear.{u_1, v, u} R C
X Y : C
f : X ⟶ Y
r : R
⊢ CategoryTheory.Functor.map (SingleFunctors.functor (singleFunctors C) n) (r • f) =
    HSMul.hSMul (β :=
      Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
        (Functor.obj (SingleFunctors.functor (singleFunctors C) n) Y))
      r (CategoryTheory.Functor.map (SingleFunctors.functor (singleFunctors C) n) f)
have dsimp : { f := fun (i : ℤ) ↦ if h : i = n then eqToHom sorry ≫ (r • f) ≫ eqToHom sorry else 0, comm' := sorry } =
  HSMul.hSMul (β :=
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ)
      { X := fun (i : ℤ) ↦ if i = n then X else 0, d := fun (x x_1 : ℤ) ↦ 0, shape := sorry, d_comp_d' := sorry :
        HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) }
      { X := fun (i : ℤ) ↦ if i = n then Y else 0, d := fun (x x_1 : ℤ) ↦ 0, shape := sorry, d_comp_d' := sorry :
        HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) })
    r
    { f := fun (i : ℤ) ↦ if h : i = n then eqToHom sorry ≫ f ≫ eqToHom sorry else 0, comm' := sorry :
      Hom
        { X := fun (i : ℤ) ↦ if i = n then X else 0, d := fun (x x_1 : ℤ) ↦ 0, shape := sorry, d_comp_d' := sorry :
          HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) }
        { X := fun (i : ℤ) ↦ if i = n then Y else 0, d := fun (x x_1 : ℤ) ↦ 0, shape := sorry, d_comp_d' := sorry :
          HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ) } }
Tactic: dsimp [CochainComplex.singleFunctors, HomologicalComplex.single]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ f ≫ g = 𝟙 X₁ ≫ f ≫ g
have rw : f ≫ g = f ≫ g
Tactic: rw [id_comp]