case intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = MonoidHom.ker f
tH : IsTorsion H
tN : IsTorsion { x // x ∈ N }
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : ↑f g ^ ngn = 1
⊢ ∃ n, 0 < n ∧ g ^ n = 1
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = MonoidHom.ker f
tH : IsTorsion H
tN : IsTorsion { x // x ∈ N }
g : G
⊢ ∃ n, 0 < n ∧ g ^ n = 1
obtain ⟨ngn, ngnpos, hngn⟩ := (isOfFinOrder_iff_pow_eq_one _).mp (tH <| f g)
case intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = MonoidHom.ker f
tH : IsTorsion H
tN : IsTorsion { x // x ∈ N }
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : ↑f g ^ ngn = 1
hmem : g ^ ngn ∈ MonoidHom.ker f
⊢ ∃ n, 0 < n ∧ g ^ n = 1
case intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = MonoidHom.ker f
tH : IsTorsion H
tN : IsTorsion { x // x ∈ N }
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : ↑f g ^ ngn = 1
⊢ ∃ n, 0 < n ∧ g ^ n = 1
have hmem := f.mem_ker.mpr ((f.map_pow g ngn).trans hngn)
case intro.intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = MonoidHom.ker f
tH : IsTorsion H
tN : IsTorsion { x // x ∈ N }
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : ↑f g ^ ngn = 1
gn : { x // x ∈ N }
h : ↑gn = g ^ ngn
hmem✝ hmem : ↑gn ∈ MonoidHom.ker f
⊢ ∃ n, 0 < n ∧ g ^ n = 1
case intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = MonoidHom.ker f
tH : IsTorsion H
tN : IsTorsion { x // x ∈ N }
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : ↑f g ^ ngn = 1
hmem : g ^ ngn ∈ MonoidHom.ker f
⊢ ∃ n, 0 < n ∧ g ^ n = 1
lift g ^ ngn to N using hN.symm ▸ hmem with gn h
case intro.intro.intro.intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = MonoidHom.ker f
tH : IsTorsion H
tN : IsTorsion { x // x ∈ N }
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : ↑f g ^ ngn = 1
gn : { x // x ∈ N }
h : ↑gn = g ^ ngn
hmem✝ hmem : ↑gn ∈ MonoidHom.ker f
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
⊢ ∃ n, 0 < n ∧ g ^ n = 1
case intro.intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = MonoidHom.ker f
tH : IsTorsion H
tN : IsTorsion { x // x ∈ N }
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : ↑f g ^ ngn = 1
gn : { x // x ∈ N }
h : ↑gn = g ^ ngn
hmem✝ hmem : ↑gn ∈ MonoidHom.ker f
⊢ ∃ n, 0 < n ∧ g ^ n = 1
obtain ⟨nn, nnpos, hnn⟩ := (isOfFinOrder_iff_pow_eq_one _).mp (tN gn)
no goals
case intro.intro.intro.intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = MonoidHom.ker f
tH : IsTorsion H
tN : IsTorsion { x // x ∈ N }
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : ↑f g ^ ngn = 1
gn : { x // x ∈ N }
h : ↑gn = g ^ ngn
hmem✝ hmem : ↑gn ∈ MonoidHom.ker f
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
⊢ ∃ n, 0 < n ∧ g ^ n = 1
exact
  ⟨ngn * nn, mul_pos ngnpos nnpos, by
    rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]⟩
no goals
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = MonoidHom.ker f
tH : IsTorsion H
tN : IsTorsion { x // x ∈ N }
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : ↑f g ^ ngn = 1
gn : { x // x ∈ N }
h : ↑gn = g ^ ngn
hmem✝ hmem : ↑gn ∈ MonoidHom.ker f
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
⊢ g ^ (ngn * nn) = 1
rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]