Theorem: Subarray.size_as_swap (Algdata/Data/Array/Subarray.lean)

State before:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ Array.size (swap x i j).as = Array.size x.as
Tactic:
rw [as_swap, Array.size_swap]
State after:
no goals