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

State before:
n : Nat
⊢ inversionNum 1 = 0
Tactic:
rewrite [inversionNum_eq_card_inversion]
State after:
n : Nat
⊢ BishopFin.card (Inversion 1) = 0

State before:
n : Nat
⊢ BishopFin.card (Inversion 1) = 0
Tactic:
show (inversions 1).toList.length = 0
State after:
n : Nat
⊢ List.length (Array.toList (inversions 1)) = 0

State before:
n : Nat
⊢ List.length (Array.toList (inversions 1)) = 0
Tactic:
rewrite [inversions_one]
State after:
n : Nat
⊢ List.length (Array.toList #[]) = 0

State before:
n : Nat
⊢ List.length (Array.toList #[]) = 0
Tactic:
rfl
State after:
no goals