awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
r : R
reg : IsSMulRegular M r
mem_ann : Membership.mem (γ := Ideal R) (annihilator R N) r
f : N →ₗ[R] M
x : N
rw : HSMul.hSMul (β := M) r ((f : (a : N) → M) x : M) = 0
rw₁ : Eq.{u_2 + 1} (α := M) ((f : (a : N) → M) (r • x) : M) (0 : M)
rw₂ : Eq.{u_2 + 1} (α := M) ((f : (a : N) → M) 0 : M) (0 : M)
rw₃ rw₄ : Eq.{u_2 + 1} (α := M) 0 0
⊢ HSMul.hSMul (β := M) r ((f : (a : N) → M) x : M) = HSMul.hSMul (β := M) r 0

Tactic:
rw [smul_zero, ← map_smul, Module.mem_annihilator.mp mem_ann x, map_zero]

Premises used: Module.mem_annihilator, smul_zero, map_zero, Iff.mp, map_smul
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
r : R
reg : IsSMulRegular M r
mem_ann : Membership.mem (γ := Ideal R) (annihilator R N) r
f : N →ₗ[R] M
x : N
⊢ HSMul.hSMul (β := M) r ((f : (a : N) → M) x : M) = HSMul.hSMul (β := M) r 0

Tactic:
have : r • (f x) = r • 0 := by
    rw [smul_zero, ← map_smul, Module.mem_annihilator.mp mem_ann x, map_zero]
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
r : R
reg : IsSMulRegular M r
mem_ann : Membership.mem (γ := Ideal R) (annihilator R N) r
f : N →ₗ[R] M
x : N
this : HSMul.hSMul (β := M) r ((f : (a : N) → M) x : M) = HSMul.hSMul (β := M) r 0
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : N) → M) x : M) ((0 : (a : N) → M) x : M)

Tactic:
simpa using reg this
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
⊢ Subsingleton (N →ₗ[R] M) ↔ ∃ (r : R), Membership.mem (γ := Ideal R) (annihilator R N) r ∧ IsSMulRegular M r

Tactic:
⟨fun hom0 ↦ ?_, fun ⟨r, mem_ann, reg⟩ ↦
    linearMap_subsingleton_of_mem_annihilator reg mem_ann⟩

Premises used: _private.0.IsSMulRegular.subsingleton_linearMap_iff.match_1, IsSMulRegular.linearMap_subsingleton_of_mem_annihilator, LinearMap, Iff.intro, Subsingleton, RingHom.id
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
refine :
  ∀ (hom0 : Subsingleton (N →ₗ[R] M)), ∃ (r : R), Membership.mem (γ := Ideal R) (annihilator R N) r ∧ IsSMulRegular M r
⊢ Subsingleton (N →ₗ[R] M) ↔ ∃ (r : R), Membership.mem (γ := Ideal R) (annihilator R N) r ∧ IsSMulRegular M r

Tactic:
refine ⟨fun hom0 ↦ ?_, fun ⟨r, mem_ann, reg⟩ ↦
    linearMap_subsingleton_of_mem_annihilator reg mem_ann⟩
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
inl : Subsingleton M → ∃ (r : R), Membership.mem (γ := Ideal R) (annihilator R N) r ∧ IsSMulRegular M r
inr : Nontrivial M → ∃ (r : R), Membership.mem (γ := Ideal R) (annihilator R N) r ∧ IsSMulRegular M r
⊢ ∃ (r : R), Membership.mem (γ := Ideal R) (annihilator R N) r ∧ IsSMulRegular M r

Tactic:
cases subsingleton_or_nontrivial M

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h : Subsingleton M
⊢ ∃ (r : R), Membership.mem (γ := Ideal R) (annihilator R N) r ∧ IsSMulRegular M r

Tactic:
⟨0, ⟨Submodule.zero_mem (Module.annihilator R N), IsSMulRegular.zero⟩⟩

Premises used: Module.annihilator, IsSMulRegular.zero, Submodule.zero_mem, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h : Subsingleton M
⊢ ∃ (r : R), Membership.mem (γ := Ideal R) (annihilator R N) r ∧ IsSMulRegular M r

Tactic:
exact ⟨0, ⟨Submodule.zero_mem (Module.annihilator R N), IsSMulRegular.zero⟩⟩
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h : Nontrivial M
inr : ∀ (h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r), False
⊢ ∃ (r : R), Membership.mem (γ := Ideal R) (annihilator R N) r ∧ IsSMulRegular M r

Tactic:
by_contra! h
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
rcases :
  ∀ (Ia : Ideal R) (hIa : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) Ia),
    ∃ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p ∧ annihilator R N ≤ p
⊢ ∃ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p ∧ annihilator R N ≤ p

Tactic:
rcases associatedPrimes.nonempty R M with ⟨Ia, hIa⟩

Premises used: associatedPrimes.nonempty
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
Ia : Ideal R
hIa : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) Ia
apply :
  (↑(annihilator R N) : Set R) ⊆
    ⋃ (i : Ideal R), ⋃ (_ : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) i), (↑i : Set R)
apply₁ : ∀ (i : Ideal R), Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) i → i ≠ Ia → i ≠ Ia → i.IsPrime
⊢ ∃ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p ∧ annihilator R N ≤ p

