Theorem: LeanColls.Seq.get_set (LeanColls/Classes/Seq.lean)

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
x : τ
j : Fin (size (set cont i x))
⊢ get (set cont i x) j = if ↑i = ↑j then x else get cont (Fin.cast ⋯ j)
Tactic:
by_cases i.val = j.val <;> simp [*]
State after:
no goals