awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : Monoid G
tG : IsTorsion G
g : G
⊢ 1 ≤ orderOf g

Tactic:
(tG g).orderOf_pos

Premises used: IsOfFinOrder.orderOf_pos, Nat.lt
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : Monoid G
tG : IsTorsion G
g : G
⊢ 1 ≤ orderOf g

Tactic:
exact (tG g).orderOf_pos

Premises used: IsOfFinOrder.orderOf_pos
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : Group G
tG : IsTorsion G
H : Subgroup G
⊢ IsTorsion.{u_1} ↥H

Tactic:
fun h ↦
  Submonoid.isOfFinOrder_coe.1 <| tG h

Premises used: Set.Mem, Submonoid.isOfFinOrder_coe, Iff.mp, Monoid.IsTorsion, Subtype.val
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
f : G →* H
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
tG : IsTorsion G
h : H
obtain : ∀ (g : G), IsOfFinOrder.{u_2} (G := H) ((f : (a : G) → H) g : H)
⊢ IsOfFinOrder h

Tactic:
obtain ⟨g, rfl⟩ := hf h

Premises used: rfl
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
f : G →* H
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
tG : IsTorsion G
g : G
⊢ IsOfFinOrder.{u_2} (G := H) ((f : (a : G) → H) g : H)

Tactic:
f.isOfFinOrder (tG g)

Premises used: MonoidHom.isOfFinOrder
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
f : G →* H
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
tG : IsTorsion G
g : G
⊢ IsOfFinOrder.{u_2} (G := H) ((f : (a : G) → H) g : H)

Tactic:
exact f.isOfFinOrder (tG g)

Premises used: MonoidHom.isOfFinOrder
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hN : N = f.ker
tH : IsTorsion H
tN : IsTorsion.{u_1} ↥N
g : G
obtain : ∀ (ngn : ℕ) (ngnpos : 0 < ngn) (hngn : HPow.hPow (α := H) ((f : (a : G) → H) g : H) ngn = 1), IsOfFinOrder g
⊢ IsOfFinOrder g

Tactic:
obtain ⟨ngn, ngnpos, hngn⟩ := (tH <| f g).exists_pow_eq_one

Premises used: IsOfFinOrder.exists_pow_eq_one, DFunLike.coe
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hN : N = f.ker
tH : IsTorsion H
tN : IsTorsion.{u_1} ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : HPow.hPow (α := H) ((f : (a : G) → H) g : H) ngn = 1
⊢ g ^ ngn ∈ f.ker

Tactic:
have hmem := MonoidHom.mem_ker.mpr ((f.map_pow g ngn).trans hngn)
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hN : N = f.ker
tH : IsTorsion H
tN : IsTorsion.{u_1} ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : HPow.hPow (α := H) ((f : (a : G) → H) g : H) ngn = 1
hmem : g ^ ngn ∈ f.ker
⊢ g ^ ngn ∈ N

Tactic:
hN.symm ▸ hmem

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hN : N = f.ker
tH : IsTorsion H
tN : IsTorsion.{u_1} ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : HPow.hPow (α := H) ((f : (a : G) → H) g : H) ngn = 1
hmem : g ^ ngn ∈ f.ker
lift : ∀ (gn : ↥N) (h : (↑gn : G) = g ^ ngn) (hmem : (↑gn : G) ∈ f.ker), IsOfFinOrder g
⊢ IsOfFinOrder g

Tactic:
lift g ^ ngn to N using hN.symm ▸ hmem with gn h
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hN : N = f.ker
tH : IsTorsion H
tN : IsTorsion.{u_1} ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : HPow.hPow (α := H) ((f : (a : G) → H) g : H) ngn = 1
gn : ↥N
h : (↑gn : G) = g ^ ngn
hmem : (↑gn : G) ∈ f.ker
obtain : ∀ (nn : ℕ) (nnpos : 0 < nn) (hnn : gn ^ nn = 1), IsOfFinOrder g
⊢ IsOfFinOrder g

Tactic:
obtain ⟨nn, nnpos, hnn⟩ := (tN gn).exists_pow_eq_one

Premises used: IsOfFinOrder.exists_pow_eq_one
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hN : N = f.ker
tH : IsTorsion H
tN : IsTorsion.{u_1} ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : HPow.hPow (α := H) ((f : (a : G) → H) g : H) ngn = 1
gn : ↥N
h : (↑gn : G) = g ^ ngn
hmem : (↑gn : G) ∈ f.ker
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
rw : (g ^ ngn) ^ nn = 1
rw₁ : (↑gn : G) ^ nn = 1
rw₂ : (↑(gn ^ nn) : G) = 1
rw₃ : Eq.{u_1 + 1} (α := G) (↑1 : G) 1
rw₄ rw₅ : Eq.{u_1 + 1} (α := G) 1 1
⊢ g ^ (ngn * nn) = 1

