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
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:
exact ⟨(Associates.mk P.asIdeal).count (Associates.mk (span {a})).factors, fun _ b ↦ hxmem _ b⟩
-- 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
⊢ Membership.mem (γ := Submodule A M) (primaryComponent M P.asIdeal) x

Tactic:
simp_all
-- 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
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
⊢ iSupIndep.{u_1 + 1, u_2} (α := Submodule A M) fun (P : HeightOneSpectrum A) ↦ primaryComponent M P.asIdeal

Tactic:
rw [iSupIndep_iff_finsetSum_eq_zero_imp_eq_zero]

Premises used: iSupIndep_iff_finsetSum_eq_zero_imp_eq_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
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, ∃ (n : ℕ), Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(i.asIdeal ^ n) : Set A)) (p i)

Tactic:
simp only [primaryComponent_mem] at hmem

Premises used: Ideal.primaryComponent_mem
-- 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
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)
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
⊢ ∀ i ∈ s, p i = 0

Tactic:
choose! f hmem using hmem
-- 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
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
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)
⊢ iSupIndep.{u_1 + 1, u_2} (α := Submodule A M) fun (i : HeightOneSpectrum A) ↦
    torsionBySet A M (↑(i.asIdeal ^ m) : Set A)

Tactic:
rw [iSupIndep_iff_supIndep]

Premises used: iSupIndep_iff_supIndep
-- 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
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
⊢ ∀ (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:
fun _ ↦ supIndep_torsionBySet_ideal
      fun _ _ _ _ hPQ ↦ (isCoprime_pow_of_ne _ _ hPQ _ _).sup_eq

Premises used: Submodule.supIndep_torsionBySet_ideal, IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne, IsCoprime.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
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
⊢ ∀ (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:
exact fun _ ↦ supIndep_torsionBySet_ideal
      fun _ _ _ _ hPQ ↦ (isCoprime_pow_of_ne _ _ hPQ _ _).sup_eq

Premises used: Submodule.supIndep_torsionBySet_ideal, IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne, IsCoprime.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
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)

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
-- 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
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)
⊢ ∀ (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

Premises used: iSupIndep_iff_finsetSum_eq_zero_imp_eq_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
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
apply : ∀ i ∈ s, Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(i.asIdeal ^ m) : Set A)) (p i)
⊢ ∀ i ∈ s, p i = 0

Tactic:
apply hSupIndep _ _ ?_ hsum
-- 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
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, Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(i.asIdeal ^ m) : Set A)) (p i)

Tactic:
fun P hP ↦ torsionBySet_le_torsionBySet_pow _ _ (Finset.le_sup hP) _ (hmem P hP)

Premises used: Set.Mem, IsDedekindDomain.HeightOneSpectrum.asIdeal, Submodule.torsionBySet_le_torsionBySet_pow, Finset.sup, Finset.le_sup
-- 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
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, Membership.mem (γ := Submodule A M) (torsionBySet A M (↑(i.asIdeal ^ m) : Set A)) (p i)

Tactic:
exact fun P hP ↦ torsionBySet_le_torsionBySet_pow _ _ (Finset.le_sup hP) _ (hmem P hP)

Premises used: IsDedekindDomain.HeightOneSpectrum.asIdeal, Submodule.torsionBySet_le_torsionBySet_pow, Finset.sup, Finset.le_sup
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
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 : M₁), (φ : (a : M₁) → M₂) a = y

Tactic:
hf y
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
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
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))
⊢ ∃ (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

Tactic:
obtain ⟨b, rfl⟩ : ∃ a, φ a = y := hf y

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
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₂)
⊢ ∃ (f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)),
    ((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

Tactic:
simp only [← mem_iSup_iff_exists_dfinsupp, iSup_primaryComponent_eq_top hM₁, mem_top]

Premises used: Submodule.mem_iSup_iff_exists_dfinsupp, Ideal.iSup_primaryComponent_eq_top, Submodule.mem_top
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
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₂)
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))
⊢ ∃ (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]

Premises used: IsDedekindDomain.HeightOneSpectrum
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
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))

Tactic:
⟨f P, Subtype.ext ?_⟩

Premises used: Exists.intro, DFunLike.coe, Subtype.ext
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
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
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₂)
⊢ ∃ (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:
refine ⟨f P, Subtype.ext ?_⟩
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
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
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₂)
⊢ 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:
simp only [map_apply_coe]

Premises used: Ideal.primaryComponent.map_apply_coe
-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
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
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
⊢ 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:
rw [eq_comm, ← sub_eq_zero]

Premises used: sub_eq_zero, eq_comm