Theorem: step_east (Maze.lean)

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

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

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

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