Theorem: List.modifyNth_ge_length (One.lean)

State before:
α✝ : Type u_1
l : List α✝
i : ℕ
f : α✝ → α✝
h : length l ≤ i
⊢ modifyNth f i l = l
Tactic:
simp only [modifyNth_eq_set_get?, zero_le, ge_iff_le, nonpos_iff_eq_zero, List.get?_eq_none.2 h,
  Option.map_eq_map, Option.map_none', Option.getD_none]
State after:
no goals