[GOAL]
G : Type u_1
H : Type u_2
inst✝ : Monoid G
⊢ ¬IsTorsion G ↔ ∃ g, ¬IsOfFinOrder g
[PROOFSTEP]
rw [IsTorsion, not_forall]
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : Monoid G
tG : IsTorsion G
src✝ : Monoid G := inst✝
g : G
⊢ g⁻¹ * g = 1
[PROOFSTEP]
erw [← pow_succ', tsub_add_cancel_of_le, pow_orderOf_eq_one]
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : Monoid G
tG : IsTorsion G
src✝ : Monoid G := inst✝
g : G
⊢ 1 ≤ orderOf g
[PROOFSTEP]
exact orderOf_pos' (tG g)
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ↑f
tG : IsTorsion G
h : H
⊢ IsOfFinOrder h
[PROOFSTEP]
obtain ⟨g, hg⟩ := hf h
[GOAL]
case intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ↑f
tG : IsTorsion G
h : H
g : G
hg : ↑f g = h
⊢ IsOfFinOrder h
[PROOFSTEP]
rw [← hg]
[GOAL]
case intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ↑f
tG : IsTorsion G
h : H
g : G
hg : ↑f g = h
⊢ IsOfFinOrder (↑f g)
[PROOFSTEP]
exact f.isOfFinOrder (tG g)
[GOAL]
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
[PROOFSTEP]
obtain ⟨ngn, ngnpos, hngn⟩ := (isOfFinOrder_iff_pow_eq_one _).mp (tH <| f g)
[GOAL]
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
[PROOFSTEP]
have hmem := f.mem_ker.mpr ((f.map_pow g ngn).trans hngn)
[GOAL]
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
[PROOFSTEP]
lift g ^ ngn to N using hN.symm ▸ hmem with gn h
[GOAL]
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
[PROOFSTEP]
obtain ⟨nn, nnpos, hnn⟩ := (isOfFinOrder_iff_pow_eq_one _).mp (tN gn)
[GOAL]
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
[PROOFSTEP]
exact ⟨ngn * nn, mul_pos ngnpos nnpos, by rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]⟩
[GOAL]
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
[PROOFSTEP]
rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
h : ExponentExists G
g : G
⊢ IsOfFinOrder g
[PROOFSTEP]
obtain ⟨n, npos, hn⟩ := h
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
g : G
n : ℕ
npos : 0 < n
hn : ∀ (g : G), g ^ n = 1
⊢ IsOfFinOrder g
[PROOFSTEP]
exact (isOfFinOrder_iff_pow_eq_one g).mpr ⟨n, npos, hn g⟩
[GOAL]
G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsTorsion R
f : M
⊢ ∃ n, 0 < n ∧ n • f = 0
[PROOFSTEP]
obtain ⟨n, npos, hn⟩ := (isOfFinAddOrder_iff_nsmul_eq_zero _).mp (tR 1)
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsTorsion R
f : M
n : ℕ
npos : 0 < n
hn : n • 1 = 0
⊢ ∃ n, 0 < n ∧ n • f = 0
[PROOFSTEP]
exact ⟨n, npos, by simp only [nsmul_eq_smul_cast R _ f, ← nsmul_one, hn, zero_smul]⟩
[GOAL]
G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsTorsion R
f : M
n : ℕ
npos : 0 < n
hn : n • 1 = 0
⊢ n • f = 0
[PROOFSTEP]
simp only [nsmul_eq_smul_cast R _ f, ← nsmul_one, hn, zero_smul]
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
x✝ : { x // x ∈ torsion G }
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1
⊢ ↑(((fun x x_1 => x * x_1)
            { val := x, property := (_ : ∃ n, n > 0 ∧ Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1) })^[n]
        1) =
    ↑1
[PROOFSTEP]
dsimp
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
x✝ : { x // x ∈ torsion G }
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1
⊢ ↑((fun x_1 => { val := x, property := (_ : ∃ n, n > 0 ∧ Function.IsPeriodicPt (fun x_2 => x * x_2) n 1) } * x_1)^[n]
        1) =
    1
[PROOFSTEP]
rw [mul_left_iterate]
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
x✝ : { x // x ∈ torsion G }
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1
⊢ ↑((fun x_1 => { val := x, property := (_ : ∃ n, n > 0 ∧ Function.IsPeriodicPt (fun x_2 => x * x_2) n 1) } ^ n * x_1)
        1) =
    1
[PROOFSTEP]
change _ * 1 = 1
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
x✝ : { x // x ∈ torsion G }
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1
⊢ ↑({ val := x, property := (_ : ∃ n, n > 0 ∧ Function.IsPeriodicPt (fun x_1 => x * x_1) n 1) } ^ n) * 1 = 1
[PROOFSTEP]
rw [_root_.mul_one, SubmonoidClass.coe_pow, Subtype.coe_mk, (isPeriodicPt_mul_iff_pow_eq_one _).mp hn]
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
a✝ b✝ : G
hg₁ : a✝ ∈ {g | ∃ n, orderOf g = p ^ n}
hg₂ : b✝ ∈ {g | ∃ n, orderOf g = p ^ n}
⊢ ∃ m, (a✝ * b✝) ^ p ^ m = 1
[PROOFSTEP]
obtain ⟨m, hm⟩ := exists_orderOf_eq_prime_pow_iff.mp hg₁
[GOAL]
case intro
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
a✝ b✝ : G
hg₁ : a✝ ∈ {g | ∃ n, orderOf g = p ^ n}
hg₂ : b✝ ∈ {g | ∃ n, orderOf g = p ^ n}
m : ℕ
hm : a✝ ^ p ^ m = 1
⊢ ∃ m, (a✝ * b✝) ^ p ^ m = 1
[PROOFSTEP]
obtain ⟨n, hn⟩ := exists_orderOf_eq_prime_pow_iff.mp hg₂
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
a✝ b✝ : G
hg₁ : a✝ ∈ {g | ∃ n, orderOf g = p ^ n}
hg₂ : b✝ ∈ {g | ∃ n, orderOf g = p ^ n}
m : ℕ
hm : a✝ ^ p ^ m = 1
n : ℕ
hn : b✝ ^ p ^ n = 1
⊢ ∃ m, (a✝ * b✝) ^ p ^ m = 1
[PROOFSTEP]
exact ⟨m + n, by rw [mul_pow, pow_add, pow_mul, hm, one_pow, Monoid.one_mul, mul_comm, pow_mul, hn, one_pow]⟩
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
a✝ b✝ : G
hg₁ : a✝ ∈ {g | ∃ n, orderOf g = p ^ n}
hg₂ : b✝ ∈ {g | ∃ n, orderOf g = p ^ n}
m : ℕ
hm : a✝ ^ p ^ m = 1
n : ℕ
hn : b✝ ^ p ^ n = 1
⊢ (a✝ * b✝) ^ p ^ (m + n) = 1
[PROOFSTEP]
rw [mul_pow, pow_add, pow_mul, hm, one_pow, Monoid.one_mul, mul_comm, pow_mul, hn, one_pow]
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
⊢ orderOf 1 = p ^ 0
[PROOFSTEP]
rw [pow_zero, orderOf_one]
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : { x // x ∈ primaryComponent G p }
⊢ ∃ n, orderOf g = p ^ n
[PROOFSTEP]
simpa [primaryComponent] using g.property
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
⊢ ∀ {x : G}, x ∈ primaryComponent G p → x ∈ primaryComponent G p' → x = 1
[PROOFSTEP]
rintro g ⟨_ | n, hn⟩ ⟨n', hn'⟩
[GOAL]
case intro.zero.intro
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hn : orderOf g = p ^ Nat.zero
n' : ℕ
hn' : orderOf g = p' ^ n'
⊢ g = 1
[PROOFSTEP]
rwa [pow_zero, orderOf_eq_one_iff] at hn 
[GOAL]
case intro.succ.intro
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
n : ℕ
hn : orderOf g = p ^ Nat.succ n
n' : ℕ
hn' : orderOf g = p' ^ n'
⊢ g = 1
[PROOFSTEP]
exact absurd (eq_of_prime_pow_eq hp.out.prime hp'.out.prime n.succ_pos (hn.symm.trans hn')) hne
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
tG : IsTorsion G
⊢ torsion G = ⊤
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
tG : IsTorsion G
x✝ : G
⊢ x✝ ∈ torsion G ↔ x✝ ∈ ⊤
[PROOFSTEP]
tauto
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : Monoid G
⊢ ¬IsTorsionFree G ↔ ∃ g, g ≠ 1 ∧ IsOfFinOrder g
[PROOFSTEP]
simp_rw [IsTorsionFree, Ne.def, not_forall, Classical.not_not, exists_prop]
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : Group G
hN : Nontrivial G
tG : IsTorsion G
⊢ ∃ g, g ≠ 1 ∧ IsOfFinOrder g
[PROOFSTEP]
obtain ⟨x, hx⟩ := (nontrivial_iff_exists_ne (1 : G)).mp hN
[GOAL]
case intro
G : Type u_1
H : Type u_2
inst✝ : Group G
hN : Nontrivial G
tG : IsTorsion G
x : G
hx : x ≠ 1
⊢ ∃ g, g ≠ 1 ∧ IsOfFinOrder g
[PROOFSTEP]
exact ⟨x, hx, tG x⟩
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : Group G
hN : Nontrivial G
tfG : IsTorsionFree G
⊢ ∃ g, ¬IsOfFinOrder g
[PROOFSTEP]
obtain ⟨x, hx⟩ := (nontrivial_iff_exists_ne (1 : G)).mp hN
[GOAL]
case intro
G : Type u_1
H : Type u_2
inst✝ : Group G
hN : Nontrivial G
tfG : IsTorsionFree G
x : G
hx : x ≠ 1
⊢ ∃ g, ¬IsOfFinOrder g
[PROOFSTEP]
exact ⟨x, (tfG x) hx⟩
[GOAL]
G : Type u_1
H✝ : Type u_2
inst✝ : Group G
tG : IsTorsionFree G
H : Subgroup G
h : { x // x ∈ H }
hne : h ≠ 1
⊢ ↑h ≠ 1
[PROOFSTEP]
norm_cast
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommGroup G
g : G ⧸ torsion G
hne : g ≠ 1
hfin : IsOfFinOrder g
⊢ g = 1
[PROOFSTEP]
induction' g using QuotientGroup.induction_on' with g
[GOAL]
case H
G : Type u_1
H : Type u_2
inst✝ : CommGroup G
g✝ : G ⧸ torsion G
hne✝ : g✝ ≠ 1
hfin✝ : IsOfFinOrder g✝
g : G
hne : ↑g ≠ 1
hfin : IsOfFinOrder ↑g
⊢ ↑g = 1
[PROOFSTEP]
obtain ⟨m, mpos, hm⟩ := (isOfFinOrder_iff_pow_eq_one _).mp hfin
[GOAL]
case H.intro.intro
G : Type u_1
H : Type u_2
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
[PROOFSTEP]
obtain ⟨n, npos, hn⟩ := (isOfFinOrder_iff_pow_eq_one _).mp ((QuotientGroup.eq_one_iff _).mp hm)
[GOAL]
case H.intro.intro.intro.intro
G : Type u_1
H : Type u_2
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
[PROOFSTEP]
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⟩)