Tactic:
rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]

Premises used: Subgroup.coe_pow, pow_mul, Subgroup.coe_one
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hN : N = f.ker
tH : IsTorsion H
tN : IsTorsion.{u_1} ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : HPow.hPow (α := H) ((f : (a : G) → H) g : H) ngn = 1
gn : ↥N
h : (↑gn : G) = g ^ ngn
hmem : (↑gn : G) ∈ f.ker
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
⊢ IsOfFinOrder g

Tactic:
exact isOfFinOrder_iff_pow_eq_one.mpr <| ⟨ngn * nn, mul_pos ngnpos nnpos, by
    rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]⟩

Premises used: Iff.mpr, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
hN : N = f.ker
tN : IsTorsion.{u_1} ↥N
⊢ IsTorsion H ↔ IsTorsion G

Tactic:
⟨fun tH ↦ IsTorsion.extension_closed hN tH tN, fun tG ↦ IsTorsion.of_surjective hf tG⟩

Premises used: IsTorsion.of_surjective, Iff.intro, IsTorsion.extension_closed
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : Group G
h : ExponentExists G
g : G
obtain : ∀ (n : ℕ) (npos : 0 < n) (hn : ∀ (g : G), g ^ n = 1), IsOfFinOrder g
⊢ IsOfFinOrder g

Tactic:
obtain ⟨n, npos, hn⟩ := h
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : Group G
g : G
n : ℕ
npos : 0 < n
hn : ∀ (g : G), g ^ n = 1
⊢ IsOfFinOrder g

Tactic:
isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, hn g⟩

Premises used: Iff.mpr, And.intro, Exists.intro, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : Group G
g : G
n : ℕ
npos : 0 < n
hn : ∀ (g : G), g ^ n = 1
⊢ IsOfFinOrder g

Tactic:
exact isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, hn g⟩

Premises used: Iff.mpr, And.intro, Exists.intro, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : Group G
tG : IsTorsion G
bounded : Set.Finite (α := ℕ) (Set.range fun (g : G) ↦ orderOf g)
⊢ ExponentExists G

Tactic:
exponent_ne_zero.mp <|
    (exponent_ne_zero_iff_range_orderOf_finite fun g ↦ (tG g).orderOf_pos).mpr bounded

Premises used: Monoid.exponent_ne_zero_iff_range_orderOf_finite, Iff.mpr, IsOfFinOrder.orderOf_pos, Monoid.exponent_ne_zero, Iff.mp
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
⊢ IsTorsion G

Tactic:
ExponentExists.isTorsion .of_finite

Premises used: ExponentExists.isTorsion, Monoid.ExponentExists.of_finite
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Nontrivial G
hG : IsTorsion G
⊢ ¬IsMulTorsionFree G

Tactic:
not_isMulTorsionFree_iff_isOfFinOrder.2 <| let ⟨x, hx⟩ := exists_ne (1 : G); ⟨x, hx, hG x⟩

Premises used: Iff.mpr, _private.0.not_isMulTorsionFree_of_isTorsion.match_1, not_isMulTorsionFree_iff_isOfFinOrder, Exists, exists_ne, Ne, And, And.intro, Exists.intro, OfNat.ofNat, IsOfFinOrder
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Nontrivial G
inst_2 : IsMulTorsionFree G
⊢ ¬IsTorsion G

Tactic:
(not_isMulTorsionFree_of_isTorsion · ‹_›)

Premises used: not_isMulTorsionFree_of_isTorsion, Not
-- Module: Mathlib.GroupTheory.Torsion
Goal:
R : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
tR : IsTorsion R
f : M
obtain : ∀ (n : ℕ) (npos : 0 < n) (hn : HSMul.hSMul (β := R) n 1 = 0), ∃ (n : ℕ), 0 < n ∧ n • f = 0
⊢ ∃ (n : ℕ), 0 < n ∧ n • f = 0

Tactic:
obtain ⟨n, npos, hn⟩ := (tR 1).exists_nsmul_eq_zero

