awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
⊢ Eq.{u_1 + 1} (α := Set (Ideal R)) {p : Ideal R | I.radical.IsMinimalPrime p} {p : Ideal R | I.IsMinimalPrime p}
have h : ∀ (p : Ideal R),
  Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.radical.IsMinimalPrime p} p ↔
    Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.IsMinimalPrime p} p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
⊢ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.radical.IsMinimalPrime p} p ↔
    Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.IsMinimalPrime p} p
have h : Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.radical.IsMinimalPrime p} p →
  Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.IsMinimalPrime p} p
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
h :
  Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.radical.IsMinimalPrime p} p →
    Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.IsMinimalPrime p} p
⊢ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.radical.IsMinimalPrime p} p ↔
    Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.IsMinimalPrime p} p
have h₁ : Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.IsMinimalPrime p} p →
  Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.radical.IsMinimalPrime p} p
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I.radical ≤ p
⊢ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.IsMinimalPrime p} p
have h : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
Tactic: refine ⟨⟨a, a.radical_le_iff.1 ha⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I.radical ≤ p
⊢ ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
have h : ∀ (b : ∀ ⦃y : Ideal R⦄, y.IsPrime → I.radical ≤ y → y ≤ p → p ≤ y) ⦃y : Ideal R⦄, y.IsPrime → I ≤ y → y ≤ p → p ≤ y
Tactic: simp only [and_imp] at *
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I ≤ p
⊢ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.radical.IsMinimalPrime p} p
have h : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
Tactic: refine ⟨⟨a, a.radical_le_iff.2 ha⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I ≤ p
⊢ ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
have h : ∀ (b : ∀ ⦃y : Ideal R⦄, y.IsPrime → I ≤ y → y ≤ p → p ≤ y) ⦃y : Ideal R⦄, y.IsPrime → I.radical ≤ y → y ≤ p → p ≤ y
Tactic: simp only [and_imp] at *
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
⊢ sInf I.minimalPrimes = I.radical
have rw : sInf I.minimalPrimes = sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}
Tactic: rw [I.radical_eq_sInf]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
⊢ sInf I.minimalPrimes = sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}
have a : sInf I.minimalPrimes ≤ sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a : sInf I.minimalPrimes ≤ sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}
⊢ sInf I.minimalPrimes = sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}
have a₁ : sInf {J : Ideal R | I ≤ J ∧ J.IsPrime} ≤ sInf I.minimalPrimes
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
hx : x ∈ sInf I.minimalPrimes
⊢ Membership.mem (γ := Submodule R R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) x
have a : ∀ (hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ I.minimalPrimes → x ∈ I_1) ⦃I_1 : Ideal R⦄,
  Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} I_1 → x ∈ I_1
