-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem drop_set {l : List α} {n m : Nat} {a : α} :
    (l.set m a).drop n = if m < n then l.drop n else (l.drop n).set (m - n) a

Proof state:
case succ.nil
α : Type u_1
a : α
n✝ : Nat
hn : ∀ {l : List α} {m : Nat}, drop n✝ (l.set m a) = if m < n✝ then drop n✝ l else (drop n✝ l).set (m - n✝) a
m : Nat
⊢ drop (n✝ + 1) ([].set m a) = if m < n✝ + 1 then drop (n✝ + 1) [] else (drop (n✝ + 1) []).set (m - (n✝ + 1)) a

Tactic:
simp

Result:
no goals

Proof state:
case succ.cons.zero
α : Type u_1
a : α
n✝ : Nat
hn : ∀ {l : List α} {m : Nat}, drop n✝ (l.set m a) = if m < n✝ then drop n✝ l else (drop n✝ l).set (m - n✝) a
hd : α
tl : List α
⊢ drop (n✝ + 1) ((hd :: tl).set 0 a) =
    if 0 < n✝ + 1 then drop (n✝ + 1) (hd :: tl) else (drop (n✝ + 1) (hd :: tl)).set (0 - (n✝ + 1)) a

Tactic:
simp_all

Result:
no goals

Proof state:
case succ.cons
α : Type u_1
a : α
n✝ : Nat
hn : ∀ {l : List α} {m : Nat}, drop n✝ (l.set m a) = if m < n✝ then drop n✝ l else (drop n✝ l).set (m - n✝) a
m : Nat
hd : α
tl : List α
⊢ drop (n✝ + 1) ((hd :: tl).set m a) =
    if m < n✝ + 1 then drop (n✝ + 1) (hd :: tl) else (drop (n✝ + 1) (hd :: tl)).set (m - (n✝ + 1)) a

Tactic:
cases m

Result:
case succ.cons.zero
α : Type u_1
a : α
n✝ : Nat
hn : ∀ {l : List α} {m : Nat}, drop n✝ (l.set m a) = if m < n✝ then drop n✝ l else (drop n✝ l).set (m - n✝) a
hd : α
tl : List α
⊢ drop (n✝ + 1) ((hd :: tl).set 0 a) =
    if 0 < n✝ + 1 then drop (n✝ + 1) (hd :: tl) else (drop (n✝ + 1) (hd :: tl)).set (0 - (n✝ + 1)) a

case succ.cons.succ
α : Type u_1
a : α
n✝¹ : Nat
hn : ∀ {l : List α} {m : Nat}, drop n✝¹ (l.set m a) = if m < n✝¹ then drop n✝¹ l else (drop n✝¹ l).set (m - n✝¹) a
hd : α
tl : List α
n✝ : Nat
⊢ drop (n✝¹ + 1) ((hd :: tl).set (n✝ + 1) a) =
    if n✝ + 1 < n✝¹ + 1 then drop (n✝¹ + 1) (hd :: tl) else (drop (n✝¹ + 1) (hd :: tl)).set (n✝ + 1 - (n✝¹ + 1)) a

Proof state:
case succ.cons.succ
α : Type u_1
a : α
n✝¹ : Nat
hn : ∀ {l : List α} {m : Nat}, drop n✝¹ (l.set m a) = if m < n✝¹ then drop n✝¹ l else (drop n✝¹ l).set (m - n✝¹) a
hd : α
tl : List α
n✝ : Nat
⊢ drop (n✝¹ + 1) ((hd :: tl).set (n✝ + 1) a) =
    if n✝ + 1 < n✝¹ + 1 then drop (n✝¹ + 1) (hd :: tl) else (drop (n✝¹ + 1) (hd :: tl)).set (n✝ + 1 - (n✝¹ + 1)) a

Tactic:
simp only [hn, set_cons_succ, drop_succ_cons, succ_lt_succ_iff]

Result:
case succ.cons.succ
α : Type u_1
a : α
n✝¹ : Nat
hn : ∀ {l : List α} {m : Nat}, drop n✝¹ (l.set m a) = if m < n✝¹ then drop n✝¹ l else (drop n✝¹ l).set (m - n✝¹) a
hd : α
tl : List α
n✝ : Nat
⊢ (if n✝ < n✝¹ then drop n✝¹ tl else (drop n✝¹ tl).set (n✝ - n✝¹) a) =
    if n✝ < n✝¹ then drop n✝¹ tl else (drop n✝¹ tl).set (n✝ + 1 - (n✝¹ + 1)) a

Proof state:
case zero
α : Type u_1
a : α
l : List α
m : Nat
⊢ drop 0 (l.set m a) = if m < 0 then drop 0 l else (drop 0 l).set (m - 0) a

Tactic:
simp

Result:
no goals

Proof state:
case succ.cons.succ
α : Type u_1
a : α
n✝¹ : Nat
hn : ∀ {l : List α} {m : Nat}, drop n✝¹ (l.set m a) = if m < n✝¹ then drop n✝¹ l else (drop n✝¹ l).set (m - n✝¹) a
hd : α
tl : List α
n✝ : Nat
⊢ (if n✝ < n✝¹ then drop n✝¹ tl else (drop n✝¹ tl).set (n✝ - n✝¹) a) =
    if n✝ < n✝¹ then drop n✝¹ tl else (drop n✝¹ tl).set (n✝ + 1 - (n✝¹ + 1)) a

Tactic:
congr 2

Result:
case succ.cons.succ.e_e.e_a
α : Type u_1
a : α
n✝¹ : Nat
hn : ∀ {l : List α} {m : Nat}, drop n✝¹ (l.set m a) = if m < n✝¹ then drop n✝¹ l else (drop n✝¹ l).set (m - n✝¹) a
hd : α
tl : List α
n✝ : Nat
⊢ n✝ - n✝¹ = n✝ + 1 - (n✝¹ + 1)

Proof state:
case succ.cons.succ.e_e.e_a
α : Type u_1
a : α
n✝¹ : Nat
hn : ∀ {l : List α} {m : Nat}, drop n✝¹ (l.set m a) = if m < n✝¹ then drop n✝¹ l else (drop n✝¹ l).set (m - n✝¹) a
hd : α
tl : List α
n✝ : Nat
⊢ n✝ - n✝¹ = n✝ + 1 - (n✝¹ + 1)

Tactic:
exact (Nat.add_sub_add_right ..).symm

Result:
no goals