awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
inst_1 : AddCommMonoid M
inst_2 : Module A M
I : Ideal A
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
⊢ 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))

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
inst_1 : AddCommMonoid M
inst_2 : Module A M
I : Ideal A
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:
simp [primaryComponent_mem]

Premises used: Ideal.primaryComponent_mem
-- 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
J : Ideal A
hD : IsCoprime I J
⊢ ∀ (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)
-- 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
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))
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))) ⊥)
⊢ Eq.{u_2 + 1} (α := Submodule A ↥(torsionBySet A M (↑J : Set A)))
    (primaryComponent (↥(torsionBySet A M (↑J : Set A))) I) ⊥

Tactic:
apply Submodule.map_injective_of_injective (Submodule.subtype_injective (torsionBySet A M ↑J))

Premises used: SetLike.coe, Submodule.subtype_injective, Submodule.torsionBySet, Submodule.map_injective_of_injective
-- 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
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))
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
⊢ 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:
ext x
-- 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
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
a : ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0) ∧ ∀ (a : A) (b : a ∈ J), a • x = 0) ↔ x = 0
⊢ 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:
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]

Premises used: exists_eq_right_right, SetLike.coe_sort_coe, Submodule.mem_bot, Submodule.mem_map, Submodule.subtype_apply, Submodule.map_bot, Submodule.mem_torsionBySet_iff, Subtype.exists, exists_and_left, Subtype.forall, exists_prop, Ideal.primaryComponent_mem, Submodule.mk_eq_zero, SetLike.mk_smul_mk
-- 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
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
⊢ x = 0 → (∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0) ∧ ∀ (a : A) (b : a ∈ J), a • x = 0

Tactic:
simp_all
-- 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
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
a :
  ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0) ∧ ∀ (a : A) (b : a ∈ J), a • x = 0) →
    ∀ (n : ℕ), (∀ (a : A) (b : a ∈ I ^ n), a • x = 0) → (∀ (a : A) (b : a ∈ J), a • x = 0) → x = 0
⊢ ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0) ∧ ∀ (a : A) (b : a ∈ J), a • x = 0) ↔ x = 0

Tactic:
refine ⟨fun ⟨⟨n, _⟩, _⟩ ↦ ?_, by simp_all⟩
-- 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
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
h : (∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0) ∧ ∀ (a : A) (b : a ∈ J), a • x = 0
n : ℕ
h_1 : ∀ (a : A) (b : a ∈ I ^ n), a • x = 0
right : ∀ (a : A) (b : a ∈ J), a • x = 0
⊢ Disjoint (α := Submodule A M) (torsionBySet A M (↑(I ^ n) : Set A)) (torsionBySet A M (↑J : Set A))

Tactic:
specialize this n
-- 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
J : Ideal A
hD : IsCoprime I J
x : M
h : (∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0) ∧ ∀ (a : A) (b : a ∈ J), a • x = 0
n : ℕ
h_1 : ∀ (a : A) (b : a ∈ I ^ n), a • x = 0
right : ∀ (a : A) (b : a ∈ J), a • x = 0
this : Disjoint (α := Submodule A M) (torsionBySet A M (↑(I ^ n) : Set A)) (torsionBySet A M (↑J : Set A))
⊢ x = 0

Tactic:
simp_all [disjoint_def]

Premises used: Submodule.disjoint_def
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
h :
  ∀ (x : M),
    x ∈ Submodule.map (N₁ ⊔ N₂).subtype (primaryComponent (↥(N₁ ⊔ N₂)) I) ↔
      x ∈ Submodule.map N₁.subtype (primaryComponent (↥N₁) I) ⊔ Submodule.map N₂.subtype (primaryComponent (↥N₂) I)
⊢ Submodule.map (N₁ ⊔ N₂).subtype (primaryComponent (↥(N₁ ⊔ N₂)) I) =
    Submodule.map N₁.subtype (primaryComponent (↥N₁) I) ⊔ Submodule.map N₂.subtype (primaryComponent (↥N₂) I)

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
x : M
h :
  ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0) ∧ ∃ y ∈ N₁, ∃ z ∈ N₂, y + z = x) ↔
    ∃ (y : M),
      ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • y = 0) ∧ y ∈ N₁) ∧
        ∃ (z : M), ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • z = 0) ∧ z ∈ N₂) ∧ y + z = x
