awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
inst_3 : IsTorsionFree R M
hr : IsRegular r
⊢ Function.Injective (β := M) fun (x : M) ↦ r • x

Tactic:
hr.isSMulRegular

Premises used: IsRegular.isSMulRegular, IsSMulRegular
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
m₁ m₂ : M
inst_3 : IsTorsionFree R M
hr : IsRegular r
⊢ r • m₁ = r • m₂ ↔ m₁ = m₂

Tactic:
(hr.smul_right_injective _).eq_iff

Premises used: Function.Injective.eq_iff, IsRegular.smul_right_injective
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
m : M
inst_3 : IsTorsionFree R M
hr : IsRegular r
rw : r • m = 0 ↔ r • m = HSMul.hSMul (β := M) r 0
rw₁ rw₂ : r • m = 0 ↔ r • m = 0
⊢ r • m = 0 ↔ m = 0

Tactic:
rw [← hr.smul_right_inj (m₁ := m), smul_zero]

Premises used: smul_zero, IsRegular.smul_right_inj
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
m : M
inst_3 : IsTorsionFree R M
hr : IsRegular r
⊢ r • m ≠ 0 ↔ m ≠ 0

Tactic:
hr.smul_eq_zero_iff_right.ne

Premises used: IsRegular.smul_eq_zero_iff_right, Iff.ne
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : IsTorsionFree R M
inst_6 : Module S R
inst_7 : IsTorsionFree S R
inst_8 : IsScalarTower S R R
inst_9 : SMulCommClass S R R
inst_10 : IsScalarTower S R M
s : S
hs : IsRegular s
x y : M
hxy : Eq.{u_3 + 1} (α := M) ((fun (x : M) ↦ s • x) x) ((fun (x : M) ↦ s • x) y)
⊢ Eq.{u_3 + 1} (α := M) ((fun (x : M) ↦ HSMul.hSMul (β := R) s 1 • x) x)
    ((fun (x : M) ↦ HSMul.hSMul (β := R) s 1 • x) y)

Tactic:
simpa using hxy
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : IsTorsionFree R M
inst_6 : Module S R
inst_7 : IsTorsionFree S R
inst_8 : IsScalarTower S R R
inst_9 : SMulCommClass S R R
inst_10 : IsScalarTower S R M
s : S
hs : IsRegular s
x y : M
hxy : Eq.{u_3 + 1} (α := M) ((fun (x : M) ↦ s • x) x) ((fun (x : M) ↦ s • x) y)
refine : IsRegular (HSMul.hSMul (β := R) s 1)
⊢ x = y

Tactic:
refine (?_ : IsRegular (s • 1 : R)).isSMulRegular (by simpa using hxy)

Premises used: IsRegular.isSMulRegular
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : IsTorsionFree R M
inst_6 : Module S R
inst_7 : IsTorsionFree S R
inst_8 : IsScalarTower S R R
inst_9 : SMulCommClass S R R
inst_10 : IsScalarTower S R M
s : S
hs : IsRegular s
x_1 y_1 : M
hxy_1 : Eq.{u_3 + 1} (α := M) ((fun (x : M) ↦ s • x) x_1) ((fun (x : M) ↦ s • x) y_1)
x y : R
hxy :
  Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ HSMul.hSMul (β := R) s 1 * x) x)
    ((fun (x : R) ↦ HSMul.hSMul (β := R) s 1 * x) y)
⊢ Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ s • x) x) ((fun (x : R) ↦ s • x) y)

Tactic:
simpa using hxy
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : IsTorsionFree R M
inst_6 : Module S R
inst_7 : IsTorsionFree S R
inst_8 : IsScalarTower S R R
inst_9 : SMulCommClass S R R
inst_10 : IsScalarTower S R M
s : S
hs : IsRegular s
x_1 y_1 : M
hxy_1 : Eq.{u_3 + 1} (α := M) ((fun (x : M) ↦ s • x) x_1) ((fun (x : M) ↦ s • x) y_1)
x y : R
hxy :
  Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ x * HSMul.hSMul (β := R) s 1) x)
    ((fun (x : R) ↦ x * HSMul.hSMul (β := R) s 1) y)
