no goals
α' : Sort u_1
α : Sort u_2
β : Sort u_3
inst✝¹ : DecidableEq α'
inst✝ : DecidableEq α
f : α → β
g : α' ≃ α
a : α
v : β
⊢ update f a v ∘ ↑g = update (f ∘ ↑g) (↑g.symm a) v
rw [← update_comp_eq_of_injective _ g.injective, g.apply_symm_apply]