Theorem: Board.pivot_lt_last (Fifteen/Data/Board/Cycle.lean)

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ↑(Board.pivot i j) < (m + 1) * (n + 1) - 1
Tactic:
conv =>
  rhs; change (m+1)*n + m; rw [Nat.add_comm _ m]
  change (Fin.rlexProd (Fin.last m) (Fin.last n)).1
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ ↑(Board.pivot i j) < ↑(Fin.rlexProd (Fin.last m) (Fin.last n))

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ↑(Board.pivot i j) < ↑(Fin.rlexProd (Fin.last m) (Fin.last n))
Tactic:
exact Fin.rlexProd_lt_of_snd _ _ j.2
State after:
no goals