no goals
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α✝¹ β : ↑(leftTransversals ↑H)
inst✝ : Normal H
hH : Nat.coprime (Nat.card { x // x ∈ H }) (index H)
α✝ : QuotientDiff H
h : { x // x ∈ H }
α : ↑(leftTransversals ↑H)
hα : h • Quotient.mk'' α = Quotient.mk'' α
⊢ h ^ index H = diff (MonoidHom.id { x // x ∈ H }) (op ↑h⁻¹ • α) α
rw [← diff_inv, smul_diff', diff_self, one_mul, inv_pow, inv_inv]