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
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}) = ⊤
⊢ Membership.mem (γ := Submodule A M) (⨆ (P : HeightOneSpectrum A), primaryComponent M P.asIdeal) x
have 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
Tactic: revert x
Cleared hypotheses: x, hmem
-- 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
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)
have 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
Tactic: refine iSup_mono (fun P x hxmem ↦ ?_)
-- 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
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
⊢ Membership.mem (γ := Submodule A M) (primaryComponent M P.asIdeal) x
have pos : ∀ (hPS : P ∈ S), Membership.mem (γ := Submodule A M) (primaryComponent M P.asIdeal) x
Tactic: by_cases hPS : P ∈ S
-- 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
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
⊢ Membership.mem (γ := Submodule A M) (primaryComponent M P.asIdeal) x
have neg : ∀ (hPS : P ∉ S), Membership.mem (γ := Submodule A M) (primaryComponent M P.asIdeal) x
Tactic: by_cases hPS : P ∈ S
-- 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
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
⊢ Membership.mem (γ := Submodule A M) (primaryComponent M P.asIdeal) x
have 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
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]
Cleared hypotheses: ha, this, hPairwise, hxmem, hPS
-- 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
⊢ iSupIndep.{u_1 + 1, u_2} (α := Submodule A M) fun (P : HeightOneSpectrum A) ↦ primaryComponent M P.asIdeal
have rw : ∀ (s : Finset (HeightOneSpectrum A)) (v : HeightOneSpectrum A → M),
  (∀ i ∈ s, Membership.mem (γ := Submodule A M) (primaryComponent M i.asIdeal) (v i)) →
    Eq.{u_2 + 1} (α := M) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
Tactic: rw [iSupIndep_iff_finsetSum_eq_zero_imp_eq_zero]
-- 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
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hmem : ∀ i ∈ s, Membership.mem (γ := Submodule A M) (primaryComponent M i.asIdeal) (p i)
hsum : Eq.{u_2 + 1} (α := M) (∑ i ∈ s, p i) 0
⊢ ∀ i ∈ s, p i = 0
have hmem₁ : ∀ i ∈ s, ∃ (n : ℕ), Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(i.asIdeal ^ n) : Set A)) (p i)
Tactic: simp only [primaryComponent_mem] at hmem
Cleared hypotheses: hmem
-- 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
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hsum : Eq.{u_2 + 1} (α := M) (∑ i ∈ s, p i) 0
hmem : ∀ i ∈ s, ∃ (n : ℕ), Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(i.asIdeal ^ n) : Set A)) (p i)
⊢ ∀ i ∈ s, p i = 0
have choose! : ∀ (f : (i : HeightOneSpectrum A) → ℕ)
  (hmem : ∀ i ∈ s, Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(i.asIdeal ^ f i) : Set A)) (p i)),
  ∀ i ∈ s, p i = 0
Tactic: choose! f hmem using hmem
Cleared hypotheses: hmem
-- 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
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hsum : Eq.{u_2 + 1} (α := M) (∑ i ∈ s, p i) 0
f : (i : HeightOneSpectrum A) → ℕ
hmem : ∀ i ∈ s, Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(i.asIdeal ^ f i) : Set A)) (p i)
m : ℕ := s.sup f
⊢ iSupIndep.{u_1 + 1, u_2} (α := Submodule A M) fun (i : HeightOneSpectrum A) ↦
    torsionBySet A M (↑(i.asIdeal ^ m) : Set A)
have rw : ∀ (s : Finset (HeightOneSpectrum A)),
  Finset.SupIndep.{u_2, u_1} (α := Submodule A M) s fun (i : HeightOneSpectrum A) ↦
    torsionBySet A M (↑(i.asIdeal ^ m) : Set A)
Tactic: rw [iSupIndep_iff_supIndep]
-- 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
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hsum : Eq.{u_2 + 1} (α := M) (∑ i ∈ s, p i) 0
f : (i : HeightOneSpectrum A) → ℕ
hmem : ∀ i ∈ s, Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(i.asIdeal ^ f i) : Set A)) (p i)
m : ℕ := s.sup f
⊢ ∀ i ∈ s, p i = 0
have hSupIndep : iSupIndep.{u_1 + 1, u_2} (α := Submodule A M) fun (i : HeightOneSpectrum A) ↦
  torsionBySet A M (↑(i.asIdeal ^ m) : Set A)
