Theorem: Partial.update_ne_comm (ReactorModel/Extensions.lean)

State before:
α : Sort u_1
β : Type u_2
inst✝ : DecidableEq α
f : α ⇀ β
a₁ a₂ : α
h : a₁ ≠ a₂
g₁ g₂ : β → β
⊢ update (update f a₁ g₁) a₂ g₂ = update (update f a₂ g₂) a₁ g₁
Tactic:
ext1 a
State after:
case h
α : Sort u_1
β : Type u_2
inst✝ : DecidableEq α
f : α ⇀ β
a₁ a₂ : α
h : a₁ ≠ a₂
g₁ g₂ : β → β
a : α
⊢ update (update f a₁ g₁) a₂ g₂ a = update (update f a₂ g₂) a₁ g₁ a

State before:
case h
α : Sort u_1
β : Type u_2
inst✝ : DecidableEq α
f : α ⇀ β
a₁ a₂ : α
h : a₁ ≠ a₂
g₁ g₂ : β → β
a : α
⊢ update (update f a₁ g₁) a₂ g₂ a = update (update f a₂ g₂) a₁ g₁ a
Tactic:
by_cases a = a₁ <;> by_cases a = a₂ <;> simp_all [update]
State after:
no goals