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

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.path i j
Tactic:
dsimp [Board.path]
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathL i j ++ Board.pathB n i ++ Board.pathR m j ++ Board.pathT i j

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathL i j ++ Board.pathB n i ++ Board.pathR m j ++ Board.pathT i j
Tactic:
simp only [List.mem_append, or_assoc, not_or]
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathL i j ∧
    ¬Board.pivot i j ∈ Board.pathB n i ∧ ¬Board.pivot i j ∈ Board.pathR m j ∧ ¬Board.pivot i j ∈ Board.pathT i j

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ¬Board.pivot i j ∈ Board.pathL i j ∧
    ¬Board.pivot i j ∈ Board.pathB n i ∧ ¬Board.pivot i j ∈ Board.pathR m j ∧ ¬Board.pivot i j ∈ Board.pathT i j
Tactic:
exact ⟨
  pivot_not_mem_pathL i j,
  pivot_not_mem_pathB i j,
  pivot_not_mem_pathR i j,
  pivot_not_mem_pathT i j
⟩
State after:
no goals