awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
a b c : ℤ
h : a + b = c
⊢ Eq (α :=
    Iso (C := CochainComplex.{v, u, 0} C ℤ ⥤ CochainComplex.{v, u, 0} C ℤ)
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) c)
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a ⋙
        CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b))
    (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b c h) (shiftFunctorAdd' C a b c h)
have w : ∀ (x : CochainComplex.{v, u, 0} C ℤ) (i : ℤ),
  Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b c h)) x) i =
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b c h)) x).f i
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
a b : ℤ
⊢ Eq (α :=
    Iso (C := CochainComplex.{v, u, 0} C ℤ ⥤ CochainComplex.{v, u, 0} C ℤ)
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (a + b))
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a ⋙
        CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b))
    (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) a b) (shiftFunctorAdd' C a b (a + b) ⋯)
have rw : Eq (α :=
  Iso (C := CochainComplex.{v, u, 0} C ℤ ⥤ CochainComplex.{v, u, 0} C ℤ)
    (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (a + b))
    (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a ⋙
      CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b))
  (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) sorry) (shiftFunctorAdd' C a b (a + b) sorry)
Tactic: rw [← CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd'_eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
a b : ℤ
rw :
  Eq (α :=
    Iso (C := CochainComplex.{v, u, 0} C ℤ ⥤ CochainComplex.{v, u, 0} C ℤ)
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (a + b))
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a ⋙
        CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b))
    (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) ⋯) (shiftFunctorAdd' C a b (a + b) ⋯)
⊢ Eq (α :=
    Iso (C := CochainComplex.{v, u, 0} C ℤ ⥤ CochainComplex.{v, u, 0} C ℤ)
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (a + b))
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a ⋙
        CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b))
    (shiftFunctorAdd (CochainComplex.{v, u, 0} C ℤ) a b) (shiftFunctorAdd' C a b (a + b) ⋯)
have rw₁ : Eq (α :=
  Iso (C := CochainComplex.{v, u, 0} C ℤ ⥤ CochainComplex.{v, u, 0} C ℤ)
    (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (a + b))
    (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a ⋙
      CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b))
  (shiftFunctorAdd' C a b (a + b) sorry) (shiftFunctorAdd' C a b (a + b) sorry)
Tactic: rw [← CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd'_eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
⊢ Eq (α :=
    Iso (C := CochainComplex.{v, u, 0} C ℤ ⥤ CochainComplex.{v, u, 0} C ℤ)
      (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 0) (𝟭 (CochainComplex.{v, u, 0} C ℤ)))
    (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ) (shiftFunctorZero' C 0 ⋯)
have w : ∀ (x : CochainComplex.{v, u, 0} C ℤ) (i : ℤ),
  Hom.f (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ)) x) i =
    (NatTrans.app (Iso.hom (shiftFunctorZero' C 0 sorry)) x).f i
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
x : CochainComplex.{v, u, 0} C ℤ
i : ℤ
⊢ Hom.f (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ)) x) i =
    (NatTrans.app (Iso.hom (shiftFunctorZero' C 0 ⋯)) x).f i
have w : (XIsoOfEq x sorry).hom = (NatTrans.app (Iso.hom (shiftFunctorZero' C 0 sorry)) x).f i
Tactic: rw [shiftFunctorZero_hom_app_f, shiftFunctorZero'_hom_app_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
x : CochainComplex.{v, u, 0} C ℤ
i : ℤ
w : (XIsoOfEq x ⋯).hom = (NatTrans.app (Iso.hom (shiftFunctorZero' C 0 ⋯)) x).f i
⊢ Hom.f (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v, u, 0} C ℤ) ℤ)) x) i =
    (NatTrans.app (Iso.hom (shiftFunctorZero' C 0 ⋯)) x).f i
have w₁ : (XIsoOfEq x sorry).hom = (XIsoOfEq x sorry).hom
Tactic: rw [shiftFunctorZero_hom_app_f, shiftFunctorZero'_hom_app_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b p : ℤ
⊢ p + b + a = p + a + b
have rw : p + (b + a) = p + a + b
Tactic: rw [add_assoc, add_comm b, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b p : ℤ
rw : p + (b + a) = p + a + b
⊢ p + b + a = p + a + b
have rw₁ : p + (a + b) = p + a + b
Tactic: rw [add_assoc, add_comm b, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K : CochainComplex.{v, u, 0} C ℤ
a b p : ℤ
rw : p + (b + a) = p + a + b
rw₁ : p + (a + b) = p + a + b
⊢ p + b + a = p + a + b
have rw₂ : p + (a + b) = p + (a + b)
Tactic: rw [add_assoc, add_comm b, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b p : ℤ
⊢ Hom.f (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v, u, 0} C ℤ) a b)) K) p = Iso.hom (XIsoOfEq K ⋯)
have rw : Hom.f
    (NatTrans.app
      (Iso.hom
        (Iso.symm (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) sorry) ≪≫
          CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) b a (a + b) sorry))
      K)
    p =
  Iso.hom (XIsoOfEq K sorry)
Tactic: rw [shiftFunctorComm_eq _ _ _ _ rfl]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b p : ℤ
⊢ Hom.f
      (NatTrans.app
        (Iso.hom
          (Iso.symm (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) ⋯) ≪≫
            CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) b a (a + b) ⋯))
        K)
      p =
    Iso.hom (XIsoOfEq K ⋯)
have dsimp : Hom.f (NatTrans.app (Iso.inv (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) sorry)) K) p ≫
    Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) b a (a + b) sorry)) K) p =
  Iso.hom (XIsoOfEq K sorry)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
a b p : ℤ
⊢ Hom.f (NatTrans.app (Iso.inv (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) a b (a + b) ⋯)) K) p ≫
      Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v, u, 0} C ℤ) b a (a + b) ⋯)) K)
        p =
    Iso.hom (XIsoOfEq K ⋯)
