apply dite (j.1 = k) <;> apply dite (i.1 = k) <;> intro hik hjk
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]
case t.t
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

case t.e
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

case e.t
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

case e.e
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]