-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem drop_append_eq_append_drop {l₁ l₂ : List α} {n : Nat} :
    drop n (l₁ ++ l₂) = drop n l₁ ++ drop (n - l₁.length) l₂

Proof state:
case cons.zero
α : Type u_1
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : Nat}, drop n (tail✝ ++ l₂) = drop n tail✝ ++ drop (n - tail✝.length) l₂
⊢ drop 0 (head✝ :: tail✝ ++ l₂) = drop 0 (head✝ :: tail✝) ++ drop (0 - (head✝ :: tail✝).length) l₂

Tactic:
simp [*]

Result:
no goals

Proof state:
case cons
α : Type u_1
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : Nat}, drop n (tail✝ ++ l₂) = drop n tail✝ ++ drop (n - tail✝.length) l₂
n : Nat
⊢ drop n (head✝ :: tail✝ ++ l₂) = drop n (head✝ :: tail✝) ++ drop (n - (head✝ :: tail✝).length) l₂

Tactic:
cases n

Result:
case cons.zero
α : Type u_1
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : Nat}, drop n (tail✝ ++ l₂) = drop n tail✝ ++ drop (n - tail✝.length) l₂
⊢ drop 0 (head✝ :: tail✝ ++ l₂) = drop 0 (head✝ :: tail✝) ++ drop (0 - (head✝ :: tail✝).length) l₂

case cons.succ
α : Type u_1
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : Nat}, drop n (tail✝ ++ l₂) = drop n tail✝ ++ drop (n - tail✝.length) l₂
n✝ : Nat
⊢ drop (n✝ + 1) (head✝ :: tail✝ ++ l₂) = drop (n✝ + 1) (head✝ :: tail✝) ++ drop (n✝ + 1 - (head✝ :: tail✝).length) l₂

Proof state:
case nil
α : Type u_1
l₂ : List α
n : Nat
⊢ drop n ([] ++ l₂) = drop n [] ++ drop (n - [].length) l₂

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : Nat}, drop n (tail✝ ++ l₂) = drop n tail✝ ++ drop (n - tail✝.length) l₂
n✝ : Nat
⊢ drop (n✝ + 1) (head✝ :: tail✝ ++ l₂) = drop (n✝ + 1) (head✝ :: tail✝) ++ drop (n✝ + 1 - (head✝ :: tail✝).length) l₂

Tactic:
simp only [cons_append, drop_succ_cons, length_cons, succ_eq_add_one, append_cancel_left_eq, *]

Result:
case cons.succ
α : Type u_1
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : Nat}, drop n (tail✝ ++ l₂) = drop n tail✝ ++ drop (n - tail✝.length) l₂
n✝ : Nat
⊢ drop (n✝ - tail✝.length) l₂ = drop (n✝ + 1 - (tail✝.length + 1)) l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
n : Nat
⊢ drop n (l₁ ++ l₂) = drop n l₁ ++ drop (n - l₁.length) l₂

Tactic:
induction l₁ generalizing n

Result:
case nil
α : Type u_1
l₂ : List α
n : Nat
⊢ drop n ([] ++ l₂) = drop n [] ++ drop (n - [].length) l₂

case cons
α : Type u_1
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : Nat}, drop n (tail✝ ++ l₂) = drop n tail✝ ++ drop (n - tail✝.length) l₂
n : Nat
⊢ drop n (head✝ :: tail✝ ++ l₂) = drop n (head✝ :: tail✝) ++ drop (n - (head✝ :: tail✝).length) l₂

Proof state:
case cons.succ.e_a
α : Type u_1
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : Nat}, drop n (tail✝ ++ l₂) = drop n tail✝ ++ drop (n - tail✝.length) l₂
n✝ : Nat
⊢ n✝ - tail✝.length = n✝ + 1 - (tail✝.length + 1)

Tactic:
omega

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : Nat}, drop n (tail✝ ++ l₂) = drop n tail✝ ++ drop (n - tail✝.length) l₂
n✝ : Nat
⊢ drop (n✝ - tail✝.length) l₂ = drop (n✝ + 1 - (tail✝.length + 1)) l₂

Tactic:
congr 1

Result:
case cons.succ.e_a
α : Type u_1
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : Nat}, drop n (tail✝ ++ l₂) = drop n tail✝ ++ drop (n - tail✝.length) l₂
n✝ : Nat
⊢ n✝ - tail✝.length = n✝ + 1 - (tail✝.length + 1)