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

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

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

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

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

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

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

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

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

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

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

State before:
case succ.zero
α : Type u_1
n : ℕ
ih : ∀ (m : ℕ) (xs : List α), drop m (take n xs) = take (n - m) (drop m xs)
xs : List α
⊢ drop zero (take (succ n) xs) = take (succ n) (drop zero xs)
Tactic:
repeat rw [list_drop_zero]
State after:
no goals

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

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

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

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

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

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

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

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