Theorem: LeanColls.Indexed.get_update (LeanColls/Classes/Indexed/Basic.lean)

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