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

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

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

State before:
case h
name : String
s : State
name' : String
⊢ State.update name (s name) s name' = s name'
Tactic:
simp [State.update]
State after:
case h
name : String
s : State
name' : String
⊢ name' = name → s name = s name'

State before:
case h
name : String
s : State
name' : String
⊢ name' = name → s name = s name'
Tactic:
intro heq
State after:
case h
name : String
s : State
name' : String
heq : name' = name
⊢ s name = s name'

State before:
case h
name : String
s : State
name' : String
heq : name' = name
⊢ s name = s name'
Tactic:
simp [*]
State after:
no goals