-- Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean
lemma homologySequenceδ_triangleh (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) :
    (homologyFunctor C (up ℤ) 0).homologySequenceδ (triangleh S.f) n₀ n₁ h =
      (homologyFunctorFactors C (up ℤ) n₀).hom.app _ ≫
        HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫
          (homologyFunctorFactors C (up ℤ) n₁).inv.app _

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ 1 + n₀ = n₁

Tactic:
omega

Result:
no goals

Proof state:
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ yoneda.map
      ((homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
        (homologyFunctor C (up ℤ) 0).homologySequenceδ
            (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f))
              ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ ((quotient C (up ℤ)).commShiftIso 1).hom.app S.X₁))
            n₀ n₁ h ≫
          (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁) =
    yoneda.map
      (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
        hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁))

Tactic:
ext ⟨A⟩ (x : A ⟶ _)

Result:
case a.w.h.op.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
⊢ (yoneda.map
          ((homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
            (homologyFunctor C (up ℤ) 0).homologySequenceδ
                (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f))
                  ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ ((quotient C (up ℤ)).commShiftIso 1).hom.app S.X₁))
                n₀ n₁ h ≫
              (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁)).app
      (Opposite.op A) x =
    (yoneda.map
          (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
            hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁))).app
      (Opposite.op A) x

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ (-a) ≫ S.f.f n₁ = b ≫ S.X₂.d n₀ n₁

Tactic:
simp only [neg_comp, neg_eq_iff_add_eq_zero, w.2]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w✝ ≫ (mappingCone S.f).homologyπ n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ (up ℤ).Rel n₀ n₁

Tactic:
simpa using h

Result:
no goals

Proof state:
case a.w.h.op.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
⊢ (yoneda.map
          ((homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
            (homologyFunctor C (up ℤ) 0).homologySequenceδ
                (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f))
                  ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ ((quotient C (up ℤ)).commShiftIso 1).hom.app S.X₁))
                n₀ n₁ h ≫
              (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁)).app
      (Opposite.op A) x =
    (yoneda.map
          (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
            hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁))).app
      (Opposite.op A) x

Tactic:
obtain ⟨A', π, _, x', w, hx'⟩ :=
  (mappingCone S.f).eq_liftCycles_homologyπ_up_to_refinements x n₁ (by simpa using h)

Result:
case a.w.h.op.h.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' : π ≫ x = (mappingCone S.f).liftCycles x' n₁ ⋯ w ≫ (mappingCone S.f).homologyπ n₀
⊢ (yoneda.map
          ((homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
            (homologyFunctor C (up ℤ) 0).homologySequenceδ
                (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f))
                  ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ ((quotient C (up ℤ)).commShiftIso 1).hom.app S.X₁))
                n₀ n₁ h ≫
              (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁)).app
      (Opposite.op A) x =
    (yoneda.map
          (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
            hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁))).app
      (Opposite.op A) x