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 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsDedekindDomain A
h : IsTorsion A M
x_1 : 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_1
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}))
x : A
h₁ :
  Membership.mem (γ := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a})) x →
    Membership.mem (γ := Ideal A) (⨅ i ∈ S, i.maxPowDividing (span {a})) x
h₂ :
  Membership.mem (γ := Ideal A) (⨅ i ∈ S, i.maxPowDividing (span {a})) x →
    Membership.mem (γ := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a})) x
⊢ Membership.mem (γ := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a})) x ↔
    Membership.mem (γ := Ideal A) (⨅ i ∈ S, i.maxPowDividing (span {a})) x

Tactic:
constructor
-- 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_1 : 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_1
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}))
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

Tactic:
aesop
-- 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_1 : 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_1
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}))
x : A
h₁ :
  (∀ (i : HeightOneSpectrum A) (i_1 : i ∈ S), x ∈ i.maxPowDividing (span {a})) →
    ∀ (i : HeightOneSpectrum A), x ∈ i.maxPowDividing (span {a})
⊢ Membership.mem (γ := Ideal A) (⨅ i ∈ S, i.maxPowDividing (span {a})) x →
    Membership.mem (γ := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a})) x

Tactic:
simp only [mem_iInf]

Premises used: Ideal.mem_iInf
-- 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_1 : IsTorsion A M
x_1 : 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_1
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}))
x : A
h : ∀ (i : HeightOneSpectrum A) (i_1 : i ∈ S), x ∈ i.maxPowDividing (span {a})
i : HeightOneSpectrum A
pos : ∀ (htop : i.maxPowDividing (span {a}) = ⊤), x ∈ i.maxPowDividing (span {a})
neg : ∀ (htop : ¬i.maxPowDividing (span {a}) = ⊤), x ∈ i.maxPowDividing (span {a})
⊢ x ∈ i.maxPowDividing (span {a})

Tactic:
by_cases htop : i.maxPowDividing (span {a}) = ⊤

Premises used: Ideal.span, Singleton.singleton, IsDedekindDomain.HeightOneSpectrum.maxPowDividing
-- 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_1 : IsTorsion A M
x_1 : 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_1
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}))
x : A
h : ∀ (i : HeightOneSpectrum A) (i_1 : i ∈ S), x ∈ i.maxPowDividing (span {a})
i : HeightOneSpectrum A
htop : i.maxPowDividing (span {a}) = ⊤
⊢ x ∈ i.maxPowDividing (span {a})

Tactic:
simp_all [S]
-- 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_1 : IsTorsion A M
x_1 : 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_1
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}))
x : A
h : ∀ (i : HeightOneSpectrum A) (i_1 : i ∈ S), x ∈ i.maxPowDividing (span {a})
i : HeightOneSpectrum A
htop : ¬i.maxPowDividing (span {a}) = ⊤
⊢ x ∈ i.maxPowDividing (span {a})

Tactic:
simp_all [S]
-- 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}))
⊢ Eq.{u_1 + 1} (α := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a}))
    (⨅ i ∈ S, i.maxPowDividing (span {a}))

Tactic:
have : (⨅ i : HeightOneSpectrum A, i.maxPowDividing (span {a})) =
      (⨅ i ∈ S, i.maxPowDividing (span {a})) := by
    ext x
    constructor
    · aesop
    · simp only [mem_iInf]
      intro h i
      by_cases htop : i.maxPowDividing (span {a}) = ⊤ <;> simp_all [S]
-- 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_1 : 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}))
this :
  Eq.{u_1 + 1} (α := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a}))
    (⨅ i ∈ S, i.maxPowDividing (span {a}))
⊢ (↑S : Set (HeightOneSpectrum A)).Pairwise fun (i j : HeightOneSpectrum A) ↦
    i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤

Tactic:
have hPairwise : (S : Set (HeightOneSpectrum _)).Pairwise
      fun i j ↦ i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤ :=
    fun r hr s hs hrs ↦ (isCoprime_pow_of_ne _ _ hrs _ _).sup_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_1 : 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}))
this :
  Eq.{u_1 + 1} (α := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a}))
    (⨅ i ∈ S, i.maxPowDividing (span {a}))
hPairwise :
  (↑S : Set (HeightOneSpectrum A)).Pairwise fun (i j : HeightOneSpectrum A) ↦
    i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
⊢ Membership.mem (γ := Submodule A M) (⨆ i ∈ S, torsionBySet A M (↑(i.maxPowDividing (span {a})) : Set A)) x

Tactic:
rw [this, ← iSup_torsionBySet_ideal_eq_torsionBySet_iInf hPairwise] at hmem

