case h.e'_2
α : Type u_1
β : Type ?u.362314
γ : Type ?u.362317
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ count a (replicate n a) = List.count a (List.replicate n a)
α : Type u_1
β : Type ?u.362314
γ : Type ?u.362317
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ count a (replicate n a) = n
convert List.count_replicate_self a n
no goals
case h.e'_2
α : Type u_1
β : Type ?u.362314
γ : Type ?u.362317
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ count a (replicate n a) = List.count a (List.replicate n a)
rw [←coe_count, coe_replicate]