⊢ Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ s • x) x) ((fun (x : R) ↦ s • x) y)

Tactic:
simpa using hxy
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : IsTorsionFree R M
inst_6 : Module S R
inst_7 : IsTorsionFree S R
inst_8 : IsScalarTower S R R
inst_9 : SMulCommClass S R R
inst_10 : IsScalarTower S R M
s : S
hs : IsRegular s
x y : M
hxy : Eq.{u_3 + 1} (α := M) ((fun (x : M) ↦ s • x) x) ((fun (x : M) ↦ s • x) y)
⊢ IsRegular (HSMul.hSMul (β := R) s 1)

Tactic:
exact ⟨fun x y hxy ↦ hs.isSMulRegular <| by simpa using hxy,
      fun x y hxy ↦ hs.isSMulRegular <| by simpa using hxy⟩
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
inst_3 : IsTorsionFree R M
inst_4 : IsCancelMulZero R
hr : r ≠ 0
⊢ IsSMulRegular M r

Tactic:
(IsRegular.of_ne_zero hr).isSMulRegular

Premises used: IsRegular.of_ne_zero, IsRegular.isSMulRegular
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
inst_3 : IsTorsionFree R M
inst_4 : IsCancelMulZero R
hr : r ≠ 0
⊢ Function.Injective (β := M) fun (x : M) ↦ r • x

Tactic:
(IsRegular.of_ne_zero hr).smul_right_injective _

Premises used: IsRegular.of_ne_zero, IsRegular.smul_right_injective
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
m₁ m₂ : M
inst_3 : IsTorsionFree R M
inst_4 : IsCancelMulZero R
hr : r ≠ 0
⊢ r • m₁ = r • m₂ ↔ m₁ = m₂

Tactic:
(IsRegular.of_ne_zero hr).smul_right_inj

Premises used: IsRegular.of_ne_zero, IsRegular.smul_right_inj
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
m : M
inst_3 : IsTorsionFree R M
inst_4 : IsCancelMulZero R
hr : r ≠ 0
⊢ r • m = 0 ↔ m = 0

Tactic:
(IsRegular.of_ne_zero hr).smul_eq_zero_iff_right

Premises used: IsRegular.of_ne_zero, IsRegular.smul_eq_zero_iff_right
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
m : M
inst_3 : IsTorsionFree R M
inst_4 : IsCancelMulZero R
hr : r ≠ 0
⊢ r • m ≠ 0 ↔ m ≠ 0

Tactic:
(smul_eq_zero_iff_right hr).ne

Premises used: smul_eq_zero_iff_right, Iff.ne
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
m : M
inst_3 : IsTorsionFree R M
inst_4 : IsCancelMulZero R
inl : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 m = 0 ↔ Eq.{u_1 + 1} (α := R) 0 0 ∨ m = 0
inr : ∀ (hr : r ≠ 0), r • m = 0 ↔ r = 0 ∨ m = 0
⊢ r • m = 0 ↔ r = 0 ∨ m = 0

Tactic:
obtain rfl | hr := eq_or_ne r 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
inst_3 : IsTorsionFree R M
inst_4 : IsCancelMulZero R
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 m = 0 ↔ Eq.{u_1 + 1} (α := R) 0 0 ∨ m = 0

Tactic:
simp [smul_eq_zero_iff_right, *]

Premises used: smul_eq_zero_iff_right
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
m : M
inst_3 : IsTorsionFree R M
inst_4 : IsCancelMulZero R
hr : r ≠ 0
⊢ r • m = 0 ↔ r = 0 ∨ m = 0

Tactic:
simp [smul_eq_zero_iff_right, *]

