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
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
h₃ : HSMul.hSMul (β := M) (p ^ (pOrder hM (s (oj.get hoj)) - pOrder hM (s i))) 0 = 0
h₄ h₅ : Eq.{u_2 + 1} (α := M) 0 0
⊢ p ^ pOrder hM (s (oj.get hoj)) • s i = 0

Tactic:
rw [← Nat.sub_add_cancel this, pow_add, mul_smul, pow_pOrder_smul, smul_zero]

Premises used: Submodule.pow_pOrder_smul, pow_add, smul_zero, Nat.sub_add_cancel, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
h :
  ∀ (x : HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)),
    Membership.mem (γ := Submodule R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)))
        (torsionBy R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a :
          Submodule R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)))
        x ↔
      Membership.mem (γ := Submodule R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)))
        (Submodule.span R
          (singleton (α := HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b))
            ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b))))
        x
⊢ Eq (α := Submodule R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)))
    (torsionBy R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a :
      Submodule R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)))
    (Submodule.span R
        (singleton (α := HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b))
          ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b))) :
      Submodule R (HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)))

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x : HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)
h :
  a • x = 0 ↔
    ∃ (a_1 : R),
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
          ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
        x
⊢ Membership.mem (γ := Submodule R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)))
      (torsionBy R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a :
        Submodule R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)))
      x ↔
    Membership.mem (γ := Submodule R (HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)))
      (Submodule.span R
        (singleton (α := HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b))
          ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b))))
      x

Tactic:
rw [mem_torsionBy_iff, Submodule.mem_span_singleton]

Premises used: Submodule.mem_span_singleton, Submodule.mem_torsionBy_iff
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x : HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)
h :
  ∀ (x : R),
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
          ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
        0 ↔
      ∃ (a_1 : R),
        HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
            ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
          (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x
⊢ a • x = 0 ↔
    ∃ (a_1 : R),
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
          ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
        x

Tactic:
obtain ⟨x, rfl⟩ := mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x : R
h :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      0 →
    ∃ (a_2 : R),
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_2
          ((mk (R ∙ a * b) : (a_3 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
        (mk (R ∙ a * b) : (a_3 : R) → R ⧸ R ∙ a * b) x
h₁ :
  (∃ (a_1 : R),
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
          ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
        (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x) →
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
        ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      0
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      0 ↔
    ∃ (a_1 : R),
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
          ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
        (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x : R
h :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
⊢ ∃ (a_1 : R), a_1 • (a * b) = a • x

Tactic:
rw [← mk_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero, Submodule.mem_span_singleton] at h

Premises used: Submodule.mem_span_singleton, Submodule.Quotient.mk_smul, Ideal.Quotient.mk_eq_mk, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x : R
h : ∃ (a_1 : R), a_1 • (a * b) = a • x
h₁ :
  ∀ (c : R) (h : c • (a * b) = a • x),
    ∃ (a_1 : R),
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
          ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
        (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x
⊢ ∃ (a_1 : R),
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
        ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x

Tactic:
obtain ⟨c, h⟩ := h
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x c : R
h : c • (a * b) = a • x
⊢ c * b = x

Tactic:
rw [smul_eq_mul, smul_eq_mul, mul_comm, mul_assoc, mul_cancel_left_mem_nonZeroDivisors ha,
      mul_comm] at h

Premises used: mul_cancel_left_mem_nonZeroDivisors, mul_assoc, mul_comm, smul_eq_mul
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x c : R
h : c * b = x
h₁ :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x
⊢ ∃ (a_1 : R),
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
        ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x

Tactic:
use c
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x c : R
h : c * b = x
h₁ :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b)
h₂ :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c (Submodule.Quotient.mk b) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b)
h₃ :
  Eq (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) (Submodule.Quotient.mk (c • b))
    ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b))
h₄ :
  Eq (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) (Submodule.Quotient.mk (c * b))
    ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b))
h₅ h₆ :
  Eq (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b))
    ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b) : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b))
    ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) (c * b) : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b))
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x

