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
p : (↑(Ω^ (M ⊕ N) X x) : Type (max (max u_1 u_2) u_3))
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)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
f : (↑(Ω^ N X x) : Type (max u_1 u_2))
⊢ Homotopic f f

Tactic:
ContinuousMap.HomotopicRel.refl _

Premises used: GenLoop.Homotopic, ContinuousMap.HomotopicRel.refl
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
f g : (↑(Ω^ N X x) : Type (max u_1 u_2))
H : Homotopic f g
⊢ Homotopic g f

Tactic:
H.symm

Premises used: GenLoop.Homotopic, ContinuousMap.HomotopicRel.symm
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
f g h : (↑(Ω^ N X x) : Type (max u_1 u_2))
H0 : Homotopic f g
H1 : Homotopic g h
⊢ Homotopic f h

Tactic:
H0.trans H1

Premises used: GenLoop.Homotopic, ContinuousMap.HomotopicRel.trans
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
⊢ Equivalence (α := (↑(Ω^ N X x) : Type (max u_1 u_2))) Homotopic

Tactic:
⟨Homotopic.refl, Homotopic.symm, Homotopic.trans⟩

Premises used: GenLoop.Homotopic.trans, GenLoop.Homotopic.symm, GenLoop.Homotopic.refl, Equivalence.mk
-- 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 :
  ∀ (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)
⊢ 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)))

Tactic:
ext t
-- 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 : { 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)

Tactic:
p.property (Cube.insertAt i (0, t)) ⟨i, Or.inl ?_⟩

Premises used: Prod.mk, Cube.insertAt, Exists.intro, Or.inl, OfNat.ofNat, DFunLike.coe, 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 : N
p : (↑(Ω^ N X x) : Type (max u_1 u_2))
t : { j : N // j ≠ i } → (↑I : Type)
H :
  Eq (α := (↑I : Type))
    ((Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (0, t) i) 0
⊢ 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)

Tactic:
refine p.property (Cube.insertAt i (0, t)) ⟨i, Or.inl ?_⟩

Premises used: Prod.mk, Cube.insertAt, Exists.intro, Or.inl, OfNat.ofNat, DFunLike.coe, 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 : N
p : (↑(Ω^ N X x) : Type (max u_1 u_2))
t : { j : N // j ≠ i } → (↑I : Type)
⊢ Eq (α := (↑I : Type))
    ((Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (0, t) i) 0

Tactic:
simp
-- 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 :
  ∀ (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)
                ⋯ :
              { 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)
⊢ 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)))

