no goals
α : Type u
β : Type v
γ : Type w
inst✝² : Group α
inst✝¹ : Monoid β
inst✝ : MulAction β α
H : Subgroup α
a : α
q : α ⧸ H
⊢ (Quotient.out' q)⁻¹ * a ^ minimalPeriod ((fun x x_1 => x • x_1) a) q * Quotient.out' q ∈ H
rw [mul_assoc, ← QuotientGroup.eq', QuotientGroup.out_eq', ← smul_eq_mul, Quotient.mk_smul_out',
  eq_comm, pow_smul_eq_iff_minimalPeriod_dvd]