⊢ x ∈ Submodule.map (N₁ ⊔ N₂).subtype (primaryComponent (↥(N₁ ⊔ N₂)) I) ↔
    x ∈ Submodule.map N₁.subtype (primaryComponent (↥N₁) I) ⊔ Submodule.map N₂.subtype (primaryComponent (↥N₂) I)

Tactic:
simp_all 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.mem_sup]

Premises used: exists_eq_right_right, SetLike.coe_sort_coe, Submodule.mem_map, Submodule.subtype_apply, Submodule.mem_torsionBySet_iff, Subtype.exists, exists_and_left, Subtype.forall, exists_prop, Ideal.primaryComponent_mem, Submodule.mem_sup, Submodule.mk_eq_zero, SetLike.mk_smul_mk
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
x : M
h :
  ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0) ∧ ∃ y ∈ N₁, ∃ z ∈ N₂, y + z = x) →
    ∃ (y : M),
      ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • y = 0) ∧ y ∈ N₁) ∧
        ∃ (z : M), ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • z = 0) ∧ z ∈ N₂) ∧ y + z = x
h₁ :
  (∃ (y : M),
      ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • y = 0) ∧ y ∈ N₁) ∧
        ∃ (z : M), ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • z = 0) ∧ z ∈ N₂) ∧ y + z = x) →
    (∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0) ∧ ∃ y ∈ N₁, ∃ z ∈ N₂, y + z = x
⊢ ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0) ∧ ∃ y ∈ N₁, ∃ z ∈ N₂, y + z = x) ↔
    ∃ (y : M),
      ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • y = 0) ∧ y ∈ N₁) ∧
        ∃ (z : M), ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • z = 0) ∧ z ∈ N₂) ∧ y + z = x

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 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ (a : A) (b : a ∈ I ^ w), a • (y + z) = 0
⊢ y ∈ N₁

Tactic:
simp [hy]
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ (a : A) (b : a ∈ I ^ w), a • (y + z) = 0
⊢ z ∈ N₂

Tactic:
simp [hz]
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ (a : A) (b : a ∈ I ^ w), a • (y + z) = 0
h₁ : ∀ (a : A) (ha : a ∈ I ^ w), a • y = 0
h₂ : ∀ (a : A) (ha : a ∈ I ^ w), a • z = 0
⊢ ∃ (y_1 : M),
    ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • y_1 = 0) ∧ y_1 ∈ N₁) ∧
      ∃ (z_1 : M), ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • z_1 = 0) ∧ z_1 ∈ N₂) ∧ y_1 + z_1 = y + z

Tactic:
refine ⟨y, ⟨⟨w, fun a ha ↦ ?_⟩, by simp [hy]⟩, z, ⟨⟨w, fun a ha ↦ ?_⟩, by simp [hz]⟩, rfl⟩
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ (a : A) (b : a ∈ I ^ w), a • (y + z) = 0
a : A
ha : a ∈ I ^ w
⊢ a • y = 0

Tactic:
((Submodule.disjoint_iff_add_eq_zero.mp hD) (Submodule.smul_mem N₁ a hy)
        (Submodule.smul_mem N₂ a hz) (h a ha ▸ (smul_add a y z).symm)).1

Premises used: Eq.rec, And.left, Submodule.disjoint_iff_add_eq_zero, Iff.mp, Eq.symm, smul_add, Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ (a : A) (b : a ∈ I ^ w), a • (y + z) = 0
a : A
ha : a ∈ I ^ w
⊢ a • y = 0

Tactic:
exact ((Submodule.disjoint_iff_add_eq_zero.mp hD) (Submodule.smul_mem N₁ a hy)
        (Submodule.smul_mem N₂ a hz) (h a ha ▸ (smul_add a y z).symm)).1

Premises used: Eq.rec, And.left, Submodule.disjoint_iff_add_eq_zero, Iff.mp, Eq.symm, smul_add, Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ (a : A) (b : a ∈ I ^ w), a • (y + z) = 0
a : A
ha : a ∈ I ^ w
⊢ a • z = 0

