awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : x ∉ I
h :
  ∀ {y : R},
    Membership.mem (γ := Ideal R)
        (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
      y * x ∈ I
y : R
hy :
  Membership.mem (γ := Submodule R R)
    (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y
⊢ y ∈ I.radical
have rw : y ∈ (colon I ⊤).radical
Tactic: rw [← I.colon_univ, ← Set.top_eq_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
⊢ Eq (α := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) {I.radical}
have h : ∀ (J : Ideal R),
  Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) J ↔ Membership.mem (γ := Set (Ideal R)) {I.radical} J
Tactic: ext J
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
J : Ideal R
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) J ↔ J = I.radical
have h : J = I.radical → Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) J
Tactic: refine ⟨IsAssociatedPrime.eq_radical hI, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
⊢ Nontrivial.{u_1} (R ⧸ I)
have refine : Ne (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) 1) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) 0)
Tactic: refine ⟨(Ideal.Quotient.mk I :) 1, (Ideal.Quotient.mk I :) 0, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
⊢ Ne (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) 1) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) 0)
have rw : ¬I = ⊤
Tactic: rw [Ne, Ideal.Quotient.eq, sub_zero, ← Ideal.eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) I.radical
have this : Nontrivial.{u_1} (R ⧸ I)
Tactic: haveI : Nontrivial (R ⧸ I) := by
    refine ⟨(Ideal.Quotient.mk I :) 1, (Ideal.Quotient.mk I :) 0, ?_⟩
    rw [Ne, Ideal.Quotient.eq, sub_zero, ← Ideal.eq_top_iff_one]
    exact hI.1
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
this : Nontrivial.{u_1} (R ⧸ I)
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) I.radical
have h : ∀ (a : Ideal R) (ha : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) a),
  Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) I.radical
Tactic: obtain ⟨a, ha⟩ := associatedPrimes.nonempty R (R ⧸ I)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (hypothesis)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
⊢ N₁.IsQuotientEquivQuotientPrime N₂ ↔
    ∃ (x : M),
      Ideal.IsPrime.{u} (α := A)
          (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
        N₂ = N₁ ⊔ A ∙ x
have hf₁ : f.ker = ⊥
Tactic: have hf₁ : ker f = ⊥ := ker_liftQ_eq_bot _ _ _ (by simp [ker_comp, submoduleOf])
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (hypothesis)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
⊢ N₁.IsQuotientEquivQuotientPrime N₂ ↔
    ∃ (x : M),
      Ideal.IsPrime.{u} (α := A)
          (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
        N₂ = N₁ ⊔ A ∙ x
have hf₂ : f.range = map N₁.mkQ N₂
Tactic: have hf₂ : range f = N₂.map N₁.mkQ := by simp [f, mapQ, range_liftQ, range_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
⊢ N₁.IsQuotientEquivQuotientPrime N₂ ↔
    ∃ (x : M),
      Ideal.IsPrime.{u} (α := A)
          (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
        N₂ = N₁ ⊔ A ∙ x
have refine_1 : N₁.IsQuotientEquivQuotientPrime N₂ →
  ∀ (h : N₁ ≤ N₂) (p : PrimeSpectrum A)
    (e : LinearEquiv.{u, u, v, u} (RingHom.id A) (↥N₂ ⧸ N₁.submoduleOf N₂) (A ⧸ p.asIdeal)),
    ∃ (x : M),
      Ideal.IsPrime.{u} (α := A)
          (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
        N₂ = N₁ ⊔ A ∙ x
Tactic: refine ⟨fun ⟨h, p, ⟨e⟩⟩ ↦ ?_, fun ⟨x, hx, hx'⟩ ↦ ⟨le_sup_left.trans_eq hx'.symm, ⟨_, hx⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
refine_1 :
  N₁.IsQuotientEquivQuotientPrime N₂ →
    ∀ (h : N₁ ≤ N₂) (p : PrimeSpectrum A)
      (e : LinearEquiv.{u, u, v, u} (RingHom.id A) (↥N₂ ⧸ N₁.submoduleOf N₂) (A ⧸ p.asIdeal)),
      ∃ (x : M),
        Ideal.IsPrime.{u} (α := A)
            (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
          N₂ = N₁ ⊔ A ∙ x
⊢ N₁.IsQuotientEquivQuotientPrime N₂ ↔
    ∃ (x : M),
      Ideal.IsPrime.{u} (α := A)
          (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
        N₂ = N₁ ⊔ A ∙ x
have refine_2 : (∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x) →
  ∀ (x : M)
    (hx :
      Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))))
    (hx' : N₂ = N₁ ⊔ A ∙ x),
    Nonempty
      (LinearEquiv.{u, u, v, u} (RingHom.id A) (↥N₂ ⧸ N₁.submoduleOf N₂)
        (A ⧸
          { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)),
              isPrime := hx : PrimeSpectrum A }.asIdeal))
Tactic: refine ⟨fun ⟨h, p, ⟨e⟩⟩ ↦ ?_, fun ⟨x, hx, hx'⟩ ↦ ⟨le_sup_left.trans_eq hx'.symm, ⟨_, hx⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h_1 : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : LinearEquiv.{u, u, v, u} (RingHom.id A) (↥N₂ ⧸ N₁.submoduleOf N₂) (A ⧸ p.asIdeal)
⊢ ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
have refine_1 : ∀ (x : M) (hx : x ∈ N₂)
  (hx' :
    Eq (α := ↥N₂ ⧸ N₁.submoduleOf N₂)
      (((N₁.submoduleOf N₂).mkQ : (a : ↥N₂) → ↥N₂ ⧸ N₁.submoduleOf N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hx) :
        ↥N₂ ⧸ N₁.submoduleOf N₂)
      ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1 : ↥N₂ ⧸ N₁.submoduleOf N₂)),
  ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
Tactic: obtain ⟨⟨x, hx⟩, hx'⟩ := Submodule.mkQ_surjective _ (e.symm 1)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (hypothesis)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h_1 : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : LinearEquiv.{u, u, v, u} (RingHom.id A) (↥N₂ ⧸ N₁.submoduleOf N₂) (A ⧸ p.asIdeal)
x : M
hx : x ∈ N₂
hx' :
  Eq (α := ↥N₂ ⧸ N₁.submoduleOf N₂)
    (((N₁.submoduleOf N₂).mkQ : (a : ↥N₂) → ↥N₂ ⧸ N₁.submoduleOf N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hx) :
      ↥N₂ ⧸ N₁.submoduleOf N₂)
    ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1 : ↥N₂ ⧸ N₁.submoduleOf N₂)
⊢ ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
have hx'' : Eq (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)
  ((f : (a : ↥N₂ ⧸ N₁.submoduleOf N₂) → M ⧸ N₁) ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1) : M ⧸ N₁)
