awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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:
(Submodule.disjoint_def.mp (iSupIndep_primaryComponent A M₂ P)) _ ?_ ?_

Premises used: Ideal.iSupIndep_primaryComponent, Iff.mp, Submodule.disjoint_def
-- 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_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₂))
refine_2 :
  Membership.mem (γ := Submodule A M₂)
    (⨆ (j : HeightOneSpectrum A),
      ⨆ (_ : j ≠ P), (fun (P : HeightOneSpectrum A) ↦ (primaryComponent M₂ P.asIdeal : Submodule A M₂)) j)
    (HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
      ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂))
⊢ 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:
refine (Submodule.disjoint_def.mp (iSupIndep_primaryComponent A M₂ P)) _ ?_ ?_

Premises used: Ideal.iSupIndep_primaryComponent, Iff.mp, Submodule.disjoint_def
-- 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
⊢ 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:
Submodule.sub_mem _ hy (primaryComponent_map_mem _ _ _)

Premises used: Set.Mem, Ideal.primaryComponent_map_mem, Submodule.sub_mem
-- 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
⊢ 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:
exact Submodule.sub_mem _ hy (primaryComponent_map_mem _ _ _)

Premises used: Ideal.primaryComponent_map_mem, Submodule.sub_mem
-- 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
⊢ P ∉ f.support (β := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) →
    Eq.{u_6 + 1} (α := M₂)
      ((fun (P : HeightOneSpectrum A) ↦
          ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂))
        P)
      0

Tactic:
aesop
-- 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 :
  Eq.{u_6 + 1} (α := M₂) ((φ : (a : M₁) → M₂) b : M₂)
    (∑ x ∈ f.support (β := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)),
        (φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) x) : M₁) :
      M₂)
⊢ HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
      ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂) =
    ∑ Q ∈ f.support (β := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) \ {P},
      (φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) Q) : M₁)

Tactic:
rw [sub_eq_iff_eq_add', ← Finset.sum_eq_add_sum_diff_singleton P (fun P ↦ φ (f P)) (by aesop)]

Premises used: Finset.sum_eq_add_sum_diff_singleton, Subtype.val, DFunLike.coe, sub_eq_iff_eq_add'
-- 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
⊢ Eq.{u_6 + 1} (α := M₂) ((φ : (a : M₁) → M₂) b : M₂)
    (∑ x ∈ f.support (β := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)),
        (φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) x) : M₁) :
      M₂)

Tactic:
simpa [DFinsupp.sumAddHom_apply, DFinsupp.sum] using congr(φ $hf).symm

Premises used: congrArg, id, DFinsupp.sum, DFinsupp.sumAddHom_apply, Eq.symm, DFunLike.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
⊢ HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
      ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂) =
    ∑ Q ∈ f.support (β := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) \ {P},
      (φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) Q) : M₁)

Tactic:
have hdiff : φ b - φ ↑(f P) = ∑ Q ∈ f.support \ {P}, φ ↑(f Q) := by
      rw [sub_eq_iff_eq_add', ← Finset.sum_eq_add_sum_diff_singleton P (fun P ↦ φ (f P)) (by aesop)]
      simpa [DFinsupp.sumAddHom_apply, DFinsupp.sum] using congr(φ $hf).symm
-- 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
hdiff :
  HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
      ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂) =
    ∑ Q ∈ f.support (β := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) \ {P},
      (φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) Q) : M₁)
refine_2 :
  Membership.mem (γ := Submodule A M₂)
    (⨆ (j : HeightOneSpectrum A),
      ⨆ (_ : j ≠ P), (fun (P : HeightOneSpectrum A) ↦ (primaryComponent M₂ P.asIdeal : Submodule A M₂)) j)
    (∑ Q ∈ f.support (β := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) \ {P},
      (φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) Q) : M₁))
⊢ Membership.mem (γ := Submodule A M₂)
    (⨆ (j : HeightOneSpectrum A),
      ⨆ (_ : j ≠ P), (fun (P : HeightOneSpectrum A) ↦ (primaryComponent M₂ P.asIdeal : Submodule A M₂)) j)
    (HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
      ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂))

