-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i : N
p : Ω (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)) const
⊢ {
      toFun := fun (t : (↑I : Type)) ↦
        Subtype.mk (p := fun (x_1 : ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X) ↦
          Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X))
            (Ω^ { j : N // j ≠ i } X x) x_1)
          (((ContinuousMap.comp
                    {
                      toFun :=
                        Subtype.val (p := fun (x_1 : ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X) ↦
                          Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X))
                            (Ω^ { j : N // j ≠ i } X x) x_1),
                      continuous_toFun := ⋯ :
                      C({ x_1 : ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X //
                          Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X))
                            (Ω^ { j : N // j ≠ i } X x) x_1 },
                        ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X) }
                    p.toContinuousMap).uncurry.curry :
              (a : (↑I : Type)) → C({ j : N // j ≠ i } → (↑I : Type), X))
            t)
          ⋯,
      continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } =
    p
have a : ∀ (x_1 : (↑I : Type)) (y : { j : N // j ≠ i } → (↑I : Type)),
  Eq.{u_2 + 1} (α := X)
    (((({
                  toFun := fun (t : (↑I : Type)) ↦
                    Subtype.mk (p := fun (x_2 : ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X) ↦
                      Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X))
                        (Ω^ { j : N // j ≠ i } X x) x_2)
                      (((ContinuousMap.comp
                                {
                                  toFun :=
                                    Subtype.val (p :=
                                      fun (x_2 : ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X) ↦
                                      Membership.mem (γ :=
                                        Set (ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X))
                                        (Ω^ { j : N // j ≠ i } X x) x_2),
                                  continuous_toFun := sorry :
                                  C({ x_2 : ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X //
                                      Membership.mem (γ :=
                                        Set (ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X))
                                        (Ω^ { j : N // j ≠ i } X x) x_2 },
                                    ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X) }
                                p.toContinuousMap).uncurry.curry :
                          (a : (↑I : Type)) → C({ j : N // j ≠ i } → (↑I : Type), X))
                        t)
                      sorry,
                  continuous_toFun := sorry, source' := sorry, target' := sorry } :
                (a : (↑I : Type)) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
              x_1 :
            (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) :
          (a : { j : N // j ≠ i } → (↑I : Type)) → X)
        y :
      X)
    ((((p : (a : (↑I : Type)) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) x_1 :
            (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) :
          (a : { j : N // j ≠ i } → (↑I : Type)) → X)
        y :
      X)
Tactic: ext