-- Mathlib/Algebra/Homology/ConcreteCategory.lean
lemma δ_apply (x₃ : (forget₂ C Ab).obj (S.X₃.X i))
    (hx₃ : (forget₂ C Ab).map (S.X₃.d i j) x₃ = 0)
    (x₂ : (forget₂ C Ab).obj (S.X₂.X i)) (hx₂ : (forget₂ C Ab).map (S.g.f i) x₂ = x₃)
    (x₁ : (forget₂ C Ab).obj (S.X₁.X j))
    (hx₁ : (forget₂ C Ab).map (S.f.f j) x₁ = (forget₂ C Ab).map (S.X₂.d i j) x₂)
    (k : ι) (hk : c.next j = k) :
    (forget₂ C Ab).map (hS.δ i j hij)
      ((forget₂ C Ab).map (S.X₃.homologyπ i) (S.X₃.cyclesMk x₃ j (c.next_eq' hij) hx₃)) =
        (forget₂ C Ab).map (S.X₁.homologyπ j) (S.X₁.cyclesMk x₁ k hk (by
          have := hS.mono_f
          apply (Preadditive.mono_iff_injective (S.f.f k)).1 inferInstance
          rw [← ConcreteCategory.forget₂_comp_apply, ← HomologicalComplex.Hom.comm,
            ConcreteCategory.forget₂_comp_apply, hx₁, ← ConcreteCategory.forget₂_comp_apply,
            HomologicalComplex.d_comp_d, Functor.map_zero, map_zero]; rfl))

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))
hx₃ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.d i j))) x₃ = 0
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.g.f i))) x₂ = x₃
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
hk : c.next j = k
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map (hS.δ i j hij)))
      ((ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.homologyπ i))) (S.X₃.cyclesMk x₃ j ⋯ hx₃)) =
    (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₁.homologyπ j))) (S.X₁.cyclesMk x₁ k hk ⋯)

Tactic:
refine hS.δ_apply' i j hij _ ((forget₂ C Ab).map (S.X₂.pOpcycles i) x₂) _ ?_ ?_

Result:
case refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))
hx₃ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.d i j))) x₃ = 0
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.g.f i))) x₂ = x₃
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
hk : c.next j = k
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map (HomologicalComplex.opcyclesMap S.g i)))
      ((ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.pOpcycles i))) x₂) =
    (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.homologyι i)))
      ((ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.homologyπ i))) (S.X₃.cyclesMk x₃ j ⋯ hx₃))

case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))
hx₃ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.d i j))) x₃ = 0
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.g.f i))) x₂ = x₃
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
hk : c.next j = k
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map (HomologicalComplex.cyclesMap S.f j))) (S.X₁.cyclesMk x₁ k hk ⋯) =
    (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.opcyclesToCycles i j)))
      ((ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.pOpcycles i))) x₂)

Proof state:
case refine_2.a
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))
hx₃ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.d i j))) x₃ = 0
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.g.f i))) x₂ = x₃
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
hk : c.next j = k
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂ =
    (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.iCycles j)))
      ((ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.opcyclesToCycles i j)))
        ((ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.pOpcycles i))) x₂))

Tactic:
conv_rhs =>
  rw [← ConcreteCategory.forget₂_comp_apply, ← ConcreteCategory.forget₂_comp_apply,
    HomologicalComplex.pOpcycles_opcyclesToCycles_assoc, HomologicalComplex.toCycles_i]

Result:
no goals