no goals
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Lattice (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' uIcc (f i) b = uIcc f (update f i b)
simpa using image_update_uIcc f i (f i) b