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

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathL i j
Tactic:
dsimp [Board.pathL]
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈
      List.ofFn fun k =>
        Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k)))

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

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ∀ (x : Fin (n - ↑j)),
    ¬Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) x))) =
        Board.pivot i j
Tactic:
intro k
State after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ¬Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k))) =
      Board.pivot i j

State before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ¬Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k))) =
      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 (n - ↑j)
⊢ ↑(Board.pivot i j) <
    ↑(Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k))))

State before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑(Board.pivot i j) <
    ↑(Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k))))
Tactic:
apply Fin.rlexProd_lt_of_snd
State after:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ Fin.castSucc j < Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k))

State before:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ Fin.castSucc j < Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) k))
Tactic:
show j.1 < j.1 + k + 1
State after:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑j < ↑j + ↑k + 1

State before:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑j < ↑j + ↑k + 1
Tactic:
rewrite [Nat.add_assoc]
State after:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑j < ↑j + (↑k + 1)

State before:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑j < ↑j + (↑k + 1)
Tactic:
exact j.1.lt_add_of_pos_right k.1.zero_lt_succ
State after:
no goals