case h.e'_2
α : Type u_1
β : Type ?u.363947
γ : Type ?u.363950
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = List.count a (List.replicate n b)
α : Type u_1
β : Type ?u.363947
γ : Type ?u.363950
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = if a = b then n else 0
convert List.count_replicate a b n
no goals
case h.e'_2
α : Type u_1
β : Type ?u.363947
γ : Type ?u.363950
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = List.count a (List.replicate n b)
rw [←coe_count, coe_replicate]