case inl
α : Type u_1
l : List α
inst✝ : DecidableEq α
a b : α
n : ℕ
h✝ : a = b
⊢ count a (replicate n b) = n

case inr
α : Type u_1
l : List α
inst✝ : DecidableEq α
a b : α
n : ℕ
h✝ : ¬a = b
⊢ count a (replicate n b) = 0
α : Type u_1
l : List α
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = if a = b then n else 0
split
no goals
case inl
α : Type u_1
l : List α
inst✝ : DecidableEq α
a b : α
n : ℕ
h✝ : a = b
⊢ count a (replicate n b) = n

case inr
α : Type u_1
l : List α
inst✝ : DecidableEq α
a b : α
n : ℕ
h✝ : ¬a = b
⊢ count a (replicate n b) = 0
exacts [‹a = b› ▸ count_replicate_self _ _, count_eq_zero.2 <| mt eq_of_mem_replicate ‹a ≠ b›]