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

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

Tactic:
induction l₁ generalizing n

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

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

Proof state:
case cons.zero
α : Type u_1
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : Nat}, take n (tail✝ ++ l₂) = take n tail✝ ++ take (n - tail✝.length) l₂
⊢ take 0 (head✝ :: tail✝ ++ l₂) = take 0 (head✝ :: tail✝) ++ take (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}, take n (tail✝ ++ l₂) = take n tail✝ ++ take (n - tail✝.length) l₂
n : Nat
⊢ take n (head✝ :: tail✝ ++ l₂) = take n (head✝ :: tail✝) ++ take (n - (head✝ :: tail✝).length) l₂

Tactic:
cases n

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

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

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

Tactic:
simp only [cons_append, take_succ_cons, length_cons, succ_eq_add_one, cons.injEq,
  append_cancel_left_eq, true_and, *]

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

Proof state:
case cons.succ
α : Type u_1
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : Nat}, take n (tail✝ ++ l₂) = take n tail✝ ++ take (n - tail✝.length) l₂
n✝ : Nat
⊢ take (n✝ - tail✝.length) l₂ = take (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}, take n (tail✝ ++ l₂) = take n tail✝ ++ take (n - tail✝.length) l₂
n✝ : Nat
⊢ n✝ - tail✝.length = n✝ + 1 - (tail✝.length + 1)

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

Tactic:
omega

Result:
no goals

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

Tactic:
simp

Result:
no goals