have rw : (XIsoOfEq K sorry).hom ≫ (XIsoOfEq K sorry).hom = Iso.hom (XIsoOfEq K sorry)
Tactic: rw [shiftFunctorAdd'_inv_app_f', shiftFunctorAdd'_hom_app_f']
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n i i' : ℤ
hi : n + i = i'
K : CochainComplex.{v, u, 0} C ℤ
⊢ i + { as := n : Discrete ℤ }.as = i'
have dsimp : i + n = i'
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n i i' : ℤ
hi : n + i = i'
K : CochainComplex.{v, u, 0} C ℤ
⊢ i + n = i'
have rw : i + n = n + i
Tactic: rw [← hi, add_comm i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n i i' : ℤ
hi : n + i = i'
K : CochainComplex.{v, u, 0} C ℤ
rw : i + n = n + i
⊢ i + n = i'
have rw₁ : n + i = n + i
Tactic: rw [← hi, add_comm i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
n : ℤ
X Y : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
x : X ⟶ Y
i : ℤ
⊢ F.map (x.f (i + n)) ≫ 𝟙 (F.obj (Y.X (i + n))) = 𝟙 (F.obj (X.X (i + n))) ≫ F.map (x.f (i + n))
have h : F.map (x.f (i + n)) ≫ 𝟙 (F.obj (Y.X (i + n))) = F.map (x.f (i + n))
Tactic: rw [id_comp, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
n : ℤ
X Y : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
x : X ⟶ Y
i : ℤ
h : F.map (x.f (i + n)) ≫ 𝟙 (F.obj (Y.X (i + n))) = F.map (x.f (i + n))
⊢ F.map (x.f (i + n)) ≫ 𝟙 (F.obj (Y.X (i + n))) = 𝟙 (F.obj (X.X (i + n))) ≫ F.map (x.f (i + n))
have h₁ : Eq (α := F.obj (X.X (i + n)) ⟶ F.obj (Y.X (i + n))) (F.map (x.f (i + n))) (F.map (x.f (i + n)))
Tactic: rw [id_comp, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
x : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
i : ℤ
⊢ Eq (α :=
    HomologicalComplex.X
        (obj
          (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (A := ℤ) 0 ⋙
            F.mapHomologicalComplex (ComplexShape.up ℤ))
          x)
        i ⟶
      HomologicalComplex.X
        (obj
          (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
            shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (A := ℤ) 0)
          x)
        i)
    (HomologicalComplex.Hom.f (NatTrans.app (Iso.hom (F.mapCochainComplexShiftIso 0)) x) i :
      HomologicalComplex.X
          (obj
            (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (A := ℤ) 0 ⋙
              F.mapHomologicalComplex (ComplexShape.up ℤ))
            x)
          i ⟶
        HomologicalComplex.X
          (obj
            (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
              shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (A := ℤ) 0)
            x)
          i)
    (HomologicalComplex.Hom.f
        (map (F.mapHomologicalComplex (ComplexShape.up ℤ))
            (NatTrans.app (Iso.hom (shiftFunctorZero (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) ℤ)) x) ≫
          NatTrans.app (Iso.inv (shiftFunctorZero (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) ℤ))
            (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) x))
        i :
      HomologicalComplex.X
          (obj
            (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (A := ℤ) 0 ⋙
              F.mapHomologicalComplex (ComplexShape.up ℤ))
            x)
          i ⟶
        HomologicalComplex.X
          (obj
            (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙
              shiftFunctor (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) (A := ℤ) 0)
            x)
          i)
have w : 𝟙 (F.obj (x.X (i + 0))) =
  F.map
      (HomologicalComplex.Hom.f
        (NatTrans.app (Iso.hom (shiftFunctorZero (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) ℤ)) x) i) ≫
    HomologicalComplex.Hom.f
      (NatTrans.app (Iso.inv (shiftFunctorZero (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) ℤ))
        (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) x))
      i
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
a b : ℤ
x : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
i : ℤ
⊢ 𝟙 (F.obj (x.X (i + (a + b)))) =
    F.map
        (HomologicalComplex.Hom.f
          (NatTrans.app (Iso.hom (shiftFunctorAdd (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) a b)) x) i) ≫
      𝟙 (F.obj (x.X (i + b + a))) ≫
        𝟙 (F.obj (x.X (i + b + a))) ≫
          HomologicalComplex.Hom.f
            (NatTrans.app (Iso.inv (shiftFunctorAdd (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) a b))
              (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) x))
            i
have w : 𝟙 (F.obj (x.X (i + (a + b)))) =
  F.map
      (HomologicalComplex.Hom.f
        (NatTrans.app (Iso.hom (shiftFunctorAdd (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) a b)) x) i) ≫
    HomologicalComplex.Hom.f
      (NatTrans.app (Iso.inv (shiftFunctorAdd (HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ)) a b))
        (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) x))
      i
