awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ 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
have change : (↑(HPow.hPow (α := ↥(torsion G)) (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x sorry)
          n) :
      G) *
    1 =
  1
Tactic: change _ * 1 = 1
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ (↑(HPow.hPow (α := ↥(torsion G)) (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x ⋯)
            n) :
        G) *
      1 =
    1
have rw : (↑(HPow.hPow (α := ↥(torsion G)) (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x sorry)
        n) :
    G) =
  1
Tactic: rw [_root_.mul_one, SubmonoidClass.coe_pow, Subtype.coe_mk,
        (isPeriodicPt_mul_iff_pow_eq_one _).mp hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ (↑(HPow.hPow (α := ↥(torsion G)) (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x ⋯)
            n) :
        G) *
      1 =
    1
have rw₁ : (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x sorry) : G) ^ n = 1
Tactic: rw [_root_.mul_one, SubmonoidClass.coe_pow, Subtype.coe_mk,
        (isPeriodicPt_mul_iff_pow_eq_one _).mp hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ (↑(HPow.hPow (α := ↥(torsion G)) (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x ⋯)
            n) :
        G) *
      1 =
    1
have rw₂ : x ^ n = 1
Tactic: rw [_root_.mul_one, SubmonoidClass.coe_pow, Subtype.coe_mk,
        (isPeriodicPt_mul_iff_pow_eq_one _).mp hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ (↑(HPow.hPow (α := ↥(torsion G)) (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x ⋯)
            n) :
        G) *
      1 =
    1
have rw₃ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [_root_.mul_one, SubmonoidClass.coe_pow, Subtype.coe_mk,
        (isPeriodicPt_mul_iff_pow_eq_one _).mp hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ (a * b) ^ p ^ (m + n) = 1
have rw : a ^ p ^ (m + n) * 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ (a * b) ^ p ^ (m + n) = 1
have rw₁ : a ^ (p ^ m * p ^ n) * b ^ (p ^ m * p ^ n) = 1
Tactic: rw [mul_pow, pow_add, pow_mul, hm, one_pow, one_mul, mul_comm, pow_mul, hn, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ (a * b) ^ p ^ (m + n) = 1
have rw₂ : (a ^ p ^ m) ^ p ^ n * b ^ (p ^ m * p ^ n) = 1
Tactic: rw [mul_pow, pow_add, pow_mul, hm, one_pow, one_mul, mul_comm, pow_mul, hn, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ (a * b) ^ p ^ (m + n) = 1
have rw₃ : HPow.hPow (α := G) 1 (p ^ n) * b ^ (p ^ m * p ^ n) = 1
Tactic: rw [mul_pow, pow_add, pow_mul, hm, one_pow, one_mul, mul_comm, pow_mul, hn, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ (a * b) ^ p ^ (m + n) = 1
have rw₄ : 1 * b ^ (p ^ m * p ^ n) = 1
Tactic: rw [mul_pow, pow_add, pow_mul, hm, one_pow, one_mul, mul_comm, pow_mul, hn, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ (a * b) ^ p ^ (m + n) = 1
have rw₅ : b ^ (p ^ m * p ^ n) = 1
Tactic: rw [mul_pow, pow_add, pow_mul, hm, one_pow, one_mul, mul_comm, pow_mul, hn, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ (a * b) ^ p ^ (m + n) = 1
have rw₆ : b ^ (p ^ n * p ^ m) = 1
Tactic: rw [mul_pow, pow_add, pow_mul, hm, one_pow, one_mul, mul_comm, pow_mul, hn, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ (a * b) ^ p ^ (m + n) = 1
have rw₇ : (b ^ p ^ n) ^ p ^ m = 1
Tactic: rw [mul_pow, pow_add, pow_mul, hm, one_pow, one_mul, mul_comm, pow_mul, hn, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ (a * b) ^ p ^ (m + n) = 1
have rw₈ : HPow.hPow (α := G) 1 (p ^ m) = 1
Tactic: rw [mul_pow, pow_add, pow_mul, hm, one_pow, one_mul, mul_comm, pow_mul, hn, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ (a * b) ^ p ^ (m + n) = 1
have rw₉ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [mul_pow, pow_add, pow_mul, hm, one_pow, one_mul, mul_comm, pow_mul, hn, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
inst : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : ↥(primaryComponent G p)
⊢ ∃ (n : ℕ), orderOf g = p ^ n
have rw : Membership.mem (γ := Submonoid G) (primaryComponent G p) (↑g : G)
Tactic: rw [← orderOf_submonoid, ← mem_primaryComponent_iff_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (hypothesis)
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
⊢ g = 1
have hg₁ : ∃ (n : ℕ), orderOf g = p ^ n
Tactic: rw [mem_primaryComponent_iff_orderOf] at hg hg'
Cleared hypotheses: hg, hg'
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (hypothesis)
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
⊢ g = 1
have hg'₁ : ∃ (n : ℕ), orderOf g = p' ^ n
Tactic: rw [mem_primaryComponent_iff_orderOf] at hg hg'
Cleared hypotheses: hg, hg'
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ g = 1
have zero : ∀ (hn : orderOf g = HPow.hPow (β := ℕ) p 0), g = 1
Tactic: obtain ⟨_ | n, hn⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ g = 1
have succ : ∀ (n : ℕ) (hn : orderOf g = p ^ (n + 1)), g = 1
Tactic: obtain ⟨_ | n, hn⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ g = 1
have zero : ∀ (hn : orderOf g = 1), g = 1
Tactic: rwa [pow_zero, orderOf_eq_one_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ g = 1
have zero₁ : ∀ (hn : g = 1), g = 1
Tactic: rwa [pow_zero, orderOf_eq_one_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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)
⊢ g = 1
have succ : ∀ (w : ℕ) (hn' : orderOf g = p' ^ w), g = 1
Tactic: obtain ⟨_, hn'⟩ := hg'
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
inst : CommMonoid G
tG : IsTorsion G
⊢ Eq (α := Submonoid G) (torsion G) ⊤
have h : ∀ (x : G), Membership.mem (γ := Submonoid G) (torsion G) x ↔ Membership.mem (γ := Submonoid G) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
inst : CommMonoid G
tG : IsTorsion G
x : G
⊢ Membership.mem (γ := Submonoid G) (torsion G) x ↔ Membership.mem (γ := Submonoid G) ⊤ x
have h : Membership.mem (γ := Submonoid G) (torsion G) x → Membership.mem (γ := Submonoid G) ⊤ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ Membership.mem (γ := Submonoid G) (torsion G) x ↔ Membership.mem (γ := Submonoid G) ⊤ x
have h₁ : Membership.mem (γ := Submonoid G) ⊤ x → Membership.mem (γ := Submonoid G) (torsion G) x
Tactic: tauto
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
inst : CommGroup G
⊢ IsMulTorsionFree G ↔ Eq (α := Subgroup G) (torsion G) ⊥
have rw : (∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a) ↔
  ∀ ⦃x : G⦄, Membership.mem (γ := Subgroup G) (torsion G) x → Membership.mem (γ := Subgroup G) ⊥ x
Tactic: rw [isMulTorsionFree_iff_not_isOfFinOrder, eq_bot_iff, SetLike.le_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
hn : n ≠ 0
⊢ IsTorsion.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (MonoidHom.range (G := G) (powMonoidHom n)))
have simp : ∀ (g : HasQuotient.Quotient G (B := Subgroup G) (MonoidHom.range (G := G) (powMonoidHom n))),
  ∃ (n_1 : ℕ), 0 < n_1 ∧ g ^ n_1 = 1
Tactic: simp only [Monoid.IsTorsion, isOfFinOrder_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
have 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
Tactic: refine fun g ↦ QuotientGroup.induction_on g fun a ↦ ⟨n, hn.pos, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
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
⊢ HPow.hPow (α := HasQuotient.Quotient G (B := Subgroup G) (MonoidHom.range (G := G) (powMonoidHom n)))
      (↑a : G ⧸ (powMonoidHom n).range) n =
    1
have rw : Membership.mem (γ := Subgroup G) (MonoidHom.range (G := G) (powMonoidHom n)) (a ^ n)
Tactic: rw [← QuotientGroup.mk_pow, QuotientGroup.eq_one_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : CommGroup G
inst_1 : CommGroup H
p : ℕ
g : G
h : g ∈ Subsemigroup.carrier (Submonoid.toSubsemigroup (CommMonoid.primaryComponent G p))
k : ℕ
hk : g ^ p ^ k = 1
⊢ g⁻¹ ^ p ^ k = 1
have rw : (g ^ p ^ k)⁻¹ = 1
Tactic: rw [inv_pow, hk, inv_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : CommGroup G
inst_1 : CommGroup H
p : ℕ
g : G
h : g ∈ Subsemigroup.carrier (Submonoid.toSubsemigroup (CommMonoid.primaryComponent G p))
k : ℕ
hk : g ^ p ^ k = 1
rw : (g ^ p ^ k)⁻¹ = 1
⊢ g⁻¹ ^ p ^ k = 1
have rw₁ : Eq.{u_1 + 1} (α := G) 1⁻¹ 1
Tactic: rw [inv_pow, hk, inv_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : CommGroup G
inst_1 : CommGroup H
p : ℕ
g : G
h : g ∈ Subsemigroup.carrier (Submonoid.toSubsemigroup (CommMonoid.primaryComponent G p))
k : ℕ
hk : g ^ p ^ k = 1
rw : (g ^ p ^ k)⁻¹ = 1
rw₁ : Eq.{u_1 + 1} (α := G) 1⁻¹ 1
⊢ g⁻¹ ^ p ^ k = 1
have rw₂ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [inv_pow, hk, inv_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : CommGroup G
inst_1 : CommGroup H
⊢ IsMulTorsionFree.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (torsion G))
have refine : ∀ (g : HasQuotient.Quotient G (B := Subgroup G) (torsion G)) (hne : g ≠ 1) (hfin : IsOfFinOrder g), g = 1
Tactic: refine .of_not_isOfFinOrder fun g hne hfin ↦ hne ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : CommGroup G
inst_1 : CommGroup H
g : HasQuotient.Quotient G (B := Subgroup G) (torsion G)
hne : g ≠ 1
hfin : IsOfFinOrder g
⊢ g = 1
have mk : ∀ (g : G)
  (hne :
    Ne (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
      (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1)
  (hfin :
    IsOfFinOrder (G := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
      (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g)),
  Eq (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1
Tactic: obtain ⟨g⟩ := g
Cleared hypotheses: hne, hfin
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : CommGroup G
inst_1 : CommGroup H
g_1 : HasQuotient.Quotient G (B := Subgroup G) (torsion G)
g : G
hne :
  Ne (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1
hfin :
  IsOfFinOrder (G := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g)
⊢ Eq (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1
have mk : ∀ (m : ℕ) (mpos : 0 < m)
  (hm :
    HPow.hPow (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
        (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) m =
      1),
  Eq (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1
Tactic: obtain ⟨m, mpos, hm⟩ := hfin.exists_pow_eq_one
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : CommGroup G
inst_1 : CommGroup H
g_1 : HasQuotient.Quotient G (B := Subgroup G) (torsion G)
g : G
hne :
  Ne (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1
hfin :
  IsOfFinOrder (G := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g)
m : ℕ
mpos : 0 < m
hm :
  HPow.hPow (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
      (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) m =
    1
⊢ Eq (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1
have mk : ∀ (n : ℕ) (npos : 0 < n) (hn : HPow.hPow (α := G) ((fun (x : G) ↦ x ^ m) g) n = 1),
  Eq (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1
Tactic: obtain ⟨n, npos, hn⟩ := ((QuotientGroup.eq_one_iff _).mp hm).exists_pow_eq_one
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
m : M
h : m ∈ AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (AddCommGroup.torsion M)))
n : ℕ
hn : n > 0
hn' : Function.IsPeriodicPt (fun (x : M) ↦ m + x) n 0
⊢ Function.IsPeriodicPt (fun (x : M) ↦ r • m + x) n 0
have simp : ∀ (hn' : n • m = 0), r • n • m = 0
Tactic: simp only [Function.IsPeriodicPt, Function.IsFixedPt, add_left_iterate, add_zero,
      smul_comm n] at hn' ⊢
Cleared hypotheses: hn'
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
m : M
h : m ∈ AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (AddCommGroup.torsion M)))
n : ℕ
hn : n > 0
hn' : Function.IsPeriodicPt (fun (x : M) ↦ m + x) n 0
⊢ Function.IsPeriodicPt (fun (x : M) ↦ r • m + x) n 0
have simp : ∀ (hn' : n • m = 0), r • n • m = 0
Tactic: { simp only [Function.IsPeriodicPt, Function.IsFixedPt, add_left_iterate, add_zero,
      smul_comm n] at hn' ⊢; simp only [hn', smul_zero] }
Cleared hypotheses: hn'