Theorem: Finset.mulImpact_singleton (LeanCamCombi/Impact.lean)

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

State before:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Group α
n✝ : ℕ
inst✝ : Infinite α
a : α
n : ℕ
⊢ ⨅ t, (↑t).card = n
Tactic:
haveI : Nonempty {t : Finset α // t.card = n} := nonempty_subtype.2 (exists_card_eq _)
State after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Group α
n✝ : ℕ
inst✝ : Infinite α
a : α
n : ℕ
this : Nonempty { t // t.card = n }
⊢ ⨅ t, (↑t).card = n

State before:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Group α
n✝ : ℕ
inst✝ : Infinite α
a : α
n : ℕ
this : Nonempty { t // t.card = n }
⊢ ⨅ t, (↑t).card = n
Tactic:
exact Eq.trans (iInf_congr Subtype.prop) ciInf_const
State after:
no goals