no goals
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.19213
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : α
x : γ
⊢ update f (inl i) x (inl j) = update (f ∘ inl) i x j
rw [← update_inl_comp_inl, Function.comp_apply]