ι : Type ?u.198909
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
k : ℕ
h : drop k l = []
⊢ length l ≤ k
ι : Type ?u.198909
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
k : ℕ
⊢ drop k l = [] ↔ length l ≤ k
refine' ⟨fun h => _, drop_eq_nil_of_le⟩
case zero
ι : Type ?u.198909
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
k : ℕ
h✝ : drop k l✝ = []
l : List α
h : drop zero l = []
⊢ length l ≤ zero

case succ
ι : Type ?u.198909
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
k✝ : ℕ
h✝ : drop k✝ l✝ = []
k : ℕ
hk : ∀ {l : List α}, drop k l = [] → length l ≤ k
l : List α
h : drop (succ k) l = []
⊢ length l ≤ succ k
ι : Type ?u.198909
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
k : ℕ
h : drop k l = []
⊢ length l ≤ k
induction' k with k hk generalizing l
case zero
ι : Type ?u.198909
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
k : ℕ
h✝ : drop k l✝ = []
l : List α
h : l = []
⊢ length l ≤ zero
case zero
ι : Type ?u.198909
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
k : ℕ
h✝ : drop k l✝ = []
l : List α
h : drop zero l = []
⊢ length l ≤ zero
simp only [drop] at h
no goals
case zero
ι : Type ?u.198909
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
k : ℕ
h✝ : drop k l✝ = []
l : List α
h : l = []
⊢ length l ≤ zero
simp [h]
case succ.nil
ι : Type ?u.198909
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
k✝ : ℕ
h✝ : drop k✝ l = []
k : ℕ
hk : ∀ {l : List α}, drop k l = [] → length l ≤ k
h : drop (succ k) [] = []
⊢ length [] ≤ succ k

case succ.cons
ι : Type ?u.198909
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
k✝ : ℕ
h✝ : drop k✝ l = []
k : ℕ
hk : ∀ {l : List α}, drop k l = [] → length l ≤ k
head✝ : α
tail✝ : List α
h : drop (succ k) (head✝ :: tail✝) = []
⊢ length (head✝ :: tail✝) ≤ succ k
case succ
ι : Type ?u.198909
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l✝ : List α
k✝ : ℕ
h✝ : drop k✝ l✝ = []
k : ℕ
hk : ∀ {l : List α}, drop k l = [] → length l ≤ k
l : List α
h : drop (succ k) l = []
⊢ length l ≤ succ k
cases l
no goals
case succ.nil
ι : Type ?u.198909
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
k✝ : ℕ
h✝ : drop k✝ l = []
k : ℕ
hk : ∀ {l : List α}, drop k l = [] → length l ≤ k
h : drop (succ k) [] = []
⊢ length [] ≤ succ k
simp
case succ.cons
ι : Type ?u.198909
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
k✝ : ℕ
h✝ : drop k✝ l = []
k : ℕ
hk : ∀ {l : List α}, drop k l = [] → length l ≤ k
head✝ : α
tail✝ : List α
h : drop k tail✝ = []
⊢ length (head✝ :: tail✝) ≤ succ k
case succ.cons
ι : Type ?u.198909
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
k✝ : ℕ
h✝ : drop k✝ l = []
k : ℕ
hk : ∀ {l : List α}, drop k l = [] → length l ≤ k
head✝ : α
tail✝ : List α
h : drop (succ k) (head✝ :: tail✝) = []
⊢ length (head✝ :: tail✝) ≤ succ k
simp only [drop] at h
no goals
case succ.cons
ι : Type ?u.198909
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
k✝ : ℕ
h✝ : drop k✝ l = []
k : ℕ
hk : ∀ {l : List α}, drop k l = [] → length l ≤ k
head✝ : α
tail✝ : List α
h : drop k tail✝ = []
⊢ length (head✝ :: tail✝) ≤ succ k
simpa [Nat.succ_le_succ_iff] using hk h