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

State before:
n i : Nat
h : i + 1 < n
⊢ inversionNum (transposAdj i h) = 1
Tactic:
rewrite [inversionNum_eq_card_inversion]
State after:
n i : Nat
h : i + 1 < n
⊢ BishopFin.card (Inversion (transposAdj i h)) = 1

State before:
n i : Nat
h : i + 1 < n
⊢ BishopFin.card (Inversion (transposAdj i h)) = 1
Tactic:
refine Nat.le_antisymm ?le ?ge
State after:
case le
n i : Nat
h : i + 1 < n
⊢ BishopFin.card (Inversion (transposAdj i h)) ≤ 1

case ge
n i : Nat
h : i + 1 < n
⊢ 1 ≤ BishopFin.card (Inversion (transposAdj i h))

State before:
case le
n i : Nat
h : i + 1 < n
⊢ BishopFin.card (Inversion (transposAdj i h)) ≤ 1

case ge
n i : Nat
h : i + 1 < n
⊢ 1 ≤ BishopFin.card (Inversion (transposAdj i h))
Tactic:
. exact BishopFin.card_subsingleton
State after:
case ge
n i : Nat
h : i + 1 < n
⊢ 1 ≤ BishopFin.card (Inversion (transposAdj i h))

State before:
case ge
n i : Nat
h : i + 1 < n
⊢ 1 ≤ BishopFin.card (Inversion (transposAdj i h))
Tactic:
. exact BishopFin.card_nonempty
State after:
no goals

State before:
case le
n i : Nat
h : i + 1 < n
⊢ BishopFin.card (Inversion (transposAdj i h)) ≤ 1
Tactic:
exact BishopFin.card_subsingleton
State after:
no goals

State before:
case ge
n i : Nat
h : i + 1 < n
⊢ 1 ≤ BishopFin.card (Inversion (transposAdj i h))
Tactic:
exact BishopFin.card_nonempty
State after:
no goals