Tactic: have hx'' : N₁.mkQ x = f (e.symm 1) := by simp [f, ← hx']
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h_1 : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : LinearEquiv.{u, u, v, u} (RingHom.id A) (↥N₂ ⧸ N₁.submoduleOf N₂) (A ⧸ p.asIdeal)
x : M
hx : x ∈ N₂
hx' :
  Eq (α := ↥N₂ ⧸ N₁.submoduleOf N₂)
    (((N₁.submoduleOf N₂).mkQ : (a : ↥N₂) → ↥N₂ ⧸ N₁.submoduleOf N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hx) :
      ↥N₂ ⧸ N₁.submoduleOf N₂)
    ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1 : ↥N₂ ⧸ N₁.submoduleOf N₂)
hx'' :
  Eq (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)
    ((f : (a : ↥N₂ ⧸ N₁.submoduleOf N₂) → M ⧸ N₁) ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1) : M ⧸ N₁)
⊢ ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
have refine_1 : Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))
Tactic: refine ⟨x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h_1 : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : LinearEquiv.{u, u, v, u} (RingHom.id A) (↥N₂ ⧸ N₁.submoduleOf N₂) (A ⧸ p.asIdeal)
x : M
hx : x ∈ N₂
hx' :
  Eq (α := ↥N₂ ⧸ N₁.submoduleOf N₂)
    (((N₁.submoduleOf N₂).mkQ : (a : ↥N₂) → ↥N₂ ⧸ N₁.submoduleOf N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hx) :
      ↥N₂ ⧸ N₁.submoduleOf N₂)
    ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1 : ↥N₂ ⧸ N₁.submoduleOf N₂)
hx'' :
  Eq (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)
    ((f : (a : ↥N₂ ⧸ N₁.submoduleOf N₂) → M ⧸ N₁) ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1) : M ⧸ N₁)
refine_1 :
  Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))
