awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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
⊢ 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
have h₆ : Eq.{w + 1} (α := HasQuotient.Quotient R (B := Submodule R R) (R ∙ a * b)) 0 0
Tactic: rw [← h, smul_comm, ← mk_eq_mk, ← Quotient.mk_smul,
      (Quotient.mk_eq_zero _).mpr <| mem_span_singleton_self _, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
M : Type u_2
inst : AddCommMonoid M
⊢ IsTorsion M ↔ Module.IsTorsion ℕ M
have refine_1 : ∀ (h : IsTorsion M) (x : M), ∃ (a : ↥ℕ⁰), a • x = 0
Tactic: refine ⟨fun h x => ?_, fun h x => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
M : Type u_2
inst : AddCommMonoid M
refine_1 : ∀ (h : IsTorsion M) (x : M), ∃ (a : ↥ℕ⁰), a • x = 0
⊢ IsTorsion M ↔ Module.IsTorsion ℕ M
have refine_2 : ∀ (h : Module.IsTorsion ℕ M) (x : M), IsOfFinAddOrder x
Tactic: refine ⟨fun h x => ?_, fun h x => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
M : Type u_2
inst : AddCommMonoid M
h : IsTorsion M
x : M
⊢ ∃ (a : ↥ℕ⁰), a • x = 0
have refine_1 : ∀ (n : ℕ) (h0 : 0 < n) (hn : n • x = 0), ∃ (a : ↥ℕ⁰), a • x = 0
Tactic: obtain ⟨n, h0, hn⟩ := (h x).exists_nsmul_eq_zero
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
M : Type u_2
inst : AddCommMonoid M
h : Module.IsTorsion ℕ M
x : M
⊢ IsOfFinAddOrder x
have refine_2 : ∃ (n : ℕ), 0 < n ∧ n • x = 0
Tactic: rw [isOfFinAddOrder_iff_nsmul_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
M : Type u_2
inst : AddCommMonoid M
h : Module.IsTorsion ℕ M
x : M
⊢ ∃ (n : ℕ), 0 < n ∧ n • x = 0
have refine_2 : ∀ (n : ↥ℕ⁰) (hn : n • x = 0), ∃ (n : ℕ), 0 < n ∧ n • x = 0
Tactic: obtain ⟨n, hn⟩ := @h x
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
⊢ IsTorsion M ↔ Module.IsTorsion ℤ M
have refine_1 : ∀ (h : IsTorsion M) (x : M), ∃ (a : ↥ℤ⁰), a • x = 0
Tactic: refine ⟨fun h x => ?_, fun h x => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
refine_1 : ∀ (h : IsTorsion M) (x : M), ∃ (a : ↥ℤ⁰), a • x = 0
⊢ IsTorsion M ↔ Module.IsTorsion ℤ M
have refine_2 : ∀ (h : Module.IsTorsion ℤ M) (x : M), IsOfFinAddOrder x
Tactic: refine ⟨fun h x => ?_, fun h x => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
h : IsTorsion M
x : M
⊢ ∃ (a : ↥ℤ⁰), a • x = 0
have refine_1 : ∀ (n : ℕ) (h0 : 0 < n) (hn : n • x = 0), ∃ (a : ↥ℤ⁰), a • x = 0
Tactic: obtain ⟨n, h0, hn⟩ := (h x).exists_nsmul_eq_zero
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
h : Module.IsTorsion ℤ M
x : M
⊢ IsOfFinAddOrder x
have refine_2 : ∃ (n : ℕ), 0 < n ∧ n • x = 0
Tactic: rw [isOfFinAddOrder_iff_nsmul_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
h : Module.IsTorsion ℤ M
x : M
⊢ ∃ (n : ℕ), 0 < n ∧ n • x = 0
have refine_2 : ∀ (n : ↥ℤ⁰) (hn : n • x = 0), ∃ (n : ℕ), 0 < n ∧ n • x = 0
Tactic: obtain ⟨n, hn⟩ := @h x
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
A : Type u_3
inst : AddCommGroup A
n : ℤ
⊢ Eq (α := AddSubgroup A) A[-n] A[n]
have h : ∀ (a : A), Membership.mem (γ := AddSubgroup A) A[-n] a ↔ Membership.mem (γ := AddSubgroup A) A[n] a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
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
⊢ Set.Infinite.{u_2} (α := M) (Set.range fun (r : R) ↦ x + r • y) ↔ y ≠ 0
have refine : ∀ (h : y ≠ 0) (r s : R) (hrs : x + r • y = x + s • y), r = s
Tactic: refine ⟨fun h hy ↦ by simp [hy] at h, fun h ↦ Set.infinite_range_of_injective fun r s hrs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (hypothesis)
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 = s
have hrs₁ : r • y = s • y
Tactic: rw [add_right_inj] at hrs
Cleared hypotheses: hrs
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : IsAddTorsionFree M
x y : M
⊢ Set.Infinite.{u_2} (α := M) (Set.range fun (n : ℕ) ↦ x + n • y) ↔ y ≠ 0
have refine : ∀ (h : y ≠ 0) (r s : ℕ) (hrs : x + r • y = x + s • y), r = s
Tactic: refine ⟨fun h hy ↦ by simp [hy] at h, fun h ↦ Set.infinite_range_of_injective fun r s hrs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Basic (hypothesis)
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
⊢ r = s
have hrs₁ : HSMul.hSMul (α := ℤ) (↑r : ℤ) y = HSMul.hSMul (α := ℤ) (↑s : ℤ) y
Tactic: rw [add_right_inj, ← natCast_zsmul, ← natCast_zsmul] at hrs
Cleared hypotheses: hrs
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Free (goal)
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
have rw : r • m = 0 ↔ r • m = HSMul.hSMul (β := M) r 0
Tactic: rw [← hr.smul_right_inj (m₁ := m), smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Free (goal)
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
⊢ r • m = 0 ↔ m = 0
have rw₁ : r • m = 0 ↔ r • m = 0
Tactic: rw [← hr.smul_right_inj (m₁ := m), smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Free (goal)
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)
⊢ x = y
have refine : IsRegular (HSMul.hSMul (β := R) s 1)
Tactic: refine (?_ : IsRegular (s • 1 : R)).isSMulRegular (by simpa using hxy)
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Free (goal)
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
have inl : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 m = 0 ↔ Eq.{u_1 + 1} (α := R) 0 0 ∨ m = 0
Tactic: obtain rfl | hr := eq_or_ne r 0
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Free (goal)
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
⊢ r • m = 0 ↔ r = 0 ∨ m = 0
have inr : ∀ (hr : r ≠ 0), r • m = 0 ↔ r = 0 ∨ m = 0
Tactic: obtain rfl | hr := eq_or_ne r 0
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Free (goal)
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
⊢ Function.Injective (β := M) fun (a : M) ↦ n • a
have simp_rw : Function.Injective (β := M) fun (a : M) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) a
Tactic: simp_rw [← Nat.cast_smul_eq_nsmul R]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Free (goal)
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
⊢ Function.Injective (β := M) fun (a : M) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) a
have hr : Ne.{u_1 + 1} (α := R) (↑n : R) 0
Tactic: apply smul_right_injective
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Free (goal)
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
⊢ r₁ = r₂
have rwa : ∀ (hr : r₁ • m - r₂ • m = 0), r₁ = r₂
Tactic: rwa [← sub_eq_zero, ← sub_smul, smul_eq_zero_iff_left hm, sub_eq_zero] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Free (goal)
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₂
⊢ r₁ = r₂
have rwa₁ : ∀ (hr : (r₁ - r₂) • m = 0), r₁ = r₂
Tactic: rwa [← sub_eq_zero, ← sub_smul, smul_eq_zero_iff_left hm, sub_eq_zero] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Free (goal)
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₂
⊢ r₁ = r₂
have rwa₂ : ∀ (hr : r₁ - r₂ = 0), r₁ = r₂
Tactic: rwa [← sub_eq_zero, ← sub_smul, smul_eq_zero_iff_left hm, sub_eq_zero] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Free (goal)
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₂
⊢ r₁ = r₂
have rwa₃ : ∀ (hr : r₁ = r₂), r₁ = r₂
Tactic: rwa [← sub_eq_zero, ← sub_smul, smul_eq_zero_iff_left hm, sub_eq_zero] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Free (goal)
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
have refine : ∀ {n m : ℕ} {h : Eq.{u_1 + 1} (α := R) (↑n : R) (↑m : R)}, n = m
Tactic: refine ⟨fun {n m h} ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Free (goal)
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)
⊢ n = m
have obtain : ∀ (x : M) (hx : x ≠ 0), n = m
Tactic: obtain ⟨x, hx⟩ := exists_ne (0 : M)
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.Free (hypothesis)
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
⊢ n = m
have h₁ : HSMul.hSMul (α := ℤ) (↑n : ℤ) x = HSMul.hSMul (α := ℤ) (↑m : ℤ) x
Tactic: replace h : (n : ℤ) • x = (m : ℤ) • x := by simp [← Nat.cast_smul_eq_nsmul R, h]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
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
⊢ Membership.mem (γ := Submodule A M) (primaryComponent M I) x ↔
    ∃ (n : ℕ), Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(I ^ n) : Set A)) x
