awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
M : Type u_3
x : X
e : M ≃ N
p : (↑(Ω^ M X x) : Type (max u_2 u_3))
⊢ (fun (p : (↑(Ω^ N X x) : Type (max u_1 u_2))) ↦
        (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X) ↦
            Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X)) (Ω^ M X x) x_2)
            ((↑p : C(N → (↑I : Type), X)).comp
              { toFun := fun (t : M → (↑I : Type)) (n : N) ↦ t ((e.symm : (a : N) → M) n), continuous_toFun := ⋯ })
            ⋯ :
          { x_2 : ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X //
            Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X)) (Ω^ M X x) x_2 }))
      ((fun (p : (↑(Ω^ M X x) : Type (max u_2 u_3))) ↦
          (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X) ↦
              Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2)
              ((↑p : C(M → (↑I : Type), X)).comp
                { toFun := fun (t : N → (↑I : Type)) (m : M) ↦ t ((e : (a : M) → N) m), continuous_toFun := ⋯ })
              ⋯ :
            { x_2 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X //
              Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2 }))
        p) =
    p
have H : ∀ (t : M → (↑I : Type)),
  Eq.{u_2 + 1} (α := X)
    (((fun (p : (↑(Ω^ N X x) : Type (max u_1 u_2))) ↦
              (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X) ↦
                  Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X)) (Ω^ M X x) x_2)
                  ((↑p : C(N → (↑I : Type), X)).comp
                    { toFun := fun (t : M → (↑I : Type)) (n : N) ↦ t ((e.symm : (a : N) → M) n),
                      continuous_toFun := sorry })
                  sorry :
                { x_2 : ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X //
                  Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X)) (Ω^ M X x) x_2 }))
            ((fun (p : (↑(Ω^ M X x) : Type (max u_2 u_3))) ↦
                (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X) ↦
                    Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2)
                    ((↑p : C(M → (↑I : Type), X)).comp
                      { toFun := fun (t : N → (↑I : Type)) (m : M) ↦ t ((e : (a : M) → N) m), continuous_toFun := sorry })
                    sorry :
                  { x_2 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X //
                    Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2 }))
              p) :
          (a : M → (↑I : Type)) → X)
        t :
      X)
    ((p : (a : M → (↑I : Type)) → X) t : X)
Tactic: ext t
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
M : Type u_3
x : X
e : M ≃ N
p : (↑(Ω^ N X x) : Type (max u_1 u_2))
⊢ (fun (p : (↑(Ω^ M X x) : Type (max u_2 u_3))) ↦
        (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X) ↦
            Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2)
            ((↑p : C(M → (↑I : Type), X)).comp
              { toFun := fun (t : N → (↑I : Type)) (m : M) ↦ t ((e : (a : M) → N) m), continuous_toFun := ⋯ })
            ⋯ :
          { x_2 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X //
            Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2 }))
      ((fun (p : (↑(Ω^ N X x) : Type (max u_1 u_2))) ↦
          (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X) ↦
              Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X)) (Ω^ M X x) x_2)
              ((↑p : C(N → (↑I : Type), X)).comp
                { toFun := fun (t : M → (↑I : Type)) (n : N) ↦ t ((e.symm : (a : N) → M) n), continuous_toFun := ⋯ })
              ⋯ :
            { x_2 : ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X //
              Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X)) (Ω^ M X x) x_2 }))
        p) =
    p
