exact Eq.trans (iInf_congr Subtype.prop) ciInf_const
α : 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
no goals