Theorem: MiniChess.Board.set_different (Talk/11MiniChess.lean)

State before:
n : ℕ
pos' pos : Pos n
p? : Option PPiece
b : Board n
⊢ pos' ≠ pos → set b pos p? pos' = b pos'
Tactic:
intro h
State after:
n : ℕ
pos' pos : Pos n
p? : Option PPiece
b : Board n
h : pos' ≠ pos
⊢ set b pos p? pos' = b pos'

State before:
n : ℕ
pos' pos : Pos n
p? : Option PPiece
b : Board n
h : pos' ≠ pos
⊢ set b pos p? pos' = b pos'
Tactic:
simp [set]
State after:
n : ℕ
pos' pos : Pos n
p? : Option PPiece
b : Board n
h : pos' ≠ pos
⊢ pos = pos' → p? = b pos'

State before:
n : ℕ
pos' pos : Pos n
p? : Option PPiece
b : Board n
h : pos' ≠ pos
⊢ pos = pos' → p? = b pos'
Tactic:
intros
State after:
n : ℕ
pos' pos : Pos n
p? : Option PPiece
b : Board n
h : pos' ≠ pos
a✝ : pos = pos'
⊢ p? = b pos'

State before:
n : ℕ
pos' pos : Pos n
p? : Option PPiece
b : Board n
h : pos' ≠ pos
a✝ : pos = pos'
⊢ p? = b pos'
Tactic:
simp_all
State after:
no goals