rcases j with ⟨j,hj⟩
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
f : τ → τ
i : ℕ
hi : i < size cont
j : Fin (size (update cont ⟨i, hi⟩ f))
⊢ get (update cont ⟨i, hi⟩ f) j = if ↑⟨i, hi⟩ = ↑j then f (get cont (Fin.cast ⋯ j)) else get cont (Fin.cast ⋯ j)
case mk.mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
f : τ → τ
i : ℕ
hi : i < size cont
j : ℕ
hj : j < size (update cont ⟨i, hi⟩ f)
⊢ get (update cont ⟨i, hi⟩ f) ⟨j, hj⟩ =
    if ↑⟨i, hi⟩ = ↑⟨j, hj⟩ then f (get cont (Fin.cast ⋯ ⟨j, hj⟩)) else get cont (Fin.cast ⋯ ⟨j, hj⟩)