Premises used: smul_eq_zero_iff_right
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
m : M
inst_3 : IsTorsionFree R M
inst_4 : IsCancelMulZero R
⊢ r • m ≠ 0 ↔ r ≠ 0 ∧ m ≠ 0

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
m : M
inst_3 : IsTorsionFree R M
inst_4 : IsCancelMulZero R
hr : r ≠ 0
hm : m ≠ 0
⊢ r • m ≠ 0

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
m : M
inst_3 : IsTorsionFree R M
inst_4 : IsCancelMulZero R
hm : m ≠ 0
⊢ r • m = 0 ↔ r = 0

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
m : M
inst_3 : IsTorsionFree R M
inst_4 : IsCancelMulZero R
hm : m ≠ 0
⊢ r • m ≠ 0 ↔ r ≠ 0

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsTorsionFree R M
inst_4 : IsCancelMulZero R
inst_5 : CharZero R
n : ℕ
hn : n ≠ 0
simp_rw : Function.Injective (β := M) fun (a : M) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) a
⊢ Function.Injective (β := M) fun (a : M) ↦ n • a

Tactic:
simp_rw [← Nat.cast_smul_eq_nsmul R]

Premises used: Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsTorsionFree R M
inst_4 : IsCancelMulZero R
inst_5 : CharZero R
n : ℕ
hn : n ≠ 0
hr : Ne.{u_1 + 1} (α := R) (↑n : R) 0
⊢ Function.Injective (β := M) fun (a : M) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) a

Tactic:
apply smul_right_injective

Premises used: smul_right_injective
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsTorsionFree R M
inst_4 : IsCancelMulZero R
inst_5 : CharZero R
n : ℕ
hn : n ≠ 0
⊢ Ne.{u_1 + 1} (α := R) (↑n : R) 0

Tactic:
simpa
-- 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 : IsTorsionFree R M
inst_8 : IsCancelMulZero R
inst_9 : CharZero R
⊢ IsAddTorsionFree R

Tactic:
.of_isTorsionFree R R

Premises used: IsAddTorsionFree.of_isTorsionFree
-- 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 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
m : M
inst_6 : IsAddTorsionFree M
n : ℤ
hn : IsRegular n
⊢ n ≠ 0

Tactic:
simpa [isRegular_iff_ne_zero] using hn

Premises used: isRegular_iff_ne_zero
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
h : ∀ (r : R) (m : M), r • m = 0 → r = 0 ∨ m = 0
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₂)
⊢ r • (m₁ - m₂) = 0

Tactic:
simpa [smul_sub, sub_eq_zero] using hm

Premises used: sub_eq_zero, smul_sub
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
h : ∀ (r : R) (m : M), r • m = 0 → r = 0 ∨ m = 0
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₂)
⊢ m₁ = m₂

Tactic:
simpa [sub_eq_zero, hr.ne_zero] using h r (m₁ - m₂) (by simpa [smul_sub, sub_eq_zero] using hm)

Premises used: sub_eq_zero, HSub.hSub, IsRegular.ne_zero
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : M
inst_3 : IsCancelMulZero R
inst_4 : IsTorsionFree R M
hm : m ≠ 0
r₁ r₂ : R
hr : r₁ • m = r₂ • m
rwa : ∀ (hr : r₁ • m - r₂ • m = 0), r₁ = r₂
rwa₁ : ∀ (hr : (r₁ - r₂) • m = 0), r₁ = r₂
rwa₂ : ∀ (hr : r₁ - r₂ = 0), r₁ = r₂
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (hr : r₁ = r₂), r₁ = r₂
⊢ r₁ = r₂

Tactic:
rwa [← sub_eq_zero, ← sub_smul, smul_eq_zero_iff_left hm, sub_eq_zero] at hr

Premises used: sub_eq_zero, sub_smul, smul_eq_zero_iff_left
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : M
r₁ r₂ : R
inst_3 : IsCancelMulZero R
inst_4 : IsTorsionFree R M
hm : m ≠ 0
⊢ r₁ • m = r₂ • m ↔ r₁ = r₂

