awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Regular.IsSMulRegular (goal)
Goal:
R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
inst_5 : AddCommGroup M''
inst_6 : Module R M''
M''' : Type u_6
inst_7 : AddCommGroup M'''
inst_8 : Module R M'''
r : R
f₁ : M →ₗ[R] M'
f₂ : M' →ₗ[R] M''
f₃ : M'' →ₗ[R] M'''
h₁₂ : Exact.{u_3, u_4, u_5} (M := M) (N := M') (P := M'') (⇑f₁ : (a : M) → M') (⇑f₂ : (a : M') → M'')
h₂₃ : Exact.{u_4, u_5, u_6} (M := M') (N := M'') (P := M''') (⇑f₂ : (a : M') → M'') (⇑f₃ : (a : M'') → M''')
h : IsSMulRegular M''' r
this : IsSMulRegular.{u_1, u_5} (M'' ⧸ f₂.range) r
⊢ Exact.{u_3, u_4, u_5} (M := QuotSMulTop r M) (N := QuotSMulTop r M') (P := QuotSMulTop r M'')
    (⇑((HSMul.hSMul (β := Submodule R M) r ⊤).mapQ (HSMul.hSMul (β := Submodule R M') r ⊤) f₁ ⋯) :
      (a : QuotSMulTop r M) → QuotSMulTop r M')
    (⇑((HSMul.hSMul (β := Submodule R M') r ⊤).mapQ (HSMul.hSMul (β := Submodule R M'') r ⊤) f₂ ⋯) :
      (a : QuotSMulTop r M') → QuotSMulTop r M'')
have rw : HSMul.hSMul (β := Submodule R M'') r ⊤ ⊓ f₂.range ≤ r • f₂.range
Tactic: rw [Exact.exact_mapQ_iff h₁₂, map_pointwise_smul, Submodule.map_top, inf_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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
⊢ Subsingleton (N →ₗ[R] M)
have apply : ∀ (f : N →ₗ[R] M) (x : N), Eq.{u_2 + 1} (α := M) ((f : (a : N) → M) x : M) ((0 : (a : N) → M) x : M)
Tactic: apply subsingleton_of_forall_eq 0 (fun f ↦ ext fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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
have rw : HSMul.hSMul (β := M) r ((f : (a : N) → M) x : M) = 0
Tactic: rw [smul_zero, ← map_smul, Module.mem_annihilator.mp mem_ann x, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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
⊢ HSMul.hSMul (β := M) r ((f : (a : N) → M) x : M) = HSMul.hSMul (β := M) r 0
have rw₁ : Eq.{u_2 + 1} (α := M) ((f : (a : N) → M) (r • x) : M) (0 : M)
Tactic: rw [smul_zero, ← map_smul, Module.mem_annihilator.mp mem_ann x, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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)
⊢ HSMul.hSMul (β := M) r ((f : (a : N) → M) x : M) = HSMul.hSMul (β := M) r 0
have rw₂ : Eq.{u_2 + 1} (α := M) ((f : (a : N) → M) 0 : M) (0 : M)
Tactic: rw [smul_zero, ← map_smul, Module.mem_annihilator.mp mem_ann x, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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)
⊢ HSMul.hSMul (β := M) r ((f : (a : N) → M) x : M) = HSMul.hSMul (β := M) r 0
have rw₃ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [smul_zero, ← map_smul, Module.mem_annihilator.mp mem_ann x, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : N) → M) x : M) ((0 : (a : N) → M) x : M)
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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
have refine : ∀ (hom0 : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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)
⊢ ∃ (r : R), Membership.mem (γ := Ideal R) (annihilator R N) r ∧ IsSMulRegular M r
have inl : Subsingleton M → ∃ (r : R), Membership.mem (γ := Ideal R) (annihilator R N) r ∧ IsSMulRegular M r
Tactic: cases subsingleton_or_nontrivial M
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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
⊢ ∃ (r : R), Membership.mem (γ := Ideal R) (annihilator R N) r ∧ IsSMulRegular M r
have inr : Nontrivial M → ∃ (r : R), Membership.mem (γ := Ideal R) (annihilator R N) r ∧ IsSMulRegular M r
Tactic: cases subsingleton_or_nontrivial M
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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
⊢ ∃ (r : R), Membership.mem (γ := Ideal R) (annihilator R N) r ∧ IsSMulRegular M r
have inr : ∀ (h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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
have 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
Tactic: rcases associatedPrimes.nonempty R M with ⟨Ia, hIa⟩
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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
⊢ ∃ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p ∧ annihilator R N ≤ p
have apply : (↑(annihilator R N) : Set R) ⊆
  ⋃ (i : Ideal R), ⋃ (_ : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) i), (↑i : Set R)
Tactic: apply (Ideal.subset_union_prime_finite (associatedPrimes.finite R M) Ia Ia _).mp
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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)
⊢ ∃ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p ∧ annihilator R N ≤ p
have apply₁ : ∀ (i : Ideal R), Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) i → i ≠ Ia → i ≠ Ia → i.IsPrime
Tactic: apply (Ideal.subset_union_prime_finite (associatedPrimes.finite R M) Ia Ia _).mp
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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) ⊆
    ⋃ (i : Ideal R), ⋃ (_ : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) i), (↑i : Set R)
have rw : (↑(annihilator R N) : Set R) ⊆ {r : R | IsSMulRegular M r}ᶜ
Tactic: rw [biUnion_associatedPrimes_eq_compl_regular R M]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (hypothesis)
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
⊢ False
have hexist : ∃ (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
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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
⊢ False
have inr : ∀ (p : Ideal R) (pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p) (hp : annihilator R N ≤ p), False
Tactic: rcases hexist with ⟨p, pass, hp⟩
Cleared hypotheses: hexist
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (hypothesis)
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 := ⋯ }
⊢ False
have loc_ne_zero : 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
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (hypothesis)
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'
⊢ False
have loc_ne_zero₁ : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Tactic: rw [Module.mem_support_iff] at loc_ne_zero
Cleared hypotheses: loc_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (hypothesis)
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)) ⊤
⊢ False
have ntr : 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 _
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (hypothesis)
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))
⊢ False
have 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})
Tactic: have := isAssociatedPrime_iff.mp <| AssociatedPrimes.mem_iff.mp
      (associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes pass)
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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})
⊢ False
have 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
Tactic: rcases this.2 with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (hypothesis)
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})
⊢ False
have this₁ : Nontrivial (Dual p.ResidueField Nₚ')
Tactic: have : Nontrivial (Module.Dual p.ResidueField Nₚ') := by simpa using ntr
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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_1 :
  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})
this : Nontrivial (Dual p.ResidueField Nₚ')
⊢ False
have inr : ∀ (g : Dual p.ResidueField Nₚ') (hg : g ≠ 0), False
Tactic: rcases exists_ne (α := Module.Dual p.ResidueField Nₚ') 0 with ⟨g, hg⟩