Tactic:
((Submodule.disjoint_iff_add_eq_zero.mp hD) (Submodule.smul_mem N₁ a hy)
        (Submodule.smul_mem N₂ a hz) (h a ha ▸ (smul_add a y z).symm)).2

Premises used: Eq.rec, And.right, Submodule.disjoint_iff_add_eq_zero, Iff.mp, Eq.symm, smul_add, Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ (a : A) (b : a ∈ I ^ w), a • (y + z) = 0
a : A
ha : a ∈ I ^ w
⊢ a • z = 0

Tactic:
exact ((Submodule.disjoint_iff_add_eq_zero.mp hD) (Submodule.smul_mem N₁ a hy)
        (Submodule.smul_mem N₂ a hz) (h a ha ▸ (smul_add a y z).symm)).2

Premises used: Eq.rec, And.right, Submodule.disjoint_iff_add_eq_zero, Iff.mp, Eq.symm, smul_add, Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
hy : ∀ (a : A) (b : a ∈ I ^ n₁), a • y = 0
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ (a : A) (b : a ∈ I ^ n₂), a • z = 0
h : ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • (y + z) = 0
h₁ : ∃ y_1 ∈ N₁, ∃ z_1 ∈ N₂, y_1 + z_1 = y + z
⊢ (∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • (y + z) = 0) ∧ ∃ y_1 ∈ N₁, ∃ z_1 ∈ N₂, y_1 + z_1 = y + z

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 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
hy : ∀ (a : A) (b : a ∈ I ^ n₁), a • y = 0
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ (a : A) (b : a ∈ I ^ n₂), a • z = 0
h : ∀ (a : A) (b : a ∈ I ^ max n₁ n₂), a • (y + z) = 0
⊢ ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • (y + z) = 0

Tactic:
use (max n₁ n₂)

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 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
hy : ∀ (a : A) (b : a ∈ I ^ n₁), a • y = 0
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ (a : A) (b : a ∈ I ^ n₂), a • z = 0
a : A
ha : a ∈ I ^ max n₁ n₂
⊢ n₁ ≤ max n₁ n₂

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
hy : ∀ (a : A) (b : a ∈ I ^ n₁), a • y = 0
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ (a : A) (b : a ∈ I ^ n₂), a • z = 0
a : A
ha : a ∈ I ^ max n₁ n₂
⊢ a • y = 0

Tactic:
specialize hy a (Ideal.pow_le_pow_right (by simp : n₁ ≤ max n₁ n₂) ha)

Premises used: Ideal.pow_le_pow_right
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ (a : A) (b : a ∈ I ^ n₂), a • z = 0
a : A
ha : a ∈ I ^ max n₁ n₂
hy : a • y = 0
⊢ n₂ ≤ max n₁ n₂

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ (a : A) (b : a ∈ I ^ n₂), a • z = 0
a : A
ha : a ∈ I ^ max n₁ n₂
hy : a • y = 0
⊢ a • z = 0

Tactic:
specialize hz a (Ideal.pow_le_pow_right (by simp : n₂ ≤ max n₁ n₂) ha)

Premises used: Ideal.pow_le_pow_right
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
z : M
hzmem : z ∈ N₂
n₂ : ℕ
a : A
ha : a ∈ I ^ max n₁ n₂
hy : a • y = 0
hz : a • z = 0
⊢ a • (y + z) = 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
I : Ideal A
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
hy : ∀ (a : A) (b : a ∈ I ^ n₁), a • y = 0
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ (a : A) (b : a ∈ I ^ n₂), a • z = 0
w : M
left : y ∈ N₁
w₁ : M
left₁ : z ∈ N₂
right : y + z = y + z
⊢ ∃ y_1 ∈ N₁, ∃ z_1 ∈ N₂, y_1 + z_1 = y + z

Tactic:
use y, hymem, z, hzmem
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsDedekindDomain A
h : IsTorsion A M
rw : ∀ (x : M), Membership.mem (γ := Submodule A M) (⨆ (P : HeightOneSpectrum A), primaryComponent M P.asIdeal) x
⊢ Eq.{u_2 + 1} (α := Submodule A M) (⨆ (P : HeightOneSpectrum A), primaryComponent M P.asIdeal) ⊤

