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
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
this_1 : p'.IsPrime
s : Finset (R ⧸ I)
hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p'
hs : (↑s.card : ℕ∞) = p'.height
hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))
this : Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))
o : Finset R
hsubset : (↑o : Set R) ⊆ (↑p : Set R)
ho : Set.InjOn (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑o : Set R)
himgo : Finset.image (⇑(Quotient.mk I) : (a : R) → R ⧸ I) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset (s := Submodule.generators I)
h : p.height ≤ (↑t.card : ℕ∞)
⊢ p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
have refine : (↑t.card : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) (↑(Submodule.spanFinrank I) : ℕ∞)
Tactic: refine le_trans h (hs ▸ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
this_1 : p'.IsPrime
s : Finset (R ⧸ I)
hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p'
hs : (↑s.card : ℕ∞) = p'.height
hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))
this : Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))
o : Finset R
hsubset : (↑o : Set R) ⊆ (↑p : Set R)
ho : Set.InjOn (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑o : Set R)
himgo : Finset.image (⇑(Quotient.mk I) : (a : R) → R ⧸ I) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset (s := Submodule.generators I)
h : p.height ≤ (↑t.card : ℕ∞)
⊢ (↑t.card : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) (↑(Submodule.spanFinrank I) : ℕ∞)
have norm_cast : t.card ≤ s.card + Submodule.spanFinrank I
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
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
this_1 : p'.IsPrime
s : Finset (R ⧸ I)
hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p'
hs : (↑s.card : ℕ∞) = p'.height
hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))
this : Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))
o : Finset R
hsubset : (↑o : Set R) ⊆ (↑p : Set R)
ho : Set.InjOn (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑o : Set R)
himgo : Finset.image (⇑(Quotient.mk I) : (a : R) → R ⧸ I) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset (s := Submodule.generators I)
h : p.height ≤ (↑t.card : ℕ∞)
⊢ ⋯.toFinset (s := Submodule.generators I).card = Submodule.spanFinrank I
have rw : (Submodule.generators I).ncard = Submodule.spanFinrank I
Tactic: rw [← Set.ncard_eq_toFinset_card (hs := Submodule.FG.finite_generators hI)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
this_1 : p'.IsPrime
s : Finset (R ⧸ I)
hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p'
hs : (↑s.card : ℕ∞) = p'.height
hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))
this : Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))
o : Finset R
hsubset : (↑o : Set R) ⊆ (↑p : Set R)
ho : Set.InjOn (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑o : Set R)
himgo : Finset.image (⇑(Quotient.mk I) : (a : R) → R ⧸ I) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset (s := Submodule.generators I)
h : p.height ≤ (↑t.card : ℕ∞)
⊢ t.card ≤ s.card + Submodule.spanFinrank I
have this₁ : sorry.toFinset (s := Submodule.generators I).card = Submodule.spanFinrank I
Tactic: have : (Submodule.FG.finite_generators hI).toFinset.card = I.spanFinrank := by
      rw [← Set.ncard_eq_toFinset_card (hs := Submodule.FG.finite_generators hI)]
      exact Submodule.FG.generators_ncard hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
