Theorem: LoVe.update_override (LoVe/LoVelib.lean)

State before:
name : String
val₁ val₂ : ℕ
s : State
⊢ State.update name val₁ (State.update name val₂ s) = State.update name val₁ s
Tactic:
apply funext
State after:
case h
name : String
val₁ val₂ : ℕ
s : State
⊢ ∀ (x : String), State.update name val₁ (State.update name val₂ s) x = State.update name val₁ s x

State before:
case h
name : String
val₁ val₂ : ℕ
s : State
⊢ ∀ (x : String), State.update name val₁ (State.update name val₂ s) x = State.update name val₁ s x
Tactic:
intro name'
State after:
case h
name : String
val₁ val₂ : ℕ
s : State
name' : String
⊢ State.update name val₁ (State.update name val₂ s) name' = State.update name val₁ s name'

State before:
case h
name : String
val₁ val₂ : ℕ
s : State
name' : String
⊢ State.update name val₁ (State.update name val₂ s) name' = State.update name val₁ s name'
Tactic:
cases Classical.em (name' = name) with
| inl h => simp [h]
| inr h => simp [h]
State after:
no goals

State before:
case h.inl
name : String
val₁ val₂ : ℕ
s : State
name' : String
h : name' = name
⊢ State.update name val₁ (State.update name val₂ s) name' = State.update name val₁ s name'
Tactic:
simp [h]
State after:
no goals

State before:
case h.inr
name : String
val₁ val₂ : ℕ
s : State
name' : String
h : ¬name' = name
⊢ State.update name val₁ (State.update name val₂ s) name' = State.update name val₁ s name'
Tactic:
simp [h]
State after:
no goals