awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
⊢ span t ≤ p

Tactic:
have hI'p : span t ≤ p := hI'q.trans hqp.le
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
⊢ p.IsPrime

Tactic:
have := hp.isPrime
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this : p.IsPrime
rwa rwa₁ rwa₂ rwa₃ : span t ≤ p
⊢ RingHom.ker f ≤ p

Tactic:
rwa [mk_ker]

Premises used: Ideal.mk_ker
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this : p.IsPrime
⊢ IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)

Tactic:
have : (p.map f).IsPrime := map_isPrime_of_surjective hf (by rwa [mk_ker])
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
h : height (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p) ≤ 1
e : LE.le (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) (map f p) (map f q)
⊢ p ≤ q

Tactic:
simpa only [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot, f, mk_ker,
        sup_eq_left.mpr hI'q, sup_eq_left.mpr hI'p] using comap_mono (f := f) e

Premises used: Iff.mpr, sup_eq_left, Ideal.comap_mono, Ideal.comap_map_of_surjective, RingHom.ker_eq_comap_bot, Ideal.mk_ker
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
h : height (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p) ≤ 1
⊢ LT.lt (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) (map f q) (map f p)

Tactic:
have h_lt : q.map f < p.map f := (map_mono hqp.le).lt_of_not_ge fun e ↦ hqp.not_ge <| by
      simpa only [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot, f, mk_ker,
        sup_eq_left.mpr hI'q, sup_eq_left.mpr hI'p] using comap_mono (f := f) e
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
h : height (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p) ≤ 1
h_lt : LT.lt (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) (map f q) (map f p)
rwa rwa₁ rwa₂ rwa₃ : span t ≤ q
⊢ RingHom.ker f ≤ q

Tactic:
rwa [mk_ker]

Premises used: Ideal.mk_ker
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
h : height (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p) ≤ 1
h_lt : LT.lt (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) (map f q) (map f p)
⊢ IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f q)

Tactic:
have : (q.map f).IsPrime := map_isPrime_of_surjective hf (by rwa [mk_ker])
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this_2 : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
h : height (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p) ≤ 1
h_lt : LT.lt (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) (map f q) (map f p)
this : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f q)
⊢ FiniteHeight (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)

Tactic:
have : (p.map f).FiniteHeight := ⟨Or.inr (h.trans_lt (WithTop.coe_lt_top 1)).ne⟩
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this_2 : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
h : height (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p) ≤ 1
h_lt : LT.lt (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) (map f q) (map f p)
this_3 : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f q)
this : FiniteHeight (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
⊢ height (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f q) < 1

Tactic:
have := (height_strict_mono_of_isPrime_of_isPrime h_lt).trans_le h
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this_2 : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
h : height (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p) ≤ 1
h_lt : LT.lt (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) (map f q) (map f p)
this_3 : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f q)
this_4 : FiniteHeight (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
this : height (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f q) < 1
⊢ Membership.mem (γ := Set (Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))))
    (minimalPrimes (HasQuotient.Quotient R (B := Ideal R) (span t))) (map f q)

Tactic:
rw [ENat.lt_one_iff_eq_zero, height_eq_zero_iff] at this

Premises used: Ideal.height_eq_zero_iff, ENat.lt_one_iff_eq_zero
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this_2 : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
h : height (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p) ≤ 1
h_lt : LT.lt (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) (map f q) (map f p)
this_3 : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f q)
this_4 : FiniteHeight (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
this :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))))
    (minimalPrimes (HasQuotient.Quotient R (B := Ideal R) (span t))) (map f q)
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f ⊥)) (comap f (map f q))

Tactic:
have := minimalPrimes_comap_of_surjective hf this
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this_2 : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
h : height (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p) ≤ 1
h_lt : LT.lt (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) (map f q) (map f p)
this_3 : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f q)
this_4 : FiniteHeight (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
this_5 :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))))
    (minimalPrimes (HasQuotient.Quotient R (B := Ideal R) (span t))) (map f q)
this : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f ⊥)) (comap f (map f q))
rwa :
  ∀ (this : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f ⊥)) (q ⊔ comap f ⊥)),
    Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
rwa₁ :
  ∀ (this : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (RingHom.ker f)) (q ⊔ RingHom.ker f)),
    Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
rwa₂ :
  ∀ (this : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) (q ⊔ span t)),
    Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (this : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q),
    Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q

