rw [List.get_set_ne _ _ _ ?h]
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).get ?m.18570 = get cont (Fin.cast ⋯ j)

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ Fin (update (toList cont) (Fin.cast ⋯ i) f).length

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑?m.18570
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ (toList cont).get ⟨?m.18745, ⋯⟩ = get cont (Fin.cast ⋯ j)

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ℕ

case h
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ?m.18745 < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑i ≠ ?m.18745

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑⟨?m.18745, ?h⟩