no goals
ι : Type ?u.17053
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
m n : ℕ
a : α
⊢ replicate (m + n) a = replicate m a ++ replicate n a
induction m <;> simp [*, zero_add, succ_add, replicate]