simp only [mulImpact, singleton_mul', card_smul_finset]
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Group α
n✝ : ℕ
inst✝ : Infinite α
a : α
n : ℕ
⊢ {a}.mulImpact n = n
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Group α
n✝ : ℕ
inst✝ : Infinite α
a : α
n : ℕ
⊢ ⨅ t, (↑t).card = n