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
f g : (↑(Ω^ N X x) : Type (max u_1 u_2))
x_1 : N → (↑I : Type)
h : ¬(↑(x_1 i) : ℝ) ≤ 1 / 2
neg :
  Eq.{u_2 + 1} (α := X)
    ((g : (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) : ℝ) - 1), fun (j : { j : N // ¬j = i }) ↦
              x_1 (↑j : N)) :
          N → (↑I : Type)) :
      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)
    (((↑((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)

Tactic:
change g _ = _

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)
    ((g : (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) : ℝ) - 1), fun (j : { j : N // ¬j = i }) ↦
              x_1 (↑j : N)) :
          N → (↑I : Type)) :
      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)

Tactic:
congr 1
-- 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 : (↑(Ω^ N X x) : Type (max u_1 u_2))
h :
  ∀ (x_1 : N → (↑I : Type)),
    Eq.{u_2 + 1} (α := X) ((f : (a : N → (↑I : Type)) → X) fun (j : N) ↦ if j = i then σ (x_1 i) else x_1 j : X)
      ((fromLoop i (Path.symm (toLoop i f)) : (a : N → (↑I : Type)) → X) x_1 : X)
⊢ Eq (α := (N → (↑I : Type)) → X)
    (fun (t : N → (↑I : Type)) ↦ (f : (a : N → (↑I : Type)) → X) fun (j : N) ↦ if j = i then σ (t i) else t j)
    (⇑(fromLoop i (Path.symm (toLoop i f))) : (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 : (↑(Ω^ N X x) : Type (max u_1 u_2))
x_1 : N → (↑I : Type)
h :
  Eq.{u_2 + 1} (α := X) ((f : (a : N → (↑I : Type)) → X) fun (j : N) ↦ if j = i then σ (x_1 i) else x_1 j : 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))
            (σ
                (((↑(Cube.splitAt i) : C(N → (↑I : Type), (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))) :
                      (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))
                    x_1).1,
              (((↑(Cube.splitAt i) : C(N → (↑I : Type), (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))) :
                    (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))
                  x_1).2) :
          N → (↑I : Type)) :
      X)
⊢ Eq.{u_2 + 1} (α := X) ((f : (a : N → (↑I : Type)) → X) fun (j : N) ↦ if j = i then σ (x_1 i) else x_1 j : X)
    ((fromLoop i (Path.symm (toLoop i f)) : (a : N → (↑I : Type)) → X) x_1 : 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 : (↑(Ω^ N X x) : Type (max u_1 u_2))
x_1 : N → (↑I : Type)
h :
  Eq (α := N → (↑I : Type)) (fun (j : N) ↦ if j = i then σ (x_1 i) else x_1 j)
    (((↑(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))
        (σ
            (((↑(Cube.splitAt i) : C(N → (↑I : Type), (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))) :
                  (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))
                x_1).1,
          (((↑(Cube.splitAt i) : C(N → (↑I : Type), (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))) :
                (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))
              x_1).2) :
      N → (↑I : Type))
⊢ Eq.{u_2 + 1} (α := X) ((f : (a : N → (↑I : Type)) → X) fun (j : N) ↦ if j = i then σ (x_1 i) else x_1 j : 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))
            (σ
                (((↑(Cube.splitAt i) : C(N → (↑I : Type), (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))) :
                      (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))
                    x_1).1,
              (((↑(Cube.splitAt i) : C(N → (↑I : Type), (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))) :
                    (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))
                  x_1).2) :
          N → (↑I : Type)) :
      X)

Tactic:
congr
-- 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 : (↑(Ω^ N X x) : Type (max u_1 u_2))
x_1 : N → (↑I : Type)
h :
  ∀ (x : N),
    (if x = i then σ (x_1 i) else x_1 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))
        (σ
            (((↑(Cube.splitAt i) : C(N → (↑I : Type), (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))) :
                  (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))
                x_1).1,
          (((↑(Cube.splitAt i) : C(N → (↑I : Type), (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))) :
                (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))
              x_1).2)
        x
