Theorem: List.length_drop (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
x✝¹ : List α
x✝ : 0 < length x✝¹
⊢ length (drop 0 x✝¹) = length x✝¹ - 0
Tactic:
simp only [drop, Nat.sub_zero]
State after:
no goals

State before:
α : Type u_1
n : Nat
x : α
xs : List α
h : n + 1 < length (x :: xs)
ih : length (drop n xs) = length xs - n
⊢ length (drop (n + 1) (x :: xs)) = length (x :: xs) - (n + 1)
Tactic:
simp only [drop, Nat.add, length]
State after:
α : Type u_1
n : Nat
x : α
xs : List α
h : n + 1 < length (x :: xs)
ih : length (drop n xs) = length xs - n
⊢ length (drop n xs) = length xs + 1 - (n + 1)

State before:
α : Type u_1
n : Nat
x : α
xs : List α
h : n + 1 < length (x :: xs)
ih : length (drop n xs) = length xs - n
⊢ length (drop n xs) = length xs + 1 - (n + 1)
Tactic:
rw [Nat.succ_sub_succ_eq_sub]
State after:
α : Type u_1
n : Nat
x : α
xs : List α
h : n + 1 < length (x :: xs)
ih : length (drop n xs) = length xs - n
⊢ length (drop n xs) = length xs - n

State before:
α : Type u_1
n : Nat
x : α
xs : List α
h : n + 1 < length (x :: xs)
ih : length (drop n xs) = length xs - n
⊢ length (drop n xs) = length xs - n
Tactic:
exact ih
State after:
no goals