Tactic:
rw [hdiff]
-- 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
hdiff :
  HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
      ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂) =
    ∑ Q ∈ f.support (β := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) \ {P},
      (φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) Q) : M₁)
Q : HeightOneSpectrum A
hQ : Q ∈ f.support (β := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) \ {P}
⊢ Q ≠ P

Tactic:
grind
-- 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
hdiff :
  HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
      ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂) =
    ∑ Q ∈ f.support (β := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) \ {P},
      (φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) Q) : M₁)
⊢ Membership.mem (γ := Submodule A M₂)
    (⨆ (j : HeightOneSpectrum A),
      ⨆ (_ : j ≠ P), (fun (P : HeightOneSpectrum A) ↦ (primaryComponent M₂ P.asIdeal : Submodule A M₂)) j)
    (∑ Q ∈ f.support (β := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) \ {P},
      (φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) Q) : M₁))

Tactic:
exact Submodule.sum_mem _ fun Q hQ ↦ Submodule.mem_iSup_of_mem Q <|
        Submodule.mem_iSup_of_mem (by grind) (primaryComponent_map_mem _ _ _)

Premises used: Submodule.sum_mem, Submodule.mem_iSup_of_mem
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
R : Type u_4
inst : Zero R
inst_1 : Zero β
inst_2 : SMul R β
inst_3 : NoZeroSMulDivisors R β
extract_lets :
  let this := e.zero;
  let this_1 := Equiv.smul R e;
  NoZeroSMulDivisors R α
⊢ let this := e.zero;
  let this_1 := Equiv.smul R e;
  NoZeroSMulDivisors R α

Tactic:
extract_lets
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
R : Type u_4
inst : Zero R
inst_1 : Zero β
inst_2 : SMul R β
inst_3 : NoZeroSMulDivisors R β
this : Zero α := e.zero
this_1 : SMul R α := Equiv.smul R e
⊢ NoZeroSMulDivisors R α

Tactic:
⟨fun {r} m ↦ ?_⟩

Premises used: NoZeroSMulDivisors.mk
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
R : Type u_4
inst : Zero R
inst_1 : Zero β
inst_2 : SMul R β
inst_3 : NoZeroSMulDivisors R β
this : Zero α := e.zero
this_1 : SMul R α := Equiv.smul R e
refine : ∀ {r : R} (m : α), r • m = 0 → r = 0 ∨ m = 0
⊢ NoZeroSMulDivisors R α

Tactic:
refine ⟨fun {r} m ↦ ?_⟩
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
R : Type u_4
inst : Zero R
inst_1 : Zero β
inst_2 : SMul R β
inst_3 : NoZeroSMulDivisors R β
this : Zero α := e.zero
this_1 : SMul R α := Equiv.smul R e
r : R
m : α
⊢ r • m = 0 → r = 0 ∨ m = 0

Tactic:
simpa [smul_def, zero_def, Equiv.eq_symm_apply] using eq_zero_or_eq_zero_of_smul_eq_zero

Premises used: NoZeroSMulDivisors.eq_zero_or_eq_zero_of_smul_eq_zero, Equiv.zero_def, Equiv.smul_def, Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
e_1 e : α ≃ β
inst_1 : AddCommMonoid β
inst_2 : Module R β
this : AddCommMonoid α := e.addCommMonoid
⊢ ∀ (r s : R) (x : α), (r + s) • x = r • x + s • x

Tactic:
simp [add_def, smul_def, add_smul]

Premises used: Equiv.add_def, Equiv.smul_def, add_smul
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
e_1 e : α ≃ β
inst_1 : AddCommMonoid β
inst_2 : Module R β
this : AddCommMonoid α := e.addCommMonoid
⊢ ∀ (x : α), HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 x = 0

Tactic:
simp [smul_def, zero_smul, zero_def]

