Theorem: step_north (Maze.lean)

State before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
N : Escapable { size := s, position := { x := x, y := y }, walls := w }
⊢ Escapable { size := s, position := { x := x, y := y + 1 }, walls := w }
Tactic:
have hmm : GameState.mk s ⟨x,y⟩ w = make_move ⟨s,⟨x, y+1⟩,w⟩ Move.north :=
  by have h' : y + 1 - 1 = y := rfl
     simp [h', hclear']
State after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
N : 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, y := y + 1 }, walls := w } Move.north
⊢ Escapable { size := s, position := { x := x, y := y + 1 }, walls := w }

State before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
N : 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, y := y + 1 }, walls := w } Move.north
⊢ Escapable { size := s, position := { x := x, y := y + 1 }, walls := w }
Tactic:
rw [hmm] at N
State after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
N : Escapable (make_move { size := s, position := { x := x, y := y + 1 }, walls := w } Move.north)
hmm :
  { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x, y := y + 1 }, walls := w } Move.north
⊢ Escapable { size := s, position := { x := x, y := y + 1 }, walls := w }

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

State before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
N : 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, y := y + 1 }, walls := w } Move.north
Tactic:
have h' : y + 1 - 1 = y := rfl
State after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
N : Escapable { size := s, position := { x := x, y := y }, walls := w }
h' : y + 1 - 1 = y
⊢ { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x, y := y + 1 }, walls := w } Move.north

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