no goals
α : Type u
β : Type v
ι : Type u_2
π : ι → Type u_1
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → SemilatticeSup (π i)
f : (i : ι) → π i
i : ι
a b : π i
j : ι
⊢ update f i (a ⊔ b) j = (update f i a ⊔ update f i b) j
obtain rfl | hji := eq_or_ne j i <;> simp [update_noteq, *]