-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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
⊢ 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α)
have rw : Sigma.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0)
      ((fun (f : homotopyCofiber φ ⟶ K) ↦
          (Sigma.mk (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) (inr φ ≫ f)
              ((Homotopy.ofEq sorry).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq sorry))) :
            (α : 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 sorry).trans
                        ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq sorry))) :
                    (α : 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 sorry).trans
                        ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq sorry))) :
                    (α : 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 sorry).trans
                            ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq sorry))) :
                        (α : 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
Tactic: rw [descSigma_ext_iff]