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 : Ideal R
hI : I ≠ ⊤
J : Ideal R
hJ₁ : J ≤ I
hJ₂ : Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1})
hJ₃ : I.height ≤ J.height
⊢ Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1})

Tactic:
hJ₂
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
J : Ideal R
hJ₁ : J ≤ I
hJ₂ : Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1})
hJ₃ : I.height ≤ J.height
h : (↑I.height : Cardinal.{u_1}) = (↑I.height.toNat : Cardinal.{u_1})
⊢ Submodule.spanRank J ≤ (↑I.height : Cardinal.{u_1})

Tactic:
convert! hJ₂
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
J : Ideal R
hJ₁ : J ≤ I
hJ₂ : Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1})
hJ₃ : I.height ≤ J.height
⊢ (↑I.height : Cardinal.{u_1}) = (↑I.height.toNat : Cardinal.{u_1})

Tactic:
Cardinal.ofENat_eq_nat.mpr (ENat.coe_toNat (I.height_ne_top hI)).symm

Premises used: Iff.mpr, ENat.coe_toNat, Cardinal.ofENat_eq_nat, Ideal.height_ne_top, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
J : Ideal R
hJ₁ : J ≤ I
hJ₂ : Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1})
hJ₃ : I.height ≤ J.height
⊢ (↑I.height : Cardinal.{u_1}) = (↑I.height.toNat : Cardinal.{u_1})

Tactic:
exact Cardinal.ofENat_eq_nat.mpr (ENat.coe_toNat (I.height_ne_top hI)).symm

Premises used: Iff.mpr, ENat.coe_toNat, Cardinal.ofENat_eq_nat, Ideal.height_ne_top, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
J : Ideal R
hJ₁ : J ≤ I
hJ₂ : Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1})
hJ₃ : I.height ≤ J.height
⊢ (↑I.height : Cardinal.{u_1}) ≤ (↑J.height : Cardinal.{u_1})

Tactic:
Cardinal.ofENat_le_ofENat_of_le hJ₃

Premises used: Cardinal.ofENat_le_ofENat_of_le
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
J : Ideal R
hJ₁ : J ≤ I
hJ₂ : Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1})
hJ₃ : I.height ≤ J.height
⊢ (↑I.height : Cardinal.{u_1}) ≤ (↑J.height : Cardinal.{u_1})

Tactic:
exact Cardinal.ofENat_le_ofENat_of_le hJ₃

Premises used: Cardinal.ofENat_le_ofENat_of_le
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
hJ₁ : ⊤ ≤ I
hJ₂ : Submodule.spanRank (R := R) (M := R) ⊤ ≤ (↑I.height.toNat : Cardinal.{u_1})
hJ₃ : I.height ≤ height.{u_1} (R := R) ⊤
⊢ False

Tactic:
hI (top_le_iff.mp hJ₁)

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
hJ₁ : ⊤ ≤ I
hJ₂ : Submodule.spanRank (R := R) (M := R) ⊤ ≤ (↑I.height.toNat : Cardinal.{u_1})
hJ₃ : I.height ≤ height.{u_1} (R := R) ⊤
⊢ False

Tactic:
exact hI (top_le_iff.mp hJ₁)

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
n : ℕ∞
mp : p.height ≤ n → ∃ (I : Ideal R), p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})
mpr : (∃ (I : Ideal R), p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})) → p.height ≤ n
⊢ p.height ≤ n ↔ ∃ (I : Ideal R), p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
n : ℕ∞
h : p.height ≤ n
mp :
  ∀ (I : Ideal R) (hI : I ≤ p) (e₁ : Submodule.spanRank I = (↑p.height : Cardinal.{u_1})) (e₂ : I.height = p.height),
    ∃ (I : Ideal R), p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})
⊢ ∃ (I : Ideal R), p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})

Tactic:
obtain ⟨I, hI, e₁, e₂⟩ := exists_spanRank_eq_and_height_eq p (IsPrime.ne_top ‹_›)

Premises used: Ideal.exists_spanRank_eq_and_height_eq, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
n : ℕ∞
h : p.height ≤ n
I : Ideal R
hI : I ≤ p
e₁ : Submodule.spanRank I = (↑p.height : Cardinal.{u_1})
e₂ : I.height = p.height
⊢ ∃ (I : Ideal R), p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})

Tactic:
⟨I, Ideal.mem_minimalPrimes_of_height_eq hI e₂.ge, e₁.symm ▸ ?_⟩

Premises used: Eq.ge, Ideal.mem_minimalPrimes_of_height_eq, Eq.rec, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
n : ℕ∞
h : p.height ≤ n
I : Ideal R
hI : I ≤ p
e₁ : Submodule.spanRank I = (↑p.height : Cardinal.{u_1})
e₂ : I.height = p.height
mp : (↑p.height : Cardinal.{u_1}) ≤ (↑n : Cardinal.{u_1})
⊢ ∃ (I : Ideal R), p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})

