-- 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 q : (↑(Ω^ N X x) : Type (max u_1 u_2))
H : (↑p : C(N → (↑I : Type), X)).HomotopyRel (↑q : C(N → (↑I : Type), X)) (Cube.boundary N)
t y : (↑I : Type)
yH : Membership.mem (γ := Set (↑I : Type)) {0, 1} y
refine_5 :
  ∀ (y_1 : { j : N // j ≠ i } → (↑I : Type)),
    Eq.{u_2 + 1} (α := X)
      (((({
                    toFun := fun (x_1 : (↑I : Type)) ↦
                      ContinuousMap.toFun
                        (ContinuousMap.Homotopy.toContinuousMap (f₀ := (toLoop i p).toContinuousMap) (f₁ :=
                          (toLoop i q).toContinuousMap)
                          {
                            toFun := fun (t : (↑I : Type) × (↑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)
                                ((homotopyTo i H :
                                    (a : (↑I : Type) × (↑I : Type)) → C({ j : N // j ≠ i } → (↑I : Type), X))
                                  t)
                                ⋯,
                            continuous_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯ })
                        (t, x_1),
                    continuous_toFun := ⋯ } :
                  (a : (↑I : Type)) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
                y :
              (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) :
            (a : { j : N // j ≠ i } → (↑I : Type)) → X)
          y_1 :
        X)
      (((((toLoop i p).toContinuousMap : (a : (↑I : Type)) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) y :
              (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) :
            (a : { j : N // j ≠ i } → (↑I : Type)) → X)
          y_1 :
        X)
⊢ Eq (α := (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
    (({
            toFun := fun (x_1 : (↑I : Type)) ↦
              ContinuousMap.toFun
                (ContinuousMap.Homotopy.toContinuousMap (f₀ := (toLoop i p).toContinuousMap) (f₁ :=
                  (toLoop i q).toContinuousMap)
                  {
                    toFun := fun (t : (↑I : Type) × (↑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)
                        ((homotopyTo i H : (a : (↑I : Type) × (↑I : Type)) → C({ j : N // j ≠ i } → (↑I : Type), X)) t)
                        ⋯,
                    continuous_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯ })
                (t, x_1),
            continuous_toFun := ⋯ } :
          (a : (↑I : Type)) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
        y :
      (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
    (((toLoop i p).toContinuousMap : (a : (↑I : Type)) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) y :
      (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))

Tactic:
ext