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
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)
    ((H : (a : (↑I : Type) × (N → (↑I : Type))) → X)
        (((1, x_1).1,
            (Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type))
              ((1, x_1).2, y)) :
          (↑I : Type) × (N → (↑I : Type))) :
      X)
    ((q : (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)) (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)

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)
y : { j : N // j ≠ i } → (↑I : Type)
⊢ 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)

Tactic:
apply H.apply_zero

Premises used: ContinuousMap.HomotopyWith.apply_zero
-- 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)
⊢ Eq.{u_2 + 1} (α := X)
    ((H : (a : (↑I : Type) × (N → (↑I : Type))) → X)
        (((1, x_1).1,
            (Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type))
              ((1, x_1).2, y)) :
          (↑I : Type) × (N → (↑I : Type))) :
      X)
    ((q : (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)

Tactic:
apply H.apply_one

Premises used: ContinuousMap.HomotopyWith.apply_one
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i : N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
H : (↑p : C(N → (↑I : Type), X)).HomotopyRel (↑q : C(N → (↑I : Type), X)) (Cube.boundary N)
t y : (↑I : Type)
yH : Membership.mem (γ := Set (↑I : Type)) {0, 1} y
y_1 : { j : N // j ≠ i } → (↑I : Type)
refine_5 :
  Eq.{u_2 + 1} (α := X)
    ((((homotopyTo i H : (a : (↑I : Type) × (↑I : Type)) → C({ j : N // ¬j = i } → (↑I : Type), X)) (t, y) :
            ContinuousMap.{u_1, u_2} ({ j : N // ¬j = i } → (↑I : Type)) X) :
          (a : { j : N // ¬j = i } → (↑I : Type)) → X)
        y_1 :
      X)
    ((((toLoop i p : (a : (↑I : Type)) → (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) y :
            (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) :
          (a : { j : N // ¬j = i } → (↑I : Type)) → X)
        y_1 :
      X)
⊢ Eq.{u_2 + 1} (α := X)
    (((({
                  toFun := fun (x_1 : (↑I : Type)) ↦
                    ContinuousMap.toFun
                      (ContinuousMap.Homotopy.toContinuousMap (f₀ := (toLoop i p).toContinuousMap) (f₁ :=
                        (toLoop i q).toContinuousMap)
                        {
                          toFun := fun (t : (↑I : Type) × (↑I : Type)) ↦
                            Subtype.mk (p := fun (x_2 : ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X) ↦
                              Membership.mem (γ := Set (ContinuousMap.{u_1, u_2} ({ j : N // j ≠ i } → (↑I : Type)) X))
                                (Ω^ { j : N // j ≠ i } X x) x_2)
                              ((homotopyTo i H :
                                  (a : (↑I : Type) × (↑I : Type)) → C({ j : N // j ≠ i } → (↑I : Type), X))
                                t)
                              ⋯,
                          continuous_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯ })
                      (t, x_1),
                  continuous_toFun := ⋯ } :
                (a : (↑I : Type)) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
              y :
            (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) :
          (a : { j : N // j ≠ i } → (↑I : Type)) → X)
        y_1 :
      X)
    (((((toLoop i p).toContinuousMap : (a : (↑I : Type)) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) y :
            (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2))) :
          (a : { j : N // j ≠ i } → (↑I : Type)) → X)
        y_1 :
      X)

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)
t y : (↑I : Type)
yH : Membership.mem (γ := Set (↑I : Type)) {0, 1} y
y_1 : { j : N // j ≠ i } → (↑I : Type)
refine_5 :
  Eq.{u_2 + 1} (α := X)
    ((H : (a : (↑I : Type) × (N → (↑I : Type))) → X)
        (((t, y).1,
            (Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type))
              ((t, y).2, y_1)) :
          (↑I : Type) × (N → (↑I : Type))) :
      X)
    ((((toLoop i p : (a : (↑I : Type)) → (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) y :
            (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) :
          (a : { j : N // ¬j = i } → (↑I : Type)) → X)
        y_1 :
      X)
⊢ Eq.{u_2 + 1} (α := X)
    ((((homotopyTo i H : (a : (↑I : Type) × (↑I : Type)) → C({ j : N // ¬j = i } → (↑I : Type), X)) (t, y) :
            ContinuousMap.{u_1, u_2} ({ j : N // ¬j = i } → (↑I : Type)) X) :
          (a : { j : N // ¬j = i } → (↑I : Type)) → X)
        y_1 :
      X)
    ((((toLoop i p : (a : (↑I : Type)) → (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) y :
            (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) :
          (a : { j : N // ¬j = i } → (↑I : Type)) → X)
        y_1 :
      X)

Tactic:
rw [homotopyTo_apply]

Premises used: GenLoop.homotopyTo_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)
t y : (↑I : Type)
yH : Membership.mem (γ := Set (↑I : Type)) {0, 1} y
y_1 : { j : N // j ≠ i } → (↑I : Type)
refine_5 :
  Membership.mem (α := N → (↑I : Type)) (Cube.boundary N)
    ((Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) ((t, y).2, y_1) :
      N → (↑I : Type))
⊢ Eq.{u_2 + 1} (α := X)
    ((H : (a : (↑I : Type) × (N → (↑I : Type))) → X)
        (((t, y).1,
            (Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type))
              ((t, y).2, y_1)) :
          (↑I : Type) × (N → (↑I : Type))) :
      X)
    ((((toLoop i p : (a : (↑I : Type)) → (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) y :
            (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) :
          (a : { j : N // ¬j = i } → (↑I : Type)) → X)
        y_1 :
      X)

Tactic:
apply H.eq_fst

Premises used: ContinuousMap.HomotopyRel.eq_fst
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i : N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
H : (↑p : C(N → (↑I : Type), X)).HomotopyRel (↑q : C(N → (↑I : Type), X)) (Cube.boundary N)
t y : (↑I : Type)
yH : Membership.mem (γ := Set (↑I : Type)) {0, 1} y
y_1 : { 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)) ((t, y).2, y_1) i)
      0 ∨
    Eq (α := (↑I : Type))
      ((Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) ((t, y).2, y_1) i) 1
⊢ Membership.mem (α := N → (↑I : Type)) (Cube.boundary N)
    ((Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) ((t, y).2, y_1) :
      N → (↑I : Type))

Tactic:
use i
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i : N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
H : (↑p : C(N → (↑I : Type), X)).HomotopyRel (↑q : C(N → (↑I : Type), X)) (Cube.boundary N)
t y : (↑I : Type)
yH : Membership.mem (γ := Set (↑I : Type)) {0, 1} y
y_1 : { j : N // j ≠ i } → (↑I : Type)
h : ((t, y).2, y_1).1 = 0 ∨ ((t, y).2, y_1).1 = 1
⊢ Eq (α := (↑I : Type))
      ((Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) ((t, y).2, y_1) i)
      0 ∨
    Eq (α := (↑I : Type))
      ((Cube.insertAt i : (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type)) ((t, y).2, y_1) i) 1

Tactic:
rw [funSplitAt_symm_apply, dif_pos rfl]

Premises used: Homeomorph.funSplitAt_symm_apply, dif_pos, 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 y : (↑I : Type)
yH : Membership.mem (γ := Set (↑I : Type)) {0, 1} y
y_1 : { j : N // j ≠ i } → (↑I : Type)
⊢ ((t, y).2, y_1).1 = 0 ∨ ((t, y).2, y_1).1 = 1

Tactic:
yH

Premises used: Set.insert, Set.Mem, setOf, Set.singleton
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i : N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
H : (↑p : C(N → (↑I : Type), X)).HomotopyRel (↑q : C(N → (↑I : Type), X)) (Cube.boundary N)
t y : (↑I : Type)
yH : Membership.mem (γ := Set (↑I : Type)) {0, 1} y
y_1 : { j : N // j ≠ i } → (↑I : Type)
⊢ ((t, y).2, y_1).1 = 0 ∨ ((t, y).2, y_1).1 = 1

Tactic:
exact yH
-- 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 : Path.Homotopy (toLoop i p) (toLoop i q)
⊢ 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 q : (↑(Ω^ N X x) : Type (max u_1 u_2))
⊢ Path.Homotopic (toLoop i p) (toLoop i q) → Homotopic p q

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

Premises used: GenLoop.Homotopic, GenLoop.homotopyFrom, ContinuousMap.HomotopicRel, ContinuousMap.HomotopyWith.mk, Nonempty.map, Path.Homotopic, ContinuousMap.Homotopy.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 q : (↑(Ω^ N X x) : Type (max u_1 u_2))
refine_1 :
  ∀ (H : Path.Homotopy (toLoop i p) (toLoop i q)) (x_1 : N → (↑I : Type)),
    (homotopyFrom i H).toFun (0, x_1) = ((↑p : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) x_1
refine_2 :
  ∀ (H : Path.Homotopy (toLoop i p) (toLoop i q)) (x_1 : N → (↑I : Type)),
    (homotopyFrom i H).toFun (1, x_1) = ((↑q : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) x_1
refine_3 :
  ∀ (H : Path.Homotopy (toLoop i p) (toLoop i q)) (t : (↑I : Type)),
    ∀ x_1 ∈ Cube.boundary N,
      Eq.{u_2 + 1} (α := X)
        (({
                toFun := fun (x_2 : N → (↑I : Type)) ↦
                  (ContinuousMap.Homotopy.toContinuousMap (f₀ := (↑p : C(N → (↑I : Type), X))) (f₁ :=
                        (↑q : C(N → (↑I : Type), X)))
                        { toContinuousMap := homotopyFrom i H, map_zero_left := ⋯, map_one_left := ⋯ :
                          (↑p : C(N → (↑I : Type), X)).Homotopy (↑q : C(N → (↑I : Type), X)) }).toFun
                    (t, x_2),
                continuous_toFun := ⋯ : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X } :
              (a : N → (↑I : Type)) → X)
            x_1 :
          X)
        (((↑p : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) x_1 : X)
⊢ Path.Homotopic (toLoop i p) (toLoop i q) → Homotopic p q

Tactic:
refine Nonempty.map fun H ↦ ⟨⟨homotopyFrom i H, ?_, ?_⟩, ?_⟩

Premises used: Nonempty.map
-- 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 : Path.Homotopy (toLoop i p) (toLoop i q)
t : (↑I : Type)
y : N → (↑I : Type)
j : N
jH : y j = 0 ∨ y j = 1
refine_3 :
  Eq.{u_2 + 1} (α := X)
    (Function.uncurry
        (fun (x_1 : (↑I : Type)) (y : (↑I : Type) × ({ j : N // ¬j = i } → (↑I : Type))) ↦
          Function.uncurry
            (fun (x_2 : (↑I : Type)) (y : { j : N // ¬j = i } → (↑I : Type)) ↦
              (((H : (a : (↑I : Type) × (↑I : Type)) → (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2)))
                      (x_1, x_2) :
                    (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) :
                  (a : { j : N // ¬j = i } → (↑I : Type)) → X)
                y)
            y)
        (Prod.map id (⇑(Cube.splitAt i) : (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // ¬j = i } → (↑I : Type)))
          (t, y)) :
      X)
    (((↑p : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y : X)
⊢ Eq.{u_2 + 1} (α := X)
    (({
            toFun := fun (x_1 : N → (↑I : Type)) ↦
              (ContinuousMap.Homotopy.toContinuousMap (f₀ := (↑p : C(N → (↑I : Type), X))) (f₁ :=
                    (↑q : C(N → (↑I : Type), X)))
                    { toContinuousMap := homotopyFrom i H, map_zero_left := ⋯, map_one_left := ⋯ :
                      (↑p : C(N → (↑I : Type), X)).Homotopy (↑q : C(N → (↑I : Type), X)) }).toFun
                (t, x_1),
            continuous_toFun := ⋯ : ContinuousMap.{u_1, u_2} (N → (↑I : Type)) X } :
          (a : N → (↑I : Type)) → X)
        y :
      X)
    (((↑p : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y : X)

Tactic:
erw [homotopyFrom_apply]

Premises used: GenLoop.homotopyFrom_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 : Path.Homotopy (toLoop i p) (toLoop i q)
t : (↑I : Type)
y : N → (↑I : Type)
j : N
jH : y j = 0 ∨ y j = 1
refine_3 :
  ∀ (H : Path.Homotopy (toLoop j p) (toLoop j q)),
    Eq.{u_2 + 1} (α := X)
      (Function.uncurry
          (fun (x_1 : (↑I : Type)) (y : (↑I : Type) × ({ j_1 : N // ¬j_1 = j } → (↑I : Type))) ↦
            Function.uncurry
              (fun (x_2 : (↑I : Type)) (y : { j_1 : N // ¬j_1 = j } → (↑I : Type)) ↦
                (((H : (a : (↑I : Type) × (↑I : Type)) → (↑(Ω^ { j_1 : N // ¬j_1 = j } X x) : Type (max u_1 u_2)))
                        (x_1, x_2) :
                      (↑(Ω^ { j_1 : N // ¬j_1 = j } X x) : Type (max u_1 u_2))) :
                    (a : { j_1 : N // ¬j_1 = j } → (↑I : Type)) → X)
                  y)
              y)
          (Prod.map id
            (⇑(Cube.splitAt j) : (a : N → (↑I : Type)) → (↑I : Type) × ({ j_1 : N // ¬j_1 = j } → (↑I : Type)))
            (t, y)) :
        X)
      (((↑p : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y : X)
refine_3₁ :
  ∀ (h : j ≠ i),
    Eq.{u_2 + 1} (α := X)
      (Function.uncurry
          (fun (x_1 : (↑I : Type)) (y : (↑I : Type) × ({ j : N // ¬j = i } → (↑I : Type))) ↦
            Function.uncurry
              (fun (x_2 : (↑I : Type)) (y : { j : N // ¬j = i } → (↑I : Type)) ↦
                (((H : (a : (↑I : Type) × (↑I : Type)) → (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2)))
                        (x_1, x_2) :
                      (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) :
                    (a : { j : N // ¬j = i } → (↑I : Type)) → X)
                  y)
              y)
          (Prod.map id (⇑(Cube.splitAt i) : (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // ¬j = i } → (↑I : Type)))
            (t, y)) :
        X)
      (((↑p : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y : X)
⊢ Eq.{u_2 + 1} (α := X)
    (Function.uncurry
        (fun (x_1 : (↑I : Type)) (y : (↑I : Type) × ({ j : N // ¬j = i } → (↑I : Type))) ↦
          Function.uncurry
            (fun (x_2 : (↑I : Type)) (y : { j : N // ¬j = i } → (↑I : Type)) ↦
              (((H : (a : (↑I : Type) × (↑I : Type)) → (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2)))
                      (x_1, x_2) :
                    (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) :
                  (a : { j : N // ¬j = i } → (↑I : Type)) → X)
                y)
            y)
        (Prod.map id (⇑(Cube.splitAt i) : (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // ¬j = i } → (↑I : Type)))
          (t, y)) :
      X)
    (((↑p : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y : X)

Tactic:
obtain rfl | h := 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
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
t : (↑I : Type)
y : N → (↑I : Type)
j : N
jH : y j = 0 ∨ y j = 1
H : Path.Homotopy (toLoop j p) (toLoop j q)
refine_3 :
  Eq.{u_2 + 1} (α := X)
    ((((H : (a : (↑I : Type) × (↑I : Type)) → (↑(Ω^ { j_1 : N // ¬j_1 = j } X x) : Type (max u_1 u_2))) (t, y j) :
            (↑(Ω^ { j_1 : N // ¬j_1 = j } X x) : Type (max u_1 u_2))) :
          (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 : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y : X)
⊢ Eq.{u_2 + 1} (α := X)
    (Function.uncurry
        (fun (x_1 : (↑I : Type)) (y : (↑I : Type) × ({ j_1 : N // ¬j_1 = j } → (↑I : Type))) ↦
          Function.uncurry
            (fun (x_2 : (↑I : Type)) (y : { j_1 : N // ¬j_1 = j } → (↑I : Type)) ↦
              (((H : (a : (↑I : Type) × (↑I : Type)) → (↑(Ω^ { j_1 : N // ¬j_1 = j } X x) : Type (max u_1 u_2)))
                      (x_1, x_2) :
                    (↑(Ω^ { j_1 : N // ¬j_1 = j } X x) : Type (max u_1 u_2))) :
                  (a : { j_1 : N // ¬j_1 = j } → (↑I : Type)) → X)
                y)
            y)
        (Prod.map id (⇑(Cube.splitAt j) : (a : N → (↑I : Type)) → (↑I : Type) × ({ j_1 : N // ¬j_1 = j } → (↑I : Type)))
          (t, y)) :
      X)
    (((↑p : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y : X)

Tactic:
simp only [Prod.map_apply, id_eq, funSplitAt_apply, Function.uncurry_apply_pair]

Premises used: Prod.map_apply, Homeomorph.funSplitAt_apply, Function.uncurry_apply_pair, id_eq
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
t : (↑I : Type)
y : N → (↑I : Type)
j : N
jH : y j = 0 ∨ y j = 1
H : Path.Homotopy (toLoop j p) (toLoop j q)
refine_3 :
  Eq.{u_2 + 1} (α := X)
    (((((toLoop j p).toContinuousMap : (a : (↑I : Type)) → (↑(Ω^ { j_1 : N // j_1 ≠ j } X x) : Type (max u_1 u_2)))
              (y j) :
            (↑(Ω^ { j_1 : N // j_1 ≠ j } X x) : Type (max u_1 u_2))) :
          (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 : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y : X)
refine_3₁ : Membership.mem (γ := Set (↑I : Type)) {0, 1} (y j)
⊢ Eq.{u_2 + 1} (α := X)
    ((((H : (a : (↑I : Type) × (↑I : Type)) → (↑(Ω^ { j_1 : N // ¬j_1 = j } X x) : Type (max u_1 u_2))) (t, y j) :
            (↑(Ω^ { j_1 : N // ¬j_1 = j } X x) : Type (max u_1 u_2))) :
          (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 : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y : X)

Tactic:
rw [H.eq_fst]

Premises used: ContinuousMap.HomotopyRel.eq_fst
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
t : (↑I : Type)
y : N → (↑I : Type)
j : N
jH : y j = 0 ∨ y j = 1
H : Path.Homotopy (toLoop j p) (toLoop j q)
⊢ Eq.{u_2 + 1} (α := X)
    (((((toLoop j p).toContinuousMap : (a : (↑I : Type)) → (↑(Ω^ { j_1 : N // j_1 ≠ j } X x) : Type (max u_1 u_2)))
              (y j) :
            (↑(Ω^ { j_1 : N // j_1 ≠ j } X x) : Type (max u_1 u_2))) :
          (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 : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y : X)

Tactic:
congr_arg p ((Cube.splitAt j).left_inv _)

Premises used: Homeomorph.toEquiv, congr_arg, DFunLike.coe, Cube.splitAt, Equiv.left_inv
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
t : (↑I : Type)
y : N → (↑I : Type)
j : N
jH : y j = 0 ∨ y j = 1
H : Path.Homotopy (toLoop j p) (toLoop j q)
⊢ Membership.mem (γ := Set (↑I : Type)) {0, 1} (y j)

Tactic:
jH

Premises used: Set.insert, Set.Mem, setOf, Set.singleton
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
t : (↑I : Type)
y : N → (↑I : Type)
j : N
jH : y j = 0 ∨ y j = 1
H : Path.Homotopy (toLoop j p) (toLoop j q)
⊢ Eq.{u_2 + 1} (α := X)
    (((((toLoop j p).toContinuousMap : (a : (↑I : Type)) → (↑(Ω^ { j_1 : N // j_1 ≠ j } X x) : Type (max u_1 u_2)))
              (y j) :
            (↑(Ω^ { j_1 : N // j_1 ≠ j } X x) : Type (max u_1 u_2))) :
          (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 : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) y : X)

Tactic:
exacts [congr_arg p ((Cube.splitAt j).left_inv _), jH]

Premises used: Homeomorph.toEquiv, congr_arg, DFunLike.coe, Cube.splitAt, Equiv.left_inv