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

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathT i j
Tactic:
dsimp [Board.pathT, 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 { val := m - ↑x - 1, isLt := (_ : m - ↑x - 1 < m + 1) } (Fin.castSucc j)

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 { val := m - ↑x - 1, isLt := (_ : m - ↑x - 1 < m + 1) } (Fin.castSucc j)
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 { val := m - ↑x - 1, isLt := (_ : m - ↑x - 1 < m + 1) } (Fin.castSucc j) =
        Fin.rlexProd (Fin.castSucc i) (Fin.castSucc j)

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

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

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

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

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

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

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

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

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