Tactic:
ext t
-- 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 : { 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)
              ⋯ :
            { 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:
p.property (Cube.insertAt i (1, t)) ⟨i, Or.inr ?_⟩

Premises used: Prod.mk, Cube.insertAt, Exists.intro, OfNat.ofNat, DFunLike.coe, Or.inr, 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 : N
p : (↑(Ω^ N X x) : Type (max u_1 u_2))
t : { j : N // j ≠ i } → (↑I : Type)
H :
  Eq (α := (↑I : Type))
    ((Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (1, t) i) 1
⊢ 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)
              ⋯ :
            { 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:
refine p.property (Cube.insertAt i (1, t)) ⟨i, Or.inr ?_⟩

Premises used: Prod.mk, Cube.insertAt, Exists.intro, OfNat.ofNat, DFunLike.coe, Or.inr, 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 : N
p : (↑(Ω^ N X x) : Type (max u_1 u_2))
t : { j : N // j ≠ i } → (↑I : Type)
⊢ Eq (α := (↑I : Type))
    ((Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) (1, t) i) 1

Tactic:
simp
-- 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 := (↑(Ω^ N X x) : Type (max u_1 u_2))) (toLoop i)

Tactic:
Path.continuous_uncurry_iff.1 <|
    Continuous.subtype_mk
      (continuous_eval.comp <|
        Continuous.prodMap
          (ContinuousMap.continuous_curry.comp <|
            (ContinuousMap.continuous_precomp _).comp continuous_subtype_val)
          continuous_id)
      _

Premises used: continuous_subtype_val, Continuous.prodMap, Continuous.comp, Continuous.subtype_mk, Path.continuous_uncurry_iff, continuous_id, Iff.mp, ContinuousEval.continuous_eval, ContinuousMap.continuous_precomp, ContinuousMap.continuous_curry
-- 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
⊢ Continuous (X :=
    { 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 })
    (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))

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 : Ω (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)) const
y : N → (↑I : Type)
j : N
Hj : y j = 0 ∨ y j = 1
simp :
  (((↑((p.toContinuousMap :
                (a : (↑I : Type)) → { x_1 : C({ j : N // j ≠ i } → (↑I : Type), X) // x_1 ∈ Ω^ { j : N // j ≠ i } X x })
              (y i)) :
          C({ j : N // j ≠ i } → (↑I : Type), X)) :
        (a : { j : N // j ≠ i } → (↑I : Type)) → X)
      fun (j : { j : N // ¬j = i }) ↦ y (↑j : N)) =
    x
⊢ ((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.comp
          (↑(Cube.splitAt i) : C(N → (↑I : Type), (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))) :
        (a : N → (↑I : Type)) → X)
      y =
    x

Tactic:
simp only [ContinuousMap.comp_apply, ContinuousMap.coe_coe,
      funSplitAt_apply, ContinuousMap.uncurry_apply, ContinuousMap.coe_mk,
      Function.uncurry_apply_pair]

Premises used: ContinuousMap.uncurry_apply, ContinuousMap.comp_apply, ContinuousMap.coe_mk, ContinuousMap.coe_coe, Homeomorph.funSplitAt_apply, Function.uncurry_apply_pair
-- 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
y : N → (↑I : Type)
j : N
Hj : y j = 0 ∨ y j = 1
inl :
  ∀ (p : Ω (↑(Ω^ { j_1 : N // j_1 ≠ j } X x) : Type (max u_1 u_2)) const),
    (((↑((p.toContinuousMap :
                  (a : (↑I : Type)) →
                    { x_1 : C({ j_1 : N // j_1 ≠ j } → (↑I : Type), X) // x_1 ∈ Ω^ { j_1 : N // j_1 ≠ j } X x })
                (y j)) :
            C({ j_1 : N // j_1 ≠ j } → (↑I : Type), X)) :
          (a : { j_1 : N // j_1 ≠ j } → (↑I : Type)) → X)
        fun (j_1 : { j_1 : N // ¬j_1 = j }) ↦ y (↑j_1 : N)) =
      x
inr :
  ∀ (Hne : j ≠ i),
    (((↑((p.toContinuousMap :
                  (a : (↑I : Type)) →
                    { x_1 : C({ j : N // j ≠ i } → (↑I : Type), X) // x_1 ∈ Ω^ { j : N // j ≠ i } X x })
                (y i)) :
            C({ j : N // j ≠ i } → (↑I : Type), X)) :
          (a : { j : N // j ≠ i } → (↑I : Type)) → X)
        fun (j : { j : N // ¬j = i }) ↦ y (↑j : N)) =
      x
⊢ (((↑((p.toContinuousMap :
                (a : (↑I : Type)) → { x_1 : C({ j : N // j ≠ i } → (↑I : Type), X) // x_1 ∈ Ω^ { j : N // j ≠ i } X x })
              (y i)) :
          C({ j : N // j ≠ i } → (↑I : Type), X)) :
        (a : { j : N // j ≠ i } → (↑I : Type)) → X)
      fun (j : { j : N // ¬j = i }) ↦ y (↑j : N)) =
    x

Tactic:
obtain rfl | Hne := eq_or_ne j i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
y : N → (↑I : Type)
j : N
Hj : y j = 0 ∨ y j = 1
p : Ω (↑(Ω^ { j_1 : N // j_1 ≠ j } X x) : Type (max u_1 u_2)) const
inl :
  ∀ (Hj : y j = 0),
    (((↑((p.toContinuousMap :
                  (a : (↑I : Type)) →
                    { x_1 : C({ j_1 : N // j_1 ≠ j } → (↑I : Type), X) // x_1 ∈ Ω^ { j_1 : N // j_1 ≠ j } X x })
                (y j)) :
            C({ j_1 : N // j_1 ≠ j } → (↑I : Type), X)) :
          (a : { j_1 : N // j_1 ≠ j } → (↑I : Type)) → X)
        fun (j_1 : { j_1 : N // ¬j_1 = j }) ↦ y (↑j_1 : N)) =
      x
inl₁ :
  ∀ (Hj : y j = 1),
    (((↑((p.toContinuousMap :
                  (a : (↑I : Type)) →
                    { x_1 : C({ j_1 : N // j_1 ≠ j } → (↑I : Type), X) // x_1 ∈ Ω^ { j_1 : N // j_1 ≠ j } X x })
                (y j)) :
            C({ j_1 : N // j_1 ≠ j } → (↑I : Type), X)) :
          (a : { j_1 : N // j_1 ≠ j } → (↑I : Type)) → X)
        fun (j_1 : { j_1 : N // ¬j_1 = j }) ↦ y (↑j_1 : N)) =
      x
⊢ (((↑((p.toContinuousMap :
                (a : (↑I : Type)) →
                  { x_1 : C({ j_1 : N // j_1 ≠ j } → (↑I : Type), X) // x_1 ∈ Ω^ { j_1 : N // j_1 ≠ j } X x })
              (y j)) :
          C({ j_1 : N // j_1 ≠ j } → (↑I : Type), X)) :
        (a : { j_1 : N // j_1 ≠ j } → (↑I : Type)) → X)
      fun (j_1 : { j_1 : N // ¬j_1 = j }) ↦ y (↑j_1 : N)) =
    x

Tactic:
rcases Hj with Hj | Hj
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
y : N → (↑I : Type)
j : N
p : Ω (↑(Ω^ { j_1 : N // j_1 ≠ j } X x) : Type (max u_1 u_2)) const
Hj : y j = 0
inl :
  (((↑const : C({ j_1 : N // j_1 ≠ j } → (↑I : Type), X)) : (a : { j_1 : N // j_1 ≠ j } → (↑I : Type)) → X)
      fun (j_1 : { j_1 : N // ¬j_1 = j }) ↦ y (↑j_1 : N)) =
    x
⊢ (((↑((p.toContinuousMap :
                (a : (↑I : Type)) →
                  { x_1 : C({ j_1 : N // j_1 ≠ j } → (↑I : Type), X) // x_1 ∈ Ω^ { j_1 : N // j_1 ≠ j } X x })
              (y j)) :
          C({ j_1 : N // j_1 ≠ j } → (↑I : Type), X)) :
        (a : { j_1 : N // j_1 ≠ j } → (↑I : Type)) → X)
      fun (j_1 : { j_1 : N // ¬j_1 = j }) ↦ y (↑j_1 : N)) =
    x

Tactic:
simp only [Hj, p.coe_toContinuousMap, p.source, p.target]

Premises used: Path.source, Path.coe_toContinuousMap, Path.target
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
y : N → (↑I : Type)
j : N
p : Ω (↑(Ω^ { j_1 : N // j_1 ≠ j } X x) : Type (max u_1 u_2)) const
Hj : y j = 1
inl :
  (((↑const : C({ j_1 : N // j_1 ≠ j } → (↑I : Type), X)) : (a : { j_1 : N // j_1 ≠ j } → (↑I : Type)) → X)
      fun (j_1 : { j_1 : N // ¬j_1 = j }) ↦ y (↑j_1 : N)) =
    x
⊢ (((↑((p.toContinuousMap :
                (a : (↑I : Type)) →
                  { x_1 : C({ j_1 : N // j_1 ≠ j } → (↑I : Type), X) // x_1 ∈ Ω^ { j_1 : N // j_1 ≠ j } X x })
              (y j)) :
          C({ j_1 : N // j_1 ≠ j } → (↑I : Type), X)) :
        (a : { j_1 : N // j_1 ≠ j } → (↑I : Type)) → X)
      fun (j_1 : { j_1 : N // ¬j_1 = j }) ↦ y (↑j_1 : N)) =
    x

Tactic:
simp only [Hj, p.coe_toContinuousMap, p.source, p.target]

Premises used: Path.source, Path.coe_toContinuousMap, Path.target
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
y : N → (↑I : Type)
j : N
p : Ω (↑(Ω^ { j_1 : N // j_1 ≠ j } X x) : Type (max u_1 u_2)) const
Hj : y j = 0
⊢ (((↑const : C({ j_1 : N // j_1 ≠ j } → (↑I : Type), X)) : (a : { j_1 : N // j_1 ≠ j } → (↑I : Type)) → X)
      fun (j_1 : { j_1 : N // ¬j_1 = j }) ↦ y (↑j_1 : N)) =
    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
y : N → (↑I : Type)
j : N
p : Ω (↑(Ω^ { j_1 : N // j_1 ≠ j } X x) : Type (max u_1 u_2)) const
Hj : y j = 1
⊢ (((↑const : C({ j_1 : N // j_1 ≠ j } → (↑I : Type), X)) : (a : { j_1 : N // j_1 ≠ j } → (↑I : Type)) → X)
      fun (j_1 : { j_1 : N // ¬j_1 = j }) ↦ y (↑j_1 : N)) =
    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 : Ω (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)) const
y : N → (↑I : Type)
j : N
Hj : y j = 0 ∨ y j = 1
Hne : j ≠ i
⊢ (((↑((p.toContinuousMap :
                (a : (↑I : Type)) → { x_1 : C({ j : N // j ≠ i } → (↑I : Type), X) // x_1 ∈ Ω^ { j : N // j ≠ i } X x })
              (y i)) :
          C({ j : N // j ≠ i } → (↑I : Type), X)) :
        (a : { j : N // j ≠ i } → (↑I : Type)) → X)
      fun (j : { j : N // ¬j = i }) ↦ y (↑j : N)) =
    x

Tactic:
GenLoop.boundary _ _ ⟨⟨j, Hne⟩, Hj⟩

Premises used: Subtype.mk, Exists.intro, GenLoop.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 : N
p : Ω (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)) const
y : N → (↑I : Type)
j : N
Hj : y j = 0 ∨ y j = 1
Hne : j ≠ i
⊢ (((↑((p.toContinuousMap :
                (a : (↑I : Type)) → { x_1 : C({ j : N // j ≠ i } → (↑I : Type), X) // x_1 ∈ Ω^ { j : N // j ≠ i } X x })
              (y i)) :
          C({ j : N // j ≠ i } → (↑I : Type), X)) :
        (a : { j : N // j ≠ i } → (↑I : Type)) → X)
      fun (j : { j : N // ¬j = i }) ↦ y (↑j : N)) =
    x

Tactic:
exact GenLoop.boundary _ _ ⟨⟨j, Hne⟩, Hj⟩

Premises used: Exists.intro, GenLoop.boundary