no goals
ι : Type ?u.18676
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
n : ℕ
a : α
⊢ map f (replicate n a) = replicate n (f a)
induction n <;> [rfl; simp only [*, replicate, map]]