-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
rw :
  Eq (α := K.cycles j' ⟶ K.homology j')
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (K.homologyπ j' ≫ Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
rw₁ :
  Eq (α := K.cycles j' ⟶ K.homology j')
    (K.homologyπ j' ≫
      CategoryStruct.comp (Y := (K.restriction e).homology j)
        (Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
        (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
rw₂ :
  Eq (α := K.cycles j' ⟶ K.homology j')
    (K.homologyπ j' ≫
      CategoryStruct.comp (Y := (K.restriction e).homology j)
        (Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
        (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
    (CategoryStruct.comp (Y := (K.restriction e).cycles j) (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk''))
      ((K.restriction e).homologyπ j ≫ Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
rw₃ :
  K.homologyπ j' ≫ 𝟙 (K.homology j') =
    CategoryStruct.comp (Y := (K.restriction e).cycles j) (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk''))
      ((K.restriction e).homologyπ j ≫ Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
rw₄ :
  K.homologyπ j' ≫ 𝟙 (K.homology j') =
    CategoryStruct.comp (Y := (K.restriction e).cycles j) (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk''))
      (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ K.homologyπ j')
⊢ Eq (α := K.cycles j' ⟶ (K.restriction e).homology j)
    (K.homologyπ j' ≫ Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
    (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
have rw₅ : Eq (α := K.cycles j' ⟶ K.homology j') (K.homologyπ j')
  (CategoryStruct.comp (Y := (K.restriction e).cycles j) (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk''))
    (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ K.homologyπ j'))
Tactic: rw [← cancel_mono (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom,
    assoc, assoc, Iso.inv_hom_id, homologyπ_restrictionHomologyIso_hom, comp_id,
    Iso.inv_hom_id_assoc]