Theorem: List.map_replicate (LeanSAT/Reflect/CNF/Relabel.lean)

State before:
n : Nat
α✝¹ : Type u_1
a : α✝¹
α✝ : Type u_2
f : α✝¹ → α✝
⊢ map f (replicate n a) = replicate n (f a)
Tactic:
induction n <;> simp_all
State after:
no goals