awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ℤ).next i = (up ℤ).next i'
have simp : n + (i + 1) = i' + 1
Tactic: simp only [next]
-- 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
a : ℤ
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C 0 a a ⋯)) K =
    CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
      (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v_1, u_1, 0} C ℤ) ℤ)) K)
have h₁ : (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C 0 a a sorry)) K).τ₁ =
  ShortComplex.Hom.τ₁
    (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
      (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v_1, u_1, 0} C ℤ) ℤ)) K))
Tactic: ext
-- 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
a : ℤ
K : CochainComplex.{v_1, u_1, 0} C ℤ
h₁ :
  (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C 0 a a ⋯)) K).τ₁ =
    ShortComplex.Hom.τ₁
      (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v_1, u_1, 0} C ℤ) ℤ)) K))
⊢ NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C 0 a a ⋯)) K =
    CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
      (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v_1, u_1, 0} C ℤ) ℤ)) K)
have h₂ : (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C 0 a a sorry)) K).τ₂ =
  ShortComplex.Hom.τ₂
    (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
      (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v_1, u_1, 0} C ℤ) ℤ)) K))
Tactic: ext
-- 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
a : ℤ
K : CochainComplex.{v_1, u_1, 0} C ℤ
h₁ :
  (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C 0 a a ⋯)) K).τ₁ =
    ShortComplex.Hom.τ₁
      (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v_1, u_1, 0} C ℤ) ℤ)) K))
h₂ :
  (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C 0 a a ⋯)) K).τ₂ =
    ShortComplex.Hom.τ₂
      (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v_1, u_1, 0} C ℤ) ℤ)) K))
⊢ NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C 0 a a ⋯)) K =
    CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
      (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v_1, u_1, 0} C ℤ) ℤ)) K)
have h₃ : (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C 0 a a sorry)) K).τ₃ =
  ShortComplex.Hom.τ₃
    (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
      (NatTrans.app (Iso.hom (shiftFunctorZero (CochainComplex.{v_1, u_1, 0} C ℤ) ℤ)) K))