Premises used: Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf
-- 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_1 : 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}))
this :
  Eq.{u_1 + 1} (α := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a}))
    (⨅ i ∈ S, i.maxPowDividing (span {a}))
hPairwise :
  (↑S : Set (HeightOneSpectrum A)).Pairwise fun (i j : HeightOneSpectrum A) ↦
    i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
hmem₁ : Membership.mem (γ := Submodule A M) (⨆ i ∈ S, torsionBySet A M (↑(i.maxPowDividing (span {a})) : Set A)) x
⊢ Eq.{u_1 + 1} (α := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a}))
    (⨅ i ∈ S, i.maxPowDividing (span {a}))

Tactic:
rw [this, ← iSup_torsionBySet_ideal_eq_torsionBySet_iInf hPairwise] at hmem

Premises used: Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf
-- 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_1 : 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}))
this :
  Eq.{u_1 + 1} (α := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a}))
    (⨅ i ∈ S, i.maxPowDividing (span {a}))
hPairwise :
  (↑S : Set (HeightOneSpectrum A)).Pairwise fun (i j : HeightOneSpectrum A) ↦
    i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
hmem₁ : Membership.mem (γ := Submodule A M) (⨆ i ∈ S, torsionBySet A M (↑(i.maxPowDividing (span {a})) : Set A)) x
this₁ :
  Eq.{u_1 + 1} (α := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a}))
    (⨅ i ∈ S, i.maxPowDividing (span {a}))
⊢ (↑S : Set (HeightOneSpectrum A)).Pairwise fun (i j : HeightOneSpectrum A) ↦
    i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤

Tactic:
rw [this, ← iSup_torsionBySet_ideal_eq_torsionBySet_iInf hPairwise] at hmem

Premises used: Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf
-- 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
ha0 : Ne (α := Ideal A) (span {a}) ⊥
this_1 : 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}))
hmem : Membership.mem (γ := Submodule A M) (⨆ i ∈ S, torsionBySet A M (↑(i.maxPowDividing (span {a})) : Set A)) x
this :
  Eq.{u_1 + 1} (α := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a}))
    (⨅ i ∈ S, i.maxPowDividing (span {a}))
hPairwise :
  (↑S : Set (HeightOneSpectrum A)).Pairwise fun (i j : HeightOneSpectrum A) ↦
    i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
revert :
  ∀ (x : M)
    (hmem : Membership.mem (γ := Submodule A M) (⨆ i ∈ S, torsionBySet A M (↑(i.maxPowDividing (span {a})) : Set A)) x),
    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:
revert 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
a : A
ha : Membership.mem (γ := Submonoid A) A⁰ a
ha0 : Ne (α := Ideal A) (span {a}) ⊥
this_1 : 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}))
this :
  Eq.{u_1 + 1} (α := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a}))
    (⨅ i ∈ S, i.maxPowDividing (span {a}))
hPairwise :
  (↑S : Set (HeightOneSpectrum A)).Pairwise fun (i j : HeightOneSpectrum A) ↦
    i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
⊢ LE.le.{u_2} (α := Submodule A M) (⨆ i ∈ S, torsionBySet A M (↑(i.maxPowDividing (span {a})) : Set A))
    (⨆ (P : HeightOneSpectrum A), primaryComponent M P.asIdeal)

Tactic:
iSup_mono (fun P x hxmem ↦ ?_)

Premises used: Set.Mem, iSup_mono
-- 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
a : A
ha : Membership.mem (γ := Submonoid A) A⁰ a
ha0 : Ne (α := Ideal A) (span {a}) ⊥
this_1 : 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}))
this :
  Eq.{u_1 + 1} (α := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a}))
    (⨅ i ∈ S, i.maxPowDividing (span {a}))
hPairwise :
  (↑S : Set (HeightOneSpectrum A)).Pairwise fun (i j : HeightOneSpectrum A) ↦
    i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
refine :
  ∀ (P : HeightOneSpectrum A) (x : M)
    (hxmem :
      Membership.mem (γ := Submodule A M) (⨆ (_ : P ∈ S), torsionBySet A M (↑(P.maxPowDividing (span {a})) : Set A)) x),
    Membership.mem (γ := Submodule A M) (primaryComponent M P.asIdeal) x
⊢ LE.le.{u_2} (α := Submodule A M) (⨆ i ∈ S, torsionBySet A M (↑(i.maxPowDividing (span {a})) : Set A))
    (⨆ (P : HeightOneSpectrum A), primaryComponent M P.asIdeal)

Tactic:
refine iSup_mono (fun P x hxmem ↦ ?_)

Premises used: iSup_mono
-- 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
a : A
ha : Membership.mem (γ := Submonoid A) A⁰ a
ha0 : Ne (α := Ideal A) (span {a}) ⊥
this_1 : 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}))
this :
  Eq.{u_1 + 1} (α := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a}))
    (⨅ i ∈ S, i.maxPowDividing (span {a}))