have 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
Tactic: simp only [primaryComponent, mem_torsionBySet_iff, SetLike.coe_sort_coe, Subtype.forall]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
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
⊢ Membership.mem (γ := Submodule A M) (⨆ (i : ℕ), torsionBySet A M (↑(I ^ i) : Set A)) x ↔
    ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
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
⊢ Membership.mem (γ := Submodule A M) (⨆ (i : ℕ), torsionBySet A M (↑(I ^ i) : Set A)) x ↔
    ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
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
⊢ ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0
have 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
Tactic: rw [Submodule.mem_iSup_of_directed] at a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
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
⊢ ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0
have mp₁ : Directed (fun (x1 x2 : Submodule A M) ↦ x1 ≤ x2) fun (i : ℕ) ↦ torsionBySet A M (↑(I ^ i) : Set A)
Tactic: rw [Submodule.mem_iSup_of_directed] at a
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
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 : ℕ
⊢ ∃ (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)
have 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))
Tactic: use max x y
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
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)
⊢ Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ I) ((φ : (a : M₁) → M₂) (↑c : M₁) : M₂)
have 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₂)
Tactic: obtain ⟨c, hc⟩ := c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
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
⊢ 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₂)
have 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₂)
Tactic: simp only [primaryComponent_mem, mem_torsionBySet_iff, SetLike.coe_sort_coe, Subtype.forall,
    ← map_smul] at ⊢ hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
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
⊢ ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), Eq.{u_4 + 1} (α := M₂) ((φ : (a : M₁) → M₂) (a • c) : M₂) (0 : M₂)
have 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₂)
Tactic: obtain ⟨n, hn⟩ := hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
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
⊢ ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), Eq.{u_4 + 1} (α := M₂) ((φ : (a : M₁) → M₂) (a • c) : M₂) (0 : M₂)
have h : ∀ (a : A) (b : a ∈ I ^ n), Eq.{u_4 + 1} (α := M₂) ((φ : (a : M₁) → M₂) (a • c) : M₂) (0 : M₂)
Tactic: use n
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
inst_1 : AddCommMonoid M
inst_2 : Module A M
I : Ideal A
⊢ Eq (α := Submodule A M)
    (Submodule.map (M := ↥(torsionBySet A M (↑I : Set A))) (Submodule.subtype (torsionBySet A M (↑I : Set A)))
      (primaryComponent (↥(torsionBySet A M (↑I : Set A))) I))
    (primaryComponent M I ⊓ torsionBySet A M (↑I : Set A))