Premises used: IsOfFinAddOrder.exists_nsmul_eq_zero, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Torsion
Goal:
R : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
tR : IsTorsion R
f : M
n : ℕ
npos : 0 < n
hn : HSMul.hSMul (β := R) n 1 = 0
⊢ n • f = 0

Tactic:
simp only [← Nat.cast_smul_eq_nsmul R _ f, ← nsmul_one, hn, zero_smul]

Premises used: zero_smul, Nat.cast_smul_eq_nsmul, nsmul_one
-- Module: Mathlib.GroupTheory.Torsion
Goal:
R : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
tR : IsTorsion R
f : M
n : ℕ
npos : 0 < n
hn : HSMul.hSMul (β := R) n 1 = 0
⊢ ∃ (n : ℕ), 0 < n ∧ n • f = 0

Tactic:
exact ⟨n, npos, by simp only [← Nat.cast_smul_eq_nsmul R _ f, ← nsmul_one, hn, zero_smul]⟩
-- Module: Mathlib.GroupTheory.Torsion
Goal:
R : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : Ring R
inst_2 : Finite R
inst_3 : Module R M
⊢ IsTorsion M

Tactic:
(is_add_torsion_of_finite : IsTorsion R).module_of_torsion _ _

Premises used: is_add_torsion_of_finite, AddMonoid.IsTorsion.module_of_torsion
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
g : G
⊢ Membership.mem (γ := Submonoid G) (torsion G) g ↔ IsOfFinOrder g

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Function.periodicPts, IsOfFinOrder
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : CommMonoid G
inst_1 : CommMonoid H
⊢ Eq (α := Submonoid (G × H)) (torsion (G × H)) (Submonoid.prod (torsion G) (torsion H))

Tactic:
simp [Submonoid.ext_iff, Submonoid.mem_prod, mem_torsion, IsOfFinOrder.prod_iff]

Premises used: CommMonoid.mem_torsion, Submonoid.ext_iff, IsOfFinOrder.prod_iff, Submonoid.mem_prod
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
x_1 : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun (x_2 : G) ↦ x * x_2) n 1
dsimp :
  Eq.{u_1 + 1} (α := G)
    (↑((fun (x_2 : ↥(torsion G)) ↦
              Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x ⋯ * x_2)^[n]
          1) :
      G)
    1
⊢ Eq.{u_1 + 1} (α := G)
    (↑((fun (x_2 : ↥(torsion G)) ↦
              Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x ⋯ * x_2)^[n]
          1) :
      G)
    (↑1 : G)

Tactic:
dsimp
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
x_1 : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun (x_2 : G) ↦ x * x_2) n 1
rw :
  Eq.{u_1 + 1} (α := G)
    (↑((fun (x_2 : ↥(torsion G)) ↦
            HPow.hPow (α := ↥(torsion G))
                (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x ⋯) n *
              x_2)
          1) :
      G)
    1
⊢ Eq.{u_1 + 1} (α := G)
    (↑((fun (x_2 : ↥(torsion G)) ↦
              Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x ⋯ * x_2)^[n]
          1) :
      G)
    1

Tactic:
rw [mul_left_iterate]

Premises used: mul_left_iterate
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
x_1 : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun (x_2 : G) ↦ x * x_2) n 1
change :
  (↑(HPow.hPow (α := ↥(torsion G)) (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x ⋯)
            n) :
        G) *
      1 =
    1
⊢ Eq.{u_1 + 1} (α := G)
    (↑((fun (x_2 : ↥(torsion G)) ↦
            HPow.hPow (α := ↥(torsion G))
                (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x ⋯) n *
              x_2)
          1) :
      G)
    1

Tactic:
change _ * 1 = 1
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
x_1 : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun (x_2 : G) ↦ x * x_2) n 1
rw :
  (↑(HPow.hPow (α := ↥(torsion G)) (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x ⋯)
          n) :
      G) =
    1
rw₁ : (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x ⋯) : G) ^ n = 1
rw₂ : x ^ n = 1
rw₃ rw₄ : Eq.{u_1 + 1} (α := G) 1 1
⊢ (↑(HPow.hPow (α := ↥(torsion G)) (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x ⋯)
            n) :
        G) *
      1 =
    1

Tactic:
rw [_root_.mul_one, SubmonoidClass.coe_pow, Subtype.coe_mk,
        (isPeriodicPt_mul_iff_pow_eq_one _).mp hn]

