awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
hM : IsTorsion R M
S : Finset M
hS : Eq (α := Submodule R M) (span R (↑S : Set M)) ⊤
⊢ ((↑(annihilator.{u_1, u_2} (M := M) ⊤) : Set R) ∩ (↑R⁰ : Set R)).Nonempty
have refine : (↑(∏ x ∈ S, Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) sorry) : R) ∈ (↑(annihilator.{u_1, u_2} (M := M) ⊤) : Set R)
Tactic: refine ⟨_, ?_, (∏ x ∈ S, (@hM x).choose : R⁰).prop⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
hM : IsTorsion R M
S : Finset M
hS : Eq (α := Submodule R M) (span R (↑S : Set M)) ⊤
⊢ (↑(∏ x ∈ S, Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) ⋯) : R) ∈ (↑(annihilator.{u_1, u_2} (M := M) ⊤) : Set R)
have rw : ∀ (n : (↑(↑S : Set M) : Type u_2)),
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (∏ i ∈ S, (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • i = 0) sorry) : R)) (↑n : M) = 0
Tactic: rw [Submonoid.coe_finsetProd, SetLike.mem_coe, ← hS, mem_annihilator_span]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
hM : IsTorsion R M
S : Finset M
hS : Eq (α := Submodule R M) (span R (↑S : Set M)) ⊤
n : (↑(↑S : Set M) : Type u_2)
this : DecidableEq M := Classical.decEq M
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (∏ i ∈ S, (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • i = 0) ⋯) : R)) (↑n : M) = 0
have rw : ((∏ x ∈ S.erase (↑n : M), (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) sorry) : R)) *
      (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • (↑n : M) = 0) sorry) : R)) •
    (↑n : M) =
  0
Tactic: rw [← Finset.prod_erase_mul _ _ n.prop, mul_smul, ← Submonoid.smul_def, (@hM n).choose_spec,
    smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
hM : IsTorsion R M
S : Finset M
hS : Eq (α := Submodule R M) (span R (↑S : Set M)) ⊤
n : (↑(↑S : Set M) : Type u_2)
this : DecidableEq M := Classical.decEq M
rw :
  ((∏ x ∈ S.erase (↑n : M), (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) ⋯) : R)) *
        (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • (↑n : M) = 0) ⋯) : R)) •
      (↑n : M) =
    0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (∏ i ∈ S, (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • i = 0) ⋯) : R)) (↑n : M) = 0
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (∏ x ∈ S.erase (↑n : M), (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) sorry) : R))
    ((↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • (↑n : M) = 0) sorry) : R) • (↑n : M)) =
  0
Tactic: rw [← Finset.prod_erase_mul _ _ n.prop, mul_smul, ← Submonoid.smul_def, (@hM n).choose_spec,
    smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
hM : IsTorsion R M
S : Finset M
hS : Eq (α := Submodule R M) (span R (↑S : Set M)) ⊤
n : (↑(↑S : Set M) : Type u_2)
this : DecidableEq M := Classical.decEq M
rw :
  ((∏ x ∈ S.erase (↑n : M), (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) ⋯) : R)) *
        (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • (↑n : M) = 0) ⋯) : R)) •
      (↑n : M) =
    0
rw₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R)
      (∏ x ∈ S.erase (↑n : M), (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) ⋯) : R))
      ((↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • (↑n : M) = 0) ⋯) : R) • (↑n : M)) =
    0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (∏ i ∈ S, (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • i = 0) ⋯) : R)) (↑n : M) = 0
have rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (∏ x ∈ S.erase (↑n : M), (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) sorry) : R))
    (Exists.choose (p := fun (a : ↥R⁰) ↦ a • (↑n : M) = 0) sorry • (↑n : M)) =
  0
