awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ((∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • x = 0) ∧ ∀ (a : A) (b : a ∈ J), a • x = 0) ↔ x = 0
have 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
Tactic: refine ⟨fun ⟨⟨n, _⟩, _⟩ ↦ ?_, by simp_all⟩
-- 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
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
⊢ x = 0
have this₁ : Disjoint (α := Submodule A M) (torsionBySet A M (↑(I ^ n) : Set A)) (torsionBySet A M (↑J : Set A))
Tactic: specialize this n
Cleared hypotheses: this
-- 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 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
⊢ Submodule.map (N₁ ⊔ N₂).subtype (primaryComponent (↥(N₁ ⊔ N₂)) I) =
    Submodule.map N₁.subtype (primaryComponent (↥N₁) I) ⊔ Submodule.map N₂.subtype (primaryComponent (↥N₂) I)
have 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)
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 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
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)
have 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
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]
-- 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 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
x : M
⊢ ((∃ (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
have 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
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 : 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
⊢ ((∃ (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
have 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
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 : 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_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
have h₁ : ∀ (a : A) (ha : a ∈ I ^ w), a • y = 0
Tactic: refine ⟨y, ⟨⟨w, fun a ha ↦ ?_⟩, by simp [hy]⟩, z, ⟨⟨w, fun a ha ↦ ?_⟩, by simp [hz]⟩, rfl⟩
-- 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 : 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
⊢ ∃ (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
have h₂ : ∀ (a : A) (ha : a ∈ I ^ w), a • z = 0
Tactic: refine ⟨y, ⟨⟨w, fun a ha ↦ ?_⟩, by simp [hy]⟩, z, ⟨⟨w, fun a ha ↦ ?_⟩, by simp [hz]⟩, rfl⟩
-- 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 : 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
⊢ (∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • (y + z) = 0) ∧ ∃ y_1 ∈ N₁, ∃ z_1 ∈ N₂, y_1 + z_1 = y + z
have h : ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • (y + z) = 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 : 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
⊢ (∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • (y + z) = 0) ∧ ∃ y_1 ∈ N₁, ∃ z_1 ∈ N₂, y_1 + z_1 = y + z
have h₁ : ∃ y_1 ∈ N₁, ∃ z_1 ∈ N₂, y_1 + z_1 = y + z
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 : 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
⊢ ∃ (n : ℕ), ∀ (a : A) (b : a ∈ I ^ n), a • (y + z) = 0
have h : ∀ (a : A) (b : a ∈ I ^ max n₁ n₂), a • (y + z) = 0
Tactic: use (max n₁ n₂)
-- 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 : 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 + z) = 0
have hy₁ : a • y = 0
Tactic: specialize hy a (Ideal.pow_le_pow_right (by simp : n₁ ≤ max n₁ n₂) ha)
Cleared hypotheses: hy
-- 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 : 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 • (y + z) = 0
have hz₁ : a • z = 0
Tactic: specialize hz a (Ideal.pow_le_pow_right (by simp : n₂ ≤ max n₁ n₂) ha)
Cleared hypotheses: hz
-- 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 : 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₂
⊢ ∃ y_1 ∈ N₁, ∃ z_1 ∈ N₂, y_1 + z_1 = y + z
have right : y + z = y + z
Tactic: use y, hymem, z, hzmem
-- 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 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsDedekindDomain A
h : IsTorsion A M
⊢ Eq.{u_2 + 1} (α := Submodule A M) (⨆ (P : HeightOneSpectrum A), primaryComponent M P.asIdeal) ⊤
have rw : ∀ (x : M), Membership.mem (γ := Submodule A M) (⨆ (P : HeightOneSpectrum A), primaryComponent M P.asIdeal) x
Tactic: rw [eq_top_iff']
-- 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 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsDedekindDomain A
h : IsTorsion A M
x : M
⊢ Membership.mem (γ := Submodule A M) (⨆ (P : HeightOneSpectrum A), primaryComponent M P.asIdeal) x
have 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
Tactic: obtain ⟨⟨a : A, ha : a ∈ A⁰⟩, hmem : a • x = 0⟩ := h (x := x)
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (hypothesis)
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) (⨆ (P : HeightOneSpectrum A), primaryComponent M P.asIdeal) x
have hmem₁ : 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}]
Cleared hypotheses: hmem
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (hypothesis)
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
⊢ Membership.mem (γ := Submodule A M) (⨆ (P : HeightOneSpectrum A), primaryComponent M P.asIdeal) x
have ha0 : Ne (α := Ideal A) (span {a}) ⊥
Tactic: have ha0 : span {a} ≠ ⊥ := by simpa using nonZeroDivisors.ne_zero ha
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (hypothesis)
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) (⨆ (P : HeightOneSpectrum A), primaryComponent M P.asIdeal) x
have hmem₁ : 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
Cleared hypotheses: hmem, ha0
-- 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 : 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}))
have 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
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
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
have h₁ : 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
-- 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 : 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
⊢ Membership.mem (γ := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a})) x ↔
    Membership.mem (γ := Ideal A) (⨅ i ∈ S, i.maxPowDividing (span {a})) x
have h₂ : Membership.mem (γ := Ideal A) (⨅ i ∈ S, i.maxPowDividing (span {a})) x →
  Membership.mem (γ := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {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
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 ∈ S, i.maxPowDividing (span {a})) x →
    Membership.mem (γ := Ideal A) (⨅ (i : HeightOneSpectrum A), i.maxPowDividing (span {a})) x
have h₁ : (∀ (i : HeightOneSpectrum A) (i_1 : i ∈ S), x ∈ i.maxPowDividing (span {a})) →
  ∀ (i : HeightOneSpectrum A), x ∈ i.maxPowDividing (span {a})
Tactic: simp only [mem_iInf]
-- 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 : 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
⊢ x ∈ i.maxPowDividing (span {a})
have pos : ∀ (htop : i.maxPowDividing (span {a}) = ⊤), x ∈ i.maxPowDividing (span {a})
Tactic: by_cases htop : i.maxPowDividing (span {a}) = ⊤
-- 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 : 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})
⊢ x ∈ i.maxPowDividing (span {a})
have neg : ∀ (htop : ¬i.maxPowDividing (span {a}) = ⊤), x ∈ i.maxPowDividing (span {a})
Tactic: by_cases htop : i.maxPowDividing (span {a}) = ⊤
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (hypothesis)
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}))
⊢ Membership.mem (γ := Submodule A M) (⨆ (P : HeightOneSpectrum A), primaryComponent M P.asIdeal) x
have this₁ : 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]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (hypothesis)
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}))
⊢ Membership.mem (γ := Submodule A M) (⨆ (P : HeightOneSpectrum A), primaryComponent M P.asIdeal) x
have hPairwise : (↑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
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (hypothesis)
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) (⨆ (P : HeightOneSpectrum A), primaryComponent M P.asIdeal) x
have hmem₁ : 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
Cleared hypotheses: hmem, this, hPairwise