Tactic: rw [id_comp, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K L : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel j i
⊢ HSMul.hSMul (β := K.X (i + { as := n : Discrete ℤ }.as) ⟶ L.X (j + { as := n : Discrete ℤ }.as)) n.negOnePow
      (h.hom (i + { as := n : Discrete ℤ }.as) (j + { as := n : Discrete ℤ }.as)) =
    0
have dsimp : HSMul.hSMul (β := K.X (i + n) ⟶ L.X (j + n)) n.negOnePow (h.hom (i + n) (j + n)) = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K L : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel j i
⊢ HSMul.hSMul (β := K.X (i + n) ⟶ L.X (j + n)) n.negOnePow (h.hom (i + n) (j + n)) = 0
have a : ¬(ComplexShape.up ℤ).Rel (j + n) (i + n)
Tactic: rw [h.zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
K L : CochainComplex.{v, u, 0} C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i : ℤ
⊢ HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) φ₁) i =
    (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) K).d i (i + 1) ≫
          HSMul.hSMul (β := K.X (i + 1 + { as := n : Discrete ℤ }.as) ⟶ L.X (i + { as := n : Discrete ℤ }.as))
            n.negOnePow (h.hom (i + 1 + { as := n : Discrete ℤ }.as) (i + { as := n : Discrete ℤ }.as)) +
        HSMul.hSMul (β := K.X (i + { as := n : Discrete ℤ }.as) ⟶ L.X (i - 1 + { as := n : Discrete ℤ }.as)) n.negOnePow
            (h.hom (i + { as := n : Discrete ℤ }.as) (i - 1 + { as := n : Discrete ℤ }.as)) ≫
          (Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L).d (i - 1) i +
      HomologicalComplex.Hom.f
        (CategoryTheory.Functor.map (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) φ₂) i
