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_1 : X
M : Type u_3
x : X
e : M ≃ N
p : (↑(Ω^ N X x) : Type (max u_1 u_2))
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 := ⋯ })
                    ⋯ :
                  { 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) :
            (a : N → (↑I : Type)) → X)
          t :
        X)
      ((p : (a : N → (↑I : Type)) → X) t : 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 := ⋯ })
            ⋯ :
          { 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

Tactic:
ext t
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
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 := ⋯ })
                  ⋯ :
                { 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) :
          (a : N → (↑I : Type)) → X)
        t :
      X)
    ((p : (a : N → (↑I : Type)) → X) t : X)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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
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
⊢ 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
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
M : Type u_3
y : M ⊕ N → (↑I : Type)
i : M
hi : y (Sum.inl i) = 0 ∨ y (Sum.inl i) = 1
⊢ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N

Tactic:
Or.inl ⟨i, hi⟩

Premises used: Exists.intro, Or.inl
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
M : Type u_3
y : M ⊕ N → (↑I : Type)
i : M
hi : y (Sum.inl i) = 0 ∨ y (Sum.inl i) = 1
⊢ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N

Tactic:
exact Or.inl ⟨i, hi⟩

Premises used: Or.inl
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
M : Type u_3
y : M ⊕ N → (↑I : Type)
i : N
hi : y (Sum.inr i) = 0 ∨ y (Sum.inr i) = 1
⊢ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N

Tactic:
Or.inr ⟨i, hi⟩

Premises used: Exists.intro, Or.inr
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
M : Type u_3
y : M ⊕ N → (↑I : Type)
i : N
hi : y (Sum.inr i) = 0 ∨ y (Sum.inr i) = 1
⊢ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N

Tactic:
exact Or.inr ⟨i, hi⟩

Premises used: Or.inr
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
M : Type u_3
y : M ⊕ N → (↑I : Type)
m : M
hm : (y ∘ Sum.inl) m = 0 ∨ (y ∘ Sum.inl) m = 1
⊢ Membership.mem (γ := Set (M ⊕ N → (↑I : Type))) (Cube.boundary (M ⊕ N)) y

Tactic:
⟨Sum.inl m, hm⟩

Premises used: Set.Mem, setOf, Cube.boundary, Sum.inl, Exists.intro
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
M : Type u_3
y : M ⊕ N → (↑I : Type)
m : M
hm : (y ∘ Sum.inl) m = 0 ∨ (y ∘ Sum.inl) m = 1
⊢ Membership.mem (γ := Set (M ⊕ N → (↑I : Type))) (Cube.boundary (M ⊕ N)) y

Tactic:
exact ⟨Sum.inl m, hm⟩
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
M : Type u_3
y : M ⊕ N → (↑I : Type)
n : N
hn : (y ∘ Sum.inr) n = 0 ∨ (y ∘ Sum.inr) n = 1
⊢ Membership.mem (γ := Set (M ⊕ N → (↑I : Type))) (Cube.boundary (M ⊕ N)) y

Tactic:
⟨Sum.inr n, hn⟩

Premises used: Set.Mem, setOf, Cube.boundary, Sum.inr, Exists.intro
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
M : Type u_3
y : M ⊕ N → (↑I : Type)
n : N
hn : (y ∘ Sum.inr) n = 0 ∨ (y ∘ Sum.inr) n = 1
⊢ Membership.mem (γ := Set (M ⊕ N → (↑I : Type))) (Cube.boundary (M ⊕ N)) y

Tactic:
exact ⟨Sum.inr n, hn⟩
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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
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
⊢ (((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

Premises used: Cube.boundary_sum_iff, Iff.mp
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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
⊢ 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
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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
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)))
⊢ (((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:
simp [this]
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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
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:
simpa using (p.val (y ∘ Sum.inl)).property (y ∘ Sum.inr) hN

Premises used: Function.comp, Sum.inl, Sum.inr, Subtype.val, DFunLike.coe, Subtype.property
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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 (max u_1 u_2) u_3))
y : M ⊕ N → (↑I : Type)
⊢ Eq.{u_2 + 1} (α := X)
    ((((currySum 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)
    ((p : (a : M ⊕ N → (↑I : Type)) → X) y : X)

Tactic:
simp [currySum, sumArrowHomeomorphProdArrow, Equiv.sumArrowEquivProdArrow]

Premises used: GenLoop.currySum, Homeomorph.sumArrowHomeomorphProdArrow, Equiv.sumArrowEquivProdArrow
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
M : Type u_3
x : X
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)))
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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 : (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:
fun_prop
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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 : Prod.{u_3, u_1} (M → (↑I : Type)) (N → (↑I : Type))
⊢ Eq.{u_2 + 1} (α := X) ((GenLoop.uncurry x p : (a : (M → (↑I : Type)) × (N → (↑I : Type))) → X) y : X)
    ((((p : (a : M → (↑I : Type)) → (↑(Ω^ N X x) : Type (max u_1 u_2))) y.1 : (↑(Ω^ N X x) : Type (max u_1 u_2))) :
          (a : N → (↑I : Type)) → X)
        y.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_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 ⊕ N → (↑I : Type)
hy : Membership.mem (γ := Set (M ⊕ N → (↑I : Type))) (Cube.boundary (M ⊕ N)) y
⊢ ((GenLoop.uncurry x p).comp
          { toFun := Equiv.toFun (toEquiv sumArrowHomeomorphProdArrow), continuous_toFun := ⋯ :
            C(M ⊕ N → (↑I : Type), Prod.{u_3, u_1} (M → (↑I : Type)) (N → (↑I : Type))) } :
        (a : M ⊕ N → (↑I : Type)) → X)
      y =
    x

Tactic:
simp [hy]
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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
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)
⊢ 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)))

Tactic:
ext n
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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
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:
q.2 _ (Cube.boundary_sum_iff.mpr (Or.inl hm))

Premises used: Iff.mpr, Cube.boundary_sum_iff, Or.inl, Subtype.property
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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
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:
exact q.2 _ (Cube.boundary_sum_iff.mpr (Or.inl hm))
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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)
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 := ⋯ :
                        C(M ⊕ N → (↑I : Type), Prod.{u_3, u_1} (M → (↑I : Type)) (N → (↑I : Type))) })
                    ⋯) :
                (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)
⊢ 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)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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)
    ((((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 := ⋯ :
                        C(M ⊕ N → (↑I : Type), Prod.{u_3, u_1} (M → (↑I : Type)) (N → (↑I : Type))) })
                    ⋯) :
                (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:
rfl
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
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))
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 := ⋯ })
                    ⋯ :
                  { 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) :
            (a : M ⊕ N → (↑I : Type)) → X)
          y :
        X)
      ((p : (a : M ⊕ N → (↑I : Type)) → X) y : 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 := ⋯ })
            ⋯ :
          { 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

Tactic:
ext