-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
M : Type u_3
x : X
p : (↑(Ω^ M (↑(Ω^ N X x) : Type (max u_1 u_2)) const) : Type (max (max u_1 u_2) u_3))
⊢ (fun (q : (↑(Ω^ (M ⊕ N) X x) : Type (max (max u_1 u_2) u_3))) ↦
        (Subtype.mk (p := fun (x_2 : C(M → (↑I : Type), (↑(Ω^ N X x) : Type (max u_1 u_2)))) ↦
            Membership.mem (γ := Set C(M → (↑I : Type), (↑(Ω^ N X x) : Type (max u_1 u_2))))
              (Ω^ M (↑(Ω^ N X x) : Type (max u_1 u_2)) const) x_2)
            (currySum x q) ⋯ :
          { x_2 : C(M → (↑I : Type), (↑(Ω^ N X x) : Type (max u_1 u_2))) //
            Membership.mem (γ := Set C(M → (↑I : Type), (↑(Ω^ N X x) : Type (max u_1 u_2))))
              (Ω^ M (↑(Ω^ N X x) : Type (max u_1 u_2)) const) x_2 }))
      ((fun (p : (↑(Ω^ M (↑(Ω^ N X x) : Type (max u_1 u_2)) const) : Type (max (max u_1 u_2) u_3))) ↦
          (Subtype.mk (p := fun (x_2 : C(M ⊕ N → (↑I : Type), X)) ↦
              Membership.mem (γ := Set C(M ⊕ N → (↑I : Type), X)) (Ω^ (M ⊕ N) X x) x_2)
              ((GenLoop.uncurry x p).comp
                { toFun := Equiv.toFun (toEquiv sumArrowHomeomorphProdArrow), continuous_toFun := ⋯ })
              ⋯ :
            { x_2 : C(M ⊕ N → (↑I : Type), X) //
              Membership.mem (γ := Set C(M ⊕ N → (↑I : Type), X)) (Ω^ (M ⊕ N) X x) x_2 }))
        p) =
    p
have H : ∀ (y : M → (↑I : Type)) (y_1 : N → (↑I : Type)),
  Eq.{u_2 + 1} (α := X)
    (((((fun (q : (↑(Ω^ (M ⊕ N) X x) : Type (max (max u_1 u_2) u_3))) ↦
                    (Subtype.mk (p := fun (x_2 : C(M → (↑I : Type), (↑(Ω^ N X x) : Type (max u_1 u_2)))) ↦
                        Membership.mem (γ := Set C(M → (↑I : Type), (↑(Ω^ N X x) : Type (max u_1 u_2))))
                          (Ω^ M (↑(Ω^ N X x) : Type (max u_1 u_2)) const) x_2)
                        (currySum x q) sorry :
                      { x_2 : C(M → (↑I : Type), (↑(Ω^ N X x) : Type (max u_1 u_2))) //
                        Membership.mem (γ := Set C(M → (↑I : Type), (↑(Ω^ N X x) : Type (max u_1 u_2))))
                          (Ω^ M (↑(Ω^ N X x) : Type (max u_1 u_2)) const) x_2 }))
                  ((fun (p : (↑(Ω^ M (↑(Ω^ N X x) : Type (max u_1 u_2)) const) : Type (max (max u_1 u_2) u_3))) ↦
                      (Subtype.mk (p := fun (x_2 : C(M ⊕ N → (↑I : Type), X)) ↦
                          Membership.mem (γ := Set C(M ⊕ N → (↑I : Type), X)) (Ω^ (M ⊕ N) X x) x_2)
                          ((GenLoop.uncurry x p).comp
                            { toFun := Equiv.toFun (toEquiv sumArrowHomeomorphProdArrow), continuous_toFun := sorry })
                          sorry :
                        { x_2 : C(M ⊕ N → (↑I : Type), X) //
                          Membership.mem (γ := Set C(M ⊕ N → (↑I : Type), X)) (Ω^ (M ⊕ N) X x) x_2 }))
                    p) :
                (a : M → (↑I : Type)) → (↑(Ω^ N X x) : Type (max u_1 u_2)))
              y :
            (↑(Ω^ N X x) : Type (max u_1 u_2))) :
          (a : N → (↑I : Type)) → X)
        y_1 :
      X)
    ((((p : (a : M → (↑I : Type)) → (↑(Ω^ N X x) : Type (max u_1 u_2))) y : (↑(Ω^ N X x) : Type (max u_1 u_2))) :
          (a : N → (↑I : Type)) → X)
        y_1 :
      X)
Tactic: ext