simpa [← size_def] using j.isLt
case hj
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
⊢ ↑j < ((toList cont).set (↑i) x).length
no goals