hPairwise :
  (↑S : Set (HeightOneSpectrum A)).Pairwise fun (i j : HeightOneSpectrum A) ↦
    i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
P : HeightOneSpectrum A
x : M
hxmem : Membership.mem (γ := Submodule A M) (⨆ (_ : P ∈ S), torsionBySet A M (↑(P.maxPowDividing (span {a})) : Set A)) x
pos : ∀ (hPS : P ∈ S), Membership.mem (γ := Submodule A M) (primaryComponent M P.asIdeal) x
neg : ∀ (hPS : P ∉ S), Membership.mem (γ := Submodule A M) (primaryComponent M P.asIdeal) x
⊢ Membership.mem (γ := Submodule A M) (primaryComponent M P.asIdeal) x

Tactic:
by_cases hPS : P ∈ S
-- 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
a : A
ha : Membership.mem (γ := Submonoid A) A⁰ a
ha0 : Ne (α := Ideal A) (span {a}) ⊥
this_1 : 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}))
this :
  Eq.{u_1 + 1} (α := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a}))
    (⨅ i ∈ S, i.maxPowDividing (span {a}))
hPairwise :
  (↑S : Set (HeightOneSpectrum A)).Pairwise fun (i j : HeightOneSpectrum A) ↦
    i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
P : HeightOneSpectrum A
x : M
hxmem : Membership.mem (γ := Submodule A M) (⨆ (_ : P ∈ S), torsionBySet A M (↑(P.maxPowDividing (span {a})) : Set A)) x
hPS : P ∈ S
pos :
  ∀ (ha : ¬a = 0)
    (this :
      Eq.{u_1 + 1} (α := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a}))
        (⨅ (i : HeightOneSpectrum A), ⨅ (_ : ¬i.maxPowDividing (span {a}) = ⊤), i.maxPowDividing (span {a})))
    (hPairwise :
      (↑(toFinset (mulSupport (M := Ideal A) fun (v : HeightOneSpectrum A) ↦ v.maxPowDividing (span {a}))) :
            Set (HeightOneSpectrum A)).Pairwise
        fun (i j : HeightOneSpectrum A) ↦ i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤)
    (hxmem : ∀ (a_1 : A) (b : a_1 ∈ P.maxPowDividing (span {a})), a_1 • x = 0) (hPS : ¬P.maxPowDividing (span {a}) = ⊤),
    ∃ (n : ℕ), ∀ (a : A) (b : a ∈ P.asIdeal ^ n), a • x = 0
⊢ Membership.mem (γ := Submodule A M) (primaryComponent M P.asIdeal) x

Tactic:
simp_all only [mem_nonZeroDivisors_iff_ne_zero, ne_eq, mem_toFinset, mem_mulSupport,
      one_eq_top, primaryComponent_mem, mem_torsionBySet_iff, SetLike.coe_sort_coe,
      Subtype.forall, iSup_pos, S]

Premises used: Ideal.one_eq_top, SetLike.coe_sort_coe, Submodule.mem_torsionBySet_iff, Function.mem_mulSupport, Subtype.forall, iSup_pos, ne_eq, Ideal.primaryComponent_mem, mem_nonZeroDivisors_iff_ne_zero, Set.mem_toFinset
-- 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
a : A
ha0 : Ne (α := Ideal A) (span {a}) ⊥
this_1 : 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}))
P : HeightOneSpectrum A
x : M
ha : ¬a = 0
this :
  Eq.{u_1 + 1} (α := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a}))
    (⨅ (i : HeightOneSpectrum A), ⨅ (_ : ¬i.maxPowDividing (span {a}) = ⊤), i.maxPowDividing (span {a}))
hPairwise :
  (↑(toFinset (mulSupport (M := Ideal A) fun (v : HeightOneSpectrum A) ↦ v.maxPowDividing (span {a}))) :
        Set (HeightOneSpectrum A)).Pairwise
    fun (i j : HeightOneSpectrum A) ↦ i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
hxmem : ∀ (a_1 : A) (b : a_1 ∈ P.maxPowDividing (span {a})), a_1 • x = 0
hPS : ¬P.maxPowDividing (span {a}) = ⊤
⊢ ∃ (n : ℕ), ∀ (a : A) (b : a ∈ P.asIdeal ^ n), a • x = 0

Tactic:
⟨(Associates.mk P.asIdeal).count (Associates.mk (span {a})).factors, fun _ b ↦ hxmem _ b⟩

Premises used: Associates.mk, Associates.count, IsDedekindDomain.HeightOneSpectrum.asIdeal, Exists.intro, Ideal.span, Associates.factors, Singleton.singleton