-- Mathlib/GroupTheory/PGroup.lean
theorem comap_of_ker_isPGroup {H : Subgroup G} (hH : IsPGroup p H) {K : Type*} [Group K]
    (ϕ : K →* G) (hϕ : IsPGroup p ϕ.ker) : IsPGroup p (H.comap ϕ)

Proof state:
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ϕ (↑g ^ p ^ j) = ↑1
⊢ ∃ k, g ^ p ^ k = 1

Tactic:
obtain ⟨k, hk⟩ := hϕ ⟨g.1 ^ p ^ j, hj⟩

Result:
case intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ⟨↑g ^ p ^ j, hj⟩ ^ p ^ k = 1
⊢ ∃ k, g ^ p ^ k = 1

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
⊢ IsPGroup p ↥(Subgroup.comap ϕ H)

Tactic:
intro g

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
⊢ ∃ k, g ^ p ^ k = 1

Proof state:
case intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ⟨↑g ^ p ^ j, hj⟩ ^ p ^ k = 1
⊢ ∃ k, g ^ p ^ k = 1

Tactic:
rw [Subtype.ext_iff, ϕ.ker.coe_pow, Subtype.coe_mk, ← pow_mul, ← pow_add] at hk

Result:
case intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ↑g ^ p ^ (j + k) = ↑1
⊢ ∃ k, g ^ p ^ k = 1

Proof state:
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ⟨ϕ ↑g, ⋯⟩ ^ p ^ j = 1
⊢ ∃ k, g ^ p ^ k = 1

Tactic:
rw [Subtype.ext_iff, H.coe_pow, Subtype.coe_mk, ← ϕ.map_pow] at hj

Result:
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ϕ (↑g ^ p ^ j) = ↑1
⊢ ∃ k, g ^ p ^ k = 1

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ↑g ^ p ^ (j + k) = ↑1
⊢ g ^ p ^ (j + k) = 1

Tactic:
rwa [Subtype.ext_iff, (H.comap ϕ).coe_pow]

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
⊢ ∃ k, g ^ p ^ k = 1

Tactic:
obtain ⟨j, hj⟩ := hH ⟨ϕ g.1, g.2⟩

Result:
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ⟨ϕ ↑g, ⋯⟩ ^ p ^ j = 1
⊢ ∃ k, g ^ p ^ k = 1

Proof state:
case intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ↑g ^ p ^ (j + k) = ↑1
⊢ ∃ k, g ^ p ^ k = 1

Tactic:
exact ⟨j + k, by rwa [Subtype.ext_iff, (H.comap ϕ).coe_pow]⟩

Result:
no goals