Theorem: Permutation.inversions_size_eq_card (Fifteen/Data/Permutation/Inversion.lean)

State before:
n : Nat
x : Permutation n
⊢ List.length (inversions x).data = List.length (Array.toList (inversions x))
Tactic:
rw [Array.toList_eq]
State after:
no goals