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

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

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

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

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

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

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

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