Tactic:
rw [← h, ← mk_eq_mk, ← Quotient.mk_smul, smul_eq_mul, mk_eq_mk]

Premises used: Submodule.Quotient.mk_smul, Ideal.Quotient.mk_eq_mk, smul_eq_mul
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x : R
h :
  ∃ (a_1 : R),
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a_1
        ((mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      (mk (R ∙ a * b) : (a_2 : R) → R ⧸ R ∙ a * b) x
h₁ :
  ∀ (c : R)
    (h :
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
          ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
        (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x),
    HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
      0
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0

Tactic:
obtain ⟨c, h⟩ := h
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type w
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
x c : R
h :
  HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    (mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x
h₁ :
  a •
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
h₂ :
  c •
      HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
        ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) b : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0
h₃ : c • HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a (Submodule.Quotient.mk b) = 0
h₄ : HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c (Submodule.Quotient.mk (a • b)) = 0
h₅ : HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) c 0 = 0
h₆ h₇ : Eq.{w + 1} (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) 0 0
⊢ HSMul.hSMul (β := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) a
      ((mk (R ∙ a * b) : (a_1 : R) → R ⧸ R ∙ a * b) x : HasQuotient.Quotient R (B := Ideal R) (R ∙ a * b)) =
    0

Tactic:
rw [← h, smul_comm, ← mk_eq_mk, ← Quotient.mk_smul,
      (Quotient.mk_eq_zero _).mpr <| mem_span_singleton_self _, smul_zero]

Premises used: Iff.mpr, smul_zero, Submodule.Quotient.mk_smul, Ideal.Quotient.mk_eq_mk, SMulCommClass.smul_comm, Ideal.mem_span_singleton_self, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommMonoid M
⊢ IsTorsion M ↔ Module.IsTorsion ℕ M

Tactic:
⟨fun h x => ?_, fun h x => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommMonoid M
refine_1 : ∀ (h : IsTorsion M) (x : M), ∃ (a : ↥ℕ⁰), a • x = 0
refine_2 : ∀ (h : Module.IsTorsion ℕ M) (x : M), IsOfFinAddOrder x
⊢ IsTorsion M ↔ Module.IsTorsion ℕ M

Tactic:
refine ⟨fun h x => ?_, fun h x => ?_⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommMonoid M
h : IsTorsion M
x : M
refine_1 : ∀ (n : ℕ) (h0 : 0 < n) (hn : n • x = 0), ∃ (a : ↥ℕ⁰), a • x = 0
⊢ ∃ (a : ↥ℕ⁰), a • x = 0

Tactic:
obtain ⟨n, h0, hn⟩ := (h x).exists_nsmul_eq_zero

Premises used: IsOfFinAddOrder.exists_nsmul_eq_zero
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommMonoid M
h : IsTorsion M
x : M
n : ℕ
h0 : 0 < n
hn : n • x = 0
⊢ ∃ (a : ↥ℕ⁰), a • x = 0

Tactic:
⟨⟨n, mem_nonZeroDivisors_of_ne_zero <| ne_of_gt h0⟩, hn⟩

Premises used: ne_of_gt, Subtype.mk, Exists.intro, mem_nonZeroDivisors_of_ne_zero
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommMonoid M
h : IsTorsion M
x : M
n : ℕ
h0 : 0 < n
hn : n • x = 0
⊢ ∃ (a : ↥ℕ⁰), a • x = 0

Tactic:
exact ⟨⟨n, mem_nonZeroDivisors_of_ne_zero <| ne_of_gt h0⟩, hn⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommMonoid M
h : Module.IsTorsion ℕ M
x : M
refine_2 : ∃ (n : ℕ), 0 < n ∧ n • x = 0
⊢ IsOfFinAddOrder x

Tactic:
rw [isOfFinAddOrder_iff_nsmul_eq_zero]

Premises used: isOfFinAddOrder_iff_nsmul_eq_zero
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommMonoid M
h : Module.IsTorsion ℕ M
x : M
refine_2 : ∀ (n : ↥ℕ⁰) (hn : n • x = 0), ∃ (n : ℕ), 0 < n ∧ n • x = 0
⊢ ∃ (n : ℕ), 0 < n ∧ n • x = 0

Tactic:
obtain ⟨n, hn⟩ := @h x
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommMonoid M
h : Module.IsTorsion ℕ M
x : M
n : ↥ℕ⁰
hn : n • x = 0
⊢ ∃ (n : ℕ), 0 < n ∧ n • x = 0

Tactic:
⟨n, Nat.pos_of_ne_zero (nonZeroDivisors.coe_ne_zero _), hn⟩

Premises used: Nat.pos_of_ne_zero, And.intro, nonZeroDivisors.coe_ne_zero, Exists.intro, Subtype.val
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommMonoid M
h : Module.IsTorsion ℕ M
x : M
n : ↥ℕ⁰
hn : n • x = 0
⊢ ∃ (n : ℕ), 0 < n ∧ n • x = 0

Tactic:
exact ⟨n, Nat.pos_of_ne_zero (nonZeroDivisors.coe_ne_zero _), hn⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommGroup M
⊢ IsTorsion M ↔ Module.IsTorsion ℤ M

Tactic:
⟨fun h x => ?_, fun h x => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommGroup M
refine_1 : ∀ (h : IsTorsion M) (x : M), ∃ (a : ↥ℤ⁰), a • x = 0
refine_2 : ∀ (h : Module.IsTorsion ℤ M) (x : M), IsOfFinAddOrder x
⊢ IsTorsion M ↔ Module.IsTorsion ℤ M

Tactic:
refine ⟨fun h x => ?_, fun h x => ?_⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommGroup M
h : IsTorsion M
x : M
refine_1 : ∀ (n : ℕ) (h0 : 0 < n) (hn : n • x = 0), ∃ (a : ↥ℤ⁰), a • x = 0
⊢ ∃ (a : ↥ℤ⁰), a • x = 0

Tactic:
obtain ⟨n, h0, hn⟩ := (h x).exists_nsmul_eq_zero

Premises used: IsOfFinAddOrder.exists_nsmul_eq_zero
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommGroup M
h : IsTorsion M
x : M
n : ℕ
h0 : 0 < n
hn : n • x = 0
⊢ ∃ (a : ↥ℤ⁰), a • x = 0

Tactic:
⟨⟨n, mem_nonZeroDivisors_of_ne_zero <| ne_of_gt <| Int.natCast_pos.mpr h0⟩,
        (natCast_zsmul _ _).trans hn⟩

Premises used: Iff.mpr, ne_of_gt, Nat.cast, Subtype.mk, Exists.intro, mem_nonZeroDivisors_of_ne_zero, Int.natCast_pos, natCast_zsmul, Eq.trans
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommGroup M
h : IsTorsion M
x : M
n : ℕ
h0 : 0 < n
hn : n • x = 0
⊢ ∃ (a : ↥ℤ⁰), a • x = 0

Tactic:
exact
      ⟨⟨n, mem_nonZeroDivisors_of_ne_zero <| ne_of_gt <| Int.natCast_pos.mpr h0⟩,
        (natCast_zsmul _ _).trans hn⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommGroup M
h : Module.IsTorsion ℤ M
x : M
refine_2 : ∃ (n : ℕ), 0 < n ∧ n • x = 0
⊢ IsOfFinAddOrder x

Tactic:
rw [isOfFinAddOrder_iff_nsmul_eq_zero]

Premises used: isOfFinAddOrder_iff_nsmul_eq_zero
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommGroup M
h : Module.IsTorsion ℤ M
x : M
refine_2 : ∀ (n : ↥ℤ⁰) (hn : n • x = 0), ∃ (n : ℕ), 0 < n ∧ n • x = 0
⊢ ∃ (n : ℕ), 0 < n ∧ n • x = 0

Tactic:
obtain ⟨n, hn⟩ := @h x
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommGroup M
h : Module.IsTorsion ℤ M
x : M
n : ↥ℤ⁰
hn : n • x = 0
⊢ ∃ (n : ℕ), 0 < n ∧ n • x = 0

Tactic:
⟨_, Int.natAbs_pos.2 (nonZeroDivisors.coe_ne_zero n), natAbs_nsmul_eq_zero.2 hn⟩

Premises used: Iff.mpr, natAbs_nsmul_eq_zero, Int.natAbs_pos, And.intro, nonZeroDivisors.coe_ne_zero, Exists.intro
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommGroup M
h : Module.IsTorsion ℤ M
x : M
n : ↥ℤ⁰
hn : n • x = 0
⊢ ∃ (n : ℕ), 0 < n ∧ n • x = 0

Tactic:
exact ⟨_, Int.natAbs_pos.2 (nonZeroDivisors.coe_ne_zero n), natAbs_nsmul_eq_zero.2 hn⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
A : Type u_3
inst : AddCommGroup A
n : ℤ
h : ∀ (a : A), Membership.mem (γ := AddSubgroup A) A[-n] a ↔ Membership.mem (γ := AddSubgroup A) A[n] a
⊢ Eq (α := AddSubgroup A) A[-n] A[n]

Tactic:
ext a
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
A : Type u_3
inst : AddCommGroup A
n : ℤ
a : A
⊢ Membership.mem (γ := AddSubgroup A) A[-n] a ↔ Membership.mem (γ := AddSubgroup A) A[n] a

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
A : Type u_3
inst : AddCommGroup A
n : ℕ
x : ↥A[(↑n : ℤ)]
⊢ n • x = 0

Tactic:
Nat.cast_smul_eq_nsmul ℤ n x ▸ Submodule.smul_torsionBy ..

Premises used: Eq.rec, Int, Nat.cast_smul_eq_nsmul, Submodule.smul_torsionBy
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
A : Type u_3
inst : AddCommGroup A
n : ℕ
x : A
⊢ Membership.mem (γ := AddSubgroup A) A[(↑n : ℤ)] x ↔ n • x = 0

Tactic:
Nat.cast_smul_eq_nsmul ℤ n x ▸ Submodule.mem_torsionBy_iff ..

Premises used: Eq.rec, Int, Submodule.mem_torsionBy_iff, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
A : Type u_3
inst : AddCommGroup A
n s : ℕ
x : ↥A[(↑n : ℤ)]
⊢ s • x = (s % n) • x

Tactic:
nsmul_eq_mod_nsmul s (torsionBy.nsmul x)

Premises used: nsmul_eq_mod_nsmul, AddSubgroup.torsionBy.nsmul
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
A : Type u_3
inst : AddCommGroup A
n s : ℕ
x : A
h : Membership.mem (γ := AddSubgroup A) A[(↑n : ℤ)] x
⊢ s • x = (s % n) • x

Tactic:
nsmul_eq_mod_nsmul s (torsionBy.nsmul_iff.mp h)

Premises used: nsmul_eq_mod_nsmul, AddSubgroup.torsionBy.nsmul_iff, Iff.mp
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : Infinite R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
h : Set.Infinite.{u_2} (α := M) (Set.range fun (r : R) ↦ x + r • y)
hy : y = 0
⊢ False

Tactic:
simp [hy] at h
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : Infinite R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
refine : ∀ (h : y ≠ 0) (r s : R) (hrs : x + r • y = x + s • y), r = s
⊢ Set.Infinite.{u_2} (α := M) (Set.range fun (r : R) ↦ x + r • y) ↔ y ≠ 0

Tactic:
refine ⟨fun h hy ↦ by simp [hy] at h, fun h ↦ Set.infinite_range_of_injective fun r s hrs ↦ ?_⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : Infinite R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
h : y ≠ 0
r s : R
hrs : x + r • y = x + s • y
⊢ r • y = s • y

Tactic:
rw [add_right_inj] at hrs

Premises used: add_right_inj
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : Infinite R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
h : y ≠ 0
r s : R
hrs : r • y = s • y
⊢ r = s

Tactic:
smul_left_injective _ h hrs

Premises used: smul_left_injective
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : Infinite R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
x y : M
h : y ≠ 0
r s : R
hrs : r • y = s • y
⊢ r = s

Tactic:
exact smul_left_injective _ h hrs

Premises used: smul_left_injective
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : IsAddTorsionFree M
x y : M
h : Set.Infinite.{u_2} (α := M) (Set.range fun (n : ℕ) ↦ x + n • y)
hy : y = 0
⊢ False

Tactic:
simp [hy] at h
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : IsAddTorsionFree M
x y : M
refine : ∀ (h : y ≠ 0) (r s : ℕ) (hrs : x + r • y = x + s • y), r = s
⊢ Set.Infinite.{u_2} (α := M) (Set.range fun (n : ℕ) ↦ x + n • y) ↔ y ≠ 0

Tactic:
refine ⟨fun h hy ↦ by simp [hy] at h, fun h ↦ Set.infinite_range_of_injective fun r s hrs ↦ ?_⟩
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : IsAddTorsionFree M
x y : M
h : y ≠ 0
r s : ℕ
hrs : x + r • y = x + s • y
⊢ HSMul.hSMul (α := ℤ) (↑r : ℤ) y = HSMul.hSMul (α := ℤ) (↑s : ℤ) y

Tactic:
rw [add_right_inj, ← natCast_zsmul, ← natCast_zsmul] at hrs

Premises used: add_right_inj, natCast_zsmul
-- Module: Mathlib.Algebra.Module.Torsion.Basic
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : IsAddTorsionFree M
x y : M
h : y ≠ 0
r s : ℕ
hrs : HSMul.hSMul (α := ℤ) (↑r : ℤ) y = HSMul.hSMul (α := ℤ) (↑s : ℤ) y
⊢ r = s

Tactic:
simpa using smul_left_injective _ h hrs

Premises used: smul_left_injective
-- Module: Mathlib.Algebra.Module.Torsion.Field
Goal:
𝕜 : Type u_1
M : Type u_2
inst : DivisionSemiring 𝕜
inst_1 : AddCommMonoid M
inst_2 : Module 𝕜 M
r : 𝕜
hr : IsRegular r
m₁ m₂ : M
hm : Eq.{u_2 + 1} (α := M) ((fun (x : M) ↦ r • x) m₁) ((fun (x : M) ↦ r • x) m₂)
⊢ m₁ = m₂

Tactic:
simpa [hr.ne_zero] using congr(r⁻¹ • $hm)

Premises used: IsRegular.ne_zero
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : IsTorsionFree R N
f : M → N
hf : Injective f
smul : ∀ (r : R) (m : M), f (r • m) = r • f m
r : R
hr : IsRegular r
m₁ m₂ : M
hm : Eq.{u_3 + 1} (α := M) ((fun (x : M) ↦ r • x) m₁) ((fun (x : M) ↦ r • x) m₂)
⊢ Eq.{u_4 + 1} (α := N) ((fun (x : N) ↦ r • x) (f m₁)) ((fun (x : N) ↦ r • x) (f m₂))

Tactic:
simpa [smul] using congr(f $hm)
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : AddCommMonoid N
inst_6 : Module R N
r : R
m m₁ m₂ : M
inst_7 : IsAddTorsionFree M
n : ℕ
hn : IsRegular n
⊢ n ≠ 0

Tactic:
simpa [isRegular_iff_ne_zero] using hn

Premises used: isRegular_iff_ne_zero