Theorem: list_take_drop (Katydid/Std/Lists.lean)

State before:
α : Type u_1
n : ℕ
xs : List α
⊢ take n xs ++ drop n xs = xs
Tactic:
revert xs
State after:
α : Type u_1
n : ℕ
⊢ ∀ (xs : List α), take n xs ++ drop n xs = xs

State before:
α : Type u_1
n : ℕ
⊢ ∀ (xs : List α), take n xs ++ drop n xs = xs
Tactic:
induction n with
| zero =>
  intro xs
  rw [take]
  rw [drop]
  rw [list_app_nil_l]
| succ n ih =>
  intro xs
  cases xs with
  | nil =>
    rw [take, drop]
    simp only [append_nil]
  | cons x xs =>
    rw [take, drop]
    apply (congrArg (cons x))
    apply ih
State after:
no goals

State before:
case zero
α : Type u_1
⊢ ∀ (xs : List α), take zero xs ++ drop zero xs = xs
Tactic:
intro xs
State after:
case zero
α : Type u_1
xs : List α
⊢ take zero xs ++ drop zero xs = xs

State before:
case zero
α : Type u_1
xs : List α
⊢ take zero xs ++ drop zero xs = xs
Tactic:
rw [take]
State after:
case zero
α : Type u_1
xs : List α
⊢ [] ++ drop zero xs = xs

State before:
case zero
α : Type u_1
xs : List α
⊢ [] ++ drop zero xs = xs
Tactic:
rw [drop]
State after:
case zero
α : Type u_1
xs : List α
⊢ [] ++ xs = xs

State before:
case zero
α : Type u_1
xs : List α
⊢ [] ++ xs = xs
Tactic:
rw [list_app_nil_l]
State after:
no goals

State before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
⊢ ∀ (xs : List α), take (succ n) xs ++ drop (succ n) xs = xs
Tactic:
intro xs
State after:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
xs : List α
⊢ take (succ n) xs ++ drop (succ n) xs = xs

State before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
xs : List α
⊢ take (succ n) xs ++ drop (succ n) xs = xs
Tactic:
cases xs with
| nil =>
  rw [take, drop]
  simp only [append_nil]
| cons x xs =>
  rw [take, drop]
  apply (congrArg (cons x))
  apply ih
State after:
no goals

State before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
⊢ take (succ n) [] ++ drop (succ n) [] = []
Tactic:
rw [take, drop]
State after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
⊢ [] ++ [] = []

State before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
⊢ [] ++ [] = []
Tactic:
simp only [append_nil]
State after:
no goals

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
x : α
xs : List α
⊢ take (succ n) (x :: xs) ++ drop (succ n) (x :: xs) = x :: xs
Tactic:
rw [take, drop]
State after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
x : α
xs : List α
⊢ x :: take n xs ++ drop n xs = x :: xs

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
x : α
xs : List α
⊢ x :: take n xs ++ drop n xs = x :: xs
Tactic:
apply (congrArg (cons x))
State after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
x : α
xs : List α
⊢ List.append (take n xs) (drop n xs) = xs

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), take n xs ++ drop n xs = xs
x : α
xs : List α
⊢ List.append (take n xs) (drop n xs) = xs
Tactic:
apply ih
State after:
no goals