Premises used: Subtype.coe_mk, isPeriodicPt_mul_iff_pow_eq_one, SubmonoidClass.coe_pow, Iff.mp, mul_one
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : CommMonoid G
inst_1 : CommMonoid H
p : ℕ
a b : G
h : Membership.mem (γ := Set G) {g : G | ∃ (k : ℕ), g ^ p ^ k = 1} a
h_1 : Membership.mem (γ := Set G) {g : G | ∃ (k : ℕ), g ^ p ^ k = 1} b
m : ℕ
hm : a ^ p ^ m = 1
n : ℕ
hn : b ^ p ^ n = 1
rw : a ^ p ^ (m + n) * b ^ p ^ (m + n) = 1
rw₁ : a ^ (p ^ m * p ^ n) * b ^ (p ^ m * p ^ n) = 1
rw₂ : (a ^ p ^ m) ^ p ^ n * b ^ (p ^ m * p ^ n) = 1
rw₃ : HPow.hPow (α := G) 1 (p ^ n) * b ^ (p ^ m * p ^ n) = 1
rw₄ : 1 * b ^ (p ^ m * p ^ n) = 1
rw₅ : b ^ (p ^ m * p ^ n) = 1
rw₆ : b ^ (p ^ n * p ^ m) = 1
rw₇ : (b ^ p ^ n) ^ p ^ m = 1
rw₈ : HPow.hPow (α := G) 1 (p ^ m) = 1
rw₉ rw₁₀ : Eq.{u_1 + 1} (α := G) 1 1
⊢ (a * b) ^ p ^ (m + n) = 1

Tactic:
rw [mul_pow, pow_add, pow_mul, hm, one_pow, one_mul, mul_comm, pow_mul, hn, one_pow]

Premises used: one_pow, pow_add, pow_mul, mul_comm, mul_pow, one_mul
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : CommMonoid G
inst_1 : CommMonoid H
p : ℕ
⊢ HPow.hPow (α := G) 1 (HPow.hPow (β := ℕ) p 0) = 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
p : ℕ
g : G
⊢ Membership.mem (γ := Submonoid G) (primaryComponent G p) g ↔ ∃ (k : ℕ), g ^ p ^ k = 1

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
p : ℕ
inst_1 : Fact (Nat.Prime p)
g : G
⊢ Membership.mem (γ := Submonoid G) (primaryComponent G p) g ↔ ∃ (n : ℕ), orderOf g = p ^ n

Tactic:
exists_orderOf_eq_prime_pow_iff.symm

Premises used: Set.Mem, setOf, exists_orderOf_eq_prime_pow_iff, Iff.symm
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : ↥(primaryComponent G p)
rw : Membership.mem (γ := Submonoid G) (primaryComponent G p) (↑g : G)
⊢ ∃ (n : ℕ), orderOf g = p ^ n

Tactic:
rw [← orderOf_submonoid, ← mem_primaryComponent_iff_orderOf]

Premises used: orderOf_submonoid, CommMonoid.mem_primaryComponent_iff_orderOf
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : ↥(primaryComponent G p)
⊢ Membership.mem (γ := Submonoid G) (primaryComponent G p) (↑g : G)

Tactic:
g.property

Premises used: Subtype.property
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : ↥(primaryComponent G p)
⊢ Membership.mem (γ := Submonoid G) (primaryComponent G p) (↑g : G)

Tactic:
exact g.property

Premises used: Subtype.property
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg : Membership.mem (γ := Submonoid G) (primaryComponent G p) g
hg' : Membership.mem (γ := Submonoid G) (primaryComponent G p') g
⊢ ∃ (n : ℕ), orderOf g = p ^ n

Tactic:
rw [mem_primaryComponent_iff_orderOf] at hg hg'

Premises used: CommMonoid.mem_primaryComponent_iff_orderOf
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg : Membership.mem (γ := Submonoid G) (primaryComponent G p) g
hg' : Membership.mem (γ := Submonoid G) (primaryComponent G p') g
hg₁ : ∃ (n : ℕ), orderOf g = p ^ n
⊢ ∃ (n : ℕ), orderOf g = p' ^ n

Tactic:
rw [mem_primaryComponent_iff_orderOf] at hg hg'

Premises used: CommMonoid.mem_primaryComponent_iff_orderOf
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg : ∃ (n : ℕ), orderOf g = p ^ n
hg' : ∃ (n : ℕ), orderOf g = p' ^ n
zero : ∀ (hn : orderOf g = HPow.hPow (β := ℕ) p 0), g = 1
succ : ∀ (n : ℕ) (hn : orderOf g = p ^ (n + 1)), g = 1
⊢ g = 1