Tactic: ext
-- 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 m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ mn + a = a''
have rw : mn + a = m + a'
Tactic: rw [← ha'', ← ha', ← add_assoc, hmn]
-- 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 m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
rw : mn + a = m + a'
⊢ mn + a = a''
have rw₁ : mn + a = m + (n + a)
Tactic: rw [← ha'', ← ha', ← add_assoc, hmn]
-- 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 m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
rw : mn + a = m + a'
rw₁ : mn + a = m + (n + a)
⊢ mn + a = a''
have rw₂ : mn + a = m + n + a
Tactic: rw [← ha'', ← ha', ← add_assoc, hmn]
-- 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 m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
rw : mn + a = m + a'
rw₁ : mn + a = m + (n + a)
rw₂ : mn + a = m + n + a
⊢ mn + a = a''
have rw₃ : mn + a = mn + a
Tactic: rw [← ha'', ← ha', ← add_assoc, hmn]
-- 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 m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' ⋯)) K =
    CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
      NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K
have h₁ : (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' sorry)) K).τ₁ =
  (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
      NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K).τ₁
Tactic: ext
-- 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 m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
h₁ :
  (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' ⋯)) K).τ₁ =
    (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
          NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K).τ₁
⊢ NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' ⋯)) K =
    CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
      NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K
have h₂ : (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' sorry)) K).τ₂ =
  (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
      NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K).τ₂
Tactic: ext
-- 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 m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
h₁ :
  (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' ⋯)) K).τ₁ =
    (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
          NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K).τ₁
h₂ :
  (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' ⋯)) K).τ₂ =
    (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
          NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K).τ₂
⊢ NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' ⋯)) K =
    CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
      NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K
have h₃ : (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' sorry)) K).τ₃ =
  (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
      NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K).τ₃
Tactic: ext
-- 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 m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' ⋯)) K).τ₁ =
    (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
          NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K).τ₁
have h₁ : mn.negOnePow • (XIsoOfEq K sorry).hom =
  Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K)
      ((up ℤ).prev a) ≫
    (n.negOnePow •
        (XIsoOfEq (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) sorry).hom) ≫
      (m.negOnePow • (XIsoOfEq K sorry).hom)
Tactic: dsimp
-- 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 m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' ⋯)) K).τ₂ =
    (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
          NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K).τ₂
have h₂ : (XIsoOfEq K sorry).hom =
  Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) a ≫
    (XIsoOfEq (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) sorry).hom ≫
      (XIsoOfEq K sorry).hom
Tactic: dsimp
-- 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 m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ (NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C mn a a'' ⋯)) K).τ₃ =
    (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
          (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K) ≫
        NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C n a a' ha'))
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) ≫
          NatTrans.app (Iso.hom (shiftShortComplexFunctorIso C m a' a'' ha'')) K).τ₃
have h₃ : mn.negOnePow • (XIsoOfEq K sorry).hom =
  Hom.f (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' (CochainComplex.{v_1, u_1, 0} C ℤ) m n mn hmn)) K)
      ((up ℤ).next a) ≫
    (n.negOnePow •
        (XIsoOfEq (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) m) K) sorry).hom) ≫
      (m.negOnePow • (XIsoOfEq K sorry).hom)
Tactic: dsimp
-- 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
inst_2 : CategoryWithHomology.{v_1, u_1} C
a : ℤ
⊢ Eq (α :=
    Iso (C := HomologicalComplex.{v_1, u_1, 0} C (up ℤ) ⥤ C)
      (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (A := ℤ) 0 ⋙ homologyFunctor C (up ℤ) a)
      (homologyFunctor C (up ℤ) a))
    (ShiftSequence.shiftIso C 0 a a ⋯)
    (Functor.isoWhiskerRight (shiftFunctorZero (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) ℤ)
        (homologyFunctor C (up ℤ) a) ≪≫
      Functor.leftUnitor (homologyFunctor C (up ℤ) a))
have w : ∀ (K : HomologicalComplex.{v_1, u_1, 0} C (up ℤ)),
  Eq (α :=
    Functor.obj
        (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (A := ℤ) 0 ⋙
          homologyFunctor C (up ℤ) a)
        K ⟶
      Functor.obj (homologyFunctor C (up ℤ) a) K)
    (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C 0 a a sorry)) K)
    (NatTrans.app
      (Iso.hom
        (Functor.isoWhiskerRight (shiftFunctorZero (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) ℤ)
            (homologyFunctor C (up ℤ) a) ≪≫
          Functor.leftUnitor (homologyFunctor C (up ℤ) a)))
      K)
Tactic: ext K
-- 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
inst_2 : CategoryWithHomology.{v_1, u_1} C
a : ℤ
K : HomologicalComplex.{v_1, u_1, 0} C (up ℤ)
⊢ Eq (α :=
    Functor.obj
        (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (A := ℤ) 0 ⋙
          homologyFunctor C (up ℤ) a)
        K ⟶
      Functor.obj (homologyFunctor C (up ℤ) a) K)
    (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C 0 a a ⋯)) K)
    (NatTrans.app
      (Iso.hom
        (Functor.isoWhiskerRight (shiftFunctorZero (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) ℤ)
            (homologyFunctor C (up ℤ) a) ≪≫
          Functor.leftUnitor (homologyFunctor C (up ℤ) a)))
      K)
have w : Eq (α :=
  (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (A := ℤ) 0) K).homology a ⟶
    K.homology a)
  (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C 0 a a sorry)) K :
    Functor.obj
        (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (A := ℤ) 0 ⋙
          homologyFunctor C (up ℤ) a)
        K ⟶
      Functor.obj (homologyFunctor C (up ℤ) a) K)
  (ShortComplex.homologyMap
      (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (shiftFunctorZero (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) ℤ)) K)) ≫
    𝟙 (K.homology a))
