-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
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) ⋯ :
                        { 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) :
                  (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)
⊢ (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

Tactic:
ext