awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
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
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
have h_lt : 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
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
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)
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
have this₁ : 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])
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
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)
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
have this₁ : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
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)
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
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 R)) (Ideal.minimalPrimes (span t)) q
have 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)
Tactic: rw [ENat.lt_one_iff_eq_zero, height_eq_zero_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
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 (span t)) q
have this₁ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f ⊥)) (comap f (map f q))
Tactic: have := minimalPrimes_comap_of_surjective hf this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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))
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
have rwa : ∀ (this : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f ⊥)) (q ⊔ comap f ⊥)),
  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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
have 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
Tactic: rwa [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot,
      mk_ker, sup_eq_left.mpr hI'q] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
have rwa₂ : ∀ (this : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) (q ⊔ span t)),
  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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
have rwa₃ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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)
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
have suffices : height (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p) ≤ 1
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
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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
have 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)
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, ?_⟩ ?_)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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)
⊢ height (R := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p) ≤ 1
have 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
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, ?_⟩ ?_)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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
⊢ LE.le (α := Ideal R) (span (insert x s)) (comap f r)
have refine_1 : x ∈ (↑(comap f r) : Set R) ∧ s ⊆ (↑(comap f r) : Set R)
Tactic: rw [span_le, Set.insert_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
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
⊢ x ∈ (↑(comap f r) : Set R) ∧ s ⊆ (↑(comap f r) : Set R)
have this₁ : Membership.mem (γ := Submodule R R) (comap f r) x
Tactic: have := map_le_iff_le_comap.mp hxr (subset_span rfl)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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)
have refine_1 : LE.le (α := Ideal R) (span (insert x t)) (comap f r)
Tactic: refine ⟨this, hsp.trans ((hr.comap f).isRadical.radical_le_iff.mpr ?_)⟩