Theorem: step_west (Maze.lean)

State before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
W : Escapable { size := s, position := { x := x, y := y }, walls := w }
⊢ Escapable { size := s, position := { x := x + 1, y := y }, walls := w }
Tactic:
have hmm : GameState.mk s ⟨x,y⟩ w = make_move ⟨s,⟨x+1, y⟩,w⟩ Move.west :=
         by have h' : x + 1 - 1 = x := rfl
            simp [h', hclear']
State after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
W : Escapable { size := s, position := { x := x, y := y }, walls := w }
hmm :
  { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west
⊢ Escapable { size := s, position := { x := x + 1, y := y }, walls := w }

State before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
W : Escapable { size := s, position := { x := x, y := y }, walls := w }
hmm :
  { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west
⊢ Escapable { size := s, position := { x := x + 1, y := y }, walls := w }
Tactic:
rw [hmm] at W
State after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
W : Escapable (make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west)
hmm :
  { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west
⊢ Escapable { size := s, position := { x := x + 1, y := y }, walls := w }

State before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
W : Escapable (make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west)
hmm :
  { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west
⊢ Escapable { size := s, position := { x := x + 1, y := y }, walls := w }
Tactic:
exact .Step ⟨s,⟨x+1,y⟩,w⟩ Move.west W
State after:
no goals

State before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
W : Escapable { size := s, position := { x := x, y := y }, walls := w }
⊢ { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west
Tactic:
have h' : x + 1 - 1 = x := rfl
State after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
W : Escapable { size := s, position := { x := x, y := y }, walls := w }
h' : x + 1 - 1 = x
⊢ { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west

State before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
W : Escapable { size := s, position := { x := x, y := y }, walls := w }
h' : x + 1 - 1 = x
⊢ { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west
Tactic:
simp [h', hclear']
State after:
no goals