have H : ∀ (t : N → (↑I : Type)),
  Eq.{u_2 + 1} (α := X)
    (((fun (p : (↑(Ω^ M X x) : Type (max u_2 u_3))) ↦
              (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X) ↦
                  Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2)
                  ((↑p : C(M → (↑I : Type), X)).comp
                    { toFun := fun (t : N → (↑I : Type)) (m : M) ↦ t ((e : (a : M) → N) m), continuous_toFun := sorry })
                  sorry :
                { x_2 : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X //
                  Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X)) (Ω^ N X x) x_2 }))
            ((fun (p : (↑(Ω^ N X x) : Type (max u_1 u_2))) ↦
                (Subtype.mk (p := fun (x_2 : ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X) ↦
                    Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X)) (Ω^ M X x) x_2)
                    ((↑p : C(N → (↑I : Type), X)).comp
                      { toFun := fun (t : M → (↑I : Type)) (n : N) ↦ t ((e.symm : (a : N) → M) n),
                        continuous_toFun := sorry })
                    sorry :
                  { x_2 : ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X //
                    Membership.mem (γ := Set (ContinuousMap.{u_3, u_2} (M → (↑I : Type)) X)) (Ω^ M X x) x_2 }))
              p) :
          (a : N → (↑I : Type)) → X)
        t :
      X)
    ((p : (a : N → (↑I : Type)) → X) t : X)
Tactic: ext t
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
M : Type u_3
y : M ⊕ N → (↑I : Type)
⊢ Membership.mem (γ := Set (M ⊕ N → (↑I : Type))) (Cube.boundary (M ⊕ N)) y ↔
    y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N
have mp : Membership.mem (γ := Set (M ⊕ N → (↑I : Type))) (Cube.boundary (M ⊕ N)) y →
  y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
M : Type u_3
y : M ⊕ N → (↑I : Type)
mp :
  Membership.mem (γ := Set (M ⊕ N → (↑I : Type))) (Cube.boundary (M ⊕ N)) y →
    y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N
⊢ Membership.mem (γ := Set (M ⊕ N → (↑I : Type))) (Cube.boundary (M ⊕ N)) y ↔
    y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N
have mpr : y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N →
  Membership.mem (γ := Set (M ⊕ N → (↑I : Type))) (Cube.boundary (M ⊕ N)) y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace 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))
y : M ⊕ N → (↑I : Type)
hy : Membership.mem (γ := Set (M ⊕ N → (↑I : Type))) (Cube.boundary (M ⊕ N)) y
⊢ (((p : (a : M → (↑I : Type)) → (↑(Ω^ N X x) : Type (max u_1 u_2))) (y ∘ Sum.inl) :
          (↑(Ω^ N X x) : Type (max u_1 u_2))) :
        (a : N → (↑I : Type)) → X)
      (y ∘ Sum.inr) =
    x
have inl : ∀ (hM : y ∘ Sum.inl ∈ Cube.boundary M),
  (((p : (a : M → (↑I : Type)) → (↑(Ω^ N X x) : Type (max u_1 u_2))) (y ∘ Sum.inl) :
          (↑(Ω^ N X x) : Type (max u_1 u_2))) :
        (a : N → (↑I : Type)) → X)
      (y ∘ Sum.inr) =
    x
Tactic: rcases Cube.boundary_sum_iff.mp hy with hM | hN
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace 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))
y : M ⊕ N → (↑I : Type)
hy : Membership.mem (γ := Set (M ⊕ N → (↑I : Type))) (Cube.boundary (M ⊕ N)) y
inl :
  ∀ (hM : y ∘ Sum.inl ∈ Cube.boundary M),
    (((p : (a : M → (↑I : Type)) → (↑(Ω^ N X x) : Type (max u_1 u_2))) (y ∘ Sum.inl) :
            (↑(Ω^ N X x) : Type (max u_1 u_2))) :
          (a : N → (↑I : Type)) → X)
        (y ∘ Sum.inr) =
      x
⊢ (((p : (a : M → (↑I : Type)) → (↑(Ω^ N X x) : Type (max u_1 u_2))) (y ∘ Sum.inl) :
          (↑(Ω^ N X x) : Type (max u_1 u_2))) :
        (a : N → (↑I : Type)) → X)
      (y ∘ Sum.inr) =
    x
have inr : ∀ (hN : y ∘ Sum.inr ∈ Cube.boundary N),
  (((p : (a : M → (↑I : Type)) → (↑(Ω^ N X x) : Type (max u_1 u_2))) (y ∘ Sum.inl) :
          (↑(Ω^ N X x) : Type (max u_1 u_2))) :
        (a : N → (↑I : Type)) → X)
      (y ∘ Sum.inr) =
    x
