case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ ∀ (b : G), b ∈ Finset.univ → orderOf b ∣ exponent G
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ Finset.lcm Finset.univ orderOf ∣ exponent G
apply Finset.lcm_dvd
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
g : G
a✝ : g ∈ Finset.univ
⊢ orderOf g ∣ exponent G
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ ∀ (b : G), b ∈ Finset.univ → orderOf b ∣ exponent G
intro g _
no goals
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
g : G
a✝ : g ∈ Finset.univ
⊢ orderOf g ∣ exponent G
exact order_dvd_exponent g