Tactic:
(smul_left_injective _ hm).eq_iff

Premises used: Function.Injective.eq_iff, smul_left_injective
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : IsAddTorsionFree M
⊢ CharZero R

Tactic:
⟨fun {n m h} ↦ ?_⟩

Premises used: CharZero.mk
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : IsAddTorsionFree M
refine : ∀ {n m : ℕ} {h : Eq.{u_1 + 1} (α := R) (↑n : R) (↑m : R)}, n = m
⊢ CharZero R

Tactic:
refine ⟨fun {n m h} ↦ ?_⟩
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : IsAddTorsionFree M
n m : ℕ
h : Eq.{u_1 + 1} (α := R) (↑n : R) (↑m : R)
obtain : ∀ (x : M) (hx : x ≠ 0), n = m
⊢ n = m

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : M)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : IsAddTorsionFree M
n m : ℕ
h : Eq.{u_1 + 1} (α := R) (↑n : R) (↑m : R)
x : M
hx : x ≠ 0
⊢ HSMul.hSMul (α := ℤ) (↑n : ℤ) x = HSMul.hSMul (α := ℤ) (↑m : ℤ) x

Tactic:
simp [← Nat.cast_smul_eq_nsmul R, h]

Premises used: Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : IsAddTorsionFree M
n m : ℕ
h : Eq.{u_1 + 1} (α := R) (↑n : R) (↑m : R)
x : M
hx : x ≠ 0
⊢ HSMul.hSMul (α := ℤ) (↑n : ℤ) x = HSMul.hSMul (α := ℤ) (↑m : ℤ) x

Tactic:
replace h : (n : ℤ) • x = (m : ℤ) • x := by simp [← Nat.cast_smul_eq_nsmul R, h]
-- Module: Mathlib.Algebra.Module.Torsion.Free
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : IsAddTorsionFree M
n m : ℕ
x : M
hx : x ≠ 0
h : HSMul.hSMul (α := ℤ) (↑n : ℤ) x = HSMul.hSMul (α := ℤ) (↑m : ℤ) x
⊢ n = m

Tactic:
simpa using smul_left_injective ℤ hx h

Premises used: smul_left_injective, Int
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M
inst_2 : Module A M
x : M
simp :
  Membership.mem (γ := Submodule A M) (⨆ (i : ℕ), torsionBySet A M (↑(I ^ i) : Set A)) x ↔
    ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0
⊢ Membership.mem (γ := Submodule A M) (primaryComponent M I) x ↔
    ∃ (n : ℕ), Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(I ^ n) : Set A)) x

Tactic:
simp only [primaryComponent, mem_torsionBySet_iff, SetLike.coe_sort_coe, Subtype.forall]

Premises used: SetLike.coe_sort_coe, Submodule.mem_torsionBySet_iff, Subtype.forall, Ideal.primaryComponent
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M
inst_2 : Module A M
x : M
mp :
  Membership.mem (γ := Submodule A M) (⨆ (i : ℕ), torsionBySet A M (↑(I ^ i) : Set A)) x →
    ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0
mpr :
  (∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0) →
    Membership.mem (γ := Submodule A M) (⨆ (i : ℕ), torsionBySet A M (↑(I ^ i) : Set A)) x
⊢ Membership.mem (γ := Submodule A M) (⨆ (i : ℕ), torsionBySet A M (↑(I ^ i) : Set A)) x ↔
    ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M
inst_2 : Module A M
x : M
a : Membership.mem (γ := Submodule A M) (⨆ (i : ℕ), torsionBySet A M (↑(I ^ i) : Set A)) x
mp :
  ∀ (a : ∃ (i : ℕ), Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(I ^ i) : Set A)) x),
    ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0
mp₁ : Directed (fun (x1 x2 : Submodule A M) ↦ x1 ≤ x2) fun (i : ℕ) ↦ torsionBySet A M (↑(I ^ i) : Set A)
⊢ ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0