Tactic: rw [Ideal.mem_sInf] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ I.minimalPrimes → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : J.IsPrime
⊢ x ∈ J
have a : ∀ (p : Ideal R) (hp : p ∈ I.minimalPrimes) (hp' : p ≤ J), x ∈ J
Tactic: obtain ⟨p, hp, hp'⟩ := Ideal.exists_minimalPrimes_le e
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
⊢ sInf {J : Ideal R | I ≤ J ∧ J.IsPrime} ≤ sInf I.minimalPrimes
have apply : I.minimalPrimes ⊆ {J : Ideal R | I ≤ J ∧ J.IsPrime}
Tactic: apply sInf_le_sInf _
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrimary
⊢ I.minimalPrimes = {I.radical}
have h : ∀ (J : Ideal R), J ∈ I.minimalPrimes ↔ Membership.mem (γ := Set (Ideal R)) {I.radical} J
Tactic: ext J
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ I.minimalPrimes ↔ Membership.mem (γ := Set (Ideal R)) {I.radical} J
have h : J ∈ I.minimalPrimes → Membership.mem (γ := Set (Ideal R)) {I.radical} J
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
h : J ∈ I.minimalPrimes → Membership.mem (γ := Set (Ideal R)) {I.radical} J
⊢ J ∈ I.minimalPrimes ↔ Membership.mem (γ := Set (Ideal R)) {I.radical} J
have h₁ : Membership.mem (γ := Set (Ideal R)) {I.radical} J → J ∈ I.minimalPrimes
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
H : J ∈ I.minimalPrimes
⊢ Membership.mem (γ := Set (Ideal R)) {I.radical} J
have le : I.radical ≤ J
Tactic: have le := H.out.isPrime.radical_le_iff.mpr H.le
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsPrime
⊢ I.minimalPrimes = {I}
have h : ∀ (J : Ideal R), J ∈ I.minimalPrimes ↔ Membership.mem (γ := Set (Ideal R)) {I} J
Tactic: ext J
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsPrime
J : Ideal R
⊢ J ∈ I.minimalPrimes ↔ Membership.mem (γ := Set (Ideal R)) {I} J
have h : Membership.mem (γ := Set (Ideal R)) {I} J → J ∈ I.minimalPrimes
Tactic: refine ⟨fun H => (H.2 ⟨inferInstance, rfl.le⟩ H.le).antisymm H.le, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := Set (Ideal R)) (Ideal.minimalPrimes ⊤) ∅
have h : ∀ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊤) p ↔ Membership.mem (γ := Set (Ideal R)) ∅ p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊤) p ↔ Membership.mem (γ := Set (Ideal R)) ∅ p
have h : p ∉ Ideal.minimalPrimes ⊤
Tactic: simp only [Set.notMem_empty, iff_false]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
⊢ I.minimalPrimes = ∅ ↔ I = ⊤
have mp : I.minimalPrimes = ∅ → I = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
mp : I.minimalPrimes = ∅ → I = ⊤
⊢ I.minimalPrimes = ∅ ↔ I = ⊤
have mpr : I = ⊤ → I.minimalPrimes = ∅
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
⊢ I = ⊤
have mp : ∀ (h : ¬I = ⊤), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
⊢ False
have mp : ∀ (M : Ideal R) (hM : M.IsMaximal) (hM' : I ≤ M), False
Tactic: have ⟨M, hM, hM'⟩ := Ideal.exists_le_maximal I h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
⊢ False
have mp : ∀ (p : Ideal R) (hp : p ∈ I.minimalPrimes ∧ p ≤ M), False
Tactic: have ⟨p, hp⟩ := Ideal.exists_minimalPrimes_le hM'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
p : Ideal R
hp : p ∈ I.minimalPrimes ∧ p ≤ M
⊢ False
have hp₁ : Membership.mem (γ := Set (Ideal R)) ∅ p ∧ p ≤ M
Tactic: rw [e] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
p I J : Ideal R
inst_1 : p.IsPrime
hle : I ≤ p
h :
  Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
    (map (F := R →+* R ⧸ I) (Quotient.mk I) p)
⊢ p ∈ (I ⊔ J).minimalPrimes
have refine_1 : I ⊔ J ≤ p
Tactic: refine ⟨⟨‹_›, ?_⟩, fun q ⟨_, hq⟩ hqp ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
p I J : Ideal R
inst_1 : p.IsPrime
hle : I ≤ p
h :
  Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
    (map (F := R →+* R ⧸ I) (Quotient.mk I) p)
refine_1 : I ⊔ J ≤ p
⊢ p ∈ (I ⊔ J).minimalPrimes
have refine_2 : ∀ (q : Ideal R), (fun (q : Ideal R) ↦ q.IsPrime ∧ I ⊔ J ≤ q) q → ∀ (hqp : q ≤ p), q.IsPrime → ∀ (hq : I ⊔ J ≤ q), p ≤ q
Tactic: refine ⟨⟨‹_›, ?_⟩, fun q ⟨_, hq⟩ hqp ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
p I J : Ideal R
inst_1 : p.IsPrime
hle : I ≤ p
h :
  Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
    (map (F := R →+* R ⧸ I) (Quotient.mk I) p)
⊢ I ⊔ J ≤ p
have refine_1 : I ≤ p ∧ J ≤ p
Tactic: rw [sup_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
p I J : Ideal R
inst_1 : p.IsPrime
hle : I ≤ p
h :
  Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
    (map (F := R →+* R ⧸ I) (Quotient.mk I) p)
q : Ideal R
h_1 : (fun (q : Ideal R) ↦ q.IsPrime ∧ I ⊔ J ≤ q) q
hqp : q ≤ p
left : q.IsPrime
hq : I ⊔ J ≤ q
⊢ p ≤ q
have hq₁ : I ≤ q ∧ J ≤ q
Tactic: rw [sup_le_iff] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
p I J : Ideal R
inst_1 : p.IsPrime
hle : I ≤ p
h :
  Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
    (map (F := R →+* R ⧸ I) (Quotient.mk I) p)
q : Ideal R
h_1 : (fun (q : Ideal R) ↦ q.IsPrime ∧ I ⊔ J ≤ q) q
hqp : q ≤ p
left : q.IsPrime
hq : I ≤ q ∧ J ≤ q
⊢ p ≤ q
have h2 : LE.le (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) (map (F := R →+* R ⧸ I) (Quotient.mk I) q)
Tactic: have h2 : p.map (Quotient.mk I) ≤ q.map (Quotient.mk I) :=
      h.2 ⟨isPrime_map_quotientMk_of_isPrime hq.1, map_mono hq.2⟩ (map_mono hqp)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
I p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) J))
    (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
⊢ P ∈ (map (F := R →+* S) (algebraMap R S) I ⊔ J).minimalPrimes
have refine_1 : map (F := R →+* S) (algebraMap R S) I ≤ P ∧ J ≤ P
Tactic: refine ⟨⟨inferInstance, sup_le_iff.mpr ?_⟩, fun q ⟨_, hleq⟩ hqle ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
I p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) J))
    (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
refine_1 : map (F := R →+* S) (algebraMap R S) I ≤ P ∧ J ≤ P
⊢ P ∈ (map (F := R →+* S) (algebraMap R S) I ⊔ J).minimalPrimes
have refine_2 : ∀ (q : Ideal S),
  (fun (q : Ideal S) ↦ q.IsPrime ∧ map (F := R →+* S) (algebraMap R S) I ⊔ J ≤ q) q →
    ∀ (hqle : q ≤ P), q.IsPrime → ∀ (hleq : map (F := R →+* S) (algebraMap R S) I ⊔ J ≤ q), P ≤ q
Tactic: refine ⟨⟨inferInstance, sup_le_iff.mpr ?_⟩, fun q ⟨_, hleq⟩ hqle ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
I p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) J))
    (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
⊢ map (F := R →+* S) (algebraMap R S) I ≤ P ∧ J ≤ P
have refine_1 : map (F := R →+* S) (algebraMap R S) I ≤ P
Tactic: refine ⟨?_, hJP⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
I p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) J))
    (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
⊢ map (F := R →+* S) (algebraMap R S) I ≤ P
have refine_1 : I ≤ p
Tactic: rw [Ideal.map_le_iff_le_comap, ← Ideal.under_def, ← Ideal.over_def P p]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
I p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) J))
    (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
q : Ideal S
h : (fun (q : Ideal S) ↦ q.IsPrime ∧ map (F := R →+* S) (algebraMap R S) I ⊔ J ≤ q) q
hqle : q ≤ P
left : q.IsPrime
hleq : map (F := R →+* S) (algebraMap R S) I ⊔ J ≤ q
⊢ P ≤ q
have hleq₁ : map (F := R →+* S) (algebraMap R S) I ≤ q ∧ J ≤ q
Tactic: simp only [sup_le_iff] at hleq
Cleared hypotheses: hleq
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
I p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) J))
    (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
q : Ideal S
h : (fun (q : Ideal S) ↦ q.IsPrime ∧ map (F := R →+* S) (algebraMap R S) I ⊔ J ≤ q) q
hqle : q ≤ P
left : q.IsPrime
hleq : map (F := R →+* S) (algebraMap R S) I ≤ q ∧ J ≤ q
⊢ map (F := R →+* S) (algebraMap R S) p ≤ q
have rw : p ≤ comap (F := R →+* S) (algebraMap R S) q
Tactic: rw [Ideal.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
I p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) J))
    (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
q : Ideal S
h : (fun (q : Ideal S) ↦ q.IsPrime ∧ map (F := R →+* S) (algebraMap R S) I ⊔ J ≤ q) q
hqle : q ≤ P
left : q.IsPrime
hleq : map (F := R →+* S) (algebraMap R S) I ≤ q ∧ J ≤ q
⊢ p ≤ comap (F := R →+* S) (algebraMap R S) q
have refine : comap (F := R →+* S) (algebraMap R S) q ≤ p
Tactic: refine hI.2 ⟨inferInstance, le_trans Ideal.le_comap_map (Ideal.comap_mono hleq.1)⟩ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
I p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) J))
    (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
q : Ideal S
h : (fun (q : Ideal S) ↦ q.IsPrime ∧ map (F := R →+* S) (algebraMap R S) I ⊔ J ≤ q) q
hqle : q ≤ P
left : q.IsPrime
hleq : map (F := R →+* S) (algebraMap R S) I ≤ q ∧ J ≤ q
⊢ comap (F := R →+* S) (algebraMap R S) q ≤ p
have h : p = comap (F := R →+* S) (algebraMap R S) P
Tactic: convert! Ideal.comap_mono hqle
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
I p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) J))
    (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
q : Ideal S
h : (fun (q : Ideal S) ↦ q.IsPrime ∧ map (F := R →+* S) (algebraMap R S) I ⊔ J ≤ q) q
hqle : q ≤ P
left : q.IsPrime
hleq : map (F := R →+* S) (algebraMap R S) I ≤ q ∧ J ≤ q
⊢ P ≤ q
have h1 : map (F := R →+* S) (algebraMap R S) p ≤ q
Tactic: have h1 : p.map (algebraMap R S) ≤ q := by
      rw [Ideal.map_le_iff_le_comap]
      refine hI.2 ⟨inferInstance, le_trans Ideal.le_comap_map (Ideal.comap_mono hleq.1)⟩ ?_
      convert! Ideal.comap_mono hqle
      exact Ideal.LiesOver.over
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
I p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) J))
    (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
q : Ideal S
h : (fun (q : Ideal S) ↦ q.IsPrime ∧ map (F := R →+* S) (algebraMap R S) I ⊔ J ≤ q) q
hqle : q ≤ P
left : q.IsPrime
hleq : map (F := R →+* S) (algebraMap R S) I ≤ q ∧ J ≤ q
h1 : map (F := R →+* S) (algebraMap R S) p ≤ q
⊢ P ≤ q
have h2 : LE.le (α := Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
  (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
  (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) q)
Tactic: have h2 : P.map (Ideal.Quotient.mk (p.map (algebraMap R S))) ≤
        q.map (Ideal.Quotient.mk (p.map (algebraMap R S))) :=
      hJ.2 ⟨Ideal.isPrime_map_quotientMk_of_isPrime h1, Ideal.map_mono hleq.2⟩
        (Ideal.map_mono hqle)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hI : I ∈ (N.colon {x}).minimalPrimes
⊢ ∃ (x' : M), I = N.colon {x'}
have pos : ∀ (hx : x ∈ N), ∃ (x' : M), I = N.colon {x'}
Tactic: by_cases hx : x ∈ N