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

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

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

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

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

State before:
case refl
m n : Nat
i : Fin m
k : Nat
hk : k < m - ↑i - 1
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i i_1)) (_ : ↑(Fin.succ (Fin.eadd i i_1)) < m + 1)) (Fin.last n) =
      Fin.rlexProd
        (Fin.castLT (Fin.succ (Fin.eadd i { val := k, isLt := hk }))
          (_ : ↑(Fin.succ (Fin.eadd i { val := k, isLt := hk })) < m + 1))
        (Fin.last n)
⊢ ↑i + k + 1 + (m + 1) * n < (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
i : Fin m
k : Nat
hk : k < m - ↑i - 1
ha :
  ∃ i_1,
    Fin.rlexProd (Fin.castLT (Fin.succ (Fin.eadd i i_1)) (_ : ↑(Fin.succ (Fin.eadd i i_1)) < m + 1)) (Fin.last n) =
      Fin.rlexProd
        (Fin.castLT (Fin.succ (Fin.eadd i { val := k, isLt := hk }))
          (_ : ↑(Fin.succ (Fin.eadd i { val := k, isLt := hk })) < m + 1))
        (Fin.last n)
⊢ ↑i + k + 1 + (m + 1) * n < m + (m + 1) * n

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

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

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