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

State before:
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : a ∈ Board.pathL i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
conv at ha => dsimp [Board.pathL]; rw [List.mem_ofFn]
State after:
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      a
⊢ ↑a < (m + 1) * (n + 1) - 1

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

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

State before:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ ↑(Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))) <
    (m + 1) * (n + 1) - 1
Tactic:
dsimp
State after:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ ↑i + (m + 1) * (↑j + k + 1) < (m + 1) * (n + 1) - 1

State before:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ ↑i + (m + 1) * (↑j + k + 1) < (m + 1) * (n + 1) - 1
Tactic:
conv =>
  change (i.1 + (m+1)*(j.1+k+1)).succ ≤ (m+1)*n+m
  rw [← Nat.succ_add i.1, Nat.add_comm _ m]
State after:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ Nat.succ ↑i + (m + 1) * (↑j + k + 1) ≤ m + (m + 1) * n

State before:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ Nat.succ ↑i + (m + 1) * (↑j + k + 1) ≤ m + (m + 1) * n
Tactic:
refine Nat.add_le_add i.2 ?_
State after:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ (m + 1) * (↑j + k + 1) ≤ (m + 1) * n

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

State before:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ ↑j + k + 1 ≤ n
Tactic:
rewrite [Nat.add_comm j.1 k]
State after:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ k + ↑j + 1 ≤ n

State before:
case refl
m n : Nat
i : Fin m
j : Fin n
k : Nat
hk : k < n - ↑j
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castSucc i) (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd (↑j) i_1))) =
      Fin.rlexProd (Fin.castSucc i)
        (Fin.castLE (_ : Nat.succ (↑j + (n - ↑j)) ≤ n + 1) (Fin.succ (Fin.natAdd ↑j { val := k, isLt := hk })))
⊢ k + ↑j + 1 ≤ n
Tactic:
exact Nat.add_lt_of_lt_sub hk
State after:
no goals