awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Continuous (X := Ω (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)) const) (fromLoop i)

Tactic:
((ContinuousMap.continuous_precomp _).comp <|
        ContinuousMap.continuous_uncurry.comp <|
          (ContinuousMap.continuous_postcomp _).comp continuous_induced_dom).subtype_mk
    _

Premises used: ContinuousMap.continuous_postcomp, Continuous.comp, ContinuousMap.comp, Continuous.subtype_mk, toContinuousMap, ContinuousMap.continuous_uncurry, continuous_induced_dom, ContinuousMap.continuous_precomp, GenLoop.fromLoop
-- 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
simp_rw :
  {
      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
⊢ toLoop i (fromLoop i p) = p

Tactic:
simp_rw [toLoop, fromLoop, ContinuousMap.comp_assoc,
    toContinuousMap_comp_symm, ContinuousMap.comp_id]

Premises used: ContinuousMap.comp_id, GenLoop.toLoop, Homeomorph.toContinuousMap_comp_symm, ContinuousMap.comp_assoc, GenLoop.fromLoop
-- 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
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)

Tactic:
rfl
-- 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 : (↑(Ω^ N X x) : Type (max u_1 u_2))
H :
  ∀ (y : N → (↑I : Type)),
    Eq.{u_2 + 1} (α := X) ((fromLoop i (toLoop i p) : (a : N → (↑I : Type)) → X) y : X)
      ((p : (a : N → (↑I : Type)) → X) y : X)
⊢ fromLoop i (toLoop i p) = p

