α : Type u_1
a : Array α
i j : Fin (size a)
⊢ size (set (set a i (get a j)) (Eq.rec j (_ : size a = size (set a i (get a j)))) (get a i)) = size a
α : Type u_1
a : Array α
i j : Fin (size a)
⊢ size (swap a i j) = size a
show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
no goals
α : Type u_1
a : Array α
i j : Fin (size a)
⊢ size (set (set a i (get a j)) (Eq.rec j (_ : size a = size (set a i (get a j)))) (get a i)) = size a
rw [size_set, size_set]