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

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathB n i
Tactic:
dsimp [Board.pathB]
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈
      List.ofFn fun k =>
        Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i k)) (_ : ↑(Fin.succ (Fin.eadd i k)) < m + 1)) (Fin.last n)

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈
      List.ofFn fun k =>
        Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i k)) (_ : ↑(Fin.succ (Fin.eadd i k)) < m + 1)) (Fin.last n)
Tactic:
simp only [List.mem_ofFn, not_exists]
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ ∀ (x : Fin (m - ↑i - 1)),
    ¬Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i x)) (_ : ↑(Fin.succ (Fin.eadd i x)) < m + 1)) (Fin.last n) =
        Board.pivot i j

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ∀ (x : Fin (m - ↑i - 1)),
    ¬Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i x)) (_ : ↑(Fin.succ (Fin.eadd i x)) < m + 1)) (Fin.last n) =
        Board.pivot i j
Tactic:
intro k
State after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ¬Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i k)) (_ : ↑(Fin.succ (Fin.eadd i k)) < m + 1)) (Fin.last n) =
      Board.pivot i j

State before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ¬Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i k)) (_ : ↑(Fin.succ (Fin.eadd i k)) < m + 1)) (Fin.last n) =
      Board.pivot i j
Tactic:
refine Fin.ne_of_val_ne (Nat.ne_of_gt ?_)
State after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑(Board.pivot i j) <
    ↑(Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i k)) (_ : ↑(Fin.succ (Fin.eadd i k)) < m + 1)) (Fin.last n))

State before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (m - ↑i - 1)
⊢ ↑(Board.pivot i j) <
    ↑(Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i k)) (_ : ↑(Fin.succ (Fin.eadd i k)) < m + 1)) (Fin.last n))
Tactic:
exact Fin.rlexProd_lt_of_snd _ _ j.2
State after:
no goals