G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type ?u.1048622
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
hg : g ∈ P
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
this : Subgroup.IsCommutative ↑P
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type ?u.1048622
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
hg : g ∈ P
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k
haveI : (P : Subgroup G).IsCommutative :=
  ⟨⟨fun a b => Subtype.ext (hP (le_normalizer b.2) a a.2)⟩⟩
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type ?u.1048622
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
this : Subgroup.IsCommutative ↑P
hg : g ^ k ∈ ↑P
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type ?u.1048622
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
hg : g ∈ P
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
this : Subgroup.IsCommutative ↑P
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k
replace hg := (P : Subgroup G).pow_mem hg k
case intro.intro
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type ?u.1048622
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
k : ℕ
g₀ : G
h✝ : g₀⁻¹ * g ^ k * g₀ ∈ P
this : Subgroup.IsCommutative ↑P
hg : g ^ k ∈ ↑P
n : G
hn : n ∈ normalizer ↑P
h : g₀⁻¹ * g ^ k * g₀ = n⁻¹ * g ^ k * n
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type ?u.1048622
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
this : Subgroup.IsCommutative ↑P
hg : g ^ k ∈ ↑P
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k
obtain ⟨n, hn, h⟩ := P.conj_eq_normalizer_conj_of_mem (g ^ k) g₀ hg h
no goals
case intro.intro
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type ?u.1048622
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
k : ℕ
g₀ : G
h✝ : g₀⁻¹ * g ^ k * g₀ ∈ P
this : Subgroup.IsCommutative ↑P
hg : g ^ k ∈ ↑P
n : G
hn : n ∈ normalizer ↑P
h : g₀⁻¹ * g ^ k * g₀ = n⁻¹ * g ^ k * n
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k
exact h.trans (Commute.inv_mul_cancel (hP hn (g ^ k) hg).symm)