Tactic:
rw [Submodule.mem_iSup_of_directed] at a

Premises used: Submodule.mem_iSup_of_directed
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M
inst_2 : Module A M
x : M
a : ∃ (i : ℕ), Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(I ^ i) : Set A)) x
⊢ ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0

Tactic:
simpa using a
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M
inst_2 : Module A M
x_1 : M
a : Membership.mem (γ := Submodule A M) (⨆ (i : ℕ), torsionBySet A M (↑(I ^ i) : Set A)) x_1
x y : ℕ
h :
  (fun (x1 x2 : Submodule A M) ↦ x1 ≤ x2) ((fun (i : ℕ) ↦ (torsionBySet A M (↑(I ^ i) : Set A) : Submodule A M)) x)
      ((fun (i : ℕ) ↦ (torsionBySet A M (↑(I ^ i) : Set A) : Submodule A M)) (max x y)) ∧
    (fun (x1 x2 : Submodule A M) ↦ x1 ≤ x2) ((fun (i : ℕ) ↦ (torsionBySet A M (↑(I ^ i) : Set A) : Submodule A M)) y)
      ((fun (i : ℕ) ↦ (torsionBySet A M (↑(I ^ i) : Set A) : Submodule A M)) (max x y))
⊢ ∃ (z : ℕ),
    (fun (x1 x2 : Submodule A M) ↦ x1 ≤ x2) ((fun (i : ℕ) ↦ (torsionBySet A M (↑(I ^ i) : Set A) : Submodule A M)) x)
        ((fun (i : ℕ) ↦ (torsionBySet A M (↑(I ^ i) : Set A) : Submodule A M)) z) ∧
      (fun (x1 x2 : Submodule A M) ↦ x1 ≤ x2) ((fun (i : ℕ) ↦ (torsionBySet A M (↑(I ^ i) : Set A) : Submodule A M)) y)
        ((fun (i : ℕ) ↦ (torsionBySet A M (↑(I ^ i) : Set A) : Submodule A M)) z)

Tactic:
use max x y

Premises used: Max.max
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M
inst_2 : Module A M
x_1 : M
a : Membership.mem (γ := Submodule A M) (⨆ (i : ℕ), torsionBySet A M (↑(I ^ i) : Set A)) x_1
x y : ℕ
⊢ (fun (x1 x2 : Submodule A M) ↦ x1 ≤ x2) ((fun (i : ℕ) ↦ (torsionBySet A M (↑(I ^ i) : Set A) : Submodule A M)) x)
      ((fun (i : ℕ) ↦ (torsionBySet A M (↑(I ^ i) : Set A) : Submodule A M)) (max x y)) ∧
    (fun (x1 x2 : Submodule A M) ↦ x1 ≤ x2) ((fun (i : ℕ) ↦ (torsionBySet A M (↑(I ^ i) : Set A) : Submodule A M)) y)
      ((fun (i : ℕ) ↦ (torsionBySet A M (↑(I ^ i) : Set A) : Submodule A M)) (max x y))

Tactic:
simp [torsionBySet_le_torsionBySet_pow]

Premises used: Submodule.torsionBySet_le_torsionBySet_pow
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M
inst_2 : Module A M
x : M
⊢ (∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0) →
    Membership.mem (γ := Submodule A M) (⨆ (i : ℕ), torsionBySet A M (↑(I ^ i) : Set A)) x

Tactic:
aesop (add safe Submodule.mem_iSup_of_mem)

Premises used: Submodule.mem_iSup_of_mem
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
φ : M₁ →ₗ[A] M₂
c : ↥(primaryComponent M₁ I)
obtain :
  ∀ (c : M₁) (hc : Membership.mem (γ := Submodule A M₁) (primaryComponent M₁ I) c),
    Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ I)
      ((φ : (a : M₁) → M₂)
          (↑(Subtype.mk (p := fun (x : M₁) ↦ Membership.mem (γ := Submodule A M₁) (primaryComponent M₁ I) x) c hc) :
            M₁) :
        M₂)
