no goals
α : Type ?u.19719
a : Array α
i j : Fin (size a)
⊢ j.val < size (set a i (get a j))
simp [j.2]
no goals
α : Type u_1
a : Array α
i j : Fin (size a)
⊢ swap a i j = set (set a i (get a j)) { val := j.val, isLt := (_ : j.val < size (set a i a[j.val])) } (get a i)
simp [swap, fin_cast_val]