order of element is the cardinality of its closure

Stream: mathlib4

[Zhang Ruichong]

I come with this problem:

lemma l1 (G : Type _ ) [Group G] [Fintype G] (u: G) : Nat.card (Subgroup.closure ({u} : Set G)) = orderOf u := by

This seems like a trivial question, is it provided by Mathlib?
I'm new in Lean4. Thanks for your suggestions.

[Scott Morrison]

Please use #backticks, and try to provide a #mwe. This makes it much easier for others to give suggestions.

[Scott Morrison]

Looks like order_eq_card_zpowers' or orderOf_eq_card_zpowers get you part of the way there.

[Scott Morrison]

and zpowers_eq_closure the rest of the way.