create finset from subgroup

Stream: new members

[Junjie Bai]

How can I create a Finset type from a Subgroup type, I want to make sum of the element in the Subgroup, here is my code

theorem Varphi_eq_Sum_Inf (u : ℚ) : (varphi vK vL u)
= (1 / Nat.card G(vL/vK)_[0]) * (∑ x in (G(vL/vK)_[(Int.ceil u)]) , min (u + 1) ((i[vL/vK] x)))- 1 := by sorry

G(vL/vK)_[0] is the lower numbering ramification group, and its type is Subgroup

[Yaël Dillies]

Do you mean ∑ x : G(vL/vK)_[⌈u⌉], ... instead of ∑ x in (G(vL/vK)_[(Int.ceil u)]?

[Kevin Buzzard]

You can sum over fintypes, and if you're lucky then a subgroup of a group which is a fintype might also be a fintype.

[Junjie Bai]

Thank you! so I have to state the Subgroup is fintypes first.

[Yaël Dillies]

Try open scoped Classical (or the tactic classical if you are in tactic mode), and hopefully Lean will know your subgroup is a fintype

[Junjie Bai]

Thank you, but It doesn't work, maybe I have to make the statement.