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

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

State before:
α : Type u_1
n : ℕ
⊢ ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
Tactic:
induction n with
| zero =>
  intro xs ys
  rw [Nat.zero_sub]
  repeat rw [take]
  simp only [append_nil]
| succ n ih =>
  intro xs ys
  cases xs with
  | nil =>
    repeat rw [take]
    simp only [nil_append, length_nil, ge_iff_le, nonpos_iff_eq_zero, tsub_zero]
  | cons x xs =>
    rw [take]
    rw [length]
    rw [succ_sub_succ]
    rw [<- list_app_comm_cons]
    rw [take]
    apply (congrArg (cons x))
    apply ih
State after:
no goals

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

State before:
case zero
α : Type u_1
xs ys : List α
⊢ take zero (xs ++ ys) = take zero xs ++ take (zero - length xs) ys
Tactic:
rw [Nat.zero_sub]
State after:
case zero
α : Type u_1
xs ys : List α
⊢ take zero (xs ++ ys) = take zero xs ++ take 0 ys

State before:
case zero
α : Type u_1
xs ys : List α
⊢ take zero (xs ++ ys) = take zero xs ++ take 0 ys
Tactic:
repeat rw [take]
State after:
case zero
α : Type u_1
xs ys : List α
⊢ [] = [] ++ []

State before:
case zero
α : Type u_1
xs ys : List α
⊢ [] = [] ++ []
Tactic:
simp only [append_nil]
State after:
no goals

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

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

State before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
xs ys : List α
⊢ take (succ n) (xs ++ ys) = take (succ n) xs ++ take (succ n - length xs) ys
Tactic:
cases xs with
| nil =>
  repeat rw [take]
  simp only [nil_append, length_nil, ge_iff_le, nonpos_iff_eq_zero, tsub_zero]
| cons x xs =>
  rw [take]
  rw [length]
  rw [succ_sub_succ]
  rw [<- list_app_comm_cons]
  rw [take]
  apply (congrArg (cons x))
  apply ih
State after:
no goals

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

State before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys : List α), take n (xs ++ ys) = take n xs ++ take (n - length xs) ys
ys : List α
⊢ take (succ n) ([] ++ ys) = [] ++ take (succ n - length []) ys
Tactic:
simp only [nil_append, length_nil, ge_iff_le, nonpos_iff_eq_zero, tsub_zero]
State after:
no goals

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

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

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

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

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

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

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

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