no goals
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
h1 : length (a :: as) ≤ 0
⊢ get 0 (a :: as) = default
cases h1
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
k : ℕ
head✝ : α
as : List α
h1 : length (head✝ :: as) ≤ k + 1
⊢ length as ≤ k
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
k : ℕ
head✝ : α
as : List α
h1 : length (head✝ :: as) ≤ k + 1
⊢ get (k + 1) (head✝ :: as) = default
apply get_eq_default_of_le k
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
k : ℕ
head✝ : α
as : List α
h1 : length (head✝ :: as) ≤ k + 1
⊢ Nat.succ (length as) ≤ Nat.succ k
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
k : ℕ
head✝ : α
as : List α
h1 : length (head✝ :: as) ≤ k + 1
⊢ length as ≤ k
rw [← Nat.succ_le_succ_iff]
no goals
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
k : ℕ
head✝ : α
as : List α
h1 : length (head✝ :: as) ≤ k + 1
⊢ Nat.succ (length as) ≤ Nat.succ k
apply h1