Tactic: rw [← Finset.prod_erase_mul _ _ n.prop, mul_smul, ← Submonoid.smul_def, (@hM n).choose_spec,
    smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
hM : IsTorsion R M
S : Finset M
hS : Eq (α := Submodule R M) (span R (↑S : Set M)) ⊤
n : (↑(↑S : Set M) : Type u_2)
this : DecidableEq M := Classical.decEq M
rw :
  ((∏ x ∈ S.erase (↑n : M), (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) ⋯) : R)) *
        (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • (↑n : M) = 0) ⋯) : R)) •
      (↑n : M) =
    0
rw₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R)
      (∏ x ∈ S.erase (↑n : M), (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) ⋯) : R))
      ((↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • (↑n : M) = 0) ⋯) : R) • (↑n : M)) =
    0
rw₂ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R)
      (∏ x ∈ S.erase (↑n : M), (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) ⋯) : R))
      (Exists.choose (p := fun (a : ↥R⁰) ↦ a • (↑n : M) = 0) ⋯ • (↑n : M)) =
    0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (∏ i ∈ S, (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • i = 0) ⋯) : R)) (↑n : M) = 0
have rw₃ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
    (∏ x ∈ S.erase (↑n : M), (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) sorry) : R)) 0 =
  0
Tactic: rw [← Finset.prod_erase_mul _ _ n.prop, mul_smul, ← Submonoid.smul_def, (@hM n).choose_spec,
    smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
hM : IsTorsion R M
S : Finset M
hS : Eq (α := Submodule R M) (span R (↑S : Set M)) ⊤
n : (↑(↑S : Set M) : Type u_2)
this : DecidableEq M := Classical.decEq M
rw :
  ((∏ x ∈ S.erase (↑n : M), (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) ⋯) : R)) *
        (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • (↑n : M) = 0) ⋯) : R)) •
      (↑n : M) =
    0
rw₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R)
      (∏ x ∈ S.erase (↑n : M), (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) ⋯) : R))
      ((↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • (↑n : M) = 0) ⋯) : R) • (↑n : M)) =
    0
rw₂ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R)
      (∏ x ∈ S.erase (↑n : M), (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) ⋯) : R))
      (Exists.choose (p := fun (a : ↥R⁰) ↦ a • (↑n : M) = 0) ⋯ • (↑n : M)) =
    0
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
      (∏ x ∈ S.erase (↑n : M), (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) ⋯) : R)) 0 =
    0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (∏ i ∈ S, (↑(Exists.choose (p := fun (a : ↥R⁰) ↦ a • i = 0) ⋯) : R)) (↑n : M) = 0
