Theorem: step_south (Maze.lean)

State before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y + 1 } w = true
hinbounds : y + 1 ≤ s.y
S : Escapable { size := s, position := { x := x, y := y + 1 }, walls := w }
⊢ Escapable { size := s, position := { x := x, y := y }, walls := w }
Tactic:
have hmm : GameState.mk s ⟨x,y+1⟩ w = make_move ⟨s,⟨x, y⟩,w⟩ Move.south :=
     by simp [hclear', hinbounds]
State after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y + 1 } w = true
hinbounds : y + 1 ≤ s.y
S : Escapable { size := s, position := { x := x, y := y + 1 }, walls := w }
hmm :
  { size := s, position := { x := x, y := y + 1 }, walls := w } =
    make_move { size := s, position := { x := x, y := y }, walls := w } Move.south
⊢ 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, y := y + 1 } w = true
hinbounds : y + 1 ≤ s.y
S : Escapable { size := s, position := { x := x, y := y + 1 }, walls := w }
hmm :
  { size := s, position := { x := x, y := y + 1 }, walls := w } =
    make_move { size := s, position := { x := x, y := y }, walls := w } Move.south
⊢ Escapable { size := s, position := { x := x, y := y }, walls := w }
Tactic:
rw [hmm] at S
State after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y + 1 } w = true
hinbounds : y + 1 ≤ s.y
S : Escapable (make_move { size := s, position := { x := x, y := y }, walls := w } Move.south)
hmm :
  { size := s, position := { x := x, y := y + 1 }, walls := w } =
    make_move { size := s, position := { x := x, y := y }, walls := w } Move.south
⊢ 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, y := y + 1 } w = true
hinbounds : y + 1 ≤ s.y
S : Escapable (make_move { size := s, position := { x := x, y := y }, walls := w } Move.south)
hmm :
  { size := s, position := { x := x, y := y + 1 }, walls := w } =
    make_move { size := s, position := { x := x, y := y }, walls := w } Move.south
⊢ Escapable { size := s, position := { x := x, y := y }, walls := w }
Tactic:
exact .Step ⟨s,⟨x,y⟩,w⟩ Move.south S
State after:
no goals

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