Tactic:
obtain ⟨_ | n, hn⟩ := hg
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg' : ∃ (n : ℕ), orderOf g = p' ^ n
hn : orderOf g = HPow.hPow (β := ℕ) p 0
zero : ∀ (hn : orderOf g = 1), g = 1
zero₁ zero₂ zero₃ zero₄ : ∀ (hn : g = 1), g = 1
⊢ g = 1

Tactic:
rwa [pow_zero, orderOf_eq_one_iff] at hn

Premises used: pow_zero, orderOf_eq_one_iff
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg' : ∃ (n : ℕ), orderOf g = p' ^ n
n : ℕ
hn : orderOf g = p ^ (n + 1)
succ : ∀ (w : ℕ) (hn' : orderOf g = p' ^ w), g = 1
⊢ g = 1

Tactic:
obtain ⟨_, hn'⟩ := hg'
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
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 ^ (n + 1)
w : ℕ
hn' : orderOf g = p' ^ w
⊢ g = 1

Tactic:
absurd (eq_of_prime_pow_eq hp.out.prime hp'.out.prime n.succ_pos (hn ▸ hn')) hne

Premises used: Nat.Prime.prime, eq_of_prime_pow_eq, absurd, Nat.succ_pos, Fact.out
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
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 ^ (n + 1)
w : ℕ
hn' : orderOf g = p' ^ w
⊢ g = 1

Tactic:
exact absurd (eq_of_prime_pow_eq hp.out.prime hp'.out.prime n.succ_pos (hn ▸ hn')) hne

Premises used: Nat.Prime.prime, eq_of_prime_pow_eq, absurd, Nat.succ_pos, Fact.out
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
tG : IsTorsion G
h : ∀ (x : G), Membership.mem (γ := Submonoid G) (torsion G) x ↔ Membership.mem (γ := Submonoid G) ⊤ x
⊢ Eq (α := Submonoid G) (torsion G) ⊤

Tactic:
ext
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
tG : IsTorsion G
x : G
h : Membership.mem (γ := Submonoid G) (torsion G) x → Membership.mem (γ := Submonoid G) ⊤ x
h₁ : Membership.mem (γ := Submonoid G) ⊤ x → Membership.mem (γ := Submonoid G) (torsion G) x
h₂ h₃ h₄ : Membership.mem (γ := Submonoid G) (torsion G) x → Membership.mem (γ := Submonoid G) ⊤ x
h₅ h₆ h₇ : Membership.mem (γ := Submonoid G) ⊤ x → Membership.mem (γ := Submonoid G) (torsion G) x
h₈ h₉ h₁₀ : Membership.mem (γ := Submonoid G) (torsion G) x → Membership.mem (γ := Submonoid G) ⊤ x
h₁₁ h₁₂ h₁₃ : Membership.mem (γ := Submonoid G) ⊤ x → Membership.mem (γ := Submonoid G) (torsion G) x
h₁₄ h₁₅ : Membership.mem (γ := Submonoid G) (torsion G) x → Membership.mem (γ := Submonoid G) ⊤ x
h₁₆ h₁₇ : Membership.mem (γ := Submonoid G) ⊤ x → Membership.mem (γ := Submonoid G) (torsion G) x
⊢ Membership.mem (γ := Submonoid G) (torsion G) x ↔ Membership.mem (γ := Submonoid G) ⊤ x

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
tG : IsTorsion G
a : ↥(torsion G)
⊢ Eq (α := G) ((tG.torsionMulEquiv : (a : ↥(torsion G)) → G) a : G)
    ((↑((MulEquiv.submonoidCongr ⋯ : (a : ↥(torsion G)) → ↥⊤) a) : G) : G)

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, Function.periodicPts, IsOfFinOrder, rfl
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommMonoid G
tG : IsTorsion G
a : G
⊢ (tG.torsionMulEquiv.symm : (a : G) → ↥(torsion G)) a =
    Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x)
      (↑((MulEquiv.symm Submonoid.topEquiv : (a : G) → ↥⊤) a) : G) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommGroup G
⊢ Eq (α := Submonoid G) (CommMonoid.torsion G) (Subgroup.toSubmonoid (torsion G))

Tactic:
rfl

Premises used: CommMonoid.torsion, rfl
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommGroup G
g : G
⊢ Membership.mem (γ := Subgroup G) (torsion G) g ↔ IsOfFinOrder g

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Function.periodicPts, IsOfFinOrder
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommGroup G
⊢ Eq (α := Subgroup G) (torsion G) ⊤ ↔ IsTorsion G

