case nil
ι : Type ?u.501723
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝¹ n✝ : ℕ
hn✝ : n✝ < length l
n : ℕ
hn : n < length []
⊢ getD [] n d = get [] { val := n, isLt := hn }

case cons
ι : Type ?u.501723
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝¹ n✝ : ℕ
hn✝ : n✝ < length l
hd : α
tl : List α
IH : ∀ {n : ℕ} (hn : n < length tl), getD tl n d = get tl { val := n, isLt := hn }
n : ℕ
hn : n < length (hd :: tl)
⊢ getD (hd :: tl) n d = get (hd :: tl) { val := n, isLt := hn }
ι : Type ?u.501723
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝ n : ℕ
hn : n < length l
⊢ getD l n d = get l { val := n, isLt := hn }
induction' l with hd tl IH generalizing n
no goals
case nil
ι : Type ?u.501723
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝¹ n✝ : ℕ
hn✝ : n✝ < length l
n : ℕ
hn : n < length []
⊢ getD [] n d = get [] { val := n, isLt := hn }
exact absurd hn (not_lt_of_ge (Nat.zero_le _))
case cons.zero
ι : Type ?u.501723
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝ n : ℕ
hn✝ : n < length l
hd : α
tl : List α
IH : ∀ {n : ℕ} (hn : n < length tl), getD tl n d = get tl { val := n, isLt := hn }
hn : zero < length (hd :: tl)
⊢ getD (hd :: tl) zero d = get (hd :: tl) { val := zero, isLt := hn }

case cons.succ
ι : Type ?u.501723
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝¹ n : ℕ
hn✝ : n < length l
hd : α
tl : List α
IH : ∀ {n : ℕ} (hn : n < length tl), getD tl n d = get tl { val := n, isLt := hn }
n✝ : ℕ
hn : succ n✝ < length (hd :: tl)
⊢ getD (hd :: tl) (succ n✝) d = get (hd :: tl) { val := succ n✝, isLt := hn }
case cons
ι : Type ?u.501723
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝¹ n✝ : ℕ
hn✝ : n✝ < length l
hd : α
tl : List α
IH : ∀ {n : ℕ} (hn : n < length tl), getD tl n d = get tl { val := n, isLt := hn }
n : ℕ
hn : n < length (hd :: tl)
⊢ getD (hd :: tl) n d = get (hd :: tl) { val := n, isLt := hn }
cases n
no goals
case cons.zero
ι : Type ?u.501723
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝ n : ℕ
hn✝ : n < length l
hd : α
tl : List α
IH : ∀ {n : ℕ} (hn : n < length tl), getD tl n d = get tl { val := n, isLt := hn }
hn : zero < length (hd :: tl)
⊢ getD (hd :: tl) zero d = get (hd :: tl) { val := zero, isLt := hn }
exact getD_cons_zero _ _ _
no goals
case cons.succ
ι : Type ?u.501723
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝¹ n : ℕ
hn✝ : n < length l
hd : α
tl : List α
IH : ∀ {n : ℕ} (hn : n < length tl), getD tl n d = get tl { val := n, isLt := hn }
n✝ : ℕ
hn : succ n✝ < length (hd :: tl)
⊢ getD (hd :: tl) (succ n✝) d = get (hd :: tl) { val := succ n✝, isLt := hn }
exact IH _