rw [List.get_eq_get _ (List.set (toList cont) i x) _ _ (toList_set ..) ?idx_eq]
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))
h : ↑i ≠ ↑j
⊢ (toList (set cont i x)).get (Fin.cast ⋯ j) = (toList cont).get (Fin.cast ⋯ j)
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))
h : ↑i ≠ ↑j
⊢ ((toList cont).set (↑i) x).get ?m.15919 = (toList cont).get (Fin.cast ⋯ j)

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))
h : ↑i ≠ ↑j
⊢ Fin ((toList cont).set (↑i) x).length

case idx_eq
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))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑?m.15919