⊢ ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
have refine_1₁ : N₂ = N₁ ⊔ A ∙ x
Tactic: refine ⟨x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h_1 : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : LinearEquiv.{u, u, v, u} (RingHom.id A) (↥N₂ ⧸ N₁.submoduleOf N₂) (A ⧸ p.asIdeal)
x : M
hx : x ∈ N₂
hx' :
  Eq (α := ↥N₂ ⧸ N₁.submoduleOf N₂)
    (((N₁.submoduleOf N₂).mkQ : (a : ↥N₂) → ↥N₂ ⧸ N₁.submoduleOf N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hx) :
      ↥N₂ ⧸ N₁.submoduleOf N₂)
    ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1 : ↥N₂ ⧸ N₁.submoduleOf N₂)
hx'' :
  Eq (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)
    ((f : (a : ↥N₂ ⧸ N₁.submoduleOf N₂) → M ⧸ N₁) ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1) : M ⧸ N₁)
⊢ Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))
have h₁ : colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)) = p.asIdeal
Tactic: convert! p.2
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h_1 : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : LinearEquiv.{u, u, v, u} (RingHom.id A) (↥N₂ ⧸ N₁.submoduleOf N₂) (A ⧸ p.asIdeal)
x : M
hx : x ∈ N₂
hx' :
  Eq (α := ↥N₂ ⧸ N₁.submoduleOf N₂)
    (((N₁.submoduleOf N₂).mkQ : (a : ↥N₂) → ↥N₂ ⧸ N₁.submoduleOf N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hx) :
      ↥N₂ ⧸ N₁.submoduleOf N₂)
    ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1 : ↥N₂ ⧸ N₁.submoduleOf N₂)
hx'' :
  Eq (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)
    ((f : (a : ↥N₂ ⧸ N₁.submoduleOf N₂) → M ⧸ N₁) ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1) : M ⧸ N₁)
⊢ colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)) = p.asIdeal
have h₁ : ∀ (r : A),
  Membership.mem (γ := Ideal A)
      (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) r ↔
    r ∈ p.asIdeal
Tactic: ext r
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h_1 : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : LinearEquiv.{u, u, v, u} (RingHom.id A) (↥N₂ ⧸ N₁.submoduleOf N₂) (A ⧸ p.asIdeal)
x : M
hx : x ∈ N₂
hx' :
  Eq (α := ↥N₂ ⧸ N₁.submoduleOf N₂)
    (((N₁.submoduleOf N₂).mkQ : (a : ↥N₂) → ↥N₂ ⧸ N₁.submoduleOf N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hx) :
      ↥N₂ ⧸ N₁.submoduleOf N₂)
    ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1 : ↥N₂ ⧸ N₁.submoduleOf N₂)
hx'' :
  Eq (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)
    ((f : (a : ↥N₂ ⧸ N₁.submoduleOf N₂) → M ⧸ N₁) ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1) : M ⧸ N₁)
⊢ N₂ = N₁ ⊔ A ∙ x
have refine_1 : N₂ ≤ N₁ ⊔ A ∙ x
Tactic: refine le_antisymm ?_ (sup_le h ((span_singleton_le_iff_mem _ _).mpr hx))
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (hypothesis)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h_1 : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : LinearEquiv.{u, u, v, u} (RingHom.id A) (↥N₂ ⧸ N₁.submoduleOf N₂) (A ⧸ p.asIdeal)
x : M
hx : x ∈ N₂
hx' :
  Eq (α := ↥N₂ ⧸ N₁.submoduleOf N₂)
    (((N₁.submoduleOf N₂).mkQ : (a : ↥N₂) → ↥N₂ ⧸ N₁.submoduleOf N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hx) :
      ↥N₂ ⧸ N₁.submoduleOf N₂)
    ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1 : ↥N₂ ⧸ N₁.submoduleOf N₂)
hx'' :
  Eq (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)
    ((f : (a : ↥N₂ ⧸ N₁.submoduleOf N₂) → M ⧸ N₁) ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1) : M ⧸ N₁)
