awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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) : ℕ∞)

Tactic:
le_trans h (hs ▸ ?_)

Premises used: Eq.rec, le_trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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 : ℕ∞)
refine : (↑t.card : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) (↑(Submodule.spanFinrank I) : ℕ∞)
⊢ p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)

Tactic:
refine le_trans h (hs ▸ ?_)

Premises used: le_trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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 : ℕ∞)
norm_cast : t.card ≤ s.card + Submodule.spanFinrank I
⊢ (↑t.card : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) (↑(Submodule.spanFinrank I) : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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 : ℕ∞)
rw : (Submodule.generators I).ncard = Submodule.spanFinrank I
⊢ ⋯.toFinset (s := Submodule.generators I).card = Submodule.spanFinrank I

Tactic:
rw [← Set.ncard_eq_toFinset_card (hs := Submodule.FG.finite_generators hI)]

Premises used: Set.ncard_eq_toFinset_card, Submodule.FG.finite_generators
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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 : ℕ∞)
⊢ (Submodule.generators I).ncard = Submodule.spanFinrank I

Tactic:
Submodule.FG.generators_ncard hI

Premises used: Submodule.FG.generators_ncard
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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 : ℕ∞)
⊢ (Submodule.generators I).ncard = Submodule.spanFinrank I

Tactic:
exact Submodule.FG.generators_ncard hI

Premises used: Submodule.FG.generators_ncard
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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

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
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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_2 : 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 : ℕ∞)
this : ⋯.toFinset (s := Submodule.generators I).card = Submodule.spanFinrank I
⊢ t.card ≤ s.card + Submodule.spanFinrank I

Tactic:
grind
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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)
suffices : p.height ≤ (↑t.card : ℕ∞)
⊢ p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)

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
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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 : ℕ∞)

Tactic:
Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_

Premises used: Ideal.height_le_card_of_mem_minimalPrimes_span_finset
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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)
refine : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑t : Set R))) p
⊢ p.height ≤ (↑t.card : ℕ∞)

Tactic:
refine Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_

Premises used: Ideal.height_le_card_of_mem_minimalPrimes_span_finset
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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)
rw : p ∈ (I ⊔ span (↑o : Set R)).minimalPrimes
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑t : Set R))) p

Tactic:
rw [Finset.coe_union, Set.Finite.coe_toFinset, span_union, sup_comm, span,
    Submodule.span_generators]

Premises used: Set.Finite.coe_toFinset, sup_comm, Ideal.span, Ideal.span_union, Submodule.span_generators, Finset.coe_union
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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

Tactic:
Ideal.mem_minimalPrimes_sup hrp ?_

Premises used: Set.Mem, setOf, Ideal.mem_minimalPrimes_sup
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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)
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)
⊢ p ∈ (I ⊔ span (↑o : Set R)).minimalPrimes

Tactic:
refine Ideal.mem_minimalPrimes_sup hrp ?_

Premises used: Ideal.mem_minimalPrimes_sup
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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 (span (↑s : Set (R ⧸ I)))) p'

Tactic:
hps
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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 :
  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)))
⊢ 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:
convert! hps
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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)
e_2 : 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:
simp [Ideal.map_span, ← himgo]

Premises used: Ideal.map_span
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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 ℕ∞)
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 ℕ∞)
⊢ (↑p.height : WithBot ℕ∞) ≤ ringKrullDim.{u_1} (R ⧸ I) + (↑(Submodule.spanFinrank I) : WithBot ℕ∞)

Tactic:
trans (p.map (Ideal.Quotient.mk I)).height + I.spanFinrank

Premises used: Ideal.Quotient.mk, Ideal.map, Submodule.spanFinrank, Ideal.height
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p I : Ideal R
inst_2 : p.IsPrime
h : I ≤ p
norm_cast :
  p.height ≤
    Ideal.height (R := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
⊢ (↑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:
norm_cast
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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 ≤
    Ideal.height (R := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)

Tactic:
Ideal.height_le_height_add_spanFinrank_of_le h

Premises used: Ideal.height_le_height_add_spanFinrank_of_le
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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 ≤
    Ideal.height (R := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)

Tactic:
exact Ideal.height_le_height_add_spanFinrank_of_le h

Premises used: Ideal.height_le_height_add_spanFinrank_of_le
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p I : Ideal R
inst_2 : p.IsPrime
h : I ≤ p
bc :
  (↑(Ideal.height (R := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p)) : WithBot ℕ∞) ≤
    ringKrullDim.{u_1} (R ⧸ I)
⊢ (↑(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:
gcongr
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p I : Ideal R
inst_2 : p.IsPrime
h : I ≤ p
⊢ 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
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p I : Ideal R
inst_2 : p.IsPrime
h : I ≤ p
this : Ideal.IsPrime (α := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p)
⊢ (↑(Ideal.height (R := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p)) : WithBot ℕ∞) ≤
    ringKrullDim.{u_1} (R ⧸ I)

Tactic:
Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top'

Premises used: Ideal.IsPrime.ne_top', Ideal.height_le_ringKrullDim_of_ne_top
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p I : Ideal R
inst_2 : p.IsPrime
h : I ≤ p
this : Ideal.IsPrime (α := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p)
⊢ (↑(Ideal.height (R := R ⧸ I) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p)) : WithBot ℕ∞) ≤
    ringKrullDim.{u_1} (R ⧸ I)

Tactic:
exact Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top'

Premises used: Ideal.IsPrime.ne_top', Ideal.height_le_ringKrullDim_of_ne_top
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
h : I ≤ Ring.jacobson R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
h : I ≤ Ring.jacobson R
h_1 : Nontrivial R
rw :
  ∀ ⦃m : Ideal R⦄,
    m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ ringKrullDim.{u_1} (R ⧸ I) + (↑(Submodule.spanFinrank I) : WithBot ℕ∞)
⊢ ringKrullDim R ≤ ringKrullDim.{u_1} (R ⧸ I) + (↑(Submodule.spanFinrank I) : WithBot ℕ∞)

Tactic:
rw [ringKrullDim_le_iff_isMaximal_height_le]

Premises used: ringKrullDim_le_iff_isMaximal_height_le
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
h : I ≤ Ring.jacobson R
h_1 : Nontrivial R
m : Ideal R
hm : m.IsMaximal
⊢ (↑m.height : WithBot ℕ∞) ≤ ringKrullDim.{u_1} (R ⧸ I) + (↑(Submodule.spanFinrank I) : WithBot ℕ∞)

Tactic:
height_le_ringKrullDim_quotient_add_spanFinrank <|
    le_trans h <| Ring.jacobson_le_of_isMaximal m

Premises used: Ring.jacobson_le_of_isMaximal, height_le_ringKrullDim_quotient_add_spanFinrank, le_trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
h : I ≤ Ring.jacobson R
h_1 : Nontrivial R
m : Ideal R
hm : m.IsMaximal
⊢ (↑m.height : WithBot ℕ∞) ≤ ringKrullDim.{u_1} (R ⧸ I) + (↑(Submodule.spanFinrank I) : WithBot ℕ∞)

Tactic:
exact height_le_ringKrullDim_quotient_add_spanFinrank <|
    le_trans h <| Ring.jacobson_le_of_isMaximal m

Premises used: Ring.jacobson_le_of_isMaximal, height_le_ringKrullDim_quotient_add_spanFinrank, le_trans