awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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)
⊢ 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)
have 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 sorry (2 * (↑(x_1 i) : ℝ)))) :
      X)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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)
⊢ 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)
have 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 sorry (2 * (↑(x_1 i) : ℝ) - 1))) :
      X)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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)
    (((↑((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)
have 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 sorry (2 * (↑(x_1 i) : ℝ)))) :
    X)
Tactic: change f _ = _
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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)
    (((↑((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)
have 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 sorry (2 * (↑(x_1 i) : ℝ) - 1))) :
    X)
Tactic: change g _ = _
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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))
⊢ 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)
have 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)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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)
⊢ 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)
have 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)
Tactic: change _ = f _
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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)
⊢ 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)
have 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))
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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)
⊢ 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))
have 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
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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))
⊢ transAt i (transAt j a b) (transAt j c d) = transAt j (transAt i a c) (transAt i b d)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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
⊢ 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)
have 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) : ℝ)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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
⊢ 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) : ℝ)))
have 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
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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
⊢ 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
have 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
Tactic: simp only [Function.update, eq_rec_constant, dite_eq_ite]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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
⊢ (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
have pos : x_1 = j → ¬x_1 = i
Tactic: apply ite_ite_comm
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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
⊢ 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)
have 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) : ℝ)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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
⊢ 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) : ℝ)))
have 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
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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
⊢ 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
have 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
Tactic: simp only [Function.update, eq_rec_constant, dite_eq_ite]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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
⊢ (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
have neg : x_1 = j → ¬x_1 = i
Tactic: apply ite_ite_comm
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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
⊢ 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)
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.Homotopy.HomotopyGroup (goal)
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
⊢ 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))
have 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
Tactic: ext1