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

State before:
n : Nat
⊢ inversions 1 = #[]
Tactic:
apply Array.ext'
State after:
case h
n : Nat
⊢ (inversions 1).data = #[].data

State before:
case h
n : Nat
⊢ (inversions 1).data = #[].data
Tactic:
generalize (inversions 1).data = l
State after:
case h
n : Nat
l : List (Inversion 1)
⊢ l = #[].data

State before:
case h
n : Nat
l : List (Inversion 1)
⊢ l = #[].data
Tactic:
cases l with
| nil => rfl
| cons iv l => exact iv.elim1
State after:
no goals

State before:
case h.nil
n : Nat
⊢ [] = #[].data
Tactic:
rfl
State after:
no goals

State before:
case h.cons
n : Nat
iv : Inversion 1
l : List (Inversion 1)
⊢ iv :: l = #[].data
Tactic:
exact iv.elim1
State after:
no goals