this_1 : p'.IsPrime
s : Finset (R ⧸ I)
hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p'
hs : (↑s.card : ℕ∞) = p'.height
hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))
this : Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))
o : Finset R
hsubset : (↑o : Set R) ⊆ (↑p : Set R)
ho : Set.InjOn (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑o : Set R)
himgo : Finset.image (⇑(Quotient.mk I) : (a : R) → R ⧸ I) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset (s := Submodule.generators I)
⊢ p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
have suffices : p.height ≤ (↑t.card : ℕ∞)
Tactic: suffices h : p.height ≤ t.card by
    refine le_trans h (hs ▸ ?_)
    norm_cast
    have : (Submodule.FG.finite_generators hI).toFinset.card = I.spanFinrank := by
      rw [← Set.ncard_eq_toFinset_card (hs := Submodule.FG.finite_generators hI)]
      exact Submodule.FG.generators_ncard hI
    grind
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
this_1 : p'.IsPrime
s : Finset (R ⧸ I)
hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p'
hs : (↑s.card : ℕ∞) = p'.height
hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))
this : Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))
o : Finset R
hsubset : (↑o : Set R) ⊆ (↑p : Set R)
ho : Set.InjOn (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑o : Set R)
himgo : Finset.image (⇑(Quotient.mk I) : (a : R) → R ⧸ I) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset (s := Submodule.generators I)
⊢ p.height ≤ (↑t.card : ℕ∞)
have refine : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑t : Set R))) p
Tactic: refine Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
this_1 : p'.IsPrime
s : Finset (R ⧸ I)
hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p'
hs : (↑s.card : ℕ∞) = p'.height
hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))
this : Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))
o : Finset R
hsubset : (↑o : Set R) ⊆ (↑p : Set R)
ho : Set.InjOn (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑o : Set R)
himgo : Finset.image (⇑(Quotient.mk I) : (a : R) → R ⧸ I) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset (s := Submodule.generators I)
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑t : Set R))) p
have rw : p ∈ (I ⊔ span (↑o : Set R)).minimalPrimes
Tactic: rw [Finset.coe_union, Set.Finite.coe_toFinset, span_union, sup_comm, span,
    Submodule.span_generators]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
this_1 : p'.IsPrime
s : Finset (R ⧸ I)
hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p'
hs : (↑s.card : ℕ∞) = p'.height
hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))
this : Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))
o : Finset R
hsubset : (↑o : Set R) ⊆ (↑p : Set R)
ho : Set.InjOn (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑o : Set R)
himgo : Finset.image (⇑(Quotient.mk I) : (a : R) → R ⧸ I) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset (s := Submodule.generators I)
⊢ p ∈ (I ⊔ span (↑o : Set R)).minimalPrimes
have refine : Membership.mem (γ := Set (Ideal (R ⧸ I)))
  (Ideal.minimalPrimes (map (F := R →+* R ⧸ I) (Quotient.mk I) (span (↑o : Set R))))
  (map (F := R →+* R ⧸ I) (Quotient.mk I) p)
Tactic: refine Ideal.mem_minimalPrimes_sup hrp ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
this_1 : p'.IsPrime
s : Finset (R ⧸ I)
hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p'
hs : (↑s.card : ℕ∞) = p'.height
hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))
this : Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))
o : Finset R
hsubset : (↑o : Set R) ⊆ (↑p : Set R)
ho : Set.InjOn (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑o : Set R)
himgo : Finset.image (⇑(Quotient.mk I) : (a : R) → R ⧸ I) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset (s := Submodule.generators I)
⊢ Membership.mem (γ := Set (Ideal (R ⧸ I)))
    (Ideal.minimalPrimes (map (F := R →+* R ⧸ I) (Quotient.mk I) (span (↑o : Set R))))
    (map (F := R →+* R ⧸ I) (Quotient.mk I) p)
have h : Quotient.commSemiring I = CommRing.toCommSemiring →
  Eq (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (span (↑o : Set R))) (span (↑s : Set (R ⧸ I)))
Tactic: convert! hps
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
let let₁ let₂ :
  p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
