no goals
G✝ : Type u
A : Type v
x y : G✝
a b : A
n m : ℕ
inst✝⁴ : Group G✝
inst✝³ : AddGroup A
inst✝² : Fintype G✝
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
g : G
⊢ g ^ index H ∈ H
rw [← eq_one_iff, QuotientGroup.mk_pow H, index, pow_card_eq_one']