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