haveI : Nonempty {t : Finset α // t.card = n} := nonempty_subtype.2 (exists_card_eq _)
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this : Infinite β
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝ : Infinite β
this : Nonempty { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n