have rw₄ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [← Finset.prod_erase_mul _ _ n.prop, mul_smul, ← Submonoid.smul_def, (@hM n).choose_spec,
    smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : NoZeroDivisors R
inst_4 : Nontrivial R
⊢ (↑(torsion R M) : Set M) = {x : M | Ne (α := Ideal R) (annihilator (M := M) (R ∙ x)) ⊥}
have h : ∀ (x : M),
  x ∈ (↑(torsion R M) : Set M) ↔
    Membership.mem (γ := Set M) {x : M | Ne (α := Ideal R) (annihilator (M := M) (R ∙ x)) ⊥} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : NoZeroDivisors R
inst_4 : Nontrivial R
x : M
⊢ x ∈ (↑(torsion R M) : Set M) ↔
    Membership.mem (γ := Set M) {x : M | Ne (α := Ideal R) (annihilator (M := M) (R ∙ x)) ⊥} x
have h : x ∈ (↑(torsion R M) : Set M) ↔
  Membership.mem (γ := Set M) {x : M | ∃ (x_1 : R), (∀ (n : M), (∃ (a : R), a • x = n) → x_1 • n = 0) ∧ x_1 ≠ 0} x
Tactic: simp_rw [Submodule.ne_bot_iff, mem_annihilator, mem_span_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : NoZeroDivisors R
inst_4 : Nontrivial R
x : M
h : x ∈ (↑(torsion R M) : Set M)
a : ↥R⁰
hax : a • x = 0
x_1 : M
h_1 : ∃ (a : R), a • x = x_1
b : R
hb : b • x = x_1
⊢ (↑a : R) • x_1 = 0
have rw : (↑a : R) • b • x = 0
Tactic: rw [← hb, smul_comm, ← Submonoid.smul_def, hax, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : NoZeroDivisors R
inst_4 : Nontrivial R
x : M
h : x ∈ (↑(torsion R M) : Set M)
a : ↥R⁰
hax : a • x = 0
x_1 : M
h_1 : ∃ (a : R), a • x = x_1
b : R
hb : b • x = x_1
rw : (↑a : R) • b • x = 0
⊢ (↑a : R) • x_1 = 0
have rw₁ : b • (↑a : R) • x = 0
Tactic: rw [← hb, smul_comm, ← Submonoid.smul_def, hax, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : NoZeroDivisors R
inst_4 : Nontrivial R
x : M
h : x ∈ (↑(torsion R M) : Set M)
a : ↥R⁰
hax : a • x = 0
x_1 : M
h_1 : ∃ (a : R), a • x = x_1
b : R
hb : b • x = x_1
rw : (↑a : R) • b • x = 0
rw₁ : b • (↑a : R) • x = 0
⊢ (↑a : R) • x_1 = 0
have rw₂ : b • a • x = 0
Tactic: rw [← hb, smul_comm, ← Submonoid.smul_def, hax, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : NoZeroDivisors R
inst_4 : Nontrivial R
x : M
h : x ∈ (↑(torsion R M) : Set M)
a : ↥R⁰
hax : a • x = 0
x_1 : M
h_1 : ∃ (a : R), a • x = x_1
b : R
hb : b • x = x_1
rw : (↑a : R) • b • x = 0
rw₁ : b • (↑a : R) • x = 0
rw₂ : b • a • x = 0
⊢ (↑a : R) • x_1 = 0
have rw₃ : HSMul.hSMul (β := M) b 0 = 0
Tactic: rw [← hb, smul_comm, ← Submonoid.smul_def, hax, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : NoZeroDivisors R
inst_4 : Nontrivial R
x : M
h : x ∈ (↑(torsion R M) : Set M)
a : ↥R⁰
hax : a • x = 0
x_1 : M
h_1 : ∃ (a : R), a • x = x_1
b : R
hb : b • x = x_1
rw : (↑a : R) • b • x = 0
rw₁ : b • (↑a : R) • x = 0
rw₂ : b • a • x = 0
rw₃ : HSMul.hSMul (β := M) b 0 = 0
⊢ (↑a : R) • x_1 = 0
have rw₄ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [← hb, smul_comm, ← Submonoid.smul_def, hax, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
G : Type u_3
inst : AddCommGroup G
⊢ Eq (α := AddSubgroup G) (toAddSubgroup (module_M := AddCommGroup.toIntModule G) (torsion ℤ G))
    (AddCommGroup.torsion G)
have h : ∀ (x : G),
  Membership.mem (γ := AddSubgroup G) (toAddSubgroup (module_M := AddCommGroup.toIntModule G) (torsion ℤ G)) x ↔
    Membership.mem (γ := AddSubgroup G) (AddCommGroup.torsion G) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
G : Type u_3
inst : AddCommGroup G
x : G
⊢ Membership.mem (γ := AddSubgroup G) (toAddSubgroup (module_M := AddCommGroup.toIntModule G) (torsion ℤ G)) x ↔
    Membership.mem (γ := AddSubgroup G) (AddCommGroup.torsion G) x
have h : (∃ (n : ℤ), n ≠ 0 ∧ n • x = 0) ↔
  Membership.mem (γ := AddSubgroup G) (toAddSubgroup (module_M := AddCommGroup.toIntModule G) (torsion ℤ G)) x
Tactic: refine ((isOfFinAddOrder_iff_zsmul_eq_zero (x := x)).trans ?_).symm
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
⊢ IsTorsionFree R M ↔ Eq (α := Submodule R M) (torsion R M) ⊥
have simp : (∀ (r : R) (m : M), r • m = 0 → r = 0 ∨ m = 0) ↔ ∀ (y : M) (x : R), ¬x = 0 → x • y = 0 → y = 0
Tactic: simp [torsion, torsion', subset_antisymm_iff, exists_ne, isTorsionFree_iff_smul_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
z : HasQuotient.Quotient M (B := Submodule R M) (torsion R M)
x : M
h :
  Membership.mem (γ := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (torsion R M)))
    (torsion.{u_1, u_2} R (HasQuotient.Quotient M (B := Submodule R M) (torsion R M)) :
      Submodule R (HasQuotient.Quotient M (B := Submodule R M) (torsion R M)))
    (Quotient.mk'' x)
a : ↥R⁰
hax : HSMul.hSMul (β := HasQuotient.Quotient M (B := Submodule R M) (torsion R M)) a (Quotient.mk'' x) = 0
⊢ Membership.mem (γ := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (torsion R M))) ⊥ (Quotient.mk'' x)
have hax₁ : Membership.mem (γ := Submodule R M) (torsion R M) (a • x)
Tactic: rw [Quotient.mk''_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero] at hax
Cleared hypotheses: hax
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
z : HasQuotient.Quotient M (B := Submodule R M) (torsion R M)
x : M
h :
  Membership.mem (γ := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (torsion R M)))
    (torsion.{u_1, u_2} R (HasQuotient.Quotient M (B := Submodule R M) (torsion R M)) :
      Submodule R (HasQuotient.Quotient M (B := Submodule R M) (torsion R M)))
    (Quotient.mk'' x)
a : ↥R⁰
hax : Membership.mem (γ := Submodule R M) (torsion R M) (a • x)
⊢ Membership.mem (γ := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (torsion R M))) ⊥ (Quotient.mk'' x)
have rw : Membership.mem (γ := Submodule R M) (torsion R M) x
Tactic: rw [mem_bot, Quotient.mk''_eq_mk, Quotient.mk_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
z : HasQuotient.Quotient M (B := Submodule R M) (torsion R M)
x : M
h :
  Membership.mem (γ := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (torsion R M)))
    (torsion.{u_1, u_2} R (HasQuotient.Quotient M (B := Submodule R M) (torsion R M)) :
      Submodule R (HasQuotient.Quotient M (B := Submodule R M) (torsion R M)))
    (Quotient.mk'' x)
a : ↥R⁰
hax : Membership.mem (γ := Submodule R M) (torsion R M) (a • x)
⊢ Membership.mem (γ := Submodule R M) (torsion R M) x
have obtain : ∀ (b : ↥R⁰) (h : b • a • x = 0), Membership.mem (γ := Submodule R M) (torsion R M) x
Tactic: obtain ⟨b, h⟩ := hax
Cleared hypotheses: hax
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
p : R
⊢ IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p) ↔ ∀ (x : M), ∃ (n : ℕ), p ^ n • x = 0
have mp : IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p) → ∀ (x : M), ∃ (n : ℕ), p ^ n • x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
p : R
mp : IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p) → ∀ (x : M), ∃ (n : ℕ), p ^ n • x = 0
⊢ IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p) ↔ ∀ (x : M), ∃ (n : ℕ), p ^ n • x = 0
have mpr : (∀ (x : M), ∃ (n : ℕ), p ^ n • x = 0) → IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
p : R
h : IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p)
x : M
⊢ ∃ (n : ℕ), p ^ n • x = 0
have mp : ∀ (a : R) (n : ℕ) (hn : (fun (x : ℕ) ↦ p ^ x) n = a)
  (hx :
    HSMul.hSMul (α := ↥(Submonoid.powers p))
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers p) x) a sorry) x =
      0),
  ∃ (n : ℕ), p ^ n • x = 0
