case nil
ι : Type ?u.502171
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝¹ n✝ : ℕ
hn✝ : length l ≤ n✝
n : ℕ
hn : length [] ≤ n
⊢ getD [] n d = d

case cons
ι : Type ?u.502171
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝¹ n✝ : ℕ
hn✝ : length l ≤ n✝
hd : α
tl : List α
IH : ∀ {n : ℕ}, length tl ≤ n → getD tl n d = d
n : ℕ
hn : length (hd :: tl) ≤ n
⊢ getD (hd :: tl) n d = d
ι : Type ?u.502171
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝ n : ℕ
hn : length l ≤ n
⊢ getD l n d = d
induction' l with hd tl IH generalizing n
no goals
case nil
ι : Type ?u.502171
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝¹ n✝ : ℕ
hn✝ : length l ≤ n✝
n : ℕ
hn : length [] ≤ n
⊢ getD [] n d = d
exact getD_nil _ _
case cons.zero
ι : Type ?u.502171
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝ n : ℕ
hn✝ : length l ≤ n
hd : α
tl : List α
IH : ∀ {n : ℕ}, length tl ≤ n → getD tl n d = d
hn : length (hd :: tl) ≤ zero
⊢ getD (hd :: tl) zero d = d

case cons.succ
ι : Type ?u.502171
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝¹ n : ℕ
hn✝ : length l ≤ n
hd : α
tl : List α
IH : ∀ {n : ℕ}, length tl ≤ n → getD tl n d = d
n✝ : ℕ
hn : length (hd :: tl) ≤ succ n✝
⊢ getD (hd :: tl) (succ n✝) d = d
case cons
ι : Type ?u.502171
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝¹ n✝ : ℕ
hn✝ : length l ≤ n✝
hd : α
tl : List α
IH : ∀ {n : ℕ}, length tl ≤ n → getD tl n d = d
n : ℕ
hn : length (hd :: tl) ≤ n
⊢ getD (hd :: tl) n d = d
cases n
no goals
case cons.zero
ι : Type ?u.502171
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝ n : ℕ
hn✝ : length l ≤ n
hd : α
tl : List α
IH : ∀ {n : ℕ}, length tl ≤ n → getD tl n d = d
hn : length (hd :: tl) ≤ zero
⊢ getD (hd :: tl) zero d = d
refine' absurd (Nat.zero_lt_succ _) (not_lt_of_ge hn)
no goals
case cons.succ
ι : Type ?u.502171
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝¹ n : ℕ
hn✝ : length l ≤ n
hd : α
tl : List α
IH : ∀ {n : ℕ}, length tl ≤ n → getD tl n d = d
n✝ : ℕ
hn : length (hd :: tl) ≤ succ n✝
⊢ getD (hd :: tl) (succ n✝) d = d
exact IH (Nat.le_of_succ_le_succ hn)