⊢ N₂ ≤ N₁ ⊔ A ∙ x
have this : map N₁.mkQ (A ∙ x) = map f (map (↑e.symm : A ⧸ p.asIdeal →ₗ[A] ↥N₂ ⧸ N₁.submoduleOf N₂) (A ∙ 1))
Tactic: have : (span A {x}).map N₁.mkQ = ((span A {1}).map e.symm.toLinearMap).map f := by
        simp only [map_span, Set.image_singleton, hx'', LinearEquiv.coe_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h_1 : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : LinearEquiv.{u, u, v, u} (RingHom.id A) (↥N₂ ⧸ N₁.submoduleOf N₂) (A ⧸ p.asIdeal)
x : M
hx : x ∈ N₂
hx' :
  Eq (α := ↥N₂ ⧸ N₁.submoduleOf N₂)
    (((N₁.submoduleOf N₂).mkQ : (a : ↥N₂) → ↥N₂ ⧸ N₁.submoduleOf N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hx) :
      ↥N₂ ⧸ N₁.submoduleOf N₂)
    ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1 : ↥N₂ ⧸ N₁.submoduleOf N₂)
hx'' :
  Eq (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)
    ((f : (a : ↥N₂ ⧸ N₁.submoduleOf N₂) → M ⧸ N₁) ((e.symm : (a : A ⧸ p.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂) 1) : M ⧸ N₁)
this : map N₁.mkQ (A ∙ x) = map f (map (↑e.symm : A ⧸ p.asIdeal →ₗ[A] ↥N₂ ⧸ N₁.submoduleOf N₂) (A ∙ 1))
⊢ N₂ ≤ N₁ ⊔ A ∙ x
have refine_1 : map N₁.mkQ N₂ ≤ map f (map (↑e.symm : A ⧸ p.asIdeal →ₗ[A] ↥N₂ ⧸ N₁.submoduleOf N₂) (A ∙ 1))
Tactic: rw [← N₁.ker_mkQ, sup_comm, ← comap_map_eq, ← map_le_iff_le_comap, this]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (hypothesis)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h :
  ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
x : M
hx :
  Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))
hx' : N₂ = N₁ ⊔ A ∙ x
⊢ Nonempty
    (LinearEquiv.{u, u, v, u} (RingHom.id A) (↥N₂ ⧸ N₁.submoduleOf N₂)
      (A ⧸
        { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)),
            isPrime := hx : PrimeSpectrum A }.asIdeal))
have hxN₂ : x ∈ N₂
Tactic: have hxN₂ : x ∈ N₂ := (le_sup_right.trans_eq hx'.symm) (mem_span_singleton_self x)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h :
  ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
x : M
hx :
  Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
⊢ Nonempty
    (LinearEquiv.{u, u, v, u} (RingHom.id A) (↥N₂ ⧸ N₁.submoduleOf N₂)
      (A ⧸
        { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)),
            isPrime := hx : PrimeSpectrum A }.asIdeal))
have refine_2 : { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)), isPrime := hx :
      PrimeSpectrum A }.asIdeal ≤
  comap (toSpanSingleton A (↥N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hxN₂)) (N₁.submoduleOf N₂)
Tactic: refine ⟨.symm (.ofBijective (Submodule.mapQ _ _ (toSpanSingleton A _ ⟨x, hxN₂⟩) ?_) ⟨?_, ?_⟩)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness (goal)
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
h :
  ∃ (x : M),
    Ideal.IsPrime.{u} (α := A)
        (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
      N₂ = N₁ ⊔ A ∙ x
x : M
hx :
  Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
refine_2 :
  { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)), isPrime := hx :
        PrimeSpectrum A }.asIdeal ≤
    comap (toSpanSingleton A (↥N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hxN₂)) (N₁.submoduleOf N₂)
⊢ Nonempty
    (LinearEquiv.{u, u, v, u} (RingHom.id A) (↥N₂ ⧸ N₁.submoduleOf N₂)
      (A ⧸
        { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)),
            isPrime := hx : PrimeSpectrum A }.asIdeal))
have refine_2₁ : Function.Injective.{u + 1, v + 1} (α :=
  A ⧸
    { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)),
        isPrime := hx : PrimeSpectrum A }.asIdeal)
  (β := ↥N₂ ⧸ N₁.submoduleOf N₂)
  (⇑(mapQ
        { asIdeal := colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)),
            isPrime := hx }.asIdeal
        (N₁.submoduleOf N₂) (toSpanSingleton A (↥N₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ N₂) x hxN₂)) sorry) :
    (a : A ⧸ { asIdeal := ⊥.colon {(N₁.mkQ : (a : M) → M ⧸ N₁) x}, isPrime := hx }.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂)
Tactic: refine ⟨.symm (.ofBijective (Submodule.mapQ _ _ (toSpanSingleton A _ ⟨x, hxN₂⟩) ?_) ⟨?_, ?_⟩)⟩