Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: C : Type u_1
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F : HomologicalComplex C c
inst✝⁸ : DecidableRel c.Rel
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
H : C ⥤ D
inst✝⁵ : H.Additive
inst✝⁴ : ∀ (i : ι), HasBinaryBiproduct (F.X i) (F.X i)
inst✝³ : HasHomotopyCofiber (biprod.lift (𝟙 F) (-𝟙 F))
inst✝² :
  ∀ (i : ι), HasBinaryBiproduct (((H.mapHomologicalComplex c).obj F).X i) (((H.mapHomologicalComplex c).obj F).X i)
inst✝¹ :
  HasHomotopyCofiber (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ (H.mapHomologicalComplex c).map biprod.inr ≫
      (H.mapHomologicalComplex c).map (homotopyCofiber.inr (biprod.lift (𝟙 F) (-𝟙 F))) ≫
        (homotopyCofiber.mapHomologicalComplexObjIso (biprod.lift (𝟙 F) (-𝟙 F)) H).hom ≫
          homotopyCofiber.desc ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))
            (biprod.lift ((H.mapHomologicalComplex c).map biprod.fst) ((H.mapHomologicalComplex c).map biprod.snd) ≫
              homotopyCofiber.inr
                (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F))))
            ((Homotopy.ofEq ⋯).trans
              (((homotopyCofiber.inrCompHomotopy
                        (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))
                        hc).compLeft
                    (𝟙 ((H.mapHomologicalComplex c).obj F))).trans
                (Homotopy.ofEq ⋯))) =
    biprod.inr ≫
      homotopyCofiber.inr (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))

Tactic:
homotopyCofiber.inr_mapHomologicalComplexObjIso_hom_assoc,

Goal state after:
C : Type u_1
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F : HomologicalComplex C c
inst✝⁸ : DecidableRel c.Rel
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
H : C ⥤ D
inst✝⁵ : H.Additive
inst✝⁴ : ∀ (i : ι), HasBinaryBiproduct (F.X i) (F.X i)
inst✝³ : HasHomotopyCofiber (biprod.lift (𝟙 F) (-𝟙 F))
inst✝² :
  ∀ (i : ι), HasBinaryBiproduct (((H.mapHomologicalComplex c).obj F).X i) (((H.mapHomologicalComplex c).obj F).X i)
inst✝¹ :
  HasHomotopyCofiber (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ (H.mapHomologicalComplex c).map biprod.inr ≫
      homotopyCofiber.inr ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F))) ≫
        homotopyCofiber.desc ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))
          (biprod.lift ((H.mapHomologicalComplex c).map biprod.fst) ((H.mapHomologicalComplex c).map biprod.snd) ≫
            homotopyCofiber.inr
              (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F))))
          ((Homotopy.ofEq ⋯).trans
            (((homotopyCofiber.inrCompHomotopy
                      (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))
                      hc).compLeft
                  (𝟙 ((H.mapHomologicalComplex c).obj F))).trans
              (Homotopy.ofEq ⋯))) =
    biprod.inr ≫
      homotopyCofiber.inr (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))