all_goals simp only [hik, hjk, if_true, if_false]
case t.t
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ↑j = k
hik : ↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

case t.e
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ¬↑j = k
hik : ↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

case e.t
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ↑j = k
hik : ¬↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

case e.e
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ¬↑j = k
hik : ¬↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]
no goals