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

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

State before:
α : Type u_1
n : ℕ
⊢ ∀ (m : ℕ) (xs : List α), take m (drop n xs) = drop n (take (n + m) xs)
Tactic:
induction n with
| zero =>
  intro m xs
  rw [Nat.zero_add]
  repeat rw [list_drop_zero]
| succ n ih =>
  intro m xs
  cases xs with
  | nil =>
    rw [list_drop_nil, list_take_nil, list_take_nil, list_drop_nil]
  | cons x xs =>
    rw [drop]
    rw [nat_add_succ_is_succ_add]
    rw [take]
    rw [drop]
    apply ih
State after:
no goals

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

State before:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ take m (drop zero xs) = drop zero (take (zero + m) xs)
Tactic:
rw [Nat.zero_add]
State after:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ take m (drop zero xs) = drop zero (take m xs)

State before:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ take m (drop zero xs) = drop zero (take m xs)
Tactic:
repeat rw [list_drop_zero]
State after:
no goals

State before:
case zero
α : Type u_1
m : ℕ
xs : List α
⊢ take m xs = drop zero (take m xs)
Tactic:
rw [list_drop_zero]
State after:
no goals

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

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

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

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

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

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

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

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