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
β α : ↑(leftTransversals ↑H)
⊢ diff (MonoidHom.id { x // x ∈ H }) β α *
      (↑(powCoprime hH).symm (diff (MonoidHom.id { x // x ∈ H }) β α))⁻¹ ^ index H =
    1
rw [inv_pow, ← powCoprime_apply hH, Equiv.apply_symm_apply, mul_inv_self]