Tactic:
ext
-- 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 : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
dsimp :
  (Cube.insertAt i : (a : (↑I : Type) × ({ j : N // ¬j = i } → (↑I : Type))) → N → (↑I : Type))
      (y i, fun (j : { j : N // ¬j = i }) ↦ y (↑j : N)) =
    y
⊢ ((↑(Cube.insertAt i) : C((↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)), N → (↑I : Type))) :
        (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type))
      ((((↑(Cube.splitAt i) : C(N → (↑I : Type), (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))) :
              (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))
            y).1,
        (((↑(Cube.splitAt i) : C(N → (↑I : Type), (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))) :
              (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))
            y).2) =
    y

Tactic:
dsimp
-- 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 : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
⊢ (Cube.insertAt i : (a : (↑I : Type) × ({ j : N // ¬j = i } → (↑I : Type))) → N → (↑I : Type))
      (y i, fun (j : { j : N // ¬j = i }) ↦ y (↑j : N)) =
    y

Tactic:
Equiv.apply_symm_apply _ _

Premises used: Equiv.apply_symm_apply
-- 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 : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
⊢ (Cube.insertAt i : (a : (↑I : Type) × ({ j : N // ¬j = i } → (↑I : Type))) → N → (↑I : Type))
      (y i, fun (j : { j : N // ¬j = i }) ↦ y (↑j : N)) =
    y

Tactic:
exact Equiv.apply_symm_apply _ _

Premises used: Equiv.apply_symm_apply
-- 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 : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
⊢ Eq.{u_2 + 1} (α := X) ((fromLoop i (toLoop i p) : (a : N → (↑I : Type)) → X) y : X)
    ((p : (a : N → (↑I : Type)) → X) y : X)

Tactic:
exact congr_arg p (by dsimp; exact Equiv.apply_symm_apply _ _)

Premises used: congr_arg, DFunLike.coe
-- 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 : (↑(Ω^ N X x) : Type (max u_1 u_2))
t : (↑I : Type)
tn : { j : N // j ≠ i } → (↑I : Type)
⊢ Eq.{u_2 + 1} (α := X)
    ((((toLoop i p : (a : (↑I : Type)) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) t :
            (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) :
          (a : { j : N // j ≠ i } → (↑I : Type)) → X)
        tn :
      X)
    ((p : (a : N → (↑I : Type)) → X)
        ((Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t, tn) :
          N → (↑I : Type)) :
      X)

Tactic:
rfl

Premises used: rfl
-- 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
t : N → (↑I : Type)
⊢ Eq.{u_2 + 1} (α := X) ((fromLoop i p : (a : N → (↑I : Type)) → X) t : X)
    ((((p : (a : (↑I : Type)) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) (t i) :
            (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) :
          (a : { j : N // j ≠ i } → (↑I : Type)) → X)
        ((Cube.splitAt i : (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) t).2 :
      X)

Tactic:
rfl

Premises used: rfl
-- 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 : (↑I : Type) × (↑I : Type)
tₙ : { j : N // j ≠ i } → (↑I : Type)
⊢ Eq.{u_2 + 1} (α := X)
    ((((homotopyTo i H : (a : (↑I : Type) × (↑I : Type)) → C({ j : N // j ≠ i } → (↑I : Type), X)) t :
            ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X) :
          (a : { j : N // j ≠ i } → (↑I : Type)) → X)
        tₙ :
      X)
    ((H : (a : (↑I : Type) × (N → (↑I : Type))) → X)
        ((t.1, (Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (t.2, tₙ)) :
          (↑I : Type) × (N → (↑I : Type))) :
      X)

Tactic:
rfl

Premises used: rfl
-- 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))
⊢ Homotopic p q → Path.Homotopic (toLoop i p) (toLoop i q)

Tactic:
Nonempty.map fun H ↦ ⟨⟨⟨fun t ↦ ⟨homotopyTo i H t, ?_⟩, ?_⟩, ?_, ?_⟩, ?_⟩

Premises used: GenLoop.homotopyTo, GenLoop.Homotopic, ContinuousMap.mk, ContinuousMap.HomotopicRel, ContinuousMap.HomotopyWith.mk, Subtype.mk, Nonempty.map, Path.Homotopic, ContinuousMap.Homotopy.mk, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i_1 : 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 : (↑I : Type) × (↑I : Type)
y : { j : N // j ≠ i_1 } → (↑I : Type)
i : { j : N // j ≠ i_1 }
iH : y i = 0 ∨ y i = 1
refine_1 refine_1₁ :
  Membership.mem (α := N → (↑I : Type)) (Cube.boundary N)
    ((Cube.insertAt i_1 : (a : (↑I : Type) × ({ j : N // j ≠ i_1 } → (↑I : Type))) → N → (↑I : Type)) (t.2, y) :
      N → (↑I : Type))
⊢ (((homotopyTo i_1 H : (a : (↑I : Type) × (↑I : Type)) → C({ j : N // j ≠ i_1 } → (↑I : Type), X)) t :
          ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i_1 } → (↑I : Type)) X) :
        (a : { j : N // j ≠ i_1 } → (↑I : Type)) → X)
      y =
    x

Tactic:
rw [homotopyTo_apply, H.eq_fst, p.2]

Premises used: GenLoop.homotopyTo_apply, ContinuousMap.HomotopyRel.eq_fst, Subtype.property
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i_1 : 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 : (↑I : Type) × (↑I : Type)
y : { j : N // j ≠ i_1 } → (↑I : Type)
i : { j : N // j ≠ i_1 }
iH : y i = 0 ∨ y i = 1
refine_1 :
  (t.2 = 0 ∨ t.2 = 1) ∨
    Membership.mem (γ := Set ({ j : N // j ≠ i_1 } → (↑I : Type))) (Cube.boundary { j : N // j ≠ i_1 }) y
⊢ Membership.mem (α := N → (↑I : Type)) (Cube.boundary N)
    ((Cube.insertAt i_1 : (a : (↑I : Type) × ({ j : N // j ≠ i_1 } → (↑I : Type))) → N → (↑I : Type)) (t.2, y) :
      N → (↑I : Type))

Tactic:
apply Cube.insertAt_boundary

Premises used: Cube.insertAt_boundary
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i_1 : 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 : (↑I : Type) × (↑I : Type)
y : { j : N // j ≠ i_1 } → (↑I : Type)
i : { j : N // j ≠ i_1 }
iH : y i = 0 ∨ y i = 1
refine_1 : Membership.mem (γ := Set ({ j : N // j ≠ i_1 } → (↑I : Type))) (Cube.boundary { j : N // j ≠ i_1 }) y
⊢ (t.2 = 0 ∨ t.2 = 1) ∨
    Membership.mem (γ := Set ({ j : N // j ≠ i_1 } → (↑I : Type))) (Cube.boundary { j : N // j ≠ i_1 }) y

Tactic:
right
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i_1 : 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 : (↑I : Type) × (↑I : Type)
y : { j : N // j ≠ i_1 } → (↑I : Type)
i : { j : N // j ≠ i_1 }
iH : y i = 0 ∨ y i = 1
⊢ Membership.mem (γ := Set ({ j : N // j ≠ i_1 } → (↑I : Type))) (Cube.boundary { j : N // j ≠ i_1 }) y

Tactic:
⟨i, iH⟩

Premises used: Set.Mem, setOf, Cube.boundary, Exists.intro
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i_1 : 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 : (↑I : Type) × (↑I : Type)
y : { j : N // j ≠ i_1 } → (↑I : Type)
i : { j : N // j ≠ i_1 }
iH : y i = 0 ∨ y i = 1
⊢ Membership.mem (γ := Set ({ j : N // j ≠ i_1 } → (↑I : Type))) (Cube.boundary { j : N // j ≠ i_1 }) y

Tactic:
exact ⟨i, iH⟩
-- 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)
⊢ Continuous (Y := (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) fun (t : (↑I : Type) × (↑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)
      ((homotopyTo i H : (a : (↑I : Type) × (↑I : Type)) → C({ j : N // j ≠ i } → (↑I : Type), X)) t) ⋯

Tactic:
fun_prop
-- 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)
x_1 : (↑I : Type)
refine_3 :
  ∀ (y : { j : N // j ≠ i } → (↑I : Type)),
    Eq.{u_2 + 1} (α := X)
      ((ContinuousMap.toFun
              {
                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 := ⋯ }
              (0, x_1) :
            (a : { j : N // j ≠ i } → (↑I : Type)) → X)
          y :
        X)
      (((((toLoop i p).toContinuousMap : (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)
⊢ Eq (α := (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
    (ContinuousMap.toFun
      {
        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 := ⋯ }
      (0, x_1))
    (((toLoop i p).toContinuousMap : (a : (↑I : Type)) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) x_1)

Tactic:
ext
-- 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)
x_1 : (↑I : Type)
y : { j : N // j ≠ i } → (↑I : Type)
refine_3 :
  Eq.{u_2 + 1} (α := X)
    ((((homotopyTo i H : (a : (↑I : Type) × (↑I : Type)) → C({ j : N // ¬j = i } → (↑I : Type), X)) (0, x_1) :
            ContinuousMap.{u_1, u_2} ({ j : N // ¬j = i } → (↑I : Type)) X) :
          (a : { j : N // ¬j = i } → (↑I : Type)) → X)
        y :
      X)
    ((((toLoop i 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)
⊢ Eq.{u_2 + 1} (α := X)
    ((ContinuousMap.toFun
            {
              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 := ⋯ }
            (0, x_1) :
          (a : { j : N // j ≠ i } → (↑I : Type)) → X)
        y :
      X)
    (((((toLoop i p).toContinuousMap : (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:
dsimp
-- 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)
x_1 : (↑I : Type)
y : { j : N // j ≠ i } → (↑I : Type)
refine_3 :
  Eq.{u_2 + 1} (α := X)
    ((H : (a : (↑I : Type) × (N → (↑I : Type))) → X)
        (((0, x_1).1,
            (Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type))
              ((0, x_1).2, y)) :
          (↑I : Type) × (N → (↑I : Type))) :
      X)
    ((p : (a : N → (↑I : Type)) → X)
        ((Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (x_1, y) :
          N → (↑I : Type)) :
      X)
⊢ Eq.{u_2 + 1} (α := X)
    ((((homotopyTo i H : (a : (↑I : Type) × (↑I : Type)) → C({ j : N // ¬j = i } → (↑I : Type), X)) (0, x_1) :
            ContinuousMap.{u_1, u_2} ({ j : N // ¬j = i } → (↑I : Type)) X) :
          (a : { j : N // ¬j = i } → (↑I : Type)) → X)
        y :
      X)
    ((((toLoop i 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:
rw [homotopyTo_apply, toLoop_apply]

Premises used: GenLoop.homotopyTo_apply, GenLoop.toLoop_apply
-- 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)
x_1 : (↑I : Type)
refine_4 :
  ∀ (y : { j : N // j ≠ i } → (↑I : Type)),
    Eq.{u_2 + 1} (α := X)
      ((ContinuousMap.toFun
              {
                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 := ⋯ }
              (1, x_1) :
            (a : { j : N // j ≠ i } → (↑I : Type)) → X)
          y :
        X)
      (((((toLoop i q).toContinuousMap : (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)
⊢ Eq (α := (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
    (ContinuousMap.toFun
      {
        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 := ⋯ }
      (1, x_1))
    (((toLoop i q).toContinuousMap : (a : (↑I : Type)) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) x_1)

Tactic:
ext
-- 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)
x_1 : (↑I : Type)
y : { j : N // j ≠ i } → (↑I : Type)
refine_4 :
  Eq.{u_2 + 1} (α := X)
    ((((homotopyTo i H : (a : (↑I : Type) × (↑I : Type)) → C({ j : N // ¬j = i } → (↑I : Type), X)) (1, x_1) :
            ContinuousMap.{u_1, u_2} ({ j : N // ¬j = i } → (↑I : Type)) X) :
          (a : { j : N // ¬j = i } → (↑I : Type)) → X)
        y :
      X)
    ((((toLoop i q : (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)
⊢ Eq.{u_2 + 1} (α := X)
    ((ContinuousMap.toFun
            {
              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 := ⋯ }
            (1, x_1) :
          (a : { j : N // j ≠ i } → (↑I : Type)) → X)
        y :
      X)
    (((((toLoop i q).toContinuousMap : (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:
dsimp