case zero
ι : Type ?u.502826
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝¹ n✝ n : ℕ
⊢ getD (replicate zero d) n d = d

case succ
ι : Type ?u.502826
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝¹ n✝ r : ℕ
IH : ∀ (n : ℕ), getD (replicate r d) n d = d
n : ℕ
⊢ getD (replicate (succ r) d) n d = d
ι : Type ?u.502826
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝ r n : ℕ
⊢ getD (replicate r d) n d = d
induction' r with r IH generalizing n
no goals
case zero
ι : Type ?u.502826
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝¹ n✝ n : ℕ
⊢ getD (replicate zero d) n d = d
simp
no goals
case succ
ι : Type ?u.502826
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
x : α
xs : List α
d : α
n✝¹ n✝ r : ℕ
IH : ∀ (n : ℕ), getD (replicate r d) n d = d
n : ℕ
⊢ getD (replicate (succ r) d) n d = d
cases n <;> simp [IH]