Tactic: rcases Cube.boundary_sum_iff.mp hy with hM | hN
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (hypothesis)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace 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))
y : M ⊕ N → (↑I : Type)
hy : Membership.mem (γ := Set (M ⊕ N → (↑I : Type))) (Cube.boundary (M ⊕ N)) y
hM : y ∘ Sum.inl ∈ Cube.boundary M
⊢ (((p : (a : M → (↑I : Type)) → (↑(Ω^ N X x) : Type (max u_1 u_2))) (y ∘ Sum.inl) :
          (↑(Ω^ N X x) : Type (max u_1 u_2))) :
        (a : N → (↑I : Type)) → X)
      (y ∘ Sum.inr) =
    x
have this : Eq (α := (↑(Ω^ N X x) : Type (max u_1 u_2)))
  ((p : (a : M → (↑I : Type)) → (↑(Ω^ N X x) : Type (max u_1 u_2))) (y ∘ Sum.inl) : (↑(Ω^ N X x) : Type (max u_1 u_2)))
  (const : (↑(Ω^ N X x) : Type (max u_1 u_2)))
Tactic: have : p (y ∘ Sum.inl) = const := p.property (y ∘ Sum.inl) hM
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
M : Type u_3
x : X
⊢ Continuous[_, inst]
    (Function.uncurry
      fun (x_1 : (↑(Ω^ (M ⊕ N) X x) : Type (max (max u_1 u_2) u_3)) × (M → (↑I : Type))) (y : N → (↑I : Type)) ↦
      (((↑x_1.1 : C(M ⊕ N → (↑I : Type), X)).comp
                  { toFun := Equiv.invFun (toEquiv sumArrowHomeomorphProdArrow), continuous_toFun := ⋯ :
                    C(Prod.{u_3, u_1} (M → (↑I : Type)) (N → (↑I : Type)), M ⊕ N → (↑I : Type)) }).curry.toFun
            x_1.2 :
          (a : N → (↑I : Type)) → X)
        y)
have dsimp : Continuous[_, inst]
  (Function.uncurry
    fun (x_1 : (↑(Ω^ (M ⊕ N) X x) : Type (max (max u_1 u_2) u_3)) × (M → (↑I : Type))) (y : N → (↑I : Type)) ↦
    (x_1.1 : (a : M ⊕ N → (↑I : Type)) → X)
      ((Homeomorph.symm sumArrowHomeomorphProdArrow : (a : (M → (↑I : Type)) × (N → (↑I : Type))) → M ⊕ N → (↑I : Type))
          (x_1.2, y) :
        M ⊕ N → (↑I : Type)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x_1 : X
M : Type u_3
x : X
q : (↑(Ω^ (M ⊕ N) X x) : Type (max (max u_1 u_2) u_3))
x_2 : M → (↑I : Type)
hm : x_2 ∈ Cube.boundary M
⊢ Eq (α := (↑(Ω^ N X x) : Type (max u_1 u_2)))
    ((currySum x q : (a : M → (↑I : Type)) → (↑(Ω^ N X x) : Type (max u_1 u_2))) x_2 :
      (↑(Ω^ N X x) : Type (max u_1 u_2)))
    (const : (↑(Ω^ N X x) : Type (max u_1 u_2)))
have H : ∀ (n : N → (↑I : Type)),
  Eq.{u_2 + 1} (α := X)
    ((((currySum x q : (a : M → (↑I : Type)) → (↑(Ω^ N X x) : Type (max u_1 u_2))) x_2 :
            (↑(Ω^ N X x) : Type (max u_1 u_2))) :
          (a : N → (↑I : Type)) → X)
        n :
      X)
    ((const : (a : N → (↑I : Type)) → X) n : X)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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))
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)
have H : Eq.{u_2 + 1} (α := X)
  ((((currySum x
                (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 :=
                        (⇑sumArrowHomeomorphProdArrow :
                          (a : M ⊕ N → (↑I : Type)) → (M → (↑I : Type)) × (N → (↑I : Type))),
                      continuous_toFun := sorry :
                      C(M ⊕ N → (↑I : Type), Prod.{u_3, u_1} (M → (↑I : Type)) (N → (↑I : Type))) })
                  sorry) :
              (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)
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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 (max u_1 u_2) u_3))
⊢ (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 }))
      ((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 }))
        p) =
    p
