Theorem: cmtr_inv_eq_cmtr_iff_cmtr_square_id (Controlbits/Commutator.lean)

State before:
G : Type u
inst✝ : Group G
x y : G
⊢ ⁅x, y⁆ = ⁅x, y⁻¹⁆ ↔ ⁅x, y ^ 2⁆ = 1
Tactic:
simp_rw [pow_two, commutatorElement_eq_one_iff_mul_comm, eq_comm (a := (x * (y * y))),
commutatorElement_def, mul_assoc, mul_left_cancel_iff, ← inv_mul_eq_one (a := y * (x⁻¹ * y⁻¹)),
mul_eq_one_iff_eq_inv, mul_inv_rev, inv_inv, mul_assoc, ← eq_inv_mul_iff_mul_eq (b := y),
mul_inv_eq_iff_eq_mul, mul_assoc]
State after:
no goals