rw [←this]
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this✝¹ : orderOf a > 0
this✝ : Fintype { x // x ∈ H }
this : Fintype.card { x // x ∈ H } = orderOf a
⊢ orderOf a ∣ Fintype.card α
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this✝¹ : orderOf a > 0
this✝ : Fintype { x // x ∈ H }
this : Fintype.card { x // x ∈ H } = orderOf a
⊢ Fintype.card { x // x ∈ H } ∣ Fintype.card α