-- Mathlib/Algebra/Homology/TotalComplexShift.lean
@[reassoc]
lemma D₁_totalShift₁XIso_hom (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') :
    ((shiftFunctor₁ C x).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
      x.negOnePow • ((K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁')

Proof state:
case pos.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      ((shiftFunctor₁ C x).obj K).D₁ (up ℤ) n₀ n₁ ≫
        ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq => K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (x.negOnePow •
        (((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq => K.ιTotal (up ℤ) (p + x) q n₀' ⋯) ≫ K.D₁ (up ℤ) n₀' n₁')

Tactic:
rw [ι_D₁_assoc, Linear.comp_units_smul, ι_totalDesc_assoc, ι_D₁,
  ((shiftFunctor₁ C x).obj K).d₁_eq _ rfl _ _ (by dsimp; omega),
  K.d₁_eq _ (show p + x + 1 = p + 1 + x by omega) _ _ (by dsimp; omega)]

Result:
case pos.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (((up ℤ).ε₁ (up ℤ) (up ℤ) (p, q) •
        (((shiftFunctor₁ C x).obj K).d p (p + 1)).f q ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (p + 1) q n₁ ⋯) ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq => K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    x.negOnePow •
      (up ℤ).ε₁ (up ℤ) (up ℤ) (p + x, q) • (K.d (p + x) (p + 1 + x)).f q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯

Proof state:
case pos.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (((up ℤ).ε₁ (up ℤ) (up ℤ) (p, q) •
        (((shiftFunctor₁ C x).obj K).d p (p + 1)).f q ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (p + 1) q n₁ ⋯) ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq => K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    x.negOnePow •
      (up ℤ).ε₁ (up ℤ) (up ℤ) (p + x, q) • (K.d (p + x) (p + 1 + x)).f q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯

Tactic:
dsimp

Result:
case pos.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ ((1 • (x.negOnePow • (K.d (p + x) (p + 1 + x)).f q) ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (p + 1) q n₁ ⋯) ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq => K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    x.negOnePow • 1 • (K.d (p + x) (p + 1 + x)).f q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯

Proof state:
case neg.h₁₂
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : ¬(up ℤ).Rel n₀ n₁
h' : (up ℤ).Rel n₀' n₁'
⊢ (up ℤ).Rel n₀ n₁

Tactic:
dsimp at h' ⊢

Result:
case neg.h₁₂
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : ¬(up ℤ).Rel n₀ n₁
h' : n₀' + 1 = n₁'
⊢ n₀ + 1 = n₁

Proof state:
case neg.h₁₂
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : ¬(up ℤ).Rel n₀ n₁
⊢ ¬(up ℤ).Rel n₀' n₁'

Tactic:
intro h'

Result:
case neg.h₁₂
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : ¬(up ℤ).Rel n₀ n₁
h' : (up ℤ).Rel n₀' n₁'
⊢ False

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ p + x + 1 = p + 1 + x

Tactic:
omega

Result:
no goals

Proof state:
case pos.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : (up ℤ).Rel n₀ n₁
⊢ ∀ (i₁ i₂ : ℤ) (hi : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n₀),
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n₀ hi ≫
        ((shiftFunctor₁ C x).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
      ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n₀ hi ≫
        (x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁')

Tactic:
intro p q hpq

Result:
case pos.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : (up ℤ).Rel n₀ n₁
p q : ℤ
hpq : (up ℤ).π (up ℤ) (up ℤ) (p, q) = n₀
⊢ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      ((shiftFunctor₁ C x).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁')

Proof state:
case neg.h₁₂
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : ¬(up ℤ).Rel n₀ n₁
h' : n₀' + 1 = n₁'
⊢ n₀ + 1 = n₁

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
⊢ ((shiftFunctor₁ C x).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁'

Tactic:
by_cases h : (up ℤ).Rel n₀ n₁

Result:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : (up ℤ).Rel n₀ n₁
⊢ ((shiftFunctor₁ C x).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁'

case neg
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : ¬(up ℤ).Rel n₀ n₁
⊢ ((shiftFunctor₁ C x).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁'

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ p + 1 + x + q = n₁'

Tactic:
omega

Result:
no goals