Module: Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
w✝⁵ w✝⁴ w✝³ : CochainComplex C ℤ
f : w✝⁵ ⟶ w✝⁴
g : w✝⁴ ⟶ w✝³
w✝² w✝¹ w✝ : CochainComplex C ℤ
f' : w✝² ⟶ w✝¹
g' : w✝¹ ⟶ w✝
φ : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g'
⊢ (ComposableArrows.functorArrows (CochainComplex C ℤ) 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙
            composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)).map
        φ ≫
      ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj
          (CochainComplex.mappingConeCompTriangle
            ((ComposableArrows.mk₂ f' g').map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
            ((ComposableArrows.mk₂ f' g').map' 1 2 spectralObjectMappingCone._proof_2
              spectralObjectMappingCone._proof_3))).mor₃ =
    ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj
          (CochainComplex.mappingConeCompTriangle
            ((ComposableArrows.mk₂ f g).map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
            ((ComposableArrows.mk₂ f g).map' 1 2 spectralObjectMappingCone._proof_2
              spectralObjectMappingCone._proof_3))).mor₃ ≫
      (ComposableArrows.functorArrows (CochainComplex C ℤ) 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)) ⋙
              shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        φ

Tactic:
have eq := CochainComplex.mappingConeCompTriangle_mor₃_naturality f g f' g' φ

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
w✝⁵ w✝⁴ w✝³ : CochainComplex C ℤ
f : w✝⁵ ⟶ w✝⁴
g : w✝⁴ ⟶ w✝³
w✝² w✝¹ w✝ : CochainComplex C ℤ
f' : w✝² ⟶ w✝¹
g' : w✝¹ ⟶ w✝
φ : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g'
eq :
  map g g' (φ.app 1) (φ.app 2) ⋯ ≫ (CochainComplex.mappingConeCompTriangle f' g').mor₃ =
    (CochainComplex.mappingConeCompTriangle f g).mor₃ ≫
      (shiftFunctor (CochainComplex C ℤ) 1).map (map f f' (φ.app 0) (φ.app 1) ⋯)
⊢ (ComposableArrows.functorArrows (CochainComplex C ℤ) 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙
            composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)).map
        φ ≫
      ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj
          (CochainComplex.mappingConeCompTriangle
            ((ComposableArrows.mk₂ f' g').map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
            ((ComposableArrows.mk₂ f' g').map' 1 2 spectralObjectMappingCone._proof_2
              spectralObjectMappingCone._proof_3))).mor₃ =
    ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj
          (CochainComplex.mappingConeCompTriangle
            ((ComposableArrows.mk₂ f g).map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
            ((ComposableArrows.mk₂ f g).map' 1 2 spectralObjectMappingCone._proof_2
              spectralObjectMappingCone._proof_3))).mor₃ ≫
      (ComposableArrows.functorArrows (CochainComplex C ℤ) 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)) ⋙
              shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        φ