have h : ∀ (x : M),
  Membership.mem (γ := Submodule A M)
      (Submodule.map (M := ↥(torsionBySet A M (↑I : Set A))) (Submodule.subtype (torsionBySet A M (↑I : Set A)))
        (primaryComponent (↥(torsionBySet A M (↑I : Set A))) I))
      x ↔
    Membership.mem (γ := Submodule A M) (primaryComponent M I ⊓ torsionBySet A M (↑I : Set A)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (hypothesis)
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M
inst_2 : Module A M
J : Ideal A
hD : IsCoprime I J
⊢ Eq.{u_2 + 1} (α := Submodule A ↥(torsionBySet A M (↑J : Set A)))
    (primaryComponent (↥(torsionBySet A M (↑J : Set A))) I) ⊥
have this : ∀ (n : ℕ), Disjoint (α := Submodule A M) (torsionBySet A M (↑(I ^ n) : Set A)) (torsionBySet A M (↑J : Set A))
Tactic: have (n : ℕ) : Disjoint (torsionBySet A M ↑(I ^ n)) (torsionBySet A M ↑J) :=
    Submodule.disjoint_torsionBySet_ideal (M := M) (Ideal.pow_sup_eq_top hD.sup_eq)
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M
inst_2 : Module A M
J : Ideal A
hD : IsCoprime I J
this : ∀ (n : ℕ), Disjoint (α := Submodule A M) (torsionBySet A M (↑(I ^ n) : Set A)) (torsionBySet A M (↑J : Set A))
⊢ Eq.{u_2 + 1} (α := Submodule A ↥(torsionBySet A M (↑J : Set A)))
    (primaryComponent (↥(torsionBySet A M (↑J : Set A))) I) ⊥
have a : Eq (α := Submodule A M)
  (Submodule.map (M := ↥(torsionBySet A M (↑J : Set A))) (Submodule.subtype (torsionBySet A M (↑J : Set A)))
    (primaryComponent (↥(torsionBySet A M (↑J : Set A))) I))
  (Submodule.map (M := ↥(torsionBySet A M (↑J : Set A))) (Submodule.subtype (torsionBySet A M (↑J : Set A))) ⊥)
Tactic: apply Submodule.map_injective_of_injective (Submodule.subtype_injective (torsionBySet A M ↑J))
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M
inst_2 : Module A M
J : Ideal A
hD : IsCoprime I J
this : ∀ (n : ℕ), Disjoint (α := Submodule A M) (torsionBySet A M (↑(I ^ n) : Set A)) (torsionBySet A M (↑J : Set A))
⊢ Eq (α := Submodule A M)
    (Submodule.map (M := ↥(torsionBySet A M (↑J : Set A))) (Submodule.subtype (torsionBySet A M (↑J : Set A)))
      (primaryComponent (↥(torsionBySet A M (↑J : Set A))) I))
    (Submodule.map (M := ↥(torsionBySet A M (↑J : Set A))) (Submodule.subtype (torsionBySet A M (↑J : Set A))) ⊥)
have a : ∀ (x : M),
  Membership.mem (γ := Submodule A M)
      (Submodule.map (M := ↥(torsionBySet A M (↑J : Set A))) (Submodule.subtype (torsionBySet A M (↑J : Set A)))
        (primaryComponent (↥(torsionBySet A M (↑J : Set A))) I))
      x ↔
    Membership.mem (γ := Submodule A M)
      (Submodule.map (M := ↥(torsionBySet A M (↑J : Set A))) (Submodule.subtype (torsionBySet A M (↑J : Set A))) ⊥) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommMonoid M
inst_2 : Module A M
J : Ideal A
hD : IsCoprime I J
this : ∀ (n : ℕ), Disjoint (α := Submodule A M) (torsionBySet A M (↑(I ^ n) : Set A)) (torsionBySet A M (↑J : Set A))
x : M
⊢ Membership.mem (γ := Submodule A M)
      (Submodule.map (M := ↥(torsionBySet A M (↑J : Set A))) (Submodule.subtype (torsionBySet A M (↑J : Set A)))
        (primaryComponent (↥(torsionBySet A M (↑J : Set A))) I))
      x ↔
    Membership.mem (γ := Submodule A M)
      (Submodule.map (M := ↥(torsionBySet A M (↑J : Set A))) (Submodule.subtype (torsionBySet A M (↑J : Set A))) ⊥) x
have a : ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0) ∧ ∀ (a : A) (b : a ∈ J), a • x = 0) ↔ x = 0
Tactic: simp only [mem_map, primaryComponent_mem, mem_torsionBySet_iff, SetLike.coe_sort_coe,
    Subtype.forall, subtype_apply, Subtype.exists, SetLike.mk_smul_mk, mk_eq_zero, exists_and_left,
    exists_prop, exists_eq_right_right, Submodule.map_bot, Submodule.mem_bot]