split <;> simp [*]
C : Type u_3
ι : Type u_1
τ : Type u_2
inst✝² : Indexed C ι τ
inst✝¹ : LawfulIndexed C ι τ
inst✝ : DecidableEq ι
cont : C
i j : ι
a : τ
⊢ get (set cont i a) j = if i = j then a else get cont j
no goals