have dsimp : φ₁.f (i + n) =
  HSMul.hSMul (β := K.X (i + n) ⟶ K.X (i + 1 + n)) n.negOnePow (K.d (i + n) (i + 1 + n)) ≫
        HSMul.hSMul (β := K.X (i + 1 + n) ⟶ L.X (i + n)) n.negOnePow (h.hom (i + 1 + n) (i + n)) +
      HSMul.hSMul (β := K.X (i + n) ⟶ L.X (i - 1 + n)) n.negOnePow (h.hom (i + n) (i - 1 + n)) ≫
        HSMul.hSMul (β := L.X (i - 1 + n) ⟶ L.X (i + n)) n.negOnePow (L.d (i - 1 + n) (i + n)) +
    φ₂.f (i + n)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
n : ℤ
⊢ Functor.Additive (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
have this : Functor.Additive (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
  (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
Tactic: have : ((quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor _ n)).Additive :=
    Functor.additive_of_iso ((quotient C (ComplexShape.up ℤ)).commShiftIso n)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
R : Type u_1
inst_4 : Ring R
inst_5 : Linear.{u_1, v, u} R C
n : ℤ
X Y : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
f :
  Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)
    (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)
r : R
⊢ CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) (r • f) =
    HSMul.hSMul (β :=
      Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
        (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))
        (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)))
      r (CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) f)
have obtain : ∀ (f : X ⟶ Y),
  CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
      (HSMul.hSMul (β :=
        Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y))
        r
        (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f :
          Functor.obj (quotient C (ComplexShape.up ℤ)) X ⟶ Functor.obj (quotient C (ComplexShape.up ℤ)) Y)) =
    HSMul.hSMul (β :=
      Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
        (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))
        (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)))
      r
      (CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
          (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f) :
        Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
          (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
            (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))
          (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
            (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)))
Tactic: obtain ⟨f, rfl⟩ := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Shift (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
R : Type u_1
inst_4 : Ring R
inst_5 : Linear.{u_1, v, u} R C
n : ℤ
X Y : HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)
r : R
f : X ⟶ Y
⊢ CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
      (HSMul.hSMul (β :=
        Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y))
        r
        (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f :
          Functor.obj (quotient C (ComplexShape.up ℤ)) X ⟶ Functor.obj (quotient C (ComplexShape.up ℤ)) Y)) =
    HSMul.hSMul (β :=
      Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
        (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))
        (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
          (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)))
      r
      (CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
          (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f) :
        Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
          (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
            (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))
          (Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n)
            (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) Y)))
have h₁ : Eq (α :=
  Functor.obj (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) X ⟶
    Functor.obj (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) Y)
  (CategoryStruct.comp (Y :=
    Functor.obj (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙ quotient C (ComplexShape.up ℤ))
      X)
    (NatTrans.app (Iso.inv (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) X)
    (CategoryTheory.Functor.map
        (shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n ⋙ quotient C (ComplexShape.up ℤ)) f ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n)) Y))
  (CategoryTheory.Functor.map
    (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) f)
Tactic: have h₁ := NatIso.naturality_1 ((HomotopyCategory.quotient _ _).commShiftIso n) f
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n i i' : ℤ
hi : n + i = i'
⊢ n + (up ℤ).prev i = (up ℤ).prev i'
have simp : n + (i - 1) = i' - 1
Tactic: simp only [prev]