p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
⊢ ∃ k, g ^ p ^ k = 1
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
⊢ IsPGroup p { x // x ∈ Subgroup.comap ϕ H }
intro g
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : { val := ↑ϕ ↑g, property := (_ : ↑g ∈ Subgroup.comap ϕ H) } ^ p ^ j = 1
⊢ ∃ k, g ^ p ^ k = 1
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
⊢ ∃ k, g ^ p ^ k = 1
obtain ⟨j, hj⟩ := hH ⟨ϕ g.1, g.2⟩
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : ↑ϕ (↑g ^ p ^ j) = ↑1
⊢ ∃ k, g ^ p ^ k = 1
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : { val := ↑ϕ ↑g, property := (_ : ↑g ∈ Subgroup.comap ϕ H) } ^ p ^ j = 1
⊢ ∃ k, g ^ p ^ k = 1
rw [Subtype.ext_iff, H.coe_pow, Subtype.coe_mk, ← ϕ.map_pow] at hj
case intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : ↑ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : { val := ↑g ^ p ^ j, property := hj } ^ p ^ k = 1
⊢ ∃ k, g ^ p ^ k = 1
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : ↑ϕ (↑g ^ p ^ j) = ↑1
⊢ ∃ k, g ^ p ^ k = 1
obtain ⟨k, hk⟩ := hϕ ⟨g.1 ^ p ^ j, hj⟩
case intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : ↑ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ↑g ^ p ^ (j + k) = ↑1
⊢ ∃ k, g ^ p ^ k = 1
case intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : ↑ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : { val := ↑g ^ p ^ j, property := hj } ^ p ^ k = 1
⊢ ∃ k, g ^ p ^ k = 1
rw [Subtype.ext_iff, ϕ.ker.coe_pow, Subtype.coe_mk, ← pow_mul, ← pow_add] at hk
no goals
case intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : ↑ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ↑g ^ p ^ (j + k) = ↑1
⊢ ∃ k, g ^ p ^ k = 1
exact ⟨j + k, by rwa [Subtype.ext_iff, (H.comap ϕ).coe_pow]⟩
no goals
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : ↑ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ↑g ^ p ^ (j + k) = ↑1
⊢ g ^ p ^ (j + k) = 1
rwa [Subtype.ext_iff, (H.comap ϕ).coe_pow]