Tactic:
apply (Ideal.subset_union_prime_finite (associatedPrimes.finite R M) Ia Ia _).mp

Premises used: associatedPrimes.finite, Ideal.subset_union_prime_finite, Iff.mp
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
Ia : Ideal R
hIa : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) Ia
rw : (↑(annihilator R N) : Set R) ⊆ {r : R | IsSMulRegular M r}ᶜ
⊢ (↑(annihilator R N) : Set R) ⊆
    ⋃ (i : Ideal R), ⋃ (_ : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) i), (↑i : Set R)

Tactic:
rw [biUnion_associatedPrimes_eq_compl_regular R M]

Premises used: biUnion_associatedPrimes_eq_compl_regular
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
Ia : Ideal R
hIa : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) Ia
⊢ (↑(annihilator R N) : Set R) ⊆ {r : R | IsSMulRegular M r}ᶜ

Tactic:
fun r hr ↦ h r hr

Premises used: Set.Mem, setOf, Set.Subset, IsSMulRegular, Function.Injective, Not
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
Ia : Ideal R
hIa : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) Ia
⊢ (↑(annihilator R N) : Set R) ⊆ {r : R | IsSMulRegular M r}ᶜ

Tactic:
exact fun r hr ↦ h r hr
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
Ia : Ideal R
hIa : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) Ia
⊢ ∀ (i : Ideal R), Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) i → i ≠ Ia → i ≠ Ia → i.IsPrime

Tactic:
fun I hin _ _ ↦ IsAssociatedPrime.isPrime hin

Premises used: IsAssociatedPrime.isPrime
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
Ia : Ideal R
hIa : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) Ia
⊢ ∀ (i : Ideal R), Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) i → i ≠ Ia → i ≠ Ia → i.IsPrime

Tactic:
exact fun I hin _ _ ↦ IsAssociatedPrime.isPrime hin

Premises used: IsAssociatedPrime.isPrime
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
⊢ ∃ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p ∧ annihilator R N ≤ p

Tactic:
have hexist : ∃ p ∈ associatedPrimes R M, Module.annihilator R N ≤ p := by
      rcases associatedPrimes.nonempty R M with ⟨Ia, hIa⟩
      apply (Ideal.subset_union_prime_finite (associatedPrimes.finite R M) Ia Ia _).mp
      · rw [biUnion_associatedPrimes_eq_compl_regular R M]
        exact fun r hr ↦ h r hr
      · exact fun I hin _ _ ↦ IsAssociatedPrime.isPrime hin
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
hexist : ∃ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p ∧ annihilator R N ≤ p
inr :
  ∀ (p : Ideal R) (pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p) (hp : annihilator R N ≤ p),
    False
⊢ False

Tactic:
rcases hexist with ⟨p, pass, hp⟩
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R N) p'

Tactic:
have loc_ne_zero : p' ∈ Module.support R N := Module.mem_support_iff_of_finite.mpr hp
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Membership.mem (γ := Set (PrimeSpectrum R)) (support R N) p'
⊢ Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)

Tactic:
rw [Module.mem_support_iff] at loc_ne_zero

Premises used: Module.mem_support_iff
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) :=
  Nₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
⊢ Nontrivial Nₚ'

Tactic:
have ntr : Nontrivial Nₚ' :=
      Submodule.Quotient.nontrivial_iff.mpr <| .symm <|
        Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator <|
          IsLocalRing.maximalIdeal_le_jacobson _
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) :=
  Nₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) :=
  Mₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Mₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
x : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
⊢ Ideal.IsPrime.{u_1} (α := Localization.AtPrime p) (maximalIdeal (Localization.AtPrime p)) ∧
    ∃ (x : LocalizedModule.AtPrime p M),
      Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
        (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})

Tactic:
have := isAssociatedPrime_iff.mp <| AssociatedPrimes.mem_iff.mp
      (associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes pass)
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) :=
  Nₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) :=
  Mₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Mₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
x : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this :
  Ideal.IsPrime.{u_1} (α := Localization.AtPrime p) (maximalIdeal (Localization.AtPrime p)) ∧
    ∃ (x : LocalizedModule.AtPrime p M),
      Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
        (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
inr :
  ∀ (x : LocalizedModule.AtPrime p M)
    (hx :
      Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
        (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})),
    False
⊢ False

Tactic:
rcases this.2 with ⟨x, hx⟩

Premises used: And.right
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) :=
  Nₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) :=
  Mₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Mₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
x_1 : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this :
  Ideal.IsPrime.{u_1} (α := Localization.AtPrime p) (maximalIdeal (Localization.AtPrime p)) ∧
    ∃ (x : LocalizedModule.AtPrime p M),
      Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
        (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
x : LocalizedModule.AtPrime p M
hx :
  Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
    (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
⊢ Nontrivial (Dual p.ResidueField Nₚ')

Tactic:
simpa using ntr
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) :=
  Nₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) :=
  Mₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Mₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
x_1 : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this :
  Ideal.IsPrime.{u_1} (α := Localization.AtPrime p) (maximalIdeal (Localization.AtPrime p)) ∧
    ∃ (x : LocalizedModule.AtPrime p M),
      Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
        (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
x : LocalizedModule.AtPrime p M
hx :
  Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
    (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
⊢ Nontrivial (Dual p.ResidueField Nₚ')

Tactic:
have : Nontrivial (Module.Dual p.ResidueField Nₚ') := by simpa using ntr