awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
s : Set R
hs : s ⊆ (↑p : Set R)
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span s)) +
      (↑(Submodule.spanFinrank (span s)) : WithBot ℕ∞) ≤
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span s)) + (↑s.encard : WithBot ℕ∞)
have refine_2 : (↑(Submodule.spanFinrank (span s)) : WithBot ℕ∞) ≤ (↑s.encard : WithBot ℕ∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
s : Set R
hs : s ⊆ (↑p : Set R)
⊢ (↑(Submodule.spanFinrank (span s)) : WithBot ℕ∞) ≤ (↑s.encard : WithBot ℕ∞)
have refine_2 : (↑(Submodule.spanFinrank (span s)) : ℕ∞) ≤ s.encard
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
r : R
p : Ideal R
inst_2 : p.IsPrime
hrm : r ∈ p
⊢ p.height ≤
    height (R := HasQuotient.Quotient R (B := Ideal R) (span {r}))
        (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (span {r})) (Quotient.mk (span {r})) p) +
      1
have h : 1 = Set.encard (α := R) {r}
Tactic: convert! height_le_height_add_encard_of_subset { r } (p := p) (by simpa)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
r : R
p : Ideal R
inst_2 : p.IsPrime
hrp : r ∈ p
⊢ (↑p.height : WithBot ℕ∞) ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {r})) + 1
have h : 1 = (↑(Set.encard (α := R) {r}) : WithBot ℕ∞)
Tactic: convert! Ideal.height_le_ringKrullDim_quotient_add_encard { r } (by simpa)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Set R
hs : s ⊆ (↑(Ring.jacobson R) : Set R)
⊢ ringKrullDim R ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span s)) + (↑s.encard : WithBot ℕ∞)
have refine_1 : LE.le (α := Ideal R) (Ideal.span s) (Ring.jacobson R)
Tactic: refine le_trans (ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank (Ideal.span s) ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Set R
hs : s ⊆ (↑(Ring.jacobson R) : Set R)
refine_1 : LE.le (α := Ideal R) (Ideal.span s) (Ring.jacobson R)
⊢ ringKrullDim R ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span s)) + (↑s.encard : WithBot ℕ∞)
have refine_2 : ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span s)) +
    (↑(Submodule.spanFinrank (Ideal.span s)) : WithBot ℕ∞) ≤
  ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span s)) + (↑s.encard : WithBot ℕ∞)
Tactic: refine le_trans (ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank (Ideal.span s) ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Set R
hs : s ⊆ (↑(Ring.jacobson R) : Set R)
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span s)) +
      (↑(Submodule.spanFinrank (Ideal.span s)) : WithBot ℕ∞) ≤
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span s)) + (↑s.encard : WithBot ℕ∞)
have refine_2 : (↑(Submodule.spanFinrank (Ideal.span s)) : WithBot ℕ∞) ≤ (↑s.encard : WithBot ℕ∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Set R
hs : s ⊆ (↑(Ring.jacobson R) : Set R)
⊢ (↑(Submodule.spanFinrank (Ideal.span s)) : WithBot ℕ∞) ≤ (↑s.encard : WithBot ℕ∞)
have refine_2 : (↑(Submodule.spanFinrank (Ideal.span s)) : ℕ∞) ≤ s.encard
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Finset R
hs : (↑s : Set R) ⊆ (↑(Ring.jacobson R) : Set R)
⊢ ringKrullDim R ≤
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span (↑s : Set R))) + (↑s.card : WithBot ℕ∞)
have h : (↑s.card : WithBot ℕ∞) = (↑(↑s : Set R).encard : WithBot ℕ∞)
Tactic: convert! ringKrullDim_le_ringKrullDim_quotient_add_encard s hs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Finset R
hs : (↑s : Set R) ⊆ (↑(Ring.jacobson R) : Set R)
⊢ (↑s.card : WithBot ℕ∞) = (↑(↑s : Set R).encard : WithBot ℕ∞)
have h : s.card = s.card
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
⊢ P.height ≤
    p.height +
      height (R := 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)
have obtain : ∀ (s : Finset R) (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p)
  (heq : (↑s.card : ℕ∞) = p.height),
  P.height ≤
    p.height +
      height (R := 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)
Tactic: obtain ⟨s, hp, heq⟩ := p.exists_finset_card_eq_height_of_isNoetherianRing
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
heq : (↑s.card : ℕ∞) = p.height
P' : 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
⊢ P.height ≤
    p.height +
      height (R := 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)
have obtain : ∀ (s' : Finset (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
  (hP' :
    Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
      (Ideal.minimalPrimes (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))) P')
  (heq' : (↑s'.card : ℕ∞) = P'.height),
  P.height ≤
    p.height +
      height (R := 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)
Tactic: obtain ⟨s', hP', heq'⟩ := P'.exists_finset_card_eq_height_of_isNoetherianRing
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
heq : (↑s.card : ℕ∞) = p.height
P' : 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
s' : Finset (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
hP' :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))) P'
heq' : (↑s'.card : ℕ∞) = P'.height
⊢ P.height ≤
    p.height +
      height (R := 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)
