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

State before:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ swap x i j = swap x j i
Tactic:
simp [swap]
State after:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ Array.swap x.as (castIndex x i) (castIndex x j) = Array.swap x.as (castIndex x j) (castIndex x i)

State before:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ Array.swap x.as (castIndex x i) (castIndex x j) = Array.swap x.as (castIndex x j) (castIndex x i)
Tactic:
exact x.as.swap_comm _ _
State after:
no goals