Theorem: MiniChess.foo (Talk/11MiniChess.lean)

State before:
p : Piece
n✝ : ℕ
start stop : Pos n✝
⊢ Piece.LegalMove start stop p → start ≠ stop
Tactic:
intro legal
State after:
p : Piece
n✝ : ℕ
start stop : Pos n✝
legal : Piece.LegalMove start stop p
⊢ start ≠ stop

State before:
p : Piece
n✝ : ℕ
start stop : Pos n✝
legal : Piece.LegalMove start stop p
⊢ start ≠ stop
Tactic:
cases legal with
| rookHorizontal h _ => exact h
| rookVertical h _ => exact h
| king h _ _ => exact h
State after:
no goals

State before:
case rookHorizontal
n✝ : ℕ
start stop : Pos n✝
h : start ≠ stop
a✝ : start.y = stop.y
⊢ start ≠ stop
Tactic:
exact h
State after:
no goals

State before:
case rookVertical
n✝ : ℕ
start stop : Pos n✝
h : start ≠ stop
a✝ : start.x = stop.x
⊢ start ≠ stop
Tactic:
exact h
State after:
no goals

State before:
case king
n✝ : ℕ
start stop : Pos n✝
h : start ≠ stop
a✝¹ : Nat.dist ↑start.x ↑stop.x ≤ 1
a✝ : Nat.dist ↑start.y ↑stop.y ≤ 1
⊢ start ≠ stop
Tactic:
exact h
State after:
no goals