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 : Path.Homotopy (toLoop i p) (toLoop i q)
t : (↑I : Type)
y : N → (↑I : Type)
j : N
jH : y j = 0 ∨ y j = 1
h : j ≠ i
refine_3 :
  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
⊢ 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:
rw [p.2 _ ⟨j, jH⟩]

Premises used: Exists.intro, 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 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
h : j ≠ i
refine_3 :
  Membership.mem (γ := Set ({ j : N // ¬j = i } → (↑I : Type))) (Cube.boundary { j : N // ¬j = i })
    (Prod.map id (⇑(Cube.splitAt i) : (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // ¬j = i } → (↑I : Type)))
          (t, y)).2.2
⊢ 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

Tactic:
apply boundary

Premises used: 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 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
h : j ≠ i
⊢ Membership.mem (γ := Set ({ j : N // ¬j = i } → (↑I : Type))) (Cube.boundary { j : N // ¬j = i })
    (Prod.map id (⇑(Cube.splitAt i) : (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // ¬j = i } → (↑I : Type)))
          (t, y)).2.2

Tactic:
⟨⟨j, h⟩, jH⟩

Premises used: Set.Mem, setOf, Cube.boundary, Subtype.mk, Exists.intro
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i : 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
h : j ≠ i
⊢ Membership.mem (γ := Set ({ j : N // ¬j = i } → (↑I : Type))) (Cube.boundary { j : N // ¬j = i })
    (Prod.map id (⇑(Cube.splitAt i) : (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // ¬j = i } → (↑I : Type)))
          (t, y)).2.2

Tactic:
exact ⟨⟨j, h⟩, jH⟩
-- 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)
x_1 : N → (↑I : Type)
refine_1 :
  Eq.{u_2 + 1} (α := X)
    (Function.uncurry
        (fun (x_2 : (↑I : Type)) (y : (↑I : Type) × ({ j : N // ¬j = i } → (↑I : Type))) ↦
          Function.uncurry
            (fun (x_3 : (↑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_2, x_3) :
                    (↑(Ω^ { 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)))
          (0, x_1)) :
      X)
    (((↑p : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) x_1 : X)
⊢ (homotopyFrom i H).toFun (0, x_1) = ((↑p : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) x_1

Tactic:
apply (homotopyFrom_apply _ _ _).trans

Premises used: GenLoop.homotopyFrom_apply, Eq.trans
-- 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)
x_1 : N → (↑I : Type)
refine_1 :
  Eq.{u_2 + 1} (α := X)
    ((((toLoop i p : (a : (↑I : Type)) → (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) (x_1 i) :
            (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) :
          (a : { j : N // ¬j = i } → (↑I : Type)) → X)
        fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N) :
      X)
    (((↑p : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) x_1 : X)
⊢ Eq.{u_2 + 1} (α := X)
    (Function.uncurry
        (fun (x_2 : (↑I : Type)) (y : (↑I : Type) × ({ j : N // ¬j = i } → (↑I : Type))) ↦
          Function.uncurry
            (fun (x_3 : (↑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_2, x_3) :
                    (↑(Ω^ { 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)))
          (0, x_1)) :
      X)
    (((↑p : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) x_1 : X)

Tactic:
simp only [Prod.map_apply, id_eq, funSplitAt_apply,
      Function.uncurry_apply_pair, ContinuousMap.HomotopyWith.apply_zero,
      ContinuousMap.HomotopyWith.apply_one, ne_eq, Path.coe_toContinuousMap]

Premises used: ContinuousMap.HomotopyWith.apply_one, ne_eq, Path.coe_toContinuousMap, Prod.map_apply, Homeomorph.funSplitAt_apply, ContinuousMap.HomotopyWith.apply_zero, 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
i : N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
H : Path.Homotopy (toLoop i p) (toLoop i q)
x_1 : N → (↑I : Type)
refine_1 :
  ((↑(Cube.insertAt i) : C((↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)), N → (↑I : Type))) :
        (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type))
      (x_1 i, fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N)) =
    x_1
⊢ Eq.{u_2 + 1} (α := X)
    ((((toLoop i p : (a : (↑I : Type)) → (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) (x_1 i) :
            (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) :
          (a : { j : N // ¬j = i } → (↑I : Type)) → X)
        fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N) :
      X)
    (((↑p : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) x_1 : X)

Tactic:
apply congr_arg p

Premises used: congr_arg, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i : N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
H : Path.Homotopy (toLoop i p) (toLoop i q)
x_1 : N → (↑I : Type)
refine_1 :
  ((↑(Cube.insertAt i) : C((↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)), N → (↑I : Type))) :
        (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type))
      (x_1 i, fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N)) =
    x_1
⊢ Eq.{u_2 + 1} (α := X)
    ((((toLoop i p : (a : (↑I : Type)) → (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) (x_1 i) :
            (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) :
          (a : { j : N // ¬j = i } → (↑I : Type)) → X)
        fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N) :
      X)
    (((↑p : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) x_1 : X)

Tactic:
first
    | apply congr_arg p
    | apply congr_arg q

Premises used: congr_arg, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i : N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
H : Path.Homotopy (toLoop i p) (toLoop i q)
x_1 : N → (↑I : Type)
⊢ ((↑(Cube.insertAt i) : C((↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)), N → (↑I : Type))) :
        (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type))
      (x_1 i, fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N)) =
    x_1

Tactic:
apply (Cube.splitAt i).left_inv

Premises used: Homeomorph.toEquiv, 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
i : N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
H : Path.Homotopy (toLoop i p) (toLoop i q)
x_1 : N → (↑I : Type)
refine_2 :
  Eq.{u_2 + 1} (α := X)
    (Function.uncurry
        (fun (x_2 : (↑I : Type)) (y : (↑I : Type) × ({ j : N // ¬j = i } → (↑I : Type))) ↦
          Function.uncurry
            (fun (x_3 : (↑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_2, x_3) :
                    (↑(Ω^ { 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)))
          (1, x_1)) :
      X)
    (((↑q : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) x_1 : X)
⊢ (homotopyFrom i H).toFun (1, x_1) = ((↑q : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) x_1

Tactic:
apply (homotopyFrom_apply _ _ _).trans

Premises used: GenLoop.homotopyFrom_apply, Eq.trans
-- 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)
x_1 : N → (↑I : Type)
refine_2 :
  Eq.{u_2 + 1} (α := X)
    ((((toLoop i q : (a : (↑I : Type)) → (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) (x_1 i) :
            (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) :
          (a : { j : N // ¬j = i } → (↑I : Type)) → X)
        fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N) :
      X)
    (((↑q : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) x_1 : X)
⊢ Eq.{u_2 + 1} (α := X)
    (Function.uncurry
        (fun (x_2 : (↑I : Type)) (y : (↑I : Type) × ({ j : N // ¬j = i } → (↑I : Type))) ↦
          Function.uncurry
            (fun (x_3 : (↑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_2, x_3) :
                    (↑(Ω^ { 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)))
          (1, x_1)) :
      X)
    (((↑q : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) x_1 : X)

Tactic:
simp only [Prod.map_apply, id_eq, funSplitAt_apply,
      Function.uncurry_apply_pair, ContinuousMap.HomotopyWith.apply_zero,
      ContinuousMap.HomotopyWith.apply_one, ne_eq, Path.coe_toContinuousMap]

Premises used: ContinuousMap.HomotopyWith.apply_one, ne_eq, Path.coe_toContinuousMap, Prod.map_apply, Homeomorph.funSplitAt_apply, ContinuousMap.HomotopyWith.apply_zero, 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
i : N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
H : Path.Homotopy (toLoop i p) (toLoop i q)
x_1 : N → (↑I : Type)
refine_2 :
  ((↑(Cube.insertAt i) : C((↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)), N → (↑I : Type))) :
        (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type))
      (x_1 i, fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N)) =
    x_1
⊢ Eq.{u_2 + 1} (α := X)
    ((((toLoop i q : (a : (↑I : Type)) → (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) (x_1 i) :
            (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) :
          (a : { j : N // ¬j = i } → (↑I : Type)) → X)
        fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N) :
      X)
    (((↑q : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) x_1 : X)

Tactic:
apply congr_arg q

Premises used: congr_arg, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i : N
p q : (↑(Ω^ N X x) : Type (max u_1 u_2))
H : Path.Homotopy (toLoop i p) (toLoop i q)
x_1 : N → (↑I : Type)
refine_2 :
  ((↑(Cube.insertAt i) : C((↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)), N → (↑I : Type))) :
        (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type))
      (x_1 i, fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N)) =
    x_1
⊢ Eq.{u_2 + 1} (α := X)
    ((((toLoop i q : (a : (↑I : Type)) → (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) (x_1 i) :
            (↑(Ω^ { j : N // ¬j = i } X x) : Type (max u_1 u_2))) :
          (a : { j : N // ¬j = i } → (↑I : Type)) → X)
        fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N) :
      X)
    (((↑q : C(N → (↑I : Type), X)) : (a : N → (↑I : Type)) → X) x_1 : X)

Tactic:
first
    | apply congr_arg p
    | apply congr_arg q

Premises used: congr_arg, DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i : N
f g : (↑(Ω^ N X x) : Type (max u_1 u_2))
h :
  ∀ (x_1 : N → (↑I : Type)),
    Eq.{u_2 + 1} (α := X)
      (if (↑(x_1 i) : ℝ) ≤ 1 / 2 then
          (f : (a : N → (↑I : Type)) → X)
            (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ))))
        else
          (g : (a : N → (↑I : Type)) → X)
            (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ) - 1))) :
        X)
      ((fromLoop i (Path.trans (toLoop i f) (toLoop i g)) : (a : N → (↑I : Type)) → X) x_1 : X)
⊢ Eq (α := (N → (↑I : Type)) → X)
    (fun (t : N → (↑I : Type)) ↦
      if (↑(t i) : ℝ) ≤ 1 / 2 then
        (f : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) t i (Set.projIcc 0 1 ⋯ (2 * (↑(t i) : ℝ))))
      else
        (g : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) t i (Set.projIcc 0 1 ⋯ (2 * (↑(t i) : ℝ) - 1))))
    (⇑(fromLoop i (Path.trans (toLoop i f) (toLoop i g))) : (a : N → (↑I : Type)) → X)

Tactic:
ext1
-- 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
f g : (↑(Ω^ N X x) : Type (max u_1 u_2))
x_1 : N → (↑I : Type)
h :
  Eq.{u_2 + 1} (α := X) ((fromLoop i (Path.trans (toLoop i f) (toLoop i g)) : (a : N → (↑I : Type)) → X) x_1 : X)
    (if (↑(x_1 i) : ℝ) ≤ 1 / 2 then
        (f : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ))))
      else
        (g : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ) - 1))) :
      X)
⊢ Eq.{u_2 + 1} (α := X)
    (if (↑(x_1 i) : ℝ) ≤ 1 / 2 then
        (f : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ))))
      else
        (g : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ) - 1))) :
      X)
    ((fromLoop i (Path.trans (toLoop i f) (toLoop i g)) : (a : N → (↑I : Type)) → X) x_1 : X)

Tactic:
symm
-- 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
f g : (↑(Ω^ N X x) : Type (max u_1 u_2))
x_1 : N → (↑I : Type)
h :
  Eq.{u_2 + 1} (α := X)
    (((↑(if (↑(x_1 i) : ℝ) ≤ 1 / 2 then
                (Path.extend (toLoop i f) : (a : ℝ) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
                  (2 * (↑(x_1 i) : ℝ))
              else
                (Path.extend (toLoop i g) : (a : ℝ) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
                  (2 * (↑(x_1 i) : ℝ) - 1)) :
            C({ j : N // j ≠ i } → (↑I : Type), X)) :
          (a : { j : N // j ≠ i } → (↑I : Type)) → X)
        fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N) :
      X)
    (if (↑(x_1 i) : ℝ) ≤ 1 / 2 then
        (f : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ))))
      else
        (g : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ) - 1))) :
      X)
⊢ Eq.{u_2 + 1} (α := X) ((fromLoop i (Path.trans (toLoop i f) (toLoop i g)) : (a : N → (↑I : Type)) → X) x_1 : X)
    (if (↑(x_1 i) : ℝ) ≤ 1 / 2 then
        (f : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ))))
      else
        (g : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ) - 1))) :
      X)

Tactic:
dsimp only [Path.trans, fromLoop, Path.coe_mk_mk, Function.comp_apply, mk_apply,
        ContinuousMap.comp_apply, ContinuousMap.coe_coe, funSplitAt_apply,
        ContinuousMap.uncurry_apply, ContinuousMap.coe_mk, Function.uncurry_apply_pair]

Premises used: Path.trans, GenLoop.mk_apply, ContinuousMap.uncurry_apply, ContinuousMap.comp_apply, ContinuousMap.coe_mk, Path.coe_mk_mk, ContinuousMap.coe_coe, Function.comp_apply, Homeomorph.funSplitAt_apply, GenLoop.fromLoop, 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
f g : (↑(Ω^ N X x) : Type (max u_1 u_2))
x_1 : N → (↑I : Type)
pos :
  (↑(x_1 i) : ℝ) ≤ 1 / 2 →
    Eq.{u_2 + 1} (α := X)
      (((↑((Path.extend (toLoop i f) : (a : ℝ) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
                  (2 * (↑(x_1 i) : ℝ))) :
              C({ j : N // j ≠ i } → (↑I : Type), X)) :
            (a : { j : N // j ≠ i } → (↑I : Type)) → X)
          fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N) :
        X)
      ((f : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ)))) :
        X)
neg :
  ¬(↑(x_1 i) : ℝ) ≤ 1 / 2 →
    Eq.{u_2 + 1} (α := X)
      (((↑((Path.extend (toLoop i g) : (a : ℝ) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
                  (2 * (↑(x_1 i) : ℝ) - 1)) :
              C({ j : N // j ≠ i } → (↑I : Type), X)) :
            (a : { j : N // j ≠ i } → (↑I : Type)) → X)
          fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N) :
        X)
      ((g : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ) - 1))) :
        X)
⊢ Eq.{u_2 + 1} (α := X)
    (((↑(if (↑(x_1 i) : ℝ) ≤ 1 / 2 then
                (Path.extend (toLoop i f) : (a : ℝ) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
                  (2 * (↑(x_1 i) : ℝ))
              else
                (Path.extend (toLoop i g) : (a : ℝ) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
                  (2 * (↑(x_1 i) : ℝ) - 1)) :
            C({ j : N // j ≠ i } → (↑I : Type), X)) :
          (a : { j : N // j ≠ i } → (↑I : Type)) → X)
        fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N) :
      X)
    (if (↑(x_1 i) : ℝ) ≤ 1 / 2 then
        (f : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ))))
      else
        (g : (a : N → (↑I : Type)) → X)
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ) - 1))) :
      X)

Tactic:
split_ifs
-- 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
f g : (↑(Ω^ N X x) : Type (max u_1 u_2))
x_1 : N → (↑I : Type)
h : (↑(x_1 i) : ℝ) ≤ 1 / 2
pos :
  Eq.{u_2 + 1} (α := X)
    ((f : (a : N → (↑I : Type)) → X)
        (((↑(Cube.insertAt i) : C((↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)), N → (↑I : Type))) :
              (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type))
            (Set.projIcc 0 1 Path.extend._proof_2 (2 * (↑(x_1 i) : ℝ)), fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N)) :
          N → (↑I : Type)) :
      X)
    ((f : (a : N → (↑I : Type)) → X)
        (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ)))) :
      X)
⊢ Eq.{u_2 + 1} (α := X)
    (((↑((Path.extend (toLoop i f) : (a : ℝ) → (↑(Ω^ { j : N // j ≠ i } X x) : Type (max u_1 u_2)))
                (2 * (↑(x_1 i) : ℝ))) :
            C({ j : N // j ≠ i } → (↑I : Type), X)) :
          (a : { j : N // j ≠ i } → (↑I : Type)) → X)
        fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N) :
      X)
    ((f : (a : N → (↑I : Type)) → X)
        (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ)))) :
      X)

Tactic:
change f _ = _

Premises used: DFunLike.coe
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i : N
f g : (↑(Ω^ N X x) : Type (max u_1 u_2))
x_1 : N → (↑I : Type)
h : (↑(x_1 i) : ℝ) ≤ 1 / 2
⊢ Eq.{u_2 + 1} (α := X)
    ((f : (a : N → (↑I : Type)) → X)
        (((↑(Cube.insertAt i) : C((↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)), N → (↑I : Type))) :
              (a : (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type))) → N → (↑I : Type))
            (Set.projIcc 0 1 Path.extend._proof_2 (2 * (↑(x_1 i) : ℝ)), fun (j : { j : N // ¬j = i }) ↦ x_1 (↑j : N)) :
          N → (↑I : Type)) :
      X)
    ((f : (a : N → (↑I : Type)) → X)
        (Function.update (β := fun (a : N) ↦ (↑I : Type)) x_1 i (Set.projIcc 0 1 ⋯ (2 * (↑(x_1 i) : ℝ)))) :
      X)

Tactic:
congr 1