awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
s : S
x : M
a : S
h : a • x = 0
h₁ : s • a • x = 0
h₂ : HSMul.hSMul (β := M) s 0 = 0
h₃ h₄ : Eq.{u_2 + 1} (α := M) 0 0
⊢ a • s • x = 0

Tactic:
rw [smul_comm, h, smul_zero]

Premises used: smul_zero, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
⊢ SMulCommClass.{u_3, u_1, u_2} S R ↥(torsion' R M S)

Tactic:
⟨fun _ _ _ => Subtype.ext <| smul_comm _ _ _⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
h : Eq (α := Submodule R M) (torsion' R M S) ⊤
x : M
rw : Membership.mem (γ := Submodule R M) ⊤ x
⊢ ∃ (a : S), a • x = 0

Tactic:
rw [← @mem_torsion'_iff R, h]

Premises used: Submodule.mem_torsion'_iff
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
h : Eq (α := Submodule R M) (torsion' R M S) ⊤
x : M
⊢ Membership.mem (γ := Submodule R M) ⊤ x

Tactic:
trivial
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
⊢ IsTorsion'.{u_2, u_3} (↥(torsion' R M S)) S

Tactic:
fun ⟨_, ⟨a, h⟩⟩ => ⟨a, Subtype.ext h⟩

Premises used: Exists, _private.0.Submodule.torsion'_isTorsion'.match_1, Exists.intro, HSMul.hSMul, OfNat.ofNat, Eq, Subtype.ext
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommMonoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass S R M
⊢ Eq.{u_2 + 1} (α := Submodule R ↥(torsion' R M S)) (torsion' R (↥(torsion' R M S)) S) ⊤

Tactic:
(isTorsion'_iff_torsion'_eq_top S).mp <| torsion'_isTorsion' S

Premises used: Submodule.isTorsion'_iff_torsion'_eq_top, Iff.mp, Submodule.torsion'_isTorsion'
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{u_2 + 1} (α := Submodule R ↥(torsion R M)) (torsion R ↥(torsion R M)) ⊤

Tactic:
torsion'_torsion'_eq_top R⁰

Premises used: Set.Mem, Membership.mem, nonZeroDivisors, Subtype, Submodule.torsion'_torsion'_eq_top
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ IsTorsion.{u_1, u_2} R ↥(torsion R M)

Tactic:
torsion'_isTorsion' R⁰

Premises used: Set.Mem, Membership.mem, nonZeroDivisors, Subtype, Submodule.torsion'_isTorsion'
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ IsTorsionBySet R M (↑(annihilator.{u_1, u_2} (M := M) ⊤) : Set R)

Tactic:
fun x ha =>
  mem_annihilator.mp ha.prop x mem_top

Premises used: Submodule.mem_annihilator, Subtype.prop, Iff.mp, Submodule.mem_top
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
obtain :
  ∀ (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
⊢ ((↑(annihilator.{u_1, u_2} (M := M) ⊤) : Set R) ∩ (↑R⁰ : Set R)).Nonempty

Tactic:
obtain ⟨S, hS⟩ := ‹Module.Finite R M›.fg_top

Premises used: Module.Finite.fg_top
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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

Tactic:
⟨_, ?_, (∏ x ∈ S, (@hM x).choose : R⁰).prop⟩

Premises used: Finset.prod, Set.Nonempty, Subtype.prop, And.intro, Exists.intro, Exists.choose
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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)) ⊤
refine :
  (↑(∏ x ∈ S, Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) ⋯) : R) ∈ (↑(annihilator.{u_1, u_2} (M := M) ⊤) : Set R)
⊢ ((↑(annihilator.{u_1, u_2} (M := M) ⊤) : Set R) ∩ (↑R⁰ : Set R)).Nonempty

Tactic:
refine ⟨_, ?_, (∏ x ∈ S, (@hM x).choose : R⁰).prop⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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)) ⊤
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) ⋯) : R)) (↑n : M) =
      0
⊢ (↑(∏ x ∈ S, Exists.choose (p := fun (a : ↥R⁰) ↦ a • x = 0) ⋯) : R) ∈ (↑(annihilator.{u_1, u_2} (M := M) ⊤) : Set R)

Tactic:
rw [Submonoid.coe_finsetProd, SetLike.mem_coe, ← hS, mem_annihilator_span]

Premises used: Submonoid.coe_finsetProd, Submodule.mem_annihilator_span, SetLike.mem_coe
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
rw₄ rw₅ : Eq.{u_2 + 1} (α := M) 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

Tactic:
rw [← Finset.prod_erase_mul _ _ n.prop, mul_smul, ← Submonoid.smul_def, (@hM n).choose_spec,
    smul_zero]

Premises used: Finset.prod_erase_mul, Exists.choose_spec, smul_zero, Submonoid.smul_def, Subtype.prop, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
h :
  ∀ (x : M),
    x ∈ (↑(torsion R M) : Set M) ↔
      Membership.mem (γ := Set M) {x : M | Ne (α := Ideal R) (annihilator (M := M) (R ∙ x)) ⊥} x