Tactic: have hSupIndep : iSupIndep fun i : HeightOneSpectrum A ↦ torsionBySet A M ↑(i.asIdeal ^ m) := by
    rw [iSupIndep_iff_supIndep]
    exact fun _ ↦ supIndep_torsionBySet_ideal
      fun _ _ _ _ hPQ ↦ (isCoprime_pow_of_ne _ _ hPQ _ _).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
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hsum : Eq.{u_2 + 1} (α := M) (∑ i ∈ s, p i) 0
f : (i : HeightOneSpectrum A) → ℕ
hmem : ∀ i ∈ s, Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(i.asIdeal ^ f i) : Set A)) (p i)
m : ℕ := s.sup f
hSupIndep :
  iSupIndep.{u_1 + 1, u_2} (α := Submodule A M) fun (i : HeightOneSpectrum A) ↦
    torsionBySet A M (↑(i.asIdeal ^ m) : Set A)
⊢ ∀ i ∈ s, p i = 0
have hSupIndep₁ : ∀ (s : Finset (HeightOneSpectrum A)) (v : HeightOneSpectrum A → M),
  (∀ i ∈ s, Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(i.asIdeal ^ m) : Set A)) (v i)) →
    Eq.{u_2 + 1} (α := M) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
Tactic: rw [iSupIndep_iff_finsetSum_eq_zero_imp_eq_zero] at hSupIndep
Cleared hypotheses: hSupIndep
-- 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
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hsum : Eq.{u_2 + 1} (α := M) (∑ i ∈ s, p i) 0
f : (i : HeightOneSpectrum A) → ℕ
hmem : ∀ i ∈ s, Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(i.asIdeal ^ f i) : Set A)) (p i)
m : ℕ := s.sup f
hSupIndep :
  ∀ (s : Finset (HeightOneSpectrum A)) (v : HeightOneSpectrum A → M),
    (∀ i ∈ s, Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(i.asIdeal ^ m) : Set A)) (v i)) →
      Eq.{u_2 + 1} (α := M) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
⊢ ∀ i ∈ s, p i = 0
have apply : ∀ i ∈ s, Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(i.asIdeal ^ m) : Set A)) (p i)
Tactic: apply hSupIndep _ _ ?_ hsum
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₁
inst_5 : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf : Surjective.{u_5 + 1, u_6 + 1} (α := M₁) (β := M₂) (⇑φ : (a : M₁) → M₂)
y : M₂
hy : Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) y
⊢ ∃ (a : ↥(primaryComponent M₁ P.asIdeal)),
    (map P.asIdeal φ : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal)) a =
      Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) x) y hy
have obtain : ∀ (b : M₁)
  (hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂)),
  ∃ (a : ↥(primaryComponent M₁ P.asIdeal)),
    Eq.{u_6 + 1} (α := ↥(primaryComponent M₂ P.asIdeal))
      ((map P.asIdeal φ : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal)) a :
        ↥(primaryComponent M₂ P.asIdeal))
      (Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) x)
          ((φ : (a : M₁) → M₂) b) hy :
        ↥(primaryComponent M₂ P.asIdeal))
Tactic: obtain ⟨b, rfl⟩ : ∃ a, φ a = y := hf y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₁
inst_5 : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf : Surjective.{u_5 + 1, u_6 + 1} (α := M₁) (β := M₂) (⇑φ : (a : M₁) → M₂)
b : M₁
hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂)
⊢ ∃ (a : ↥(primaryComponent M₁ P.asIdeal)),
    Eq.{u_6 + 1} (α := ↥(primaryComponent M₂ P.asIdeal))
      ((map P.asIdeal φ : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal)) a :
        ↥(primaryComponent M₂ P.asIdeal))
      (Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) x)
          ((φ : (a : M₁) → M₂) b) hy :
        ↥(primaryComponent M₂ P.asIdeal))
have obtain : ∀ (f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal))
  (hf :
    ((DFinsupp.lsum ℕ (M := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) :
              (a : (i : HeightOneSpectrum A) → ↥(primaryComponent M₁ i.asIdeal) →ₗ[A] M₁) →
                (Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) →ₗ[A] M₁)
            fun (i : HeightOneSpectrum A) ↦ Submodule.subtype (primaryComponent M₁ i.asIdeal) :
          (a : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) → M₁)
        f =
      b),
  ∃ (a : ↥(primaryComponent M₁ P.asIdeal)),
    Eq.{u_6 + 1} (α := ↥(primaryComponent M₂ P.asIdeal))
      ((map P.asIdeal φ : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal)) a :
        ↥(primaryComponent M₂ P.asIdeal))
      (Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) x)
          ((φ : (a : M₁) → M₂) b) hy :
        ↥(primaryComponent M₂ P.asIdeal))
Tactic: obtain ⟨f, hf⟩ : ∃ f : Π₀ i : HeightOneSpectrum A, primaryComponent M₁ i.asIdeal,
      (DFinsupp.lsum ℕ fun i : HeightOneSpectrum A ↦
      (primaryComponent M₁ i.asIdeal).subtype) f = b := by
    simp only [← mem_iSup_iff_exists_dfinsupp, iSup_primaryComponent_eq_top hM₁, mem_top]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₁