Tactic:
rwa [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot,
      mk_ker, sup_eq_left.mpr hI'q] at this

Premises used: Iff.mpr, sup_eq_left, Ideal.comap_map_of_surjective, RingHom.ker_eq_comap_bot, Ideal.mk_ker
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
suffices : height (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p) ≤ 1
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q

Tactic:
suffices h : (p.map f).height ≤ 1 by
    have h_lt : q.map f < p.map f := (map_mono hqp.le).lt_of_not_ge fun e ↦ hqp.not_ge <| by
      simpa only [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot, f, mk_ker,
        sup_eq_left.mpr hI'q, sup_eq_left.mpr hI'p] using comap_mono (f := f) e
    have : (q.map f).IsPrime := map_isPrime_of_surjective hf (by rwa [mk_ker])
    have : (p.map f).FiniteHeight := ⟨Or.inr (h.trans_lt (WithTop.coe_lt_top 1)).ne⟩
    have := (height_strict_mono_of_isPrime_of_isPrime h_lt).trans_le h
    rw [ENat.lt_one_iff_eq_zero, height_eq_zero_iff] at this
    have := minimalPrimes_comap_of_surjective hf this
    rwa [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot,
      mk_ker, sup_eq_left.mpr hI'q] at this
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
⊢ height (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p) ≤ 1

Tactic:
height_le_one_of_isPrincipal_of_mem_minimalPrimes ((span {x}).map f) (p.map f) ⟨⟨this,
    map_mono <| span_le.mpr <| Set.singleton_subset_iff.mpr <| hp.le <| subset_span <| .inl rfl⟩,
    fun r ⟨hr, hxr⟩ hrp ↦ map_le_iff_le_comap.mpr (hp.2 ⟨hr.comap f, ?_⟩ ?_)⟩

Premises used: Ideal.span_le, Iff.mpr, Set.singleton_subset_iff, Ideal.subset_span, Ideal.IsMinimalPrime.le, Ideal.IsPrime.comap, Ideal.map, LE.le, Ideal.map_le_iff_le_comap, And.right, And.intro, _private.0.Ideal.mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert.match_1, Ideal.map_mono, Ideal.span, Or.inl, Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes, Singleton.singleton, rfl
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
refine_1 :
  ∀ (r : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))),
    (fun (q : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) ↦ q.IsPrime ∧ map (R := R) f (span {x}) ≤ q) r →
      ∀ (hrp : r ≤ map f p) (hr : r.IsPrime) (hxr : map (R := R) f (span {x}) ≤ r),
        LE.le (α := Ideal R) (span (insert x s)) (comap f r)
refine_2 :
  ∀ (r : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))),
    (fun (q : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) ↦ q.IsPrime ∧ map (R := R) f (span {x}) ≤ q) r →
      ∀ (hrp : r ≤ map f p) (hr : r.IsPrime) (hxr : map (R := R) f (span {x}) ≤ r), comap f r ≤ p
⊢ height (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p) ≤ 1

Tactic:
refine height_le_one_of_isPrincipal_of_mem_minimalPrimes ((span {x}).map f) (p.map f) ⟨⟨this,
    map_mono <| span_le.mpr <| Set.singleton_subset_iff.mpr <| hp.le <| subset_span <| .inl rfl⟩,
    fun r ⟨hr, hxr⟩ hrp ↦ map_le_iff_le_comap.mpr (hp.2 ⟨hr.comap f, ?_⟩ ?_)⟩

Premises used: Ideal.span_le, Iff.mpr, Set.singleton_subset_iff, Ideal.subset_span, Ideal.IsMinimalPrime.le, Ideal.IsPrime.comap, Ideal.map, LE.le, Ideal.map_le_iff_le_comap, And.right, And.intro, _private.0.Ideal.mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert.match_1, Ideal.map_mono, Ideal.span, Or.inl, Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes, Singleton.singleton, rfl
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
r : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))
h : (fun (q : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) ↦ q.IsPrime ∧ map (R := R) f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map (R := R) f (span {x}) ≤ r
refine_1 : x ∈ (↑(comap f r) : Set R) ∧ s ⊆ (↑(comap f r) : Set R)
⊢ LE.le (α := Ideal R) (span (insert x s)) (comap f r)

Tactic:
rw [span_le, Set.insert_subset_iff]

Premises used: Ideal.span_le, Set.insert_subset_iff
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
r : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))
h : (fun (q : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) ↦ q.IsPrime ∧ map (R := R) f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map (R := R) f (span {x}) ≤ r
⊢ Membership.mem (γ := Submodule R R) (comap f r) x

Tactic:
have := map_le_iff_le_comap.mp hxr (subset_span rfl)
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this_2 : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
r : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))
h : (fun (q : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) ↦ q.IsPrime ∧ map (R := R) f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map (R := R) f (span {x}) ≤ r
this : Membership.mem (γ := Submodule R R) (comap f r) x
⊢ x ∈ (↑(comap f r) : Set R) ∧ s ⊆ (↑(comap f r) : Set R)

Tactic:
⟨this, hsp.trans ((hr.comap f).isRadical.radical_le_iff.mpr ?_)⟩

Premises used: Iff.mpr, Ideal.IsPrime.comap, HasSubset.Subset.trans, Ideal.IsRadical.radical_le_iff, And.intro, Ideal.IsPrime.isRadical
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this_2 : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
r : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))
h : (fun (q : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) ↦ q.IsPrime ∧ map (R := R) f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map (R := R) f (span {x}) ≤ r
this : Membership.mem (γ := Submodule R R) (comap f r) x
refine_1 : LE.le (α := Ideal R) (span (insert x t)) (comap f r)
⊢ x ∈ (↑(comap f r) : Set R) ∧ s ⊆ (↑(comap f r) : Set R)

Tactic:
refine ⟨this, hsp.trans ((hr.comap f).isRadical.radical_le_iff.mpr ?_)⟩