⊢ (↑(torsion R M) : Set M) = {x : M | Ne (α := Ideal R) (annihilator (M := M) (R ∙ x)) ⊥}

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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) ↔
    Membership.mem (γ := Set M) {x : M | ∃ (x_1 : R), (∀ (n : M), (∃ (a : R), a • x = n) → x_1 • n = 0) ∧ x_1 ≠ 0} x
⊢ x ∈ (↑(torsion R M) : Set M) ↔
    Membership.mem (γ := Set M) {x : M | Ne (α := Ideal R) (annihilator (M := M) (R ∙ x)) ⊥} x

Tactic:
simp_rw [Submodule.ne_bot_iff, mem_annihilator, mem_span_singleton]

Premises used: Submodule.mem_annihilator, Submodule.mem_span_singleton, Submodule.ne_bot_iff
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
rw₄ rw₅ : Eq.{u_2 + 1} (α := M) 0 0
⊢ (↑a : R) • x_1 = 0

Tactic:
rw [← hb, smul_comm, ← Submonoid.smul_def, hax, smul_zero]

Premises used: smul_zero, Submonoid.smul_def, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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 | ∃ (x_1 : R), (∀ (n : M), (∃ (a : R), a • x = n) → x_1 • n = 0) ∧ x_1 ≠ 0} x

Tactic:
exact
    ⟨fun ⟨a, hax⟩ =>
      ⟨a, fun _ ⟨b, hb⟩ => by rw [← hb, smul_comm, ← Submonoid.smul_def, hax, smul_zero],
        nonZeroDivisors.coe_ne_zero _⟩,
      fun ⟨a, hax, ha⟩ => ⟨⟨_, mem_nonZeroDivisors_of_ne_zero ha⟩, hax x ⟨1, one_smul _ _⟩⟩⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
G : Type u_3
inst : AddCommGroup G
h :
  ∀ (x : G),
    Membership.mem (γ := AddSubgroup G) (toAddSubgroup (module_M := AddCommGroup.toIntModule G) (torsion ℤ G)) x ↔
      Membership.mem (γ := AddSubgroup G) (AddCommGroup.torsion G) x
⊢ Eq (α := AddSubgroup G) (toAddSubgroup (module_M := AddCommGroup.toIntModule G) (torsion ℤ G))
    (AddCommGroup.torsion G)

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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

Tactic:
((isOfFinAddOrder_iff_zsmul_eq_zero (x := x)).trans ?_).symm

Premises used: Set.Mem, setOf, IsOfFinAddOrder, Function.periodicPts, Iff.trans, isOfFinAddOrder_iff_zsmul_eq_zero, Iff.symm
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
G : Type u_3
inst : AddCommGroup G
x : G
h :
  (∃ (n : ℤ), n ≠ 0 ∧ n • x = 0) ↔
    Membership.mem (γ := AddSubgroup G) (toAddSubgroup (module_M := AddCommGroup.toIntModule G) (torsion ℤ G)) x
⊢ Membership.mem (γ := AddSubgroup G) (toAddSubgroup (module_M := AddCommGroup.toIntModule G) (torsion ℤ G)) x ↔
    Membership.mem (γ := AddSubgroup G) (AddCommGroup.torsion G) x

Tactic:
refine ((isOfFinAddOrder_iff_zsmul_eq_zero (x := x)).trans ?_).symm

Premises used: Iff.trans, isOfFinAddOrder_iff_zsmul_eq_zero, Iff.symm
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
G : Type u_3
inst : AddCommGroup G
x : G
⊢ (∃ (n : ℤ), n ≠ 0 ∧ n • x = 0) ↔
    Membership.mem (γ := AddSubgroup G) (toAddSubgroup (module_M := AddCommGroup.toIntModule G) (torsion ℤ G)) x

Tactic:
simp [mem_nonZeroDivisors_iff_ne_zero]

Premises used: mem_nonZeroDivisors_iff_ne_zero
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
simp : (∀ (r : R) (m : M), r • m = 0 → r = 0 ∨ m = 0) ↔ ∀ (y : M) (x : R), ¬x = 0 → x • y = 0 → y = 0
⊢ IsTorsionFree R M ↔ Eq (α := Submodule R M) (torsion R M) ⊥

Tactic:
simp [torsion, torsion', subset_antisymm_iff, exists_ne, isTorsionFree_iff_smul_eq_zero]

Premises used: Submodule.torsion, Submodule.torsion', exists_ne, subset_antisymm_iff, Module.isTorsionFree_iff_smul_eq_zero
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
⊢ (∀ (r : R) (m : M), r • m = 0 → r = 0 ∨ m = 0) ↔ ∀ (y : M) (x : R), ¬x = 0 → x • y = 0 → y = 0

Tactic:
grind
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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 M) (torsion R M) (a • x)

Tactic:
rw [Quotient.mk''_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero] at hax

