refine' le_ciInf fun t => _
case refine'_2
α : 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 }
this : Nonempty { t // t.card = n }
⊢ s.mulImpact n ≤ (map { toFun := ⇑f, inj' := hf } s).mulImpact n
case refine'_2
α : 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 }
this : Nonempty { t // t.card = n }
t : { t // t.card = n }
⊢ s.mulImpact n ≤ (map { toFun := ⇑f, inj' := hf } s * ↑t).card