-- Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean
@[reassoc]
lemma liftCycles_shift_homologyπ
    (K : CochainComplex C ℤ) {A : C} {n i : ℤ} (f : A ⟶ (K⟦n⟧).X i) (j : ℤ)
    (hj : (up ℤ).next i = j) (hf : f ≫ (K⟦n⟧).d i j = 0) (i' : ℤ) (hi' : n + i = i') (j' : ℤ)
    (hj' : (up ℤ).next i' = j') :
    (K⟦n⟧).liftCycles f j hj hf ≫ (K⟦n⟧).homologyπ i =
      K.liftCycles (f ≫ (K.shiftFunctorObjXIso n i i' (by omega)).hom) j' hj' (by
        simp only [next] at hj hj'
        obtain rfl : i' = i + n

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : (up ℤ).next i = j
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj' : (up ℤ).next i' = j'
⊢ (sc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i).liftCycles f ⋯ ≫
      (sc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i).homologyπ =
    ((shiftFunctor C n ⋙ shortComplexFunctor C (up ℤ) i).obj K).liftCycles f ⋯ ≫
      ((shiftFunctor C n ⋙ shortComplexFunctor C (up ℤ) i).obj K).homologyπ

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{?u.81256, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hf : f ≫ (n.negOnePow • K.d (i + n) (j + n)) = 0
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
⊢ (f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n) = 0

Tactic:
simp only [Linear.comp_units_smul] at hf

Result:
C : Type u_1
inst✝² : Category.{?u.81256, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
hf : n.negOnePow • f ≫ K.d (i + n) (j + n) = 0
⊢ (f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n) = 0

Proof state:
C : Type u_1
inst✝² : Category.{?u.81256, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : (up ℤ).next i = j
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj' : (up ℤ).next i' = j'
⊢ (f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) ≫ K.d i' j' = 0

Tactic:
simp only [next] at hj hj'

Result:
C : Type u_1
inst✝² : Category.{?u.81256, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj : i + 1 = j
hj' : i' + 1 = j'
⊢ (f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) ≫ K.d i' j' = 0

Proof state:
C : Type u_1
inst✝² : Category.{?u.81256, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
hf : n.negOnePow • f ≫ K.d (i + n) (j + n) = 0
⊢ 1 • (f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n) = 0

Tactic:
rw [← Int.units_mul_self n.negOnePow, mul_smul, comp_id, hf, smul_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : (up ℤ).next i = j
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj' : (up ℤ).next i' = j'
⊢ liftCycles ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) f j hj hf ≫
      homologyπ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i =
    liftCycles K (f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) j' hj' ⋯ ≫
      homologyπ K i' ≫ ((homologyFunctor C (up ℤ) 0).shiftIso n i i' hi').inv.app K

Tactic:
simp only [liftCycles, homologyπ,
  shiftFunctorObjXIso, Functor.shiftIso, Functor.ShiftSequence.shiftIso,
  ShiftSequence.shiftIso_inv_app, ShortComplex.homologyπ_naturality,
  ShortComplex.liftCycles_comp_cyclesMap_assoc, shiftShortComplexFunctorIso_inv_app_τ₂,
  assoc, Iso.hom_inv_id, comp_id]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : (up ℤ).next i = j
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj' : (up ℤ).next i' = j'
⊢ (sc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i).liftCycles f ⋯ ≫
      (sc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i).homologyπ =
    ((shiftFunctor C n ⋙ shortComplexFunctor C (up ℤ) i).obj K).liftCycles f ⋯ ≫
      ((shiftFunctor C n ⋙ shortComplexFunctor C (up ℤ) i).obj K).homologyπ

Proof state:
C : Type u_1
inst✝² : Category.{?u.81256, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
j' : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j'
⊢ (f ≫ (K.shiftFunctorObjXIso n i (i + n) ⋯).hom) ≫ K.d (i + n) j' = 0

Tactic:
obtain rfl : j' = j + n := by omega

Result:
C : Type u_1
inst✝² : Category.{?u.81256, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
⊢ (f ≫ (K.shiftFunctorObjXIso n i (i + n) ⋯).hom) ≫ K.d (i + n) (j + n) = 0

Proof state:
C : Type u_1
inst✝² : Category.{?u.81256, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj : i + 1 = j
hj' : i' + 1 = j'
⊢ i' = i + n

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{?u.81256, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
j' : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j'
⊢ j' = j + n

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{?u.81256, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
⊢ (f ≫ (K.shiftFunctorObjXIso n i (i + n) ⋯).hom) ≫ K.d (i + n) (j + n) = 0

Tactic:
dsimp at hf ⊢

Result:
C : Type u_1
inst✝² : Category.{?u.81256, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hf : f ≫ (n.negOnePow • K.d (i + n) (j + n)) = 0
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
⊢ (f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n) = 0