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

State before:
m n : Nat
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
conv at ha => dsimp [Board.pathR]; rw [List.mem_ofFn]
State after:
m n : Nat
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : ∃ i, Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } = a
⊢ ↑a < (m + 1) * (n + 1) - 1

State before:
m n : Nat
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : ∃ i, Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } = a
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
have ⟨⟨k,hk⟩,ha⟩ := ha
State after:
m n : Nat
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha✝ : ∃ i, Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } = a
k : Nat
hk : k < n - ↑j
ha :
  Fin.rlexProd (Fin.last m)
      { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) } =
    a
⊢ ↑a < (m + 1) * (n + 1) - 1

State before:
m n : Nat
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha✝ : ∃ i, Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } = a
k : Nat
hk : k < n - ↑j
ha :
  Fin.rlexProd (Fin.last m)
      { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) } =
    a
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
cases ha
State after:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ ↑(Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }) <
    (m + 1) * (n + 1) - 1

State before:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ ↑(Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }) <
    (m + 1) * (n + 1) - 1
Tactic:
simp
State after:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ m + (m + 1) * (n - k - 1) < (m + 1) * (n + 1) - 1

State before:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ m + (m + 1) * (n - k - 1) < (m + 1) * (n + 1) - 1
Tactic:
conv => rhs; change (m+1)*n + m; rw [Nat.add_comm _ m]
State after:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ m + (m + 1) * (n - k - 1) < m + (m + 1) * n

State before:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ m + (m + 1) * (n - k - 1) < m + (m + 1) * n
Tactic:
refine Nat.add_lt_add_left ?_ m
State after:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ (m + 1) * (n - k - 1) < (m + 1) * n

State before:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ (m + 1) * (n - k - 1) < (m + 1) * n
Tactic:
refine Nat.mul_lt_mul_of_pos_left ?_ m.zero_lt_succ
State after:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ n - k - 1 < n

State before:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ n - k - 1 < n
Tactic:
rewrite [← Nat.sub_add_eq]
State after:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ n - (k + 1) < n

State before:
case refl
m n : Nat
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i,
    Fin.rlexProd (Fin.last m) { val := n - ↑i - 1, isLt := (_ : n - ↑i - 1 < n + 1) } =
      Fin.rlexProd (Fin.last m)
        { val := n - ↑{ val := k, isLt := hk } - 1, isLt := (_ : n - ↑{ val := k, isLt := hk } - 1 < n + 1) }
⊢ n - (k + 1) < n
Tactic:
exact n.sub_lt j.pos k.zero_lt_succ
State after:
no goals