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

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

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

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

State before:
case zero
α : Type u_1
xs : List α
⊢ length (drop zero xs) = length xs - zero
Tactic:
rw [drop]
State after:
case zero
α : Type u_1
xs : List α
⊢ length xs = length xs - zero

State before:
case zero
α : Type u_1
xs : List α
⊢ length xs = length xs - zero
Tactic:
rw [Nat.sub_zero]
State after:
no goals

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

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

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

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

State before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs : List α), length (drop n xs) = length xs - n
⊢ 0 = 0 - succ n
Tactic:
rw [Nat.zero_sub]
State after:
no goals

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

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

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

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