Premises used: Equiv.zero_def, Equiv.smul_def, zero_smul
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
e_1 e : α ≃ β
inst_1 : AddCommMonoid β
inst_2 : Module R β
this : AddCommMonoid α := e.addCommMonoid
module : Module R α := Equiv.module R e
r : R
x : α
a :
  Eq.{u_2 + 1} (α := α) ((e.symm : (a : β) → α) ((AddEquiv.toEquiv e.addEquiv).toFun (r • x)) : α)
    ((e.symm : (a : β) → α)
        (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) ((AddEquiv.toEquiv e.addEquiv).toFun x)) :
      α)
⊢ (AddEquiv.toEquiv e.addEquiv).toFun (r • x) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) ((AddEquiv.toEquiv e.addEquiv).toFun x)

Tactic:
apply e.symm.injective

Premises used: Equiv.injective, Equiv.symm
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
e_1 e : α ≃ β
inst_1 : AddCommMonoid β
inst_2 : Module R β
this : AddCommMonoid α := e.addCommMonoid
module : Module R α := Equiv.module R e
r : R
x : α
a :
  (AddEquiv.toEquiv e.addEquiv : (a : α) → β) (r • x) =
    HSMul.hSMul (β := β) r ((AddEquiv.toEquiv e.addEquiv : (a : α) → β) x : β)
⊢ Eq.{u_2 + 1} (α := α) ((e.symm : (a : β) → α) ((AddEquiv.toEquiv e.addEquiv).toFun (r • x)) : α)
    ((e.symm : (a : β) → α)
        (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) ((AddEquiv.toEquiv e.addEquiv).toFun x)) :
      α)

Tactic:
simp only [toFun_as_coe, RingHom.id_apply, EmbeddingLike.apply_eq_iff_eq]

Premises used: RingHom.id_apply, Equiv.toFun_as_coe, EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
e_1 e : α ≃ β
inst_1 : AddCommMonoid β
inst_2 : Module R β
this : AddCommMonoid α := e.addCommMonoid
module : Module R α := Equiv.module R e
r : R
x : α
⊢ (AddEquiv.toEquiv e.addEquiv : (a : α) → β) (r • x) =
    HSMul.hSMul (β := β) r ((AddEquiv.toEquiv e.addEquiv : (a : α) → β) x : β)

Tactic:
Iff.mpr (apply_eq_iff_eq_symm_apply _) rfl

Premises used: Iff.mpr, rfl, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
e_1 e : α ≃ β
inst_1 : AddCommMonoid β
inst_2 : Module R β
this : AddCommMonoid α := e.addCommMonoid
module : Module R α := Equiv.module R e
r : R
x : α
⊢ (AddEquiv.toEquiv e.addEquiv : (a : α) → β) (r • x) =
    HSMul.hSMul (β := β) r ((AddEquiv.toEquiv e.addEquiv : (a : α) → β) x : β)

Tactic:
exact Iff.mpr (apply_eq_iff_eq_symm_apply _) rfl

Premises used: Iff.mpr, rfl, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
e : α ≃ β
inst_1 : AddCommMonoid β
inst_2 : Module R β
inst_3 : Module.IsTorsionFree R β
extract_lets :
  let this := e.addCommMonoid;
  let this_1 : Module R α := Equiv.module R e;
  Module.IsTorsionFree R α
⊢ let this := e.addCommMonoid;
  let this_1 : Module R α := Equiv.module R e;
  Module.IsTorsionFree R α

Tactic:
extract_lets
-- Module: Mathlib.Algebra.Module.TransferInstance
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
e : α ≃ β
inst_1 : AddCommMonoid β
inst_2 : Module R β
inst_3 : Module.IsTorsionFree R β
this : AddCommMonoid α := e.addCommMonoid
this_1 : Module R α := Equiv.module R e
⊢ ∀ (r : R) (m : α),
    (linearEquiv R e : (a : α) → β) (r • m) = HSMul.hSMul (β := β) r ((linearEquiv R e : (a : α) → β) m : β)

Tactic:
simp