-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma δ_descCochain (n' : ℤ) (hn' : n + 1 = n') :
    δ n n' (descCochain φ α β h) =
      (fst φ).1.comp (δ m n α +
          n'.negOnePow • (Cochain.ofHom φ).comp β (zero_add n)) (by omega) +
      (snd φ).comp (δ n n' β) (zero_add n')

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ δ n n' (descCochain φ α β h) =
    (↑(fst φ)).comp (δ m n α + n'.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯ + (snd φ).comp (δ n n' β) ⋯

Tactic:
dsimp only [descCochain]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ δ n n' ((↑(fst φ)).comp α ⋯ + (snd φ).comp β ⋯) =
    (↑(fst φ)).comp (δ m n α + n'.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯ + (snd φ).comp (δ n n' β) ⋯

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ (↑(fst φ)).comp (δ m n α) ⋯ +
      ((snd φ).comp (δ n n' β) ⋯ + -(n.negOnePow • (↑(fst φ)).comp ((Cochain.ofHom φ).comp β ⋯) ⋯)) =
    (↑(fst φ)).comp (δ m n α) ⋯ + -(n.negOnePow • (↑(fst φ)).comp ((Cochain.ofHom φ).comp β ⋯) ⋯) +
      (snd φ).comp (δ n n' β) ⋯

Tactic:
abel

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ m + 1 = n

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ 1 + 1 = 2

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ δ n n' ((↑(fst φ)).comp α ⋯ + (snd φ).comp β ⋯) =
    (↑(fst φ)).comp (δ m n α + n'.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯ + (snd φ).comp (δ n n' β) ⋯

Tactic:
simp only [δ_add, Cochain.comp_add, δ_comp (fst φ).1 α _ 2 n n' hn' (by omega) (by omega),
  Cocycle.δ_eq_zero, Cochain.zero_comp, smul_zero, add_zero,
  δ_comp (snd φ) β (zero_add n) 1 n' n' hn' (zero_add 1) hn', δ_snd, Cochain.neg_comp,
  smul_neg, Cochain.comp_assoc_of_second_is_zero_cochain, Cochain.comp_units_smul, ← hn',
  Int.negOnePow_succ, Units.neg_smul, Cochain.comp_neg]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ (↑(fst φ)).comp (δ m n α) ⋯ +
      ((snd φ).comp (δ n n' β) ⋯ + -(n.negOnePow • (↑(fst φ)).comp ((Cochain.ofHom φ).comp β ⋯) ⋯)) =
    (↑(fst φ)).comp (δ m n α) ⋯ + -(n.negOnePow • (↑(fst φ)).comp ((Cochain.ofHom φ).comp β ⋯) ⋯) +
      (snd φ).comp (δ n n' β) ⋯

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.131283, u_1} C
inst✝³ : Category.{?u.131287, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ 1 + n = n'

Tactic:
omega

Result:
no goals