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 G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹¹ : HasHomotopyCofiber φ
inst✝¹⁰ : DecidableRel c.Rel
inst✝⁹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝⁸ : K.HasCylinder
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
⊢ (Iso.refl (Arrow.mk ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))).left).hom ≫
      (Arrow.mk (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))).hom =
    (Arrow.mk ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))).hom ≫
      ((H.mapHomologicalComplex c).mapBiprod F F).hom

Tactic:
apply biprod.hom_ext

Goal state after:
case h₀
C : Type u_1
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹¹ : HasHomotopyCofiber φ
inst✝¹⁰ : DecidableRel c.Rel
inst✝⁹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝⁸ : K.HasCylinder
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
⊢ ((Iso.refl (Arrow.mk ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))).left).hom ≫
        (Arrow.mk (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))).hom) ≫
      biprod.fst =
    ((Arrow.mk ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))).hom ≫
        ((H.mapHomologicalComplex c).mapBiprod F F).hom) ≫
      biprod.fst

case h₁
C : Type u_1
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹¹ : HasHomotopyCofiber φ
inst✝¹⁰ : DecidableRel c.Rel
inst✝⁹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝⁸ : K.HasCylinder
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
⊢ ((Iso.refl (Arrow.mk ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))).left).hom ≫
        (Arrow.mk (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))).hom) ≫
      biprod.snd =
    ((Arrow.mk ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))).hom ≫
        ((H.mapHomologicalComplex c).mapBiprod F F).hom) ≫
      biprod.snd