have H : ∀ (y : M ⊕ N → (↑I : Type)),
  Eq.{u_2 + 1} (α := X)
    (((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 := sorry })
                  sorry :
                { x_2 : C(M ⊕ N → (↑I : Type), X) //
                  Membership.mem (γ := Set C(M ⊕ N → (↑I : Type), X)) (Ω^ (M ⊕ N) X x) x_2 }))
            ((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) sorry :
                  { 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 }))
              p) :
          (a : M ⊕ N → (↑I : Type)) → X)
        y :
      X)
    ((p : (a : M ⊕ N → (↑I : Type)) → X) y : X)
Tactic: ext
-- 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 : (↑(Ω^ N X x) : Type (max u_1 u_2))
⊢ Eq (α := (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
    (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.curry
              ((↑p : C(N → (↑I : Type), X)).comp
                (↑(Cube.insertAt i) : C((↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)), N → (↑I : Type)))) :
            (a : (↑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 //
        Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X))
          (Ω^ { j : N // j ≠ i } X x) x_1 })
    (const : (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
have H : ∀ (t : { j : N // j ≠ i } → (↑I : Type)),
  Eq.{u_2 + 1} (α := X)
    (((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.curry
                    ((↑p : C(N → (↑I : Type), X)).comp
                      (↑(Cube.insertAt i) : C((↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)), N → (↑I : Type)))) :
                  (a : (↑I : Type)) → C({ j : N // j ≠ i } → (↑I : Type), X))
                0)
              sorry :
            { 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 }) :
          (a : { j : N // j ≠ i } → (↑I : Type)) → X)
        t :
      X)
    ((const : (a : { j : N // j ≠ i } → (↑I : Type)) → X) t : X)
Tactic: ext t
-- 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 : (↑(Ω^ N X x) : Type (max u_1 u_2))
t : { j : N // j ≠ i } → (↑I : Type)
⊢ Eq.{u_2 + 1} (α := X)
    (((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.curry
                    ((↑p : C(N → (↑I : Type), X)).comp
                      (↑(Cube.insertAt i) : C((↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)), N → (↑I : Type)))) :
                  (a : (↑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 //
              Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X))
                (Ω^ { j : N // j ≠ i } X x) x_1 }) :
          (a : { j : N // j ≠ i } → (↑I : Type)) → X)
        t :
      X)
    ((const : (a : { j : N // j ≠ i } → (↑I : Type)) → X) t : X)
have H : Eq (α := (↑I : Type))
  ((Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (0, t) i) 0
Tactic: refine p.property (Cube.insertAt i (0, t)) ⟨i, Or.inl ?_⟩
-- 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 : (↑(Ω^ N X x) : Type (max u_1 u_2))
⊢ Eq (α := (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
    (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.curry
              ((↑p : C(N → (↑I : Type), X)).comp
                (↑(Cube.insertAt i) : C((↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)), N → (↑I : Type)))) :
            (a : (↑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 //
        Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X))
          (Ω^ { j : N // j ≠ i } X x) x_1 })
    (const : (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
have H : ∀ (t : { j : N // j ≠ i } → (↑I : Type)),
  Eq.{u_2 + 1} (α := X)
    (((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.curry
                    ((↑p : C(N → (↑I : Type), X)).comp
                      (↑(Cube.insertAt i) : C((↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)), N → (↑I : Type)))) :
                  (a : (↑I : Type)) → C({ j : N // j ≠ i } → (↑I : Type), X))
                1)
              sorry :
            { 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 }) :
          (a : { j : N // j ≠ i } → (↑I : Type)) → X)
        t :
      X)
    ((const : (a : { j : N // j ≠ i } → (↑I : Type)) → X) t : X)
Tactic: ext t