-- Mathlib/Algebra/Homology/HomologySequence.lean
lemma δ_eq {A : C} (x₃ : A ⟶ S.X₃.X i) (hx₃ : x₃ ≫ S.X₃.d i j = 0)
    (x₂ : A ⟶ S.X₂.X i) (hx₂ : x₂ ≫ S.g.f i = x₃)
    (x₁ : A ⟶ S.X₁.X j) (hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j)
    (k : ι) (hk : c.next j = k) :
    S.X₃.liftCycles x₃ j (c.next_eq' hij) hx₃ ≫ S.X₃.homologyπ i ≫ hS.δ i j hij =
      S.X₁.liftCycles x₁ k hk (by
        have := hS.mono_f
        rw [← cancel_mono (S.f.f k), assoc, ← S.f.comm, reassoc_of% hx₁,
          d_comp_d, comp_zero, zero_comp]) ≫ S.X₁.homologyπ j

Proof state:
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{?u.136756, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
this : Mono S.f
⊢ x₁ ≫ S.X₁.d j k = 0

Tactic:
rw [← cancel_mono (S.f.f k), assoc, ← S.f.comm, reassoc_of% hx₁,
  d_comp_d, comp_zero, zero_comp]

Result:
no goals

Proof state:
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ S.X₃.liftCycles x₃ j ⋯ hx₃ ≫ S.X₃.homologyπ i ≫ hS.δ i j hij = S.X₁.liftCycles x₁ k hk ⋯ ≫ S.X₁.homologyπ j

Tactic:
simpa only [assoc] using hS.δ_eq' i j hij (S.X₃.liftCycles x₃ j
  (c.next_eq' hij) hx₃ ≫ S.X₃.homologyπ i)
  (x₂ ≫ S.X₂.pOpcycles i) (S.X₁.liftCycles x₁ k hk _)
    (by simp only [assoc, HomologicalComplex.p_opcyclesMap,
      HomologicalComplex.homology_π_ι,
      HomologicalComplex.liftCycles_i_assoc, reassoc_of% hx₂])
    (by rw [← cancel_mono (S.X₂.iCycles j), HomologicalComplex.liftCycles_comp_cyclesMap,
      HomologicalComplex.liftCycles_i, assoc, assoc, opcyclesToCycles_iCycles,
      HomologicalComplex.p_fromOpcycles, hx₁])

Result:
no goals

Proof state:
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ S.X₁.liftCycles x₁ k hk ⋯ ≫ HomologicalComplex.cyclesMap S.f j = (x₂ ≫ S.X₂.pOpcycles i) ≫ S.X₂.opcyclesToCycles i j

Tactic:
rw [← cancel_mono (S.X₂.iCycles j), HomologicalComplex.liftCycles_comp_cyclesMap,
HomologicalComplex.liftCycles_i, assoc, assoc, opcyclesToCycles_iCycles,
HomologicalComplex.p_fromOpcycles, hx₁]

Result:
no goals

Proof state:
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ (x₂ ≫ S.X₂.pOpcycles i) ≫ HomologicalComplex.opcyclesMap S.g i =
    (S.X₃.liftCycles x₃ j ⋯ hx₃ ≫ S.X₃.homologyπ i) ≫ S.X₃.homologyι i

Tactic:
simp only [assoc, HomologicalComplex.p_opcyclesMap,
HomologicalComplex.homology_π_ι,
HomologicalComplex.liftCycles_i_assoc, reassoc_of% hx₂]

Result:
no goals

Proof state:
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{?u.136756, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ x₁ ≫ S.X₁.d j k = 0

Tactic:
have := hS.mono_f

Result:
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{?u.136756, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
this : Mono S.f
⊢ x₁ ≫ S.X₁.d j k = 0