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

State before:
C : Type u_2
ι : Type u_3
τ : Type u_1
inst✝¹ : Indexed C ι τ
inst✝ : LawfulIndexed C ι τ
i : ι
f : τ → τ
cont : C
⊢ get (update cont i f) i = f (get cont i)
Tactic:
simp [LawfulIndexed.get_update_eq]
State after:
no goals