case h
α : Type u_1
β : α → Type ?u.32641
inst✝ : DecidableEq α
a : α
n : ℕ
i : α
⊢ ↑(↑toDfinsupp (replicate n a)) i = ↑(Dfinsupp.single a n) i
α : Type u_1
β : α → Type ?u.32641
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ ↑toDfinsupp (replicate n a) = Dfinsupp.single a n
ext i
case h
α : Type u_1
β : α → Type ?u.32641
inst✝ : DecidableEq α
a : α
n : ℕ
i : α
⊢ count i (replicate n a) = ↑(Dfinsupp.single a n) i
case h
α : Type u_1
β : α → Type ?u.32641
inst✝ : DecidableEq α
a : α
n : ℕ
i : α
⊢ ↑(↑toDfinsupp (replicate n a)) i = ↑(Dfinsupp.single a n) i
dsimp [toDfinsupp]
no goals
case h
α : Type u_1
β : α → Type ?u.32641
inst✝ : DecidableEq α
a : α
n : ℕ
i : α
⊢ count i (replicate n a) = ↑(Dfinsupp.single a n) i
simp [count_replicate, eq_comm]