Theorem: mem_commutatorSet_of_isConj_sq (Jordan/Mathlib/Commutators.lean)

State before:
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
hg : IsConj g (g ^ 2)
⊢ g ∈ commutatorSet G
Tactic:
obtain ⟨h, hg⟩ := hg
State after:
case intro
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ∈ commutatorSet G

State before:
case intro
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ∈ commutatorSet G
Tactic:
use ↑h
State after:
case h
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ ∃ g₂, ⁅↑h, g₂⁆ = g

State before:
case h
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ ∃ g₂, ⁅↑h, g₂⁆ = g
Tactic:
use g
State after:
case h
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ ⁅↑h, g⁆ = g

State before:
case h
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ ⁅↑h, g⁆ = g
Tactic:
rw [commutatorElement_def, hg]
State after:
case h
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ^ 2 * ↑h * (↑h)⁻¹ * g⁻¹ = g

State before:
case h
G✝ : Type ?u.8
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ^ 2 * ↑h * (↑h)⁻¹ * g⁻¹ = g
Tactic:
simp only [IsUnit.mul_inv_cancel_right, Units.isUnit, mul_inv_eq_iff_eq_mul, pow_two]
State after:
no goals