Tactic: let ⟨⟨a, ⟨n, hn⟩⟩, hx⟩ := @h x
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
p : R
h : IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p)
x : M
a : R
n : ℕ
hn : p ^ n = a
hx :
  HSMul.hSMul (α := ↥(Submonoid.powers p))
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers p) x) a ⋯) x =
    0
⊢ ∃ (n : ℕ), p ^ n • x = 0
have h₁ : p ^ n • x = 0
Tactic: use n
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
p : R
h : IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p)
x : M
a : R
n : ℕ
hn : p ^ n = a
hx :
  HSMul.hSMul (α := ↥(Submonoid.powers p))
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers p) x) a ⋯) x =
    0
⊢ p ^ n • x = 0
have h₁ : a • x = 0
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
p : R
h : ∀ (x : M), ∃ (n : ℕ), p ^ n • x = 0
x : M
⊢ ∃ (a : ↥(Submonoid.powers p)), a • x = 0
have mpr : ∀ (n : ℕ) (hn : p ^ n • x = 0), ∃ (a : ↥(Submonoid.powers p)), a • x = 0
Tactic: let ⟨n, hn⟩ := h x
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : Eq (α := Submodule R M) (span R (Set.range s)) ⊤
oj : Option (Fin d) := List.argmax (β := ℕ) (fun (i : Fin d) ↦ pOrder hM (s i)) (List.finRange d)
⊢ ∃ (j : Fin d), IsTorsionBy R M (p ^ pOrder hM (s j))
have hoj : oj.isSome = true
Tactic: have hoj : oj.isSome :=
    Option.ne_none_iff_isSome.mp fun eq_none =>
      hd <| List.finRange_eq_nil_iff.mp <| List.argmax_eq_none.mp eq_none
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : Eq (α := Submodule R M) (span R (Set.range s)) ⊤
oj : Option (Fin d) := List.argmax (β := ℕ) (fun (i : Fin d) ↦ pOrder hM (s i)) (List.finRange d)
hoj : oj.isSome = true
⊢ ∃ (j : Fin d), IsTorsionBy R M (p ^ pOrder hM (s j))
have h : IsTorsionBy R M (p ^ pOrder hM (s (oj.get hoj)))
Tactic: use Option.get _ hoj
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : Eq (α := Submodule R M) (span R (Set.range s)) ⊤
oj : Option (Fin d) := List.argmax (β := ℕ) (fun (i : Fin d) ↦ pOrder hM (s i)) (List.finRange d)
hoj : oj.isSome = true
⊢ IsTorsionBy R M (p ^ pOrder hM (s (oj.get hoj)))
have h : ∀ (y : Fin d), s y ∈ (↑(torsionBy R M (p ^ pOrder hM (s (oj.get hoj)))) : Set M)
Tactic: rw [isTorsionBy_iff_torsionBy_eq_top, eq_top_iff, ← hs, Submodule.span_le,
    Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : Eq (α := Submodule R M) (span R (Set.range s)) ⊤
oj : Option (Fin d) := List.argmax (β := ℕ) (fun (i : Fin d) ↦ pOrder hM (s i)) (List.finRange d)
hoj : oj.isSome = true
i : Fin d
⊢ s i ∈ (↑(torsionBy R M (p ^ pOrder hM (s (oj.get hoj)))) : Set M)
have h : p ^ pOrder hM (s (oj.get hoj)) • s i = 0
Tactic: change (p ^ pOrder hM (s (Option.get oj hoj))) • s i = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : Eq (α := Submodule R M) (span R (Set.range s)) ⊤
oj : Option (Fin d) := List.argmax (β := ℕ) (fun (i : Fin d) ↦ pOrder hM (s i)) (List.finRange d)
hoj : oj.isSome = true
i : Fin d
⊢ p ^ pOrder hM (s (oj.get hoj)) • s i = 0
have this : pOrder hM (s i) ≤ pOrder hM (s (oj.get hoj))
Tactic: have : pOrder hM (s i) ≤ pOrder hM (s <| Option.get _ hoj) :=
    List.le_of_mem_argmax (List.mem_finRange i) (Option.get_mem hoj)
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : Eq (α := Submodule R M) (span R (Set.range s)) ⊤
oj : Option (Fin d) := List.argmax (β := ℕ) (fun (i : Fin d) ↦ pOrder hM (s i)) (List.finRange d)
hoj : oj.isSome = true
i : Fin d
this : pOrder hM (s i) ≤ pOrder hM (s (oj.get hoj))
⊢ p ^ pOrder hM (s (oj.get hoj)) • s i = 0
have h : p ^ (pOrder hM (s (oj.get hoj)) - pOrder hM (s i) + pOrder hM (s i)) • s i = 0
Tactic: rw [← Nat.sub_add_cancel this, pow_add, mul_smul, pow_pOrder_smul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : Eq (α := Submodule R M) (span R (Set.range s)) ⊤
oj : Option (Fin d) := List.argmax (β := ℕ) (fun (i : Fin d) ↦ pOrder hM (s i)) (List.finRange d)
hoj : oj.isSome = true
i : Fin d
this : pOrder hM (s i) ≤ pOrder hM (s (oj.get hoj))
h : p ^ (pOrder hM (s (oj.get hoj)) - pOrder hM (s i) + pOrder hM (s i)) • s i = 0
⊢ p ^ pOrder hM (s (oj.get hoj)) • s i = 0
have h₁ : (p ^ (pOrder hM (s (oj.get hoj)) - pOrder hM (s i)) * p ^ pOrder hM (s i)) • s i = 0
Tactic: rw [← Nat.sub_add_cancel this, pow_add, mul_smul, pow_pOrder_smul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : Eq (α := Submodule R M) (span R (Set.range s)) ⊤
oj : Option (Fin d) := List.argmax (β := ℕ) (fun (i : Fin d) ↦ pOrder hM (s i)) (List.finRange d)
hoj : oj.isSome = true
i : Fin d
this : pOrder hM (s i) ≤ pOrder hM (s (oj.get hoj))
h : p ^ (pOrder hM (s (oj.get hoj)) - pOrder hM (s i) + pOrder hM (s i)) • s i = 0
h₁ : (p ^ (pOrder hM (s (oj.get hoj)) - pOrder hM (s i)) * p ^ pOrder hM (s i)) • s i = 0
⊢ p ^ pOrder hM (s (oj.get hoj)) • s i = 0
have h₂ : p ^ (pOrder hM (s (oj.get hoj)) - pOrder hM (s i)) • p ^ pOrder hM (s i) • s i = 0
Tactic: rw [← Nat.sub_add_cancel this, pow_add, mul_smul, pow_pOrder_smul, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : Eq (α := Submodule R M) (span R (Set.range s)) ⊤
oj : Option (Fin d) := List.argmax (β := ℕ) (fun (i : Fin d) ↦ pOrder hM (s i)) (List.finRange d)
hoj : oj.isSome = true
i : Fin d
this : pOrder hM (s i) ≤ pOrder hM (s (oj.get hoj))
h : p ^ (pOrder hM (s (oj.get hoj)) - pOrder hM (s i) + pOrder hM (s i)) • s i = 0
h₁ : (p ^ (pOrder hM (s (oj.get hoj)) - pOrder hM (s i)) * p ^ pOrder hM (s i)) • s i = 0
h₂ : p ^ (pOrder hM (s (oj.get hoj)) - pOrder hM (s i)) • p ^ pOrder hM (s i) • s i = 0
⊢ p ^ pOrder hM (s (oj.get hoj)) • s i = 0
have h₃ : HSMul.hSMul (β := M) (p ^ (pOrder hM (s (oj.get hoj)) - pOrder hM (s i))) 0 = 0
Tactic: rw [← Nat.sub_add_cancel this, pow_add, mul_smul, pow_pOrder_smul, smul_zero]