-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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 L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
change :
  Eq (α :=
    K.X j' ⟶
      ShortComplex.RightHomologyData.Q (S := Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
        (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
          (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj))))
    (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j') (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) :
      K.X j' ⟶
        ShortComplex.RightHomologyData.Q (S := Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj))))
    (ShortComplex.Hom.τ₂ (CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)) ≫
        ShortComplex.RightHomologyData.p
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj))) :
      (Functor.obj (shortComplexFunctor C c' j') K).X₂ ⟶
        ShortComplex.RightHomologyData.Q (S := Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj))))
⊢ Eq (α :=
    (Functor.obj (shortComplexFunctor C c' j') K).X₂ ⟶
      ShortComplex.RightHomologyData.Q (S := Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
        (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
          (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj))))
    ((ShortComplex.RightHomologyData.canonical (K.sc j')).p ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) :
      (Functor.obj (shortComplexFunctor C c' j') K).X₂ ⟶
        ShortComplex.RightHomologyData.Q (S := Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj))))
    (ShortComplex.Hom.τ₂ (CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)) ≫
        ShortComplex.RightHomologyData.p
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj))) :
      (Functor.obj (shortComplexFunctor C c' j') K).X₂ ⟶
        ShortComplex.RightHomologyData.Q (S := Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj))))

Tactic:
change K.pOpcycles j' ≫ _ = _

Premises used: HomologicalComplex.pOpcycles