Tactic:
(torsion G).eq_top_iff'

Premises used: Set.Mem, setOf, CommGroup.torsion, Subgroup.eq_top_iff', Function.periodicPts, Monoid.IsTorsion, IsOfFinOrder
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommGroup G
rw :
  (∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a) ↔
    ∀ ⦃x : G⦄, Membership.mem (γ := Subgroup G) (torsion G) x → Membership.mem (γ := Subgroup G) ⊥ x
⊢ IsMulTorsionFree G ↔ Eq (α := Subgroup G) (torsion G) ⊥

Tactic:
rw [isMulTorsionFree_iff_not_isOfFinOrder, eq_bot_iff, SetLike.le_def]

Premises used: SetLike.le_def, isMulTorsionFree_iff_not_isOfFinOrder, eq_bot_iff
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommGroup G
⊢ (∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a) ↔
    ∀ ⦃x : G⦄, Membership.mem (γ := Subgroup G) (torsion G) x → Membership.mem (γ := Subgroup G) ⊥ x

Tactic:
simp [not_imp_not, CommGroup.mem_torsion]

Premises used: CommGroup.mem_torsion, not_imp_not
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : CommGroup G
inst_1 : CommGroup H
⊢ Eq (α := Subgroup (G × H)) (torsion (G × H)) (Subgroup.prod (torsion G) (torsion H))

Tactic:
simp [Subgroup.ext_iff, Subgroup.mem_prod, mem_torsion, IsOfFinOrder.prod_iff]

Premises used: IsOfFinOrder.prod_iff, Subgroup.ext_iff, CommGroup.mem_torsion, Subgroup.mem_prod
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
hn : n ≠ 0
simp :
  ∀ (g : HasQuotient.Quotient G (B := Subgroup G) (MonoidHom.range (G := G) (powMonoidHom n))),
    ∃ (n_1 : ℕ), 0 < n_1 ∧ g ^ n_1 = 1
⊢ IsTorsion.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (MonoidHom.range (G := G) (powMonoidHom n)))

Tactic:
simp only [Monoid.IsTorsion, isOfFinOrder_iff_pow_eq_one]

Premises used: Monoid.IsTorsion, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
hn : n ≠ 0
⊢ ∀ (g : HasQuotient.Quotient G (B := Subgroup G) (MonoidHom.range (G := G) (powMonoidHom n))),
    ∃ (n_1 : ℕ), 0 < n_1 ∧ g ^ n_1 = 1

Tactic:
fun g ↦ QuotientGroup.induction_on g fun a ↦ ⟨n, hn.pos, ?_⟩

Premises used: QuotientGroup.induction_on
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
hn : n ≠ 0
refine :
  ∀ (g : HasQuotient.Quotient G (B := Subgroup G) (MonoidHom.range (G := G) (powMonoidHom n))) (a : G),
    HPow.hPow (α := HasQuotient.Quotient G (B := Subgroup G) (MonoidHom.range (G := G) (powMonoidHom n)))
        (↑a : G ⧸ (powMonoidHom n).range) n =
      1
⊢ ∀ (g : HasQuotient.Quotient G (B := Subgroup G) (MonoidHom.range (G := G) (powMonoidHom n))),
    ∃ (n_1 : ℕ), 0 < n_1 ∧ g ^ n_1 = 1

Tactic:
refine fun g ↦ QuotientGroup.induction_on g fun a ↦ ⟨n, hn.pos, ?_⟩
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
hn : n ≠ 0
g : HasQuotient.Quotient G (B := Subgroup G) (MonoidHom.range (G := G) (powMonoidHom n))
a : G
rw : Membership.mem (γ := Subgroup G) (MonoidHom.range (G := G) (powMonoidHom n)) (a ^ n)
⊢ HPow.hPow (α := HasQuotient.Quotient G (B := Subgroup G) (MonoidHom.range (G := G) (powMonoidHom n)))
      (↑a : G ⧸ (powMonoidHom n).range) n =
    1

Tactic:
rw [← QuotientGroup.mk_pow, QuotientGroup.eq_one_iff]

Premises used: QuotientGroup.mk_pow, QuotientGroup.eq_one_iff
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
hn : n ≠ 0
g : HasQuotient.Quotient G (B := Subgroup G) (MonoidHom.range (G := G) (powMonoidHom n))
a : G
⊢ Membership.mem (γ := Subgroup G) (MonoidHom.range (G := G) (powMonoidHom n)) (a ^ n)

Tactic:
simp