Tactic:
refine ⟨I, Ideal.mem_minimalPrimes_of_height_eq hI e₂.ge, e₁.symm ▸ ?_⟩
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
n : ℕ∞
h : p.height ≤ n
I : Ideal R
hI : I ≤ p
e₁ : Submodule.spanRank I = (↑p.height : Cardinal.{u_1})
e₂ : I.height = p.height
mp mp₁ mp₂ mp₃ : p.height ≤ n
⊢ (↑p.height : Cardinal.{u_1}) ≤ (↑n : Cardinal.{u_1})

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
n : ℕ∞
I : Ideal R
hp : p ∈ I.minimalPrimes
hI : Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})
⊢ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) ≤ n

Tactic:
simpa using (Cardinal.toENat.monotone' hI)

Premises used: OrderRingHom.monotone', Cardinal.toENat
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
n : ℕ∞
I : Ideal R
hp : p ∈ I.minimalPrimes
hI : Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})
⊢ p.height ≤ n

Tactic:
exact le_trans
      (Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes I p hp)
      (by simpa using (Cardinal.toENat.monotone' hI))

Premises used: Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes, le_trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
obtain :
  ∀ (I : Ideal R) (hI : p ∈ I.minimalPrimes) (hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})),
    ∃ (s : Finset R),
      Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p ∧ (↑s.card : ℕ∞) = p.height
⊢ ∃ (s : Finset R),
    Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p ∧ (↑s.card : ℕ∞) = p.height

Tactic:
obtain ⟨I, hI, hr⟩ := (p.height_le_iff_exists_minimalPrimes <| p.height).mp le_rfl

Premises used: Ideal.height_le_iff_exists_minimalPrimes, le_rfl, Iff.mp, Ideal.height
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
⊢ (Submodule.generators I).Finite

Tactic:
have hs : I.generators.Finite := (IsNoetherian.noetherian I).finite_generators
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
rwa : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (Submodule.generators I))) p
rwa₁ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (Submodule.span R (Submodule.generators I))) p
rwa₂ rwa₃ rwa₄ rwa₅ : p ∈ I.minimalPrimes
⊢ Membership.mem (γ := Set (Ideal R))
    (Ideal.minimalPrimes (span (↑(hs.toFinset (s := Submodule.generators I)) : Set R))) p

Tactic:
rwa [hs.coe_toFinset, span, I.span_generators]

Premises used: Set.Finite.coe_toFinset, Ideal.span, Submodule.span_generators
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
refine : (↑hs.toFinset (s := Submodule.generators I).card : ℕ∞) = p.height
⊢ ∃ (s : Finset R),
    Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p ∧ (↑s.card : ℕ∞) = p.height

Tactic:
refine ⟨hs.toFinset, by rwa [hs.coe_toFinset, span, I.span_generators], ?_⟩
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
rw : (↑(Submodule.spanFinrank I) : ℕ∞) = p.height
⊢ (↑hs.toFinset (s := Submodule.generators I).card : ℕ∞) = p.height

Tactic:
rw [← Set.ncard_eq_toFinset_card (hs := hs), (IsNoetherian.noetherian I).generators_ncard]

Premises used: IsNoetherian.noetherian, Submodule.FG.generators_ncard, Set.ncard_eq_toFinset_card
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
⊢ (↑(Submodule.spanFinrank I) : ℕ∞) = p.height

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
refine_1 : (↑(Submodule.spanFinrank I) : ℕ∞) ≤ p.height
refine_2 : p.height ≤ (↑(Submodule.spanFinrank I) : ℕ∞)
⊢ (↑(Submodule.spanFinrank I) : ℕ∞) = p.height

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
⊢ (↑(Submodule.spanFinrank I) : Cardinal.{u_1}) ≤ (↑p.height : Cardinal.{u_1})

Tactic:
rw [Submodule.fg_iff_spanRank_eq_spanFinrank.mpr (IsNoetherian.noetherian I)] at hr

Premises used: Submodule.fg_iff_spanRank_eq_spanFinrank, Iff.mpr, IsNoetherian.noetherian
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
hr₁ : (↑(Submodule.spanFinrank I) : Cardinal.{u_1}) ≤ (↑p.height : Cardinal.{u_1})
⊢ (Submodule.generators I).Finite

Tactic:
rw [Submodule.fg_iff_spanRank_eq_spanFinrank.mpr (IsNoetherian.noetherian I)] at hr

Premises used: Submodule.fg_iff_spanRank_eq_spanFinrank, Iff.mpr, IsNoetherian.noetherian
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : (↑(Submodule.spanFinrank I) : Cardinal.{u_1}) ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
⊢ (↑(Submodule.spanFinrank I) : ℕ∞) ≤ p.height