Tactic:
rw [eq_top_iff']

Premises used: Submodule.eq_top_iff'
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsDedekindDomain A
h : IsTorsion A M
x : M
obtain :
  ∀ (a : A) (ha : Membership.mem (γ := Submonoid A) A⁰ a) (hmem : a • x = 0),
    Membership.mem (γ := Submodule A M) (⨆ (P : HeightOneSpectrum A), primaryComponent M P.asIdeal) x
⊢ Membership.mem (γ := Submodule A M) (⨆ (P : HeightOneSpectrum A), primaryComponent M P.asIdeal) x

Tactic:
obtain ⟨⟨a : A, ha : a ∈ A⁰⟩, hmem : a • x = 0⟩ := h (x := x)
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : Membership.mem (γ := Submonoid A) A⁰ a
hmem : a • x = 0
⊢ Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(span {a}) : Set A)) x

Tactic:
simp_all [← torsionBySet_eq_torsionBySet_span {a}]

Premises used: Submodule.torsionBySet_eq_torsionBySet_span, Singleton.singleton
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : Membership.mem (γ := Submonoid A) A⁰ a
hmem : a • x = 0
⊢ Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(span {a}) : Set A)) x

Tactic:
replace hmem : x ∈ torsionBySet A M (span {a}) := by
    simp_all [← torsionBySet_eq_torsionBySet_span {a}]
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : Membership.mem (γ := Submonoid A) A⁰ a
hmem : Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(span {a}) : Set A)) x
⊢ Ne (α := Ideal A) (span {a}) ⊥

Tactic:
simpa using nonZeroDivisors.ne_zero ha

Premises used: nonZeroDivisors.ne_zero
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : Membership.mem (γ := Submonoid A) A⁰ a
hmem : Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(span {a}) : Set A)) x
⊢ Ne (α := Ideal A) (span {a}) ⊥

Tactic:
have ha0 : span {a} ≠ ⊥ := by simpa using nonZeroDivisors.ne_zero ha
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : Membership.mem (γ := Submonoid A) A⁰ a
hmem : Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(span {a}) : Set A)) x
ha0 : Ne (α := Ideal A) (span {a}) ⊥
⊢ Membership.mem (γ := Submodule A M)
    (torsionBySet A M (↑(⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a})) : Set A)) x

Tactic:
rw [← iInf_maxPowDividing_eq ha0] at hmem

Premises used: Ideal.iInf_maxPowDividing_eq
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : Membership.mem (γ := Submonoid A) A⁰ a
hmem : Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(span {a}) : Set A)) x
ha0 : Ne (α := Ideal A) (span {a}) ⊥
hmem₁ :
  Membership.mem (γ := Submodule A M)
    (torsionBySet A M (↑(⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a})) : Set A)) x
⊢ Ne (α := Ideal A) (span {a}) ⊥

Tactic:
rw [← iInf_maxPowDividing_eq ha0] at hmem

Premises used: Ideal.iInf_maxPowDividing_eq
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
M : Type u_2
inst : CommRing A
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : Membership.mem (γ := Submonoid A) A⁰ a
hmem :
  Membership.mem (γ := Submodule A M)
    (torsionBySet A M (↑(⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a})) : Set A)) x
ha0 : Ne (α := Ideal A) (span {a}) ⊥
this : Fintype (↑(mulSupport (M := Ideal A) fun (v : HeightOneSpectrum A) ↦ v.maxPowDividing (span {a})) : Type u_1) :=
  Finite.fintype (s := mulSupport (M := Ideal A) fun (v : HeightOneSpectrum A) ↦ v.maxPowDividing (span {a})) ⋯
S : Finset (HeightOneSpectrum A) :=
  toFinset (mulSupport (M := Ideal A) fun (v : HeightOneSpectrum A) ↦ v.maxPowDividing (span {a}))
h₁ :
  ∀ (x : A),
    Membership.mem (γ := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a})) x ↔
      Membership.mem (γ := Ideal A) (⨅ i ∈ S, i.maxPowDividing (span {a})) x
⊢ Eq.{u_1 + 1} (α := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a}))
    (⨅ i ∈ S, i.maxPowDividing (span {a}))

Tactic:
ext x