awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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

Tactic:
⟨fun H => (H.2 ⟨inferInstance, rfl.le⟩ H.le).antisymm H.le, ?_⟩

Premises used: Ideal.IsMinimalPrime.le, LE.le.antisymm, inferInstance, Eq.le, And.right, And.intro, Iff.intro, rfl
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsPrime
J : Ideal R
h : Membership.mem (γ := Set (Ideal R)) {I} J → J ∈ I.minimalPrimes
⊢ J ∈ I.minimalPrimes ↔ Membership.mem (γ := Set (Ideal R)) {I} J

Tactic:
refine ⟨fun H => (H.2 ⟨inferInstance, rfl.le⟩ H.le).antisymm H.le, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
J : Ideal R
inst_1 : J.IsPrime
⊢ J ∈ J.minimalPrimes

Tactic:
⟨⟨inferInstance, rfl.le⟩, fun _ h _ => h.2⟩

Premises used: Set.Mem, setOf, inferInstance, Eq.le, And.right, Ideal.IsMinimalPrime, And.intro, Minimal, rfl
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
J : Ideal R
inst_1 : J.IsPrime
⊢ J ∈ J.minimalPrimes

Tactic:
exact ⟨⟨inferInstance, rfl.le⟩, fun _ h _ => h.2⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
⊢ Eq (α := Set (Ideal R)) (minimalPrimes R) {⊥}

Tactic:
Ideal.minimalPrimes_eq_subsingleton_self

Premises used: setOf, Ideal.minimalPrimes_eq_subsingleton_self
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
h :
  ∀ (p : Ideal R),
    Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊤) p ↔ Membership.mem (γ := Set (Ideal R)) ∅ p
⊢ Eq.{u_1 + 1} (α := Set (Ideal R)) (Ideal.minimalPrimes ⊤) ∅

Tactic:
ext p
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
h : p ∉ Ideal.minimalPrimes ⊤
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊤) p ↔ Membership.mem (γ := Set (Ideal R)) ∅ p

Tactic:
simp only [Set.notMem_empty, iff_false]

Premises used: iff_false, Set.notMem_empty
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
h : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊤) p
⊢ False

Tactic:
h.isPrime.ne_top (top_le_iff.mp h.le)

Premises used: Ideal.IsMinimalPrime.le, Ideal.IsMinimalPrime.isPrime, top_le_iff, Iff.mp, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
h : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊤) p
⊢ False

Tactic:
exact h.isPrime.ne_top (top_le_iff.mp h.le)

Premises used: Ideal.IsMinimalPrime.le, Ideal.IsMinimalPrime.isPrime, top_le_iff, Iff.mp, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
mp : I.minimalPrimes = ∅ → I = ⊤
mpr : I = ⊤ → I.minimalPrimes = ∅
⊢ I.minimalPrimes = ∅ ↔ I = ⊤

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
mp : ∀ (h : ¬I = ⊤), False
⊢ I = ⊤

Tactic:
by_contra h
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
mp : ∀ (M : Ideal R) (hM : M.IsMaximal) (hM' : I ≤ M), False
⊢ False

Tactic:
have ⟨M, hM, hM'⟩ := Ideal.exists_le_maximal I h
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
mp : ∀ (p : Ideal R) (hp : p ∈ I.minimalPrimes ∧ p ≤ M), False
⊢ False

Tactic:
have ⟨p, hp⟩ := Ideal.exists_minimalPrimes_le hM'
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
⊢ Membership.mem (γ := Set (Ideal R)) ∅ p ∧ p ≤ M

Tactic:
rw [e] at hp
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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 : Membership.mem (γ := Set (Ideal R)) ∅ p ∧ p ≤ M
⊢ False

Tactic:
apply Set.notMem_empty _ hp.1

Premises used: And.left, Set.notMem_empty
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := Set (Ideal R)) (Ideal.minimalPrimes ⊤) ∅

Tactic:
Ideal.minimalPrimes_top

Premises used: Ideal.minimalPrimes_top
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := Set (Ideal R)) (Ideal.minimalPrimes ⊤) ∅

Tactic:
exact Ideal.minimalPrimes_top

Premises used: Ideal.minimalPrimes_top
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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

Tactic:
⟨⟨‹_›, ?_⟩, fun q ⟨_, hq⟩ hqp ↦ ?_⟩

Premises used: Set.Mem, setOf, _private.0.Ideal.mem_minimalPrimes_sup.match_1, LE.le, Ideal.IsMinimalPrime, And.intro, Minimal
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
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
⊢ p ∈ (I ⊔ J).minimalPrimes

