-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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
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 := ⋯ :
                                    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)
                        ⋯,
                    continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } :
                  (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)
⊢ {
      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

Tactic:
ext