no goals
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Ioo a b = Ioo (update f i a) (update f i b)
rw [← Ico_diff_left, ← Ico_diff_left, image_diff (update_injective _ _), image_singleton,
  image_update_Ico]