⊢ Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ I) ((φ : (a : M₁) → M₂) (↑c : M₁) : M₂)

Tactic:
obtain ⟨c, hc⟩ := c
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
φ : M₁ →ₗ[A] M₂
c : M₁
hc : Membership.mem (γ := Submodule A M₁) (primaryComponent M₁ I) c
simp :
  ∀ (hc : ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • c = 0),
    ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), Eq.{u_4 + 1} (α := M₂) ((φ : (a : M₁) → M₂) (a • c) : M₂) (0 : M₂)
⊢ Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ I)
    ((φ : (a : M₁) → M₂)
        (↑(Subtype.mk (p := fun (x : M₁) ↦ Membership.mem (γ := Submodule A M₁) (primaryComponent M₁ I) x) c hc) : M₁) :
      M₂)

Tactic:
simp only [primaryComponent_mem, mem_torsionBySet_iff, SetLike.coe_sort_coe, Subtype.forall,
    ← map_smul] at ⊢ hc

Premises used: SetLike.coe_sort_coe, Submodule.mem_torsionBySet_iff, Subtype.forall, Ideal.primaryComponent_mem, map_smul
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
φ : M₁ →ₗ[A] M₂
c : M₁
hc : ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • c = 0
obtain :
  ∀ (n : ℕ) (hn : ∀ (a : A) (b : a ∈ I ^ n), a • c = 0),
    ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), Eq.{u_4 + 1} (α := M₂) ((φ : (a : M₁) → M₂) (a • c) : M₂) (0 : M₂)
⊢ ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), Eq.{u_4 + 1} (α := M₂) ((φ : (a : M₁) → M₂) (a • c) : M₂) (0 : M₂)

Tactic:
obtain ⟨n, hn⟩ := hc
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
φ : M₁ →ₗ[A] M₂
c : M₁
n : ℕ
hn : ∀ (a : A) (b : a ∈ I ^ n), a • c = 0
h : ∀ (a : A) (b : a ∈ I ^ n), Eq.{u_4 + 1} (α := M₂) ((φ : (a : M₁) → M₂) (a • c) : M₂) (0 : M₂)
⊢ ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), Eq.{u_4 + 1} (α := M₂) ((φ : (a : M₁) → M₂) (a • c) : M₂) (0 : M₂)

Tactic:
use n
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
φ : M₁ →ₗ[A] M₂
c : M₁
n : ℕ
hn : ∀ (a : A) (b : a ∈ I ^ n), a • c = 0
⊢ ∀ (a : A) (b : a ∈ I ^ n), Eq.{u_4 + 1} (α := M₂) ((φ : (a : M₁) → M₂) (a • c) : M₂) (0 : M₂)

Tactic:
grind
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module A M
inst_5 : Module A M₁
inst_6 : Module A M₂
φ : M₁ →ₗ[A] M₂
c : ↥(primaryComponent M₁ I)
⊢ Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ I)
    ((φ.domRestrict (primaryComponent M₁ I) : (a : ↥(primaryComponent M₁ I)) → M₂) c : M₂)

Tactic:
simpa only [LinearMap.domRestrict_apply] using primaryComponent_map_mem I φ c

Premises used: Ideal.primaryComponent_map_mem, LinearMap.domRestrict_apply
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module A M₁
inst_4 : Module A M₂
φ : M₁ →ₗ[A] M₂
⊢ Submodule.map (Submodule.subtype (primaryComponent M₁ I)) (map I φ).ker =
    Submodule.map φ.ker.subtype (primaryComponent (↥φ.ker) I)

Tactic:
aesop (add norm [map, Subtype.ext_iff, primaryComponent_mem])

Premises used: Subtype.ext_iff, Ideal.primaryComponent_mem, Ideal.primaryComponent.map