Theorem: Board.lt_last_of_mem_path (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.path i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
conv at ha =>
  dsimp [Board.path]
  simp only [List.mem_append, or_assoc]
State after:
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : a ∈ Board.pathL i j ∨ a ∈ Board.pathB n i ∨ a ∈ Board.pathR m j ∨ a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1

State before:
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
ha : a ∈ Board.pathL i j ∨ a ∈ Board.pathB n i ∨ a ∈ Board.pathR m j ∨ a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
rcases ha with hL | hB | hR | hT
State after:
case inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hL : a ∈ Board.pathL i j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hB : a ∈ Board.pathB n i
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hR : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1

State before:
case inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hL : a ∈ Board.pathL i j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hB : a ∈ Board.pathB n i
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hR : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
. exact lt_last_of_mem_pathL i j a hL
State after:
case inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hB : a ∈ Board.pathB n i
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hR : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1

State before:
case inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hB : a ∈ Board.pathB n i
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hR : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
. exact lt_last_of_mem_pathB n i a hB
State after:
case inr.inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hR : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1

State before:
case inr.inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hR : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1

case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
. exact lt_last_of_mem_pathR m j a hR
State after:
case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1

State before:
case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
. exact lt_last_of_mem_pathT i j a hT
State after:
no goals

State before:
case inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hL : a ∈ Board.pathL i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
exact lt_last_of_mem_pathL i j a hL
State after:
no goals

State before:
case inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hB : a ∈ Board.pathB n i
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
exact lt_last_of_mem_pathB n i a hB
State after:
no goals

State before:
case inr.inr.inl
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hR : a ∈ Board.pathR m j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
exact lt_last_of_mem_pathR m j a hR
State after:
no goals

State before:
case inr.inr.inr
m n : Nat
i : Fin m
j : Fin n
a : Fin ((m + 1) * (n + 1))
hT : a ∈ Board.pathT i j
⊢ ↑a < (m + 1) * (n + 1) - 1
Tactic:
exact lt_last_of_mem_pathT i j a hT
State after:
no goals