Premises used: Submodule.Quotient.mk_smul, Submodule.Quotient.mk''_eq_mk, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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)
rw : Membership.mem (γ := Submodule R M) (torsion R M) x
⊢ Membership.mem (γ := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (torsion R M))) ⊥ (Quotient.mk'' x)

Tactic:
rw [mem_bot, Quotient.mk''_eq_mk, Quotient.mk_eq_zero]

Premises used: Submodule.mem_bot, Submodule.Quotient.mk''_eq_mk, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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)
obtain : ∀ (b : ↥R⁰) (h : b • a • x = 0), Membership.mem (γ := Submodule R M) (torsion R M) x
⊢ Membership.mem (γ := Submodule R M) (torsion R M) x

Tactic:
obtain ⟨b, h⟩ := hax
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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_1 :
  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 b : ↥R⁰
h : b • a • x = 0
⊢ Membership.mem (γ := Submodule R M) (torsion R M) x

Tactic:
⟨b * a, (mul_smul _ _ _).trans h⟩

Premises used: HMul.hMul, Set.Mem, setOf, Exists.intro, SemigroupAction.mul_smul, Eq.trans
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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_1 :
  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 b : ↥R⁰
h : b • a • x = 0
⊢ Membership.mem (γ := Submodule R M) (torsion R M) x

Tactic:
exact ⟨b * a, (mul_smul _ _ _).trans h⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
⊢ IsTorsionFree.{u_1, u_2} R (HasQuotient.Quotient M (B := Submodule R M) (torsion R M))

Tactic:
isTorsionFree_iff_torsion_eq_bot.mpr torsion_eq_bot

Premises used: Iff.mpr, Submodule.isTorsionFree_iff_torsion_eq_bot, Submodule.QuotientTorsion.torsion_eq_bot
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
mpr : (∀ (x : M), ∃ (n : ℕ), p ^ n • x = 0) → IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p)
⊢ IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p) ↔ ∀ (x : M), ∃ (n : ℕ), p ^ n • x = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
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 ⋯) x =
        0),
    ∃ (n : ℕ), p ^ n • x = 0
⊢ ∃ (n : ℕ), p ^ n • x = 0

Tactic:
let ⟨⟨a, ⟨n, hn⟩⟩, hx⟩ := @h x
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
h₁ : p ^ n • x = 0
⊢ ∃ (n : ℕ), p ^ n • x = 0

Tactic:
use n
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
h₁ : a • x = 0
⊢ p ^ n • x = 0

Tactic:
rw [hn]
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
⊢ a • x = 0

Tactic:
apply hx
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
mpr : ∀ (n : ℕ) (hn : p ^ n • x = 0), ∃ (a : ↥(Submonoid.powers p)), a • x = 0
⊢ ∃ (a : ↥(Submonoid.powers p)), a • x = 0

Tactic:
let ⟨n, hn⟩ := h x
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
n : ℕ
hn : p ^ n • x = 0
⊢ ∃ (a : ↥(Submonoid.powers p)), a • x = 0

Tactic:
⟨⟨_, ⟨n, rfl⟩⟩, hn⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
n : ℕ
hn : p ^ n • x = 0
⊢ ∃ (a : ↥(Submonoid.powers p)), a • x = 0

Tactic:
exact ⟨⟨_, ⟨n, rfl⟩⟩, hn⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
p : R
hM : IsTorsion'.{u_2, u_1} M ↥(Submonoid.powers p)
x : M
inst_3 : (n : ℕ) → Decidable (p ^ n • x = 0)
⊢ p ^ pOrder hM x • x = 0

Tactic:
Nat.find_spec <| (isTorsion'_powers_iff p).mp hM x

Premises used: Submodule.isTorsion'_powers_iff, Iff.mp, Submodule.pOrder, Nat.find_spec
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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)
⊢ 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
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
h : IsTorsionBy R M (p ^ pOrder hM (s (oj.get hoj)))
⊢ ∃ (j : Fin d), IsTorsionBy R M (p ^ pOrder hM (s j))

Tactic:
use Option.get _ hoj

Premises used: Option.get
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
h : ∀ (y : Fin d), s y ∈ (↑(torsionBy R M (p ^ pOrder hM (s (oj.get hoj)))) : Set M)
⊢ IsTorsionBy R M (p ^ pOrder hM (s (oj.get hoj)))

Tactic:
rw [isTorsionBy_iff_torsionBy_eq_top, eq_top_iff, ← hs, Submodule.span_le,
    Set.range_subset_iff]

Premises used: eq_top_iff, Set.range_subset_iff, Module.isTorsionBy_iff_torsionBy_eq_top, Submodule.span_le
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
h : p ^ pOrder hM (s (oj.get hoj)) • s i = 0
⊢ s i ∈ (↑(torsionBy R M (p ^ pOrder hM (s (oj.get hoj)))) : Set M)

Tactic:
change (p ^ pOrder hM (s (Option.get oj hoj))) • s i = 0

Premises used: HPow.hPow, Option.get, Submodule.pOrder
-- Module: Mathlib.Algebra.Module.Torsion.Basic
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
⊢ 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)