⊢ p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
have let₃ : let p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p;
∀ (this : p'.IsPrime),
  p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
Tactic: classical
  let p' := p.map (algebraMap R (R ⧸ I))
  have : p'.IsPrime := isPrime_map_quotientMk_of_isPrime hrp
  obtain ⟨s, hps, hs⟩ := exists_finset_card_eq_height_of_isNoetherianRing p'
  have hsp' : (s : Set (R ⧸ I)) ⊆ (p' : Set _) := fun _ hx ↦ hps.le (subset_span hx)
  have : Set.SurjOn (Ideal.Quotient.mk I) p s := by
    refine Set.SurjOn.mono subset_rfl hsp' fun x hx ↦ ?_
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    exact ⟨x, by simpa [hrp, sup_of_le_left, p'] using hx⟩
  obtain ⟨o, hsubset, ho, himgo⟩ := s.exists_subset_injOn_image_eq_of_surjOn (p : Set R) this
  have hI : I.FG := IsNoetherian.noetherian I
  let t : Finset R := o ∪ (Submodule.FG.finite_generators hI).toFinset
  suffices h : p.height ≤ t.card by
    refine le_trans h (hs ▸ ?_)
    norm_cast
    have : (Submodule.FG.finite_generators hI).toFinset.card = I.spanFinrank := by
      rw [← Set.ncard_eq_toFinset_card (hs := Submodule.FG.finite_generators hI)]
      exact Submodule.FG.generators_ncard hI
    grind
  refine Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_
  rw [Finset.coe_union, Set.Finite.coe_toFinset, span_union, sup_comm, span,
    Submodule.span_generators]
  refine Ideal.mem_minimalPrimes_sup hrp ?_
  convert! hps
  simp [Ideal.map_span, ← himgo]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
let let₁ let₂ :
  p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
let₃ :
  let p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p;
  ∀ (this : p'.IsPrime),
    p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
⊢ p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
have let₄ : let p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p;
∀ (this : p'.IsPrime) (s : Finset (R ⧸ I))
  (hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p')
  (hs : (↑s.card : ℕ∞) = p'.height),
  p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
Tactic: classical
  let p' := p.map (algebraMap R (R ⧸ I))
  have : p'.IsPrime := isPrime_map_quotientMk_of_isPrime hrp
  obtain ⟨s, hps, hs⟩ := exists_finset_card_eq_height_of_isNoetherianRing p'
  have hsp' : (s : Set (R ⧸ I)) ⊆ (p' : Set _) := fun _ hx ↦ hps.le (subset_span hx)
  have : Set.SurjOn (Ideal.Quotient.mk I) p s := by
    refine Set.SurjOn.mono subset_rfl hsp' fun x hx ↦ ?_
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    exact ⟨x, by simpa [hrp, sup_of_le_left, p'] using hx⟩
  obtain ⟨o, hsubset, ho, himgo⟩ := s.exists_subset_injOn_image_eq_of_surjOn (p : Set R) this
  have hI : I.FG := IsNoetherian.noetherian I
  let t : Finset R := o ∪ (Submodule.FG.finite_generators hI).toFinset
  suffices h : p.height ≤ t.card by
    refine le_trans h (hs ▸ ?_)
    norm_cast
    have : (Submodule.FG.finite_generators hI).toFinset.card = I.spanFinrank := by
      rw [← Set.ncard_eq_toFinset_card (hs := Submodule.FG.finite_generators hI)]
      exact Submodule.FG.generators_ncard hI
    grind
  refine Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_
  rw [Finset.coe_union, Set.Finite.coe_toFinset, span_union, sup_comm, span,
    Submodule.span_generators]
  refine Ideal.mem_minimalPrimes_sup hrp ?_
  convert! hps
  simp [Ideal.map_span, ← himgo]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
let let₁ let₂ :
  p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
let₃ :
  let p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p;
  ∀ (this : p'.IsPrime),
    p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
let₄ :
  let p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p;
  ∀ (this : p'.IsPrime) (s : Finset (R ⧸ I))
    (hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p')
    (hs : (↑s.card : ℕ∞) = p'.height),
    p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
⊢ p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
have let₅ : let p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p;
∀ (this : p'.IsPrime) (s : Finset (R ⧸ I))
  (hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p')
  (hs : (↑s.card : ℕ∞) = p'.height) (hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))),
  p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
Tactic: classical
  let p' := p.map (algebraMap R (R ⧸ I))
  have : p'.IsPrime := isPrime_map_quotientMk_of_isPrime hrp
  obtain ⟨s, hps, hs⟩ := exists_finset_card_eq_height_of_isNoetherianRing p'
  have hsp' : (s : Set (R ⧸ I)) ⊆ (p' : Set _) := fun _ hx ↦ hps.le (subset_span hx)
  have : Set.SurjOn (Ideal.Quotient.mk I) p s := by
    refine Set.SurjOn.mono subset_rfl hsp' fun x hx ↦ ?_
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    exact ⟨x, by simpa [hrp, sup_of_le_left, p'] using hx⟩
  obtain ⟨o, hsubset, ho, himgo⟩ := s.exists_subset_injOn_image_eq_of_surjOn (p : Set R) this
  have hI : I.FG := IsNoetherian.noetherian I
  let t : Finset R := o ∪ (Submodule.FG.finite_generators hI).toFinset
  suffices h : p.height ≤ t.card by
    refine le_trans h (hs ▸ ?_)
    norm_cast
    have : (Submodule.FG.finite_generators hI).toFinset.card = I.spanFinrank := by
      rw [← Set.ncard_eq_toFinset_card (hs := Submodule.FG.finite_generators hI)]
      exact Submodule.FG.generators_ncard hI
    grind
  refine Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_
  rw [Finset.coe_union, Set.Finite.coe_toFinset, span_union, sup_comm, span,
    Submodule.span_generators]
  refine Ideal.mem_minimalPrimes_sup hrp ?_
  convert! hps
  simp [Ideal.map_span, ← himgo]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p I : Ideal R
inst_2 : p.IsPrime
h : I ≤ p
⊢ (↑p.height : WithBot ℕ∞) ≤ ringKrullDim.{u_1} (R ⧸ I) + (↑(Submodule.spanFinrank I) : WithBot ℕ∞)
have trans : (↑p.height : WithBot ℕ∞) ≤
  (↑(Ideal.height (R := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p)) : WithBot ℕ∞) +
    (↑(Submodule.spanFinrank I) : WithBot ℕ∞)
Tactic: trans (p.map (Ideal.Quotient.mk I)).height + I.spanFinrank
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p I : Ideal R
inst_2 : p.IsPrime
h : I ≤ p
trans :
  (↑p.height : WithBot ℕ∞) ≤
    (↑(Ideal.height (R := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p)) : WithBot ℕ∞) +
      (↑(Submodule.spanFinrank I) : WithBot ℕ∞)
⊢ (↑p.height : WithBot ℕ∞) ≤ ringKrullDim.{u_1} (R ⧸ I) + (↑(Submodule.spanFinrank I) : WithBot ℕ∞)
have trans₁ : (↑(Ideal.height (R := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p)) : WithBot ℕ∞) +
    (↑(Submodule.spanFinrank I) : WithBot ℕ∞) ≤
  ringKrullDim.{u_1} (R ⧸ I) + (↑(Submodule.spanFinrank I) : WithBot ℕ∞)
Tactic: trans (p.map (Ideal.Quotient.mk I)).height + I.spanFinrank
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p I : Ideal R
inst_2 : p.IsPrime
h : I ≤ p
⊢ (↑p.height : WithBot ℕ∞) ≤
    (↑(Ideal.height (R := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p)) : WithBot ℕ∞) +
      (↑(Submodule.spanFinrank I) : WithBot ℕ∞)
have norm_cast : p.height ≤
  Ideal.height (R := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
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
p I : Ideal R
inst_2 : p.IsPrime
h : I ≤ p
⊢ (↑(Ideal.height (R := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p)) : WithBot ℕ∞) +
      (↑(Submodule.spanFinrank I) : WithBot ℕ∞) ≤
    ringKrullDim.{u_1} (R ⧸ I) + (↑(Submodule.spanFinrank I) : WithBot ℕ∞)
have bc : (↑(Ideal.height (R := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p)) : WithBot ℕ∞) ≤
  ringKrullDim.{u_1} (R ⧸ I)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p I : Ideal R
inst_2 : p.IsPrime
h : I ≤ p
⊢ (↑(Ideal.height (R := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p)) : WithBot ℕ∞) ≤
    ringKrullDim.{u_1} (R ⧸ I)
have this : Ideal.IsPrime (α := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p)
Tactic: have : (Ideal.map (Ideal.Quotient.mk I) p).IsPrime :=
      Ideal.isPrime_map_quotientMk_of_isPrime h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
h : I ≤ Ring.jacobson R
⊢ ringKrullDim R ≤ ringKrullDim.{u_1} (R ⧸ I) + (↑(Submodule.spanFinrank I) : WithBot ℕ∞)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
h : I ≤ Ring.jacobson R
h_1 : Nontrivial R
⊢ ringKrullDim R ≤ ringKrullDim.{u_1} (R ⧸ I) + (↑(Submodule.spanFinrank I) : WithBot ℕ∞)
have rw : ∀ ⦃m : Ideal R⦄,
  m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ ringKrullDim.{u_1} (R ⧸ I) + (↑(Submodule.spanFinrank I) : WithBot ℕ∞)
Tactic: rw [ringKrullDim_le_iff_isMaximal_height_le]
-- 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
p : Ideal R
inst_2 : p.IsPrime
hrm : s ⊆ (↑p : Set R)
⊢ p.height ≤
    height (R := HasQuotient.Quotient R (B := Ideal R) (span s))
        (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (span s)) (Quotient.mk (span s)) p) +
      s.encard
have apply : span s ≤ p
Tactic: apply le_trans (Ideal.height_le_height_add_spanFinrank_of_le (I := span s) (p := p) ?_) ?_
-- 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
p : Ideal R
inst_2 : p.IsPrime
hrm : s ⊆ (↑p : Set R)
apply : span s ≤ p
⊢ p.height ≤
    height (R := HasQuotient.Quotient R (B := Ideal R) (span s))
        (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (span s)) (Quotient.mk (span s)) p) +
      s.encard
have apply₁ : height (R := HasQuotient.Quotient R (B := Ideal R) (span s))
      (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (span s)) (Quotient.mk (span s)) p) +
    (↑(Submodule.spanFinrank (span s)) : ℕ∞) ≤
  height (R := HasQuotient.Quotient R (B := Ideal R) (span s))
      (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (span s)) (Quotient.mk (span s)) p) +
    s.encard
Tactic: apply le_trans (Ideal.height_le_height_add_spanFinrank_of_le (I := span s) (p := p) ?_) ?_
-- 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
p : Ideal R
inst_2 : p.IsPrime
hrm : s ⊆ (↑p : Set R)
⊢ height (R := HasQuotient.Quotient R (B := Ideal R) (span s))
        (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (span s)) (Quotient.mk (span s)) p) +
      (↑(Submodule.spanFinrank (span s)) : ℕ∞) ≤
    height (R := HasQuotient.Quotient R (B := Ideal R) (span s))
        (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (span s)) (Quotient.mk (span s)) p) +
      s.encard
have bc : (↑(Submodule.spanFinrank (span s)) : ℕ∞) ≤ s.encard
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)
⊢ (↑p.height : WithBot ℕ∞) ≤
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span s)) + (↑s.encard : WithBot ℕ∞)
have refine_1 : span s ≤ p
Tactic: refine le_trans (height_le_ringKrullDim_quotient_add_spanFinrank (I := .span s) ?_) ?_
-- 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)
refine_1 : span s ≤ p
⊢ (↑p.height : WithBot ℕ∞) ≤
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span s)) + (↑s.encard : WithBot ℕ∞)
have refine_2 : 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 ℕ∞)
Tactic: refine le_trans (height_le_ringKrullDim_quotient_add_spanFinrank (I := .span s) ?_) ?_