awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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
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))
⊢ 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

Tactic:
refine ⟨fun ⟨h, p, ⟨e⟩⟩ ↦ ?_, fun ⟨x, hx, hx'⟩ ↦ ⟨le_sup_left.trans_eq hx'.symm, ⟨_, hx⟩, ?_⟩⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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)
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
⊢ ∃ (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)

Premises used: LinearEquiv.symm, Submodule.mkQ_surjective, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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₂)
⊢ 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:
simp [f, ← hx']
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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₂)
⊢ 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']
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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

Tactic:
⟨x, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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₁)))
refine_1₁ : N₂ = N₁ ⊔ A ∙ x
⊢ ∃ (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 ⟨x, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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₁)
⊢ p.asIdeal.IsPrime

Tactic:
p.2

Premises used: PrimeSpectrum.isPrime
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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₁)
h₁ : colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)) = p.asIdeal
⊢ Ideal.IsPrime.{u} (α := A) (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)))

Tactic:
convert! p.2

Premises used: PrimeSpectrum.isPrime
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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₁)
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
⊢ colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁)) = p.asIdeal

Tactic:
ext r
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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₁)
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:
simp [hx'', ← map_smul, Algebra.smul_def, show f _ = 0 ↔ _ from congr(_ ∈ $hf₁),
        Ideal.Quotient.eq_zero_iff_mem]

Premises used: congrArg, Membership.mem, id, Ideal.Quotient.eq_zero_iff_mem, Algebra.smul_def, map_smul, iff_of_eq
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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

Tactic:
le_antisymm ?_ (sup_le h ((span_singleton_le_iff_mem _ _).mpr hx))

Premises used: Iff.mpr, le_antisymm, sup_le, Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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 : N₂ ≤ N₁ ⊔ A ∙ x
⊢ N₂ = N₁ ⊔ A ∙ x

Tactic:
refine le_antisymm ?_ (sup_le h ((span_singleton_le_iff_mem _ _).mpr hx))

Premises used: Iff.mpr, le_antisymm, sup_le, Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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₁)
⊢ map N₁.mkQ (A ∙ x) = map f (map (↑e.symm : A ⧸ p.asIdeal →ₗ[A] ↥N₂ ⧸ N₁.submoduleOf N₂) (A ∙ 1))

Tactic:
simp only [map_span, Set.image_singleton, hx'', LinearEquiv.coe_coe]

Premises used: Set.image_singleton, Submodule.map_span, LinearEquiv.coe_coe
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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₁)
⊢ 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]
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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))
refine_1 : map N₁.mkQ N₂ ≤ map f (map (↑e.symm : A ⧸ p.asIdeal →ₗ[A] ↥N₂ ⧸ N₁.submoduleOf N₂) (A ∙ 1))
⊢ N₂ ≤ N₁ ⊔ A ∙ x

Tactic:
rw [← N₁.ker_mkQ, sup_comm, ← comap_map_eq, ← map_le_iff_le_comap, this]

Premises used: sup_comm, Submodule.ker_mkQ, Submodule.map_le_iff_le_comap, Submodule.comap_map_eq
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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))
⊢ map N₁.mkQ N₂ ≤ map f (map (↑e.symm : A ⧸ p.asIdeal →ₗ[A] ↥N₂ ⧸ N₁.submoduleOf N₂) (A ∙ 1))

Tactic:
simp [hf₂, Ideal.Quotient.span_singleton_one]

Premises used: Ideal.Quotient.span_singleton_one
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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
⊢ x ∈ N₂

Tactic:
have hxN₂ : x ∈ N₂ := (le_sup_right.trans_eq hx'.symm) (mem_span_singleton_self x)
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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))

Tactic:
⟨.symm (.ofBijective (Submodule.mapQ _ _ (toSpanSingleton A _ ⟨x, hxN₂⟩) ?_) ⟨?_, ?_⟩)⟩

Premises used: LinearEquiv.symm, Nonempty.intro, Submodule.mapQ, And.intro, LinearMap.toSpanSingleton, LinearEquiv.ofBijective
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
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₂)
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₂)) ⋯) :
      (a : A ⧸ { asIdeal := ⊥.colon {(N₁.mkQ : (a : M) → M ⧸ N₁) x}, isPrime := hx }.asIdeal) → ↥N₂ ⧸ N₁.submoduleOf N₂)
refine_2₂ :
  Function.Surjective.{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₂)) ⋯) :
      (a : A ⧸ { asIdeal := ⊥.colon {(N₁.mkQ : (a : M) → M ⧸ N₁) x}, isPrime := hx }.asIdeal) → ↥N₂ ⧸ 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))

Tactic:
refine ⟨.symm (.ofBijective (Submodule.mapQ _ _ (toSpanSingleton A _ ⟨x, hxN₂⟩) ?_) ⟨?_, ?_⟩)⟩