-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
lemma δ_shape (hnm : ¬ n + 1 = m) (z : Cochain F G n) : δ n m z = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
⊢ δ n m z = 0

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ (δ n m z).v p q hpq = Cochain.v 0 p q hpq

Proof state:
case h.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ ¬p + 1 = p + m - n

Tactic:
exact fun _ => hnm (by omega)

Result:
no goals

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ (Cochain.mk fun p q hpq => z.v p (p + n) ⋯ ≫ G.d (p + n) q + m.negOnePow • F.d p (p + m - n) ≫ z.v (p + m - n) q ⋯).v
      p q hpq =
    Cochain.v 0 p q hpq

Tactic:
rw [Cochain.mk_v, Cochain.zero_v, F.shape, G.shape, comp_zero, zero_add, zero_comp, smul_zero]

Result:
case h.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ ¬(ComplexShape.up ℤ).Rel (p + n) q

case h.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ ¬(ComplexShape.up ℤ).Rel p (p + m - n)

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ (δ n m z).v p q hpq = Cochain.v 0 p q hpq

Tactic:
dsimp only [δ]

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ (Cochain.mk fun p q hpq => z.v p (p + n) ⋯ ≫ G.d (p + n) q + m.negOnePow • F.d p (p + m - n) ≫ z.v (p + m - n) q ⋯).v
      p q hpq =
    Cochain.v 0 p q hpq

Proof state:
case h.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ ¬(ComplexShape.up ℤ).Rel p (p + m - n)

Tactic:
simp only [ComplexShape.up_Rel]

Result:
case h.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ ¬p + 1 = p + m - n

Proof state:
case h.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ ¬(ComplexShape.up ℤ).Rel (p + n) q

case h.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ ¬(ComplexShape.up ℤ).Rel p (p + m - n)

Tactic:
all_goals
  simp only [ComplexShape.up_Rel]
  exact fun _ => hnm (by omega)

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
x✝ : p + 1 = p + m - n
⊢ n + 1 = m

Tactic:
omega

Result:
no goals