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

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathR m j
Tactic:
dsimp [Board.pathR, Board.pivot]
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j) ∈
      List.ofFn fun x => Fin.rlexProd (Fin.last m) { val := n - ↑x - 1, isLt := (_ : n - ↑x - 1 < n + 1) }

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j) ∈
      List.ofFn fun x => Fin.rlexProd (Fin.last m) { val := n - ↑x - 1, isLt := (_ : n - ↑x - 1 < n + 1) }
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.last m) { val := n - ↑x - 1, isLt := (_ : n - ↑x - 1 < n + 1) } =
        Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ∀ (x : Fin (n - ↑j)),
    ¬Fin.rlexProd (Fin.last m) { val := n - ↑x - 1, isLt := (_ : n - ↑x - 1 < n + 1) } =
        Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)
Tactic:
intro k
State after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ¬Fin.rlexProd (Fin.last m) { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } =
      Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)

State before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ¬Fin.rlexProd (Fin.last m) { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } =
      Fin.rlexProd (Fin.castSucc i) (Fin.castSucc 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)
⊢ ↑(Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)) <
    ↑(Fin.rlexProd (Fin.last m) { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) })

State before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑(Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)) <
    ↑(Fin.rlexProd (Fin.last m) { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) })
Tactic:
apply Fin.rlexProd_lt_iff.mpr
State after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ Fin.castSucc j < { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∨
    Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∧ Fin.castSucc i < Fin.last m

State before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ Fin.castSucc j < { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∨
    Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∧ Fin.castSucc i < Fin.last m
Tactic:
show j.1 < n - k.1 - 1 ∨ _ = _ ∧ i.1 < m
State after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑j < n - ↑k - 1 ∨ Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∧ ↑i < m

State before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ↑j < n - ↑k - 1 ∨ Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∧ ↑i < m
Tactic:
rewrite [Decidable.or_iff_not_imp_left]
State after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ¬↑j < n - ↑k - 1 → Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∧ ↑i < m

State before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ ¬↑j < n - ↑k - 1 → Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) } ∧ ↑i < m
Tactic:
simp only [Nat.not_lt, Fin.is_lt, and_true]
State after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ n - ↑k - 1 ≤ ↑j → Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) }

State before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
⊢ n - ↑k - 1 ≤ ↑j → Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) }
Tactic:
intro h
State after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) }

State before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ Fin.castSucc j = { val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) }
Tactic:
apply Fin.eq_of_val_eq
State after:
case a
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑(Fin.castSucc j) = ↑{ val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) }

State before:
case a
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑(Fin.castSucc j) = ↑{ val := n - ↑k - 1, isLt := (_ : n - ↑k - 1 < n + 1) }
Tactic:
dsimp
State after:
case a
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j = n - ↑k - 1

State before:
case a
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j = n - ↑k - 1
Tactic:
apply Nat.le_antisymm ?_ h
State after:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j ≤ n - ↑k - 1

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

State before:
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j ≤ n - (↑k + 1)
Tactic:
apply Nat.le_sub_of_add_le
State after:
case h
m n : Nat
i : Fin m
j : Fin n
k : Fin (n - ↑j)
h : n - ↑k - 1 ≤ ↑j
⊢ ↑j + (↑k + 1) ≤ n

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

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

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