⊢ Eq (α := N → (↑I : Type)) (fun (j : N) ↦ if j = i then σ (x_1 i) else x_1 j)
    (((↑(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))
        (σ
            (((↑(Cube.splitAt i) : C(N → (↑I : Type), (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))) :
                  (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))
                x_1).1,
          (((↑(Cube.splitAt i) : C(N → (↑I : Type), (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))) :
                (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))
              x_1).2) :
      N → (↑I : Type))

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 : (↑(Ω^ N X x) : Type (max u_1 u_2))
x_1 : N → (↑I : Type)
x_2 : N
⊢ (if x_2 = i then σ (x_1 i) else x_1 x_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))
      (σ
          (((↑(Cube.splitAt i) : C(N → (↑I : Type), (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))) :
                (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))
              x_1).1,
        (((↑(Cube.splitAt i) : C(N → (↑I : Type), (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))) :
              (a : N → (↑I : Type)) → (↑I : Type) × ({ j : N // j ≠ i } → (↑I : Type)))
            x_1).2)
      x_2

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 j : N
h : i ≠ j
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
H :
  ∀ (y : N → (↑I : Type)),
    Eq.{u_2 + 1} (α := X) ((transAt i (transAt j a b) (transAt j c d) : (a : N → (↑I : Type)) → X) y : X)
      ((transAt j (transAt i a c) (transAt i b d) : (a : N → (↑I : Type)) → X) y : X)
⊢ transAt i (transAt j a b) (transAt j c d) = transAt j (transAt i a c) (transAt i b d)

Tactic:
ext
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i j : N
h : i ≠ j
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : (↑(y i) : ℝ) ≤ 1 / 2
h_2 : (↑(y j) : ℝ) ≤ 1 / 2
pos :
  Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ))) =
    Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)))
⊢ Eq.{u_2 + 1} (α := X)
    ((a : (a : N → (↑I : Type)) → X)
        (Function.update (β := fun (a : N) ↦ (↑I : Type))
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)))) j
          (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ)))) :
      X)
    ((a : (a : N → (↑I : Type)) → X)
        (Function.update (β := fun (a : N) ↦ (↑I : Type))
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ)))) i
          (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)))) :
      X)

Tactic:
congr 1
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i j : N
h : i ≠ j
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : (↑(y i) : ℝ) ≤ 1 / 2
h_2 : (↑(y j) : ℝ) ≤ 1 / 2
pos :
  ∀ (x : N),
    Function.update (β := fun (a : N) ↦ (↑I : Type))
        (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)))) j
        (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ))) x =
      Function.update (β := fun (a : N) ↦ (↑I : Type))
        (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ)))) i
        (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ))) x
⊢ Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ))) =
    Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)))

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 j : N
h : i ≠ j
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : (↑(y i) : ℝ) ≤ 1 / 2
h_2 : (↑(y j) : ℝ) ≤ 1 / 2
x_1 : N
pos :
  (if x_1 = j then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ))
    else if x_1 = i then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)) else y x_1) =
    if x_1 = i then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ))
    else if x_1 = j then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ)) else y x_1
⊢ Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ))) x_1 =
    Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ))) x_1

Tactic:
simp only [Function.update, eq_rec_constant, dite_eq_ite]

Premises used: Function.update, eq_rec_constant, dite_eq_ite
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i j : N
h : i ≠ j
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : (↑(y i) : ℝ) ≤ 1 / 2
h_2 : (↑(y j) : ℝ) ≤ 1 / 2
x_1 : N
pos : x_1 = j → ¬x_1 = i
⊢ (if x_1 = j then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ))
    else if x_1 = i then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)) else y x_1) =
    if x_1 = i then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ))
    else if x_1 = j then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ)) else y x_1

Tactic:
apply ite_ite_comm

Premises used: ite_ite_comm
-- 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
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : (↑(y i) : ℝ) ≤ 1 / 2
x_1 : N
h : i ≠ x_1
h_2 : (↑(y x_1) : ℝ) ≤ 1 / 2
⊢ ¬x_1 = i

Tactic:
h.symm

Premises used: Ne.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
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : (↑(y i) : ℝ) ≤ 1 / 2
x_1 : N
h : i ≠ x_1
h_2 : (↑(y x_1) : ℝ) ≤ 1 / 2
⊢ ¬x_1 = i

Tactic:
exact h.symm

Premises used: Ne.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 j : N
h : i ≠ j
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : (↑(y i) : ℝ) ≤ 1 / 2
h_2 : ¬(↑(y j) : ℝ) ≤ 1 / 2
neg :
  Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)) =
    Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)))
⊢ Eq.{u_2 + 1} (α := X)
    ((b : (a : N → (↑I : Type)) → X)
        (Function.update (β := fun (a : N) ↦ (↑I : Type))
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)))) j
          (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1))) :
      X)
    ((b : (a : N → (↑I : Type)) → X)
        (Function.update (β := fun (a : N) ↦ (↑I : Type))
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j
            (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)))
          i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)))) :
      X)

Tactic:
congr 1
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i j : N
h : i ≠ j
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : (↑(y i) : ℝ) ≤ 1 / 2
h_2 : ¬(↑(y j) : ℝ) ≤ 1 / 2
neg :
  ∀ (x : N),
    Function.update (β := fun (a : N) ↦ (↑I : Type))
        (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)))) j
        (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)) x =
      Function.update (β := fun (a : N) ↦ (↑I : Type))
        (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)))
        i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ))) x
