Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
⊢ a
      (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
        (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) =
    a
      (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
        (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))))

pp: case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
⊢ b
      (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
        (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) =
    b
      (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
        (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))))

pp: case pos
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
⊢ c
      (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
        (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) =
    c
      (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
        (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)))

pp: case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
⊢ d
      (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
        (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) =
    d
      (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
        (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)))

Tactic:
<;>

Goal state after:
case pos
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
⊢ a
      (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
        (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) =
    a
      (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
        (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))))

case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
⊢ b
      (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
        (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) =
    b
      (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
        (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))))

case pos
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
⊢ c
      (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
        (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) =
    c
      (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
        (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)))

case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
⊢ d
      (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
        (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) =
    d
      (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
        (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)))