Tactic:
refine ⟨⟨‹_›, ?_⟩, fun q ⟨_, hq⟩ hqp ↦ ?_⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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 ≤ p ∧ J ≤ p
⊢ I ⊔ J ≤ p

Tactic:
rw [sup_le_iff]

Premises used: sup_le_iff
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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)
⊢ J ≤ p

Tactic:
simpa [hle] using Ideal.comap_mono (f := Ideal.Quotient.mk I) h.le

Premises used: Ideal.IsMinimalPrime.le, Ideal.comap_mono
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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 ≤ p ∧ J ≤ p

Tactic:
refine ⟨hle, by simpa [hle] using Ideal.comap_mono (f := Ideal.Quotient.mk I) h.le⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
⊢ I ≤ q ∧ J ≤ q

Tactic:
rw [sup_le_iff] at hq

Premises used: sup_le_iff
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
⊢ 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)
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
h2 : LE.le (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) (map (F := R →+* R ⧸ I) (Quotient.mk I) q)
⊢ p ≤ q

Tactic:
simpa [comap_map_quotientMk, hq.1, sup_le_iff] using comap_mono (f := Ideal.Quotient.mk I) h2

Premises used: Ideal.comap_mono, Ideal.comap_map_quotientMk, sup_le_iff, And.left
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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

Tactic:
⟨⟨inferInstance, sup_le_iff.mpr ?_⟩, fun q ⟨_, hleq⟩ hqle ↦ ?_⟩

Premises used: Iff.mpr, Set.Mem, setOf, inferInstance, LE.le, sup_le_iff, _private.0.Ideal.map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes.match_1, Ideal.IsMinimalPrime, And.intro, Minimal
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
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
⊢ P ∈ (map (F := R →+* S) (algebraMap R S) I ⊔ J).minimalPrimes

Tactic:
refine ⟨⟨inferInstance, sup_le_iff.mpr ?_⟩, fun q ⟨_, hleq⟩ hqle ↦ ?_⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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

Tactic:
⟨?_, hJP⟩

Premises used: And.intro
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
⊢ map (F := R →+* S) (algebraMap R S) I ≤ P ∧ J ≤ P

Tactic:
refine ⟨?_, hJP⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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 : I ≤ p
⊢ map (F := R →+* S) (algebraMap R S) I ≤ P

Tactic:
rw [Ideal.map_le_iff_le_comap, ← Ideal.under_def, ← Ideal.over_def P p]

Premises used: Ideal.map_le_iff_le_comap, Ideal.under_def, Ideal.over_def
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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)
⊢ I ≤ p

Tactic:
hI.le

Premises used: Ideal.IsMinimalPrime.le
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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)
⊢ I ≤ p

Tactic:
exact hI.le

Premises used: Ideal.IsMinimalPrime.le
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
⊢ map (F := R →+* S) (algebraMap R S) I ≤ q ∧ J ≤ q

Tactic:
simp only [sup_le_iff] at hleq

Premises used: sup_le_iff
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
rw : p ≤ comap (F := R →+* S) (algebraMap R S) q
⊢ map (F := R →+* S) (algebraMap R S) p ≤ q

Tactic:
rw [Ideal.map_le_iff_le_comap]

Premises used: Ideal.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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

Tactic:
hI.2 ⟨inferInstance, le_trans Ideal.le_comap_map (Ideal.comap_mono hleq.1)⟩ ?_

Premises used: inferInstance, Ideal.comap_mono, And.right, And.left, And.intro, Ideal.le_comap_map, le_trans
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
refine : comap (F := R →+* S) (algebraMap R S) q ≤ p
⊢ p ≤ comap (F := R →+* S) (algebraMap R S) q

Tactic:
refine hI.2 ⟨inferInstance, le_trans Ideal.le_comap_map (Ideal.comap_mono hleq.1)⟩ ?_

Premises used: inferInstance, Ideal.comap_mono, And.right, And.left, And.intro, Ideal.le_comap_map, le_trans
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
⊢ LE.le (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) q) (comap (F := R →+* S) (algebraMap R S) P)

Tactic:
Ideal.comap_mono hqle

Premises used: Ideal.comap_mono
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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_1 : (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
h : p = comap (F := R →+* S) (algebraMap R S) P
⊢ comap (F := R →+* S) (algebraMap R S) q ≤ p

Tactic:
convert! Ideal.comap_mono hqle

Premises used: Ideal.comap_mono
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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) P

Tactic:
Ideal.LiesOver.over

Premises used: Ideal.LiesOver.over