case H
G : Type u_1
H : Type ?u.217260
inst✝ : CommGroup G
g✝ : G ⧸ torsion G
hne✝ : g✝ ≠ 1
hfin✝ : IsOfFinOrder g✝
g : G
hne : ↑g ≠ 1
hfin : IsOfFinOrder ↑g
⊢ ↑g = 1
G : Type u_1
H : Type ?u.217260
inst✝ : CommGroup G
g : G ⧸ torsion G
hne : g ≠ 1
hfin : IsOfFinOrder g
⊢ g = 1
induction' g using QuotientGroup.induction_on' with g
case H.intro.intro
G : Type u_1
H : Type ?u.217260
inst✝ : CommGroup G
g✝ : G ⧸ torsion G
hne✝ : g✝ ≠ 1
hfin✝ : IsOfFinOrder g✝
g : G
hne : ↑g ≠ 1
hfin : IsOfFinOrder ↑g
m : ℕ
mpos : 0 < m
hm : ↑g ^ m = 1
⊢ ↑g = 1
case H
G : Type u_1
H : Type ?u.217260
inst✝ : CommGroup G
g✝ : G ⧸ torsion G
hne✝ : g✝ ≠ 1
hfin✝ : IsOfFinOrder g✝
g : G
hne : ↑g ≠ 1
hfin : IsOfFinOrder ↑g
⊢ ↑g = 1
obtain ⟨m, mpos, hm⟩ := (isOfFinOrder_iff_pow_eq_one _).mp hfin
case H.intro.intro.intro.intro
G : Type u_1
H : Type ?u.217260
inst✝ : CommGroup G
g✝ : G ⧸ torsion G
hne✝ : g✝ ≠ 1
hfin✝ : IsOfFinOrder g✝
g : G
hne : ↑g ≠ 1
hfin : IsOfFinOrder ↑g
m : ℕ
mpos : 0 < m
hm : ↑g ^ m = 1
n : ℕ
npos : 0 < n
hn : (fun x => x ^ m) g ^ n = 1
⊢ ↑g = 1
case H.intro.intro
G : Type u_1
H : Type ?u.217260
inst✝ : CommGroup G
g✝ : G ⧸ torsion G
hne✝ : g✝ ≠ 1
hfin✝ : IsOfFinOrder g✝
g : G
hne : ↑g ≠ 1
hfin : IsOfFinOrder ↑g
m : ℕ
mpos : 0 < m
hm : ↑g ^ m = 1
⊢ ↑g = 1
obtain ⟨n, npos, hn⟩ := (isOfFinOrder_iff_pow_eq_one _).mp ((QuotientGroup.eq_one_iff _).mp hm)
no goals
case H.intro.intro.intro.intro
G : Type u_1
H : Type ?u.217260
inst✝ : CommGroup G
g✝ : G ⧸ torsion G
hne✝ : g✝ ≠ 1
hfin✝ : IsOfFinOrder g✝
g : G
hne : ↑g ≠ 1
hfin : IsOfFinOrder ↑g
m : ℕ
mpos : 0 < m
hm : ↑g ^ m = 1
n : ℕ
npos : 0 < n
hn : (fun x => x ^ m) g ^ n = 1
⊢ ↑g = 1
exact
  (QuotientGroup.eq_one_iff g).mpr
    ((isOfFinOrder_iff_pow_eq_one _).mpr ⟨m * n, mul_pos mpos npos, (pow_mul g m n).symm ▸ hn⟩)