have hsP'sub : (↑s' : Set (S ⧸ map (algebraMap R S) p)) ⊆ (↑P' : Set (S ⧸ map (algebraMap R S) p))
Tactic: have hsP'sub : (s' : Set <| S ⧸ (Ideal.map (algebraMap R S) p)) ⊆ (P' : Set <| S ⧸ _) :=
    fun x hx ↦ hP'.le (Ideal.subset_span hx)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
heq : (↑s.card : ℕ∞) = p.height
P' : 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
s' : Finset (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
hP' :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))) P'
heq' : (↑s'.card : ℕ∞) = P'.height
hsP'sub : (↑s' : Set (S ⧸ map (algebraMap R S) p)) ⊆ (↑P' : Set (S ⧸ map (algebraMap R S) p))
⊢ Set.SurjOn (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p)
    (↑P : Set S) (↑s' : Set (S ⧸ map (algebraMap R S) p))
have refine : ∀ (x : HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
  (hx : x ∈ (↑P' : Set (S ⧸ map (algebraMap R S) p))),
  Membership.mem (γ := Set (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
    ((⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) '' (↑P : Set S)) x
Tactic: refine Set.SurjOn.mono subset_rfl hsP'sub fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
heq : (↑s.card : ℕ∞) = p.height
P' : 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
s' : Finset (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
hP' :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))) P'
heq' : (↑s'.card : ℕ∞) = P'.height
hsP'sub : (↑s' : Set (S ⧸ map (algebraMap R S) p)) ⊆ (↑P' : Set (S ⧸ map (algebraMap R S) p))
x : HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)
hx : x ∈ (↑P' : Set (S ⧸ map (algebraMap R S) p))
⊢ Membership.mem (γ := Set (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
    ((⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) '' (↑P : Set S)) x
have obtain : ∀ (y : S)
  (hx :
    Membership.mem (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (↑P' : Set (S ⧸ map (algebraMap R S) p))
      ((Quotient.mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
        HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))),
  Membership.mem (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) (γ :=
    Set (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
    ((⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) '' (↑P : Set S))
    ((Quotient.mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
Tactic: obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
heq : (↑s.card : ℕ∞) = p.height
P' : 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
s' : Finset (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
hP' :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))) P'
heq' : (↑s'.card : ℕ∞) = P'.height
hsP'sub : (↑s' : Set (S ⧸ map (algebraMap R S) p)) ⊆ (↑P' : Set (S ⧸ map (algebraMap R S) p))
y : S
hx :
  Membership.mem (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    (↑P' : Set (S ⧸ map (algebraMap R S) p))
    ((Quotient.mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
⊢ Membership.mem (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) (γ :=
    Set (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
    ((⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) '' (↑P : Set S))
    ((Quotient.mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
have rw : ∀ (hx : y ∈ P),
  Membership.mem (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) (γ :=
    Set (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
    ((⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) '' (↑P : Set S))
    ((Quotient.mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
Tactic: rw [SetLike.mem_coe, Ideal.mem_quotient_iff_mem] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
heq : (↑s.card : ℕ∞) = p.height
P' : 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
s' : Finset (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
hP' :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))) P'
heq' : (↑s'.card : ℕ∞) = P'.height
hsP'sub : (↑s' : Set (S ⧸ map (algebraMap R S) p)) ⊆ (↑P' : Set (S ⧸ map (algebraMap R S) p))
y : S
hx :
  Membership.mem (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    (↑P' : Set (S ⧸ map (algebraMap R S) p))
    ((Quotient.mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
rw :
  ∀ (hx : y ∈ P),
    Membership.mem (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) (γ :=
      Set (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
      ((⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) '' (↑P : Set S))
      ((Quotient.mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
        HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
⊢ Membership.mem (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) (γ :=
    Set (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
    ((⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) '' (↑P : Set S))
    ((Quotient.mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
have hIJ : ∀
  (hx :
    Membership.mem (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) P'
      ((Quotient.mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
        HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))),
  map (F := R →+* S) (algebraMap R S) p ≤ P
Tactic: rw [SetLike.mem_coe, Ideal.mem_quotient_iff_mem] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
heq : (↑s.card : ℕ∞) = p.height
P' : 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
s' : Finset (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
hP' :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))) P'
heq' : (↑s'.card : ℕ∞) = P'.height
hsP'sub : (↑s' : Set (S ⧸ map (algebraMap R S) p)) ⊆ (↑P' : Set (S ⧸ map (algebraMap R S) p))
y : S
hx : y ∈ P
w : S
⊢ Membership.mem (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) (γ :=
    Set (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
    ((⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) '' (↑P : Set S))
    ((Quotient.mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
have left : y ∈ (↑P : Set S)
Tactic: use y, hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
heq : (↑s.card : ℕ∞) = p.height
P' : 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
s' : Finset (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
hP' :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))) P'
heq' : (↑s'.card : ℕ∞) = P'.height
hsP'sub : (↑s' : Set (S ⧸ map (algebraMap R S) p)) ⊆ (↑P' : Set (S ⧸ map (algebraMap R S) p))
y : S
hx : y ∈ P
w : S
left : y ∈ (↑P : Set S)
⊢ Membership.mem (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) (γ :=
    Set (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
    ((⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) '' (↑P : Set S))
    ((Quotient.mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
have right : Eq (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
  ((Quotient.mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
    HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
  ((Quotient.mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
    HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
Tactic: use y, hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
heq : (↑s.card : ℕ∞) = p.height
P' : 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
s' : Finset (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
hP' :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))) P'
heq' : (↑s'.card : ℕ∞) = P'.height
hsP'sub : (↑s' : Set (S ⧸ map (algebraMap R S) p)) ⊆ (↑P' : Set (S ⧸ map (algebraMap R S) p))
y : S
hx :
  Membership.mem (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) P'
    ((Quotient.mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
⊢ map (F := R →+* S) (algebraMap R S) p ≤ P
have hIJ : p ≤ comap (F := R →+* S) (algebraMap R S) P
Tactic: rw [Ideal.map_le_iff_le_comap, Ideal.LiesOver.over (p := p) (P := P)]