⊢ Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)) =
    Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)))

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 j : N
h : i ≠ j
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : (↑(y i) : ℝ) ≤ 1 / 2
h_2 : ¬(↑(y j) : ℝ) ≤ 1 / 2
x_1 : N
neg :
  (if x_1 = j then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)
    else if x_1 = i then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)) else y x_1) =
    if x_1 = i then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ))
    else if x_1 = j then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1) else y x_1
⊢ Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)) x_1 =
    Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ))) x_1

Tactic:
simp only [Function.update, eq_rec_constant, dite_eq_ite]

Premises used: Function.update, eq_rec_constant, dite_eq_ite
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i j : N
h : i ≠ j
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : (↑(y i) : ℝ) ≤ 1 / 2
h_2 : ¬(↑(y j) : ℝ) ≤ 1 / 2
x_1 : N
neg : x_1 = j → ¬x_1 = i
⊢ (if x_1 = j then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1)
    else if x_1 = i then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ)) else y x_1) =
    if x_1 = i then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ))
    else if x_1 = j then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ) - 1) else y x_1

Tactic:
apply ite_ite_comm

Premises used: ite_ite_comm
-- 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
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : (↑(y i) : ℝ) ≤ 1 / 2
x_1 : N
h : i ≠ x_1
h_2 : ¬(↑(y x_1) : ℝ) ≤ 1 / 2
⊢ ¬x_1 = i

Tactic:
h.symm

Premises used: Ne.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
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : (↑(y i) : ℝ) ≤ 1 / 2
x_1 : N
h : i ≠ x_1
h_2 : ¬(↑(y x_1) : ℝ) ≤ 1 / 2
⊢ ¬x_1 = i

Tactic:
exact h.symm

Premises used: Ne.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 j : N
h : i ≠ j
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : ¬(↑(y i) : ℝ) ≤ 1 / 2
h_2 : (↑(y j) : ℝ) ≤ 1 / 2
pos :
  Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ))) =
    Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1))
⊢ Eq.{u_2 + 1} (α := X)
    ((c : (a : N → (↑I : Type)) → X)
        (Function.update (β := fun (a : N) ↦ (↑I : Type))
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i
            (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1)))
          j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ)))) :
      X)
    ((c : (a : N → (↑I : Type)) → X)
        (Function.update (β := fun (a : N) ↦ (↑I : Type))
          (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ)))) i
          (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1))) :
      X)

Tactic:
congr 1
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i j : N
h : i ≠ j
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : ¬(↑(y i) : ℝ) ≤ 1 / 2
h_2 : (↑(y j) : ℝ) ≤ 1 / 2
pos :
  ∀ (x : N),
    Function.update (β := fun (a : N) ↦ (↑I : Type))
        (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1)))
        j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ))) x =
      Function.update (β := fun (a : N) ↦ (↑I : Type))
        (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ)))) i
        (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1)) x
⊢ Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ))) =
    Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1))

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 j : N
h : i ≠ j
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : ¬(↑(y i) : ℝ) ≤ 1 / 2
h_2 : (↑(y j) : ℝ) ≤ 1 / 2
x_1 : N
pos :
  (if x_1 = j then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ))
    else if x_1 = i then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1) else y x_1) =
    if x_1 = i then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1)
    else if x_1 = j then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ)) else y x_1
⊢ Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y i (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ))) x_1 =
    Function.update (β := fun (a : N) ↦ (↑I : Type))
      (Function.update (β := fun (a : N) ↦ (↑I : Type)) y j (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1)) x_1

Tactic:
simp only [Function.update, eq_rec_constant, dite_eq_ite]

Premises used: Function.update, eq_rec_constant, dite_eq_ite
-- Module: Mathlib.Topology.Homotopy.HomotopyGroup
Goal:
N : Type u_1
X : Type u_2
inst : TopologicalSpace X
x : X
inst_1 : DecidableEq N
i j : N
h : i ≠ j
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : ¬(↑(y i) : ℝ) ≤ 1 / 2
h_2 : (↑(y j) : ℝ) ≤ 1 / 2
x_1 : N
pos : x_1 = j → ¬x_1 = i
⊢ (if x_1 = j then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ))
    else if x_1 = i then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1) else y x_1) =
    if x_1 = i then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y i) : ℝ) - 1)
    else if x_1 = j then Set.projIcc 0 1 transAt._proof_3 (2 * (↑(y j) : ℝ)) else y x_1

Tactic:
apply ite_ite_comm

Premises used: ite_ite_comm
-- 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
a b c d : (↑(Ω^ N X x) : Type (max u_1 u_2))
y : N → (↑I : Type)
h_1 : ¬(↑(y i) : ℝ) ≤ 1 / 2
x_1 : N
h : i ≠ x_1
h_2 : (↑(y x_1) : ℝ) ≤ 1 / 2
⊢ ¬x_1 = i

Tactic:
h.symm

Premises used: Ne.symm