Tactic:
Cardinal.nat_le_ofENat.mp hr

Premises used: Iff.mp, Cardinal.nat_le_ofENat
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : (↑(Submodule.spanFinrank I) : Cardinal.{u_1}) ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
⊢ (↑(Submodule.spanFinrank I) : ℕ∞) ≤ p.height

Tactic:
exact Cardinal.nat_le_ofENat.mp hr

Premises used: Iff.mp, Cardinal.nat_le_ofENat
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
h :
  Eq (α := ℕ∞) ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)
refine_2 : p.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)
⊢ p.height ≤ (↑(Submodule.spanFinrank I) : ℕ∞)

Tactic:
convert_to p.height ≤ I.spanRank.toENat

Premises used: Cardinal.toENat, Ideal.height, DFunLike.coe, Submodule.spanRank
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
h :
  Eq (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)
    ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
⊢ Eq (α := ℕ∞) ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)

Tactic:
symm
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
⊢ Eq (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)
    ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)

Tactic:
simpa [Submodule.fg_iff_spanRank_eq_spanFinrank] using (IsNoetherian.noetherian I)

Premises used: Submodule.fg_iff_spanRank_eq_spanFinrank, IsNoetherian.noetherian
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
⊢ p.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)

Tactic:
I.height_le_spanRank_toENat_of_mem_minimalPrimes _ hI

Premises used: Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
⊢ p.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)

Tactic:
exact I.height_le_spanRank_toENat_of_mem_minimalPrimes _ hI

Premises used: Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes
-- 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
⊢ p'.IsPrime

Tactic:
have : p'.IsPrime := isPrime_map_quotientMk_of_isPrime hrp
-- 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 : p'.IsPrime
obtain :
  ∀ (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) : ℕ∞)

Tactic:
obtain ⟨s, hps, hs⟩ := exists_finset_card_eq_height_of_isNoetherianRing p'

Premises used: Ideal.exists_finset_card_eq_height_of_isNoetherianRing
-- 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 : 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
⊢ (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))

Tactic:
have hsp' : (s : Set (R ⧸ I)) ⊆ (p' : Set _) := fun _ hx ↦ hps.le (subset_span hx)
-- 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 : 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))
⊢ Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))

Tactic:
Set.SurjOn.mono subset_rfl hsp' fun x hx ↦ ?_

Premises used: Set.SurjOn.mono, subset_rfl
-- 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 : 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))
refine :
  ∀ (x : R ⧸ I) (hx : x ∈ (↑p' : Set (R ⧸ I))),
    Membership.mem (γ := Set (R ⧸ I)) ((⇑(Quotient.mk I) : (a : R) → R ⧸ I) '' (↑p : Set R)) x
⊢ Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))

Tactic:
refine Set.SurjOn.mono subset_rfl hsp' fun x hx ↦ ?_

Premises used: Set.SurjOn.mono, subset_rfl
-- 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 : 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))
x : R ⧸ I
hx : x ∈ (↑p' : Set (R ⧸ I))
obtain :
  ∀ (x : R) (hx : Membership.mem (α := R ⧸ I) (↑p' : Set (R ⧸ I)) ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)),
    Membership.mem (α := R ⧸ I) (γ := Set (R ⧸ I)) ((⇑(Quotient.mk I) : (a : R) → R ⧸ I) '' (↑p : Set R))
      ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
⊢ Membership.mem (γ := Set (R ⧸ I)) ((⇑(Quotient.mk I) : (a : R) → R ⧸ I) '' (↑p : Set R)) x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- 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 : 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))
x : R
hx : Membership.mem (α := R ⧸ I) (↑p' : Set (R ⧸ I)) ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
⊢ x ∈ (↑p : Set R) ∧
    Eq (α := R ⧸ I) ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)

Tactic:
simpa [hrp, sup_of_le_left, p'] using hx

Premises used: sup_of_le_left
-- 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 : 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))
x : R
hx : Membership.mem (α := R ⧸ I) (↑p' : Set (R ⧸ I)) ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
⊢ Membership.mem (α := R ⧸ I) (γ := Set (R ⧸ I)) ((⇑(Quotient.mk I) : (a : R) → R ⧸ I) '' (↑p : Set R))
    ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)

Tactic:
exact ⟨x, by simpa [hrp, sup_of_le_left, p'] using hx⟩
-- 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 : 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))
⊢ Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))

Tactic:
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⟩
-- 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))
obtain :
  ∀ (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),
    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) : ℕ∞)

Tactic:
obtain ⟨o, hsubset, ho, himgo⟩ := s.exists_subset_injOn_image_eq_of_surjOn (p : Set R) this

Premises used: SetLike.coe, Finset.exists_subset_injOn_image_eq_of_surjOn
-- 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
⊢ I.FG

Tactic:
have hI : I.FG := IsNoetherian.noetherian I