inst_5 : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf_1 : Surjective.{u_5 + 1, u_6 + 1} (α := M₁) (β := M₂) (⇑φ : (a : M₁) → M₂)
b : M₁
hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂)
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf :
  ((DFinsupp.lsum ℕ (M := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) :
            (a : (i : HeightOneSpectrum A) → ↥(primaryComponent M₁ i.asIdeal) →ₗ[A] M₁) →
              (Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) →ₗ[A] M₁)
          fun (i : HeightOneSpectrum A) ↦ Submodule.subtype (primaryComponent M₁ i.asIdeal) :
        (a : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) → M₁)
      f =
    b
⊢ ∃ (a : ↥(primaryComponent M₁ P.asIdeal)),
    Eq.{u_6 + 1} (α := ↥(primaryComponent M₂ P.asIdeal))
      ((map P.asIdeal φ : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal)) a :
        ↥(primaryComponent M₂ P.asIdeal))
      (Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) x)
          ((φ : (a : M₁) → M₂) b) hy :
        ↥(primaryComponent M₂ P.asIdeal))
have refine : Eq.{u_6 + 1} (α := M₂)
  ((↑((map P.asIdeal φ : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal))
          ((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P)) :
      M₂) :
    M₂)
  ((↑(Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) x)
          ((φ : (a : M₁) → M₂) b) hy) :
      M₂) :
    M₂)
Tactic: refine ⟨f P, Subtype.ext ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₁
inst_5 : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf_1 : Surjective.{u_5 + 1, u_6 + 1} (α := M₁) (β := M₂) (⇑φ : (a : M₁) → M₂)
b : M₁
hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂)
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf :
  ((DFinsupp.lsum ℕ (M := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) :
            (a : (i : HeightOneSpectrum A) → ↥(primaryComponent M₁ i.asIdeal) →ₗ[A] M₁) →
              (Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) →ₗ[A] M₁)
          fun (i : HeightOneSpectrum A) ↦ Submodule.subtype (primaryComponent M₁ i.asIdeal) :
        (a : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) → M₁)
      f =
    b
⊢ Eq.{u_6 + 1} (α := M₂)
    ((↑((map P.asIdeal φ : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal))
            ((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P)) :
        M₂) :
      M₂)
    ((↑(Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) x)
            ((φ : (a : M₁) → M₂) b) hy) :
        M₂) :
      M₂)
have simp : Eq.{u_6 + 1} (α := M₂)
  ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂)
  ((φ : (a : M₁) → M₂) b : M₂)
Tactic: simp only [map_apply_coe]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₁
inst_5 : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf_1 : Surjective.{u_5 + 1, u_6 + 1} (α := M₁) (β := M₂) (⇑φ : (a : M₁) → M₂)
b : M₁
hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂)
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf :
  ((DFinsupp.lsum ℕ (M := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) :
            (a : (i : HeightOneSpectrum A) → ↥(primaryComponent M₁ i.asIdeal) →ₗ[A] M₁) →
              (Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) →ₗ[A] M₁)
          fun (i : HeightOneSpectrum A) ↦ Submodule.subtype (primaryComponent M₁ i.asIdeal) :
        (a : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) → M₁)
      f =
    b
⊢ Eq.{u_6 + 1} (α := M₂)
    ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂)
    ((φ : (a : M₁) → M₂) b : M₂)
have rw : HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
    ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂) =
  0
Tactic: rw [eq_comm, ← sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₁
inst_5 : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf_1 : Surjective.{u_5 + 1, u_6 + 1} (α := M₁) (β := M₂) (⇑φ : (a : M₁) → M₂)
b : M₁
hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂)
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf :
  ((DFinsupp.lsum ℕ (M := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) :
            (a : (i : HeightOneSpectrum A) → ↥(primaryComponent M₁ i.asIdeal) →ₗ[A] M₁) →
              (Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) →ₗ[A] M₁)
          fun (i : HeightOneSpectrum A) ↦ Submodule.subtype (primaryComponent M₁ i.asIdeal) :
        (a : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) → M₁)
      f =
    b
⊢ HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
      ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂) =
    0
have refine_1 : Membership.mem (γ := Submodule A M₂)
  ((fun (P : HeightOneSpectrum A) ↦ (primaryComponent M₂ P.asIdeal : Submodule A M₂)) P)
  (HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
    ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂))
Tactic: refine (Submodule.disjoint_def.mp (iSupIndep_primaryComponent A M₂ P)) _ ?_ ?_