-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G K_1 : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
K : HomologicalComplex.{v_1, u_1, u_2} C c
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
x : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
rw :
  Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
        ((fun (f : homotopyCofiber φ ⟶ K) ↦
            (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) (inr φ ≫ f)
                ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))) :
              (α : G ⟶ K) × Homotopy (φ ≫ α) 0))
          ((fun (x : (α : G ⟶ K) × Homotopy (φ ≫ α) 0) ↦
              (match (motive := (α : G ⟶ K) × Homotopy (φ ≫ α) 0 → (homotopyCofiber φ ⟶ K)) x with
                | ⟨α, hα⟩ => desc φ α hα :
                homotopyCofiber φ ⟶ K))
            (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) α hα))) =
      Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
        (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) α hα) ∧
    ∀ (i j : ι),
      c.Rel j i →
        Homotopy.hom (f :=
            φ ≫
              Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                ((fun (f : homotopyCofiber φ ⟶ K) ↦
                    (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) (inr φ ≫ f)
                        ((Homotopy.ofEq ⋯).trans
                          ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))) :
                      (α : G ⟶ K) × Homotopy (φ ≫ α) 0))
                  ((fun (x : (α : G ⟶ K) × Homotopy (φ ≫ α) 0) ↦
                      (match (motive := (α : G ⟶ K) × Homotopy (φ ≫ α) 0 → (homotopyCofiber φ ⟶ K)) x with
                        | ⟨α, hα⟩ => desc φ α hα :
                        homotopyCofiber φ ⟶ K))
                    (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) α hα))))
            (g := 0)
            (Sigma.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                ((fun (f : homotopyCofiber φ ⟶ K) ↦
                    (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) (inr φ ≫ f)
                        ((Homotopy.ofEq ⋯).trans
                          ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))) :
                      (α : G ⟶ K) × Homotopy (φ ≫ α) 0))
                  ((fun (x : (α : G ⟶ K) × Homotopy (φ ≫ α) 0) ↦
                      (match (motive := (α : G ⟶ K) × Homotopy (φ ≫ α) 0 → (homotopyCofiber φ ⟶ K)) x with
                        | ⟨α, hα⟩ => desc φ α hα :
                        homotopyCofiber φ ⟶ K))
                    (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) α hα))) :
              Homotopy (D := K)
                (φ ≫
                  Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                    ((fun (f : homotopyCofiber φ ⟶ K) ↦
                        (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) (inr φ ≫ f)
                            ((Homotopy.ofEq ⋯).trans
                              ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))) :
                          (α : G ⟶ K) × Homotopy (φ ≫ α) 0))
                      ((fun (x : (α : G ⟶ K) × Homotopy (φ ≫ α) 0) ↦
                          (match (motive := (α : G ⟶ K) × Homotopy (φ ≫ α) 0 → (homotopyCofiber φ ⟶ K)) x with
                            | ⟨α, hα⟩ => desc φ α hα :
                            homotopyCofiber φ ⟶ K))
                        (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) α hα))))
                0)
            i j =
          Homotopy.hom (f :=
            φ ≫
              Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
                (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) α hα))
            (g := 0)
            (Sigma.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
              (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) α hα))
            i j
⊢ Eq (α := (α : G ⟶ K) × Homotopy (φ ≫ α) 0)
    ((fun (f : homotopyCofiber φ ⟶ K) ↦
        (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) (inr φ ≫ f)
            ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))) :
          (α : G ⟶ K) × Homotopy (φ ≫ α) 0))
      ((fun (x : (α : G ⟶ K) × Homotopy (φ ≫ α) 0) ↦
          (match (motive := (α : G ⟶ K) × Homotopy (φ ≫ α) 0 → (homotopyCofiber φ ⟶ K)) x with
            | ⟨α, hα⟩ => desc φ α hα :
            homotopyCofiber φ ⟶ K))
        (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) α hα)))
    (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) α hα)

Tactic:
rw [descSigma_ext_iff]

Premises used: HomologicalComplex.homotopyCofiber.descSigma_ext_iff