Tactic: dsimp [homologyMap]
-- 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
inst_2 : CategoryWithHomology.{v_1, u_1} C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
⊢ Eq (α :=
    Iso (C := HomologicalComplex.{v_1, u_1, 0} C (up ℤ) ⥤ C)
      (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (m + n) ⋙ homologyFunctor C (up ℤ) a)
      (homologyFunctor C (up ℤ) a''))
    (ShiftSequence.shiftIso C (m + n) a a'' ⋯)
    (Functor.isoWhiskerRight (shiftFunctorAdd (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m n)
        (homologyFunctor C (up ℤ) a) ≪≫
      Functor.associator (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m)
          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) (homologyFunctor C (up ℤ) a) ≪≫
        Functor.isoWhiskerLeft (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m)
            (ShiftSequence.shiftIso C n a a' ha') ≪≫
          ShiftSequence.shiftIso C m a' a'' ha'')
have w : ∀ (K : HomologicalComplex.{v_1, u_1, 0} C (up ℤ)),
  Eq (α :=
    Functor.obj
        (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (m + n) ⋙ homologyFunctor C (up ℤ) a)
        K ⟶
      Functor.obj (homologyFunctor C (up ℤ) a'') K)
    (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C (m + n) a a'' sorry)) K)
    (NatTrans.app
      (Iso.hom
        (Functor.isoWhiskerRight (shiftFunctorAdd (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m n)
            (homologyFunctor C (up ℤ) a) ≪≫
          Functor.associator (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m)
              (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n)
              (homologyFunctor C (up ℤ) a) ≪≫
            Functor.isoWhiskerLeft (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m)
                (ShiftSequence.shiftIso C n a a' ha') ≪≫
              ShiftSequence.shiftIso C m a' a'' ha''))
      K)
Tactic: ext K
-- 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
inst_2 : CategoryWithHomology.{v_1, u_1} C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : HomologicalComplex.{v_1, u_1, 0} C (up ℤ)
⊢ Eq (α :=
    Functor.obj
        (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (m + n) ⋙ homologyFunctor C (up ℤ) a)
        K ⟶
      Functor.obj (homologyFunctor C (up ℤ) a'') K)
    (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C (m + n) a a'' ⋯)) K)
    (NatTrans.app
      (Iso.hom
        (Functor.isoWhiskerRight (shiftFunctorAdd (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m n)
            (homologyFunctor C (up ℤ) a) ≪≫
          Functor.associator (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m)
              (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n)
              (homologyFunctor C (up ℤ) a) ≪≫
            Functor.isoWhiskerLeft (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m)
                (ShiftSequence.shiftIso C n a a' ha') ≪≫
              ShiftSequence.shiftIso C m a' a'' ha''))
      K)
have w : Eq (α :=
  (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (m + n)) K).homology a ⟶
    K.homology a'')
  (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C (m + n) a a'' sorry)) K :
    Functor.obj
        (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (m + n) ⋙ homologyFunctor C (up ℤ) a)
        K ⟶
      Functor.obj (homologyFunctor C (up ℤ) a'') K)
  (ShortComplex.homologyMap
      (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
        (NatTrans.app (Iso.hom (shiftFunctorAdd (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m n)) K)) ≫
    𝟙
        ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n)
              (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m) K)).homology
          a) ≫
      CategoryStruct.comp (Y :=
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m) K).homology a')
        (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C n a a' ha'))
            (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m) K) :
          Functor.obj
              (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n ⋙ homologyFunctor C (up ℤ) a)
              (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m) K) ⟶
            Functor.obj (homologyFunctor C (up ℤ) a')
              (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m) K))
        (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C m a' a'' ha'')) K))
Tactic: dsimp [homologyMap]
-- 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
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n i j : ℤ
h : n + i = j
⊢ QuasiIsoAt (K := Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) K)
      (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) φ) i ↔
    QuasiIsoAt φ j
have simp : IsIso (X := (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) K).homology i)
    (Y := (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) L).homology i)
    (homologyMap
      (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) φ) i) ↔
  IsIso (X := homology K j) (Y := homology L j) (homologyMap φ j)
Tactic: simp only [quasiIsoAt_iff_isIso_homologyMap]
-- 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
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
⊢ QuasiIso (K := Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) K)
      (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) φ) ↔
    QuasiIso φ
have simp : (∀ (i : ℤ), QuasiIsoAt φ (n + i)) ↔ ∀ (i : ℤ), QuasiIsoAt φ i
Tactic: simp only [quasiIso_iff, fun i ↦ quasiIsoAt_shift_iff φ n i _ rfl]
-- 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
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
⊢ (∀ (i : ℤ), QuasiIsoAt φ (n + i)) ↔ ∀ (i : ℤ), QuasiIsoAt φ i
have mp : (∀ (i : ℤ), QuasiIsoAt φ (n + i)) → ∀ (i : ℤ), QuasiIsoAt φ i
Tactic: constructor
-- 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
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
mp : (∀ (i : ℤ), QuasiIsoAt φ (n + i)) → ∀ (i : ℤ), QuasiIsoAt φ i
⊢ (∀ (i : ℤ), QuasiIsoAt φ (n + i)) ↔ ∀ (i : ℤ), QuasiIsoAt φ i
have mpr : (∀ (i : ℤ), QuasiIsoAt φ i) → ∀ (i : ℤ), QuasiIsoAt φ (n + i)
Tactic: constructor