-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem splitAt_go (n : Nat) (l acc : List α) :
    splitAt.go l xs n acc =
      if n < xs.length then (acc.reverse ++ xs.take n, xs.drop n) else (l, [])

Proof state:
α : Type u_1
xs : List α
n : Nat
l acc : List α
⊢ splitAt.go l xs n acc = if n < xs.length then (acc.reverse ++ take n xs, drop n xs) else (l, [])

Tactic:
induction xs generalizing n acc with
| nil => simp [splitAt.go]
| cons x xs ih =>
  cases n with
  | zero => simp [splitAt.go]
  | succ n =>
    rw [splitAt.go, take_succ_cons, drop_succ_cons, ih n (x :: acc),
      reverse_cons, append_assoc, singleton_append, length_cons]
    simp only [Nat.succ_lt_succ_iff]

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
l : List α
x : α
xs : List α
ih :
  ∀ (n : Nat) (acc : List α),
    splitAt.go l xs n acc = if n < xs.length then (acc.reverse ++ take n xs, drop n xs) else (l, [])
acc : List α
⊢ splitAt.go l (x :: xs) 0 acc =
    if 0 < (x :: xs).length then (acc.reverse ++ take 0 (x :: xs), drop 0 (x :: xs)) else (l, [])

Tactic:
simp [splitAt.go]

Result:
no goals

Proof state:
case nil
α : Type u_1
l : List α
n : Nat
acc : List α
⊢ splitAt.go l [] n acc = if n < [].length then (acc.reverse ++ take n [], drop n []) else (l, [])

Tactic:
simp [splitAt.go]

Result:
no goals

Proof state:
case cons
α : Type u_1
l : List α
x : α
xs : List α
ih :
  ∀ (n : Nat) (acc : List α),
    splitAt.go l xs n acc = if n < xs.length then (acc.reverse ++ take n xs, drop n xs) else (l, [])
n : Nat
acc : List α
⊢ splitAt.go l (x :: xs) n acc =
    if n < (x :: xs).length then (acc.reverse ++ take n (x :: xs), drop n (x :: xs)) else (l, [])

Tactic:
cases n with
| zero => simp [splitAt.go]
| succ n =>
  rw [splitAt.go, take_succ_cons, drop_succ_cons, ih n (x :: acc),
    reverse_cons, append_assoc, singleton_append, length_cons]
  simp only [Nat.succ_lt_succ_iff]

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
l : List α
x : α
xs : List α
ih :
  ∀ (n : Nat) (acc : List α),
    splitAt.go l xs n acc = if n < xs.length then (acc.reverse ++ take n xs, drop n xs) else (l, [])
acc : List α
n : Nat
⊢ splitAt.go l (x :: xs) (n + 1) acc =
    if n + 1 < (x :: xs).length then (acc.reverse ++ take (n + 1) (x :: xs), drop (n + 1) (x :: xs)) else (l, [])

Tactic:
rw [splitAt.go, take_succ_cons, drop_succ_cons, ih n (x :: acc),
  reverse_cons, append_assoc, singleton_append, length_cons]

Result:
case cons.succ
α : Type u_1
l : List α
x : α
xs : List α
ih :
  ∀ (n : Nat) (acc : List α),
    splitAt.go l xs n acc = if n < xs.length then (acc.reverse ++ take n xs, drop n xs) else (l, [])
acc : List α
n : Nat
⊢ (if n < xs.length then (acc.reverse ++ x :: take n xs, drop n xs) else (l, [])) =
    if n + 1 < xs.length + 1 then (acc.reverse ++ x :: take n xs, drop n xs) else (l, [])

Proof state:
case cons.succ
α : Type u_1
l : List α
x : α
xs : List α
ih :
  ∀ (n : Nat) (acc : List α),
    splitAt.go l xs n acc = if n < xs.length then (acc.reverse ++ take n xs, drop n xs) else (l, [])
acc : List α
n : Nat
⊢ (if n < xs.length then (acc.reverse ++ x :: take n xs, drop n xs) else (l, [])) =
    if n + 1 < xs.length + 1 then (acc.reverse ++ x :: take n xs, drop n xs) else (l, [])

Tactic:
simp only [Nat.succ_lt_succ_iff]

Result:
no goals