case nil
ι : Type ?u.208871
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
n : ℕ
⊢ sizeOf (drop n []) ≤ sizeOf []

case cons
ι : Type ?u.208871
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
head✝ : α
tail✝ : List α
lih : ∀ (n : ℕ), sizeOf (drop n tail✝) ≤ sizeOf tail✝
n : ℕ
⊢ sizeOf (drop n (head✝ :: tail✝)) ≤ sizeOf (head✝ :: tail✝)
ι : Type ?u.208871
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
l : List α
⊢ ∀ (n : ℕ), sizeOf (drop n l) ≤ sizeOf l
induction' l with _ _ lih <;> intro n
no goals
case nil
ι : Type ?u.208871
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
n : ℕ
⊢ sizeOf (drop n []) ≤ sizeOf []
rw [drop_nil]
case cons.zero
ι : Type ?u.208871
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
head✝ : α
tail✝ : List α
lih : ∀ (n : ℕ), sizeOf (drop n tail✝) ≤ sizeOf tail✝
⊢ sizeOf (drop zero (head✝ :: tail✝)) ≤ sizeOf (head✝ :: tail✝)

case cons.succ
ι : Type ?u.208871
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
head✝ : α
tail✝ : List α
lih : ∀ (n : ℕ), sizeOf (drop n tail✝) ≤ sizeOf tail✝
n : ℕ
n_ih✝ : sizeOf (drop n (head✝ :: tail✝)) ≤ sizeOf (head✝ :: tail✝)
⊢ sizeOf (drop (succ n) (head✝ :: tail✝)) ≤ sizeOf (head✝ :: tail✝)
case cons
ι : Type ?u.208871
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
head✝ : α
tail✝ : List α
lih : ∀ (n : ℕ), sizeOf (drop n tail✝) ≤ sizeOf tail✝
n : ℕ
⊢ sizeOf (drop n (head✝ :: tail✝)) ≤ sizeOf (head✝ :: tail✝)
induction' n with n
no goals
case cons.zero
ι : Type ?u.208871
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
head✝ : α
tail✝ : List α
lih : ∀ (n : ℕ), sizeOf (drop n tail✝) ≤ sizeOf tail✝
⊢ sizeOf (drop zero (head✝ :: tail✝)) ≤ sizeOf (head✝ :: tail✝)
rfl
no goals
case cons.succ
ι : Type ?u.208871
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
head✝ : α
tail✝ : List α
lih : ∀ (n : ℕ), sizeOf (drop n tail✝) ≤ sizeOf tail✝
n : ℕ
n_ih✝ : sizeOf (drop n (head✝ :: tail✝)) ≤ sizeOf (head✝ :: tail✝)
⊢ sizeOf (drop (succ n) (head✝ :: tail✝)) ≤ sizeOf (head✝ :: tail✝)
exact Trans.trans (lih _) le_add_self