case h
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_1
inst✝ : DecidableEq α
β : α → Sort u_2
a : α
v w : β a
f : (a : α) → β a
b : α
⊢ update (update f a v) a w b = update f a w b
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b : β✝ a✝
α : Sort u_1
inst✝ : DecidableEq α
β : α → Sort u_2
a : α
v w : β a
f : (a : α) → β a
⊢ update (update f a v) a w = update f a w
funext b
no goals
case h
α✝ : Sort u
β✝ : α✝ → Sort v
α' : Sort w
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq α'
f✝ g : (a : α✝) → β✝ a
a✝ : α✝
b✝ : β✝ a✝
α : Sort u_1
inst✝ : DecidableEq α
β : α → Sort u_2
a : α
v w : β a
f : (a : α) → β a
b : α
⊢ update (update f a v) a w b = update f a w b
by_cases h : b = a <;> simp [update, h]