awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal A
inst_4 : J.IsPrime
e : OrderIso.{u_2, u_1} { p : Ideal A // p.IsPrime }
  { p : Ideal R // p.IsPrime ∧ Disjoint (↑S : Set R) (↑p : Set R) } :=
  orderIsoOfPrime S A
H : ∀ (p : Ideal R) (hp : p ≤ comap (F := R →+* A) (algebraMap R A) J), Disjoint (↑S : Set R) (↑p : Set R)
⊢ Order.krullDim.{u_2} (↑(Set.Iic { asIdeal := J, isPrime := inst_4 : PrimeSpectrum A }) : Type u_2) =
    Order.krullDim.{u_1} (↑(Set.Iic { asIdeal := comap (F := R →+* A) (algebraMap R A) J, isPrime := ⋯ }) : Type u_1)

Tactic:
Order.krullDim_eq_of_orderIso
    { toFun I := ⟨⟨I.1.1.comap (algebraMap R A), (e ⟨_, I.1.2⟩).2.1⟩, Ideal.comap_mono I.2⟩
      invFun I := ⟨⟨_, (e.symm ⟨_, I.1.2, H _ I.2⟩).2⟩, Ideal.map_le_iff_le_comap.mpr I.2⟩
      left_inv I := Subtype.ext <| PrimeSpectrum.ext_iff.mpr <|
        congrArg (fun I ↦ I.1) (e.left_inv ⟨_, I.1.2⟩)
      right_inv I := Subtype.ext <| PrimeSpectrum.ext_iff.mpr <|
        congrArg (fun I ↦ I.1) (e.right_inv ⟨_, I.1.2, H _ I.2⟩)
      map_rel_iff' {I₁ I₂} := @RelIso.map_rel_iff _ _ _ _ e ⟨_, I₁.1.2⟩ ⟨_, I₂.1.2⟩ }

Premises used: Iff.mpr, PrimeSpectrum.mk, Algebra.algebraMap, RelIso.mk, PrimeSpectrum.isPrime, Equiv.mk, Order.krullDim_eq_of_orderIso, Ideal.comap_mono, OrderIso.symm, Subtype.mk, Ideal.map_le_iff_le_comap, And.left, RelIso.map_rel_iff, PrimeSpectrum.ext_iff, And.intro, Ideal.comap, Subtype.val, DFunLike.coe, PrimeSpectrum.asIdeal, Subtype.property, Subtype.ext
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal A
inst_4 : J.IsPrime
e : OrderIso.{u_2, u_1} { p : Ideal A // p.IsPrime }
  { p : Ideal R // p.IsPrime ∧ Disjoint (↑S : Set R) (↑p : Set R) } :=
  orderIsoOfPrime S A
H : ∀ (p : Ideal R) (hp : p ≤ comap (F := R →+* A) (algebraMap R A) J), Disjoint (↑S : Set R) (↑p : Set R)
⊢ Order.krullDim.{u_2} (↑(Set.Iic { asIdeal := J, isPrime := inst_4 : PrimeSpectrum A }) : Type u_2) =
    Order.krullDim.{u_1} (↑(Set.Iic { asIdeal := comap (F := R →+* A) (algebraMap R A) J, isPrime := ⋯ }) : Type u_1)

Tactic:
exact Order.krullDim_eq_of_orderIso
    { toFun I := ⟨⟨I.1.1.comap (algebraMap R A), (e ⟨_, I.1.2⟩).2.1⟩, Ideal.comap_mono I.2⟩
      invFun I := ⟨⟨_, (e.symm ⟨_, I.1.2, H _ I.2⟩).2⟩, Ideal.map_le_iff_le_comap.mpr I.2⟩
      left_inv I := Subtype.ext <| PrimeSpectrum.ext_iff.mpr <|
        congrArg (fun I ↦ I.1) (e.left_inv ⟨_, I.1.2⟩)
      right_inv I := Subtype.ext <| PrimeSpectrum.ext_iff.mpr <|
        congrArg (fun I ↦ I.1) (e.right_inv ⟨_, I.1.2, H _ I.2⟩)
      map_rel_iff' {I₁ I₂} := @RelIso.map_rel_iff _ _ _ _ e ⟨_, I₁.1.2⟩ ⟨_, I₂.1.2⟩ }

Premises used: Iff.mpr, RelIso.mk, Equiv.mk, Order.krullDim_eq_of_orderIso, PrimeSpectrum.ext_iff, Subtype.ext
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal A
inst_4 : J.IsPrime
⊢ primeHeight (comap (F := R →+* A) (algebraMap R A) J) = J.primeHeight

Tactic:
simpa [Ideal.height_eq_primeHeight] using IsLocalization.height_under_eq_of_isPrime S J

Premises used: _private.0.IsLocalization.height_under_eq_of_isPrime, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal A
rw :
  Eq (α := ℕ∞)
    (⨅ (J_1 : Ideal R),
      ⨅ (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap (F := R →+* A) (algebraMap R A) J)) J_1),
        J_1.height)
    (⨅ J_1 ∈ J.minimalPrimes, J_1.height)
⊢ height (under R J) = J.height

Tactic:
rw [(J.comap _).height_eq_inf_minimalPrimes, J.height_eq_inf_minimalPrimes]

Premises used: Ideal.comap, Ideal.height_eq_inf_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal A
simp :
  Eq (α := ℕ∞) (⨅ b ∈ J.minimalPrimes, height (comap (F := R →+* A) (algebraMap R A) b))
    (⨅ J_1 ∈ J.minimalPrimes, J_1.height)
⊢ Eq (α := ℕ∞)
    (⨅ (J_1 : Ideal R),
      ⨅ (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap (F := R →+* A) (algebraMap R A) J)) J_1),
        J_1.height)
    (⨅ J_1 ∈ J.minimalPrimes, J_1.height)

Tactic:
simp only [IsLocalization.minimalPrimes_comap S A, iInf_image]

Premises used: IsLocalization.minimalPrimes_comap, iInf_image
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal A
apply : ∀ (p : Ideal A) (hp : p ∈ J.minimalPrimes), height (comap (F := R →+* A) (algebraMap R A) p) = p.height
⊢ Eq (α := ℕ∞) (⨅ b ∈ J.minimalPrimes, height (comap (F := R →+* A) (algebraMap R A) b))
    (⨅ J_1 ∈ J.minimalPrimes, J_1.height)

Tactic:
apply iInf_congr (fun p ↦ iInf_congr fun hp ↦ ?_)

Premises used: iInf_congr
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J p : Ideal A
hp : p ∈ J.minimalPrimes
⊢ p.IsPrime

Tactic:
have := hp.isPrime
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J p : Ideal A
hp : p ∈ J.minimalPrimes
this : p.IsPrime
⊢ height (comap (F := R →+* A) (algebraMap R A) p) = p.height

Tactic:
IsLocalization.height_under_eq_of_isPrime S _

Premises used: _private.0.IsLocalization.height_under_eq_of_isPrime
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J p : Ideal A
hp : p ∈ J.minimalPrimes
this : p.IsPrime
⊢ height (comap (F := R →+* A) (algebraMap R A) p) = p.height

Tactic:
exact IsLocalization.height_under_eq_of_isPrime S _

Premises used: _private.0.IsLocalization.height_under_eq_of_isPrime
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
A : Type u_2
inst_2 : CommRing A
inst_3 : Algebra R A
inst_4 : IsLocalization.AtPrime A I
⊢ IsLocalRing A

Tactic:
have := IsLocalization.AtPrime.isLocalRing A I
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
A : Type u_2
inst_2 : CommRing A
inst_3 : Algebra R A
inst_4 : IsLocalization.AtPrime A I
this : IsLocalRing A
rw : (↑(height (IsLocalRing.maximalIdeal A)) : WithBot ℕ∞) = (↑I.height : WithBot ℕ∞)
rw₁ : (↑(height (under R (IsLocalRing.maximalIdeal A))) : WithBot ℕ∞) = (↑I.height : WithBot ℕ∞)
rw₂ rw₃ :
  (↑(height (under R (IsLocalRing.maximalIdeal A))) : WithBot ℕ∞) =
    (↑(height (under R (IsLocalRing.maximalIdeal A))) : WithBot ℕ∞)
⊢ ringKrullDim A = (↑I.height : WithBot ℕ∞)

Tactic:
rw [← IsLocalRing.maximalIdeal_height_eq_ringKrullDim,
      ← IsLocalization.height_under I.primeCompl,
      ← IsLocalization.AtPrime.under_maximalIdeal A I]

Premises used: IsLocalization.height_under, IsLocalization.AtPrime.isLocalRing, Ideal.primeCompl, IsLocalRing.maximalIdeal_height_eq_ringKrullDim, IsLocalization.AtPrime.under_maximalIdeal
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
p : Ideal R
inst_4 : p.IsPrime
h : Disjoint (↑M : Set R) (↑p : Set R)
P : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) p
⊢ P.IsPrime

Tactic:
have : P.IsPrime := isPrime_of_isPrime_disjoint M S p ‹_› h
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
p : Ideal R
inst_4 : p.IsPrime
h : Disjoint (↑M : Set R) (↑p : Set R)
P : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) p
this : P.IsPrime
⊢ IsLocalization.AtPrime.{u_1, u_2} (Localization.AtPrime P) (comap (F := R →+* S) (algebraMap R S) P)

Tactic:
have := isLocalization_isLocalization_atPrime_isLocalization (M := M) (Localization.AtPrime P) P
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
p : Ideal R
inst_4 : p.IsPrime
h : Disjoint (↑M : Set R) (↑p : Set R)
P : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) p
this_1 : P.IsPrime
this : IsLocalization.AtPrime.{u_1, u_2} (Localization.AtPrime P) (comap (F := R →+* S) (algebraMap R S) P)
⊢ IsLocalization.AtPrime.{u_1, u_2} (Localization.AtPrime (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) p

Tactic:
simp_rw [P, under_map_of_isPrime_disjoint M S _ h] at this

Premises used: IsLocalization.under_map_of_isPrime_disjoint
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
p : Ideal R
inst_4 : p.IsPrime
h : Disjoint (↑M : Set R) (↑p : Set R)
P : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) p
this_1 : P.IsPrime
this : IsLocalization.AtPrime.{u_1, u_2} (Localization.AtPrime (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) p
⊢ ringKrullDim.{u_2} (Localization.AtPrime P) = ringKrullDim.{u_1} (Localization.AtPrime p)

Tactic:
have := ringKrullDim_eq_of_ringEquiv (IsLocalization.algEquiv p.primeCompl
    (Localization.AtPrime P) (Localization.AtPrime p)).toRingEquiv
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
p : Ideal R
inst_4 : p.IsPrime
h : Disjoint (↑M : Set R) (↑p : Set R)
P : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) p
this_1 : P.IsPrime
this_2 :
  IsLocalization.AtPrime.{u_1, u_2} (Localization.AtPrime (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) p
this : ringKrullDim.{u_2} (Localization.AtPrime P) = ringKrullDim.{u_1} (Localization.AtPrime p)
⊢ (↑P.height : WithBot ℕ∞) = (↑p.height : WithBot ℕ∞)

Tactic:
rw [AtPrime.ringKrullDim_eq_height P, AtPrime.ringKrullDim_eq_height p] at this

Premises used: IsLocalization.AtPrime.ringKrullDim_eq_height
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
p : Ideal R
inst_4 : p.IsPrime
h : Disjoint (↑M : Set R) (↑p : Set R)
P : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) p
this_1 : P.IsPrime
this_2 :
  IsLocalization.AtPrime.{u_1, u_2} (Localization.AtPrime (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) p
this : (↑P.height : WithBot ℕ∞) = (↑p.height : WithBot ℕ∞)
⊢ height.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) p) = p.height

Tactic:
WithBot.coe_eq_coe.mp this

Premises used: Iff.mp, WithBot.coe_eq_coe
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
p : Ideal R
inst_4 : p.IsPrime
h : Disjoint (↑M : Set R) (↑p : Set R)
P : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) p
this_1 : P.IsPrime
this_2 :
  IsLocalization.AtPrime.{u_1, u_2} (Localization.AtPrime (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) p
this : (↑P.height : WithBot ℕ∞) = (↑p.height : WithBot ℕ∞)
⊢ height.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) p) = p.height

Tactic:
exact WithBot.coe_eq_coe.mp this

Premises used: Iff.mp, WithBot.coe_eq_coe
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : J.IsPrime
e : I ≤ J
e' : J.primeHeight = I.height
inst_2 : J.FiniteHeight
⊢ J.height = I.height

Tactic:
rw [← J.height_eq_primeHeight] at e'

Premises used: _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : J.IsPrime
e : I ≤ J
e' : J.primeHeight = I.height
inst_2 : J.FiniteHeight
e'₁ : J.height = I.height
⊢ J.FiniteHeight

Tactic:
rw [← J.height_eq_primeHeight] at e'

Premises used: _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : J.IsPrime
e : I ≤ J
e' : J.height = I.height
inst_2 : J.FiniteHeight
⊢ J ∈ I.minimalPrimes

Tactic:
mem_minimalPrimes_of_height_eq e (e' ▸ le_refl _)

Premises used: le_refl, Ideal.mem_minimalPrimes_of_height_eq, Eq.rec
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : J.IsPrime
e : I ≤ J
e' : J.height = I.height
inst_2 : J.FiniteHeight
⊢ J ∈ I.minimalPrimes

Tactic:
exact mem_minimalPrimes_of_height_eq e (e' ▸ le_refl _)

Premises used: le_refl, Ideal.mem_minimalPrimes_of_height_eq, Eq.rec
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hr : (↑0 : ℕ∞) ≤ I.height
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ (↑0 : Cardinal.{u_1}) ∧ (↑0 : ℕ∞) ≤ J.height

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
succ :
  ∀ (J : Ideal R) (h₁ : J ≤ I) (h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})) (h₃ : (↑r : ℕ∞) ≤ J.height),
    ∃ J ≤ I, Submodule.spanRank J ≤ (↑(r + 1) : Cardinal.{u_1}) ∧ (↑(r + 1) : ℕ∞) ≤ J.height
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ (↑(r + 1) : Cardinal.{u_1}) ∧ (↑(r + 1) : ℕ∞) ≤ J.height

Tactic:
obtain ⟨J, h₁, h₂, h₃⟩ := ih ((WithTop.coe_le_coe.mpr r.le_succ).trans hr)

Premises used: Iff.mpr, Nat.le_succ, LE.le.trans, WithTop.coe_le_coe
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
⊢ S.Finite

Tactic:
have hS : Set.Finite S := Set.Finite.subset J.finite_minimalPrimes_of_isNoetherianRing
      (fun _ h => h.1)
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
⊢ ¬(↑I : Set R) ⊆ ⋃ K ∈ hS.toFinset (s := S), (↑K : Set R)

Tactic:
(Ideal.subset_union_prime ⊥ ⊥ ?_).not.mpr ?_

Premises used: Iff.mpr, Iff.not, Bot.bot, Ideal.subset_union_prime
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
refine_1 : ∀ i ∈ hS.toFinset (s := S), i ≠ ⊥ → i ≠ ⊥ → i.IsPrime
refine_2 : ¬∃ i ∈ hS.toFinset (s := S), I ≤ i
⊢ ¬(↑I : Set R) ⊆ ⋃ K ∈ hS.toFinset (s := S), (↑K : Set R)

Tactic:
refine (Ideal.subset_union_prime ⊥ ⊥ ?_).not.mpr ?_

Premises used: Iff.mpr, Iff.not, Bot.bot, Ideal.subset_union_prime
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
K : Ideal R
hK : K ∈ hS.toFinset (s := S)
⊢ K ∈ S

Tactic:
rw [Set.Finite.mem_toFinset] at hK

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
K : Ideal R
hK : K ∈ S
⊢ K.IsPrime

Tactic:
hK.1.isPrime

Premises used: Ideal.IsMinimalPrime.isPrime, And.left
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
K : Ideal R
hK : K ∈ S
⊢ K.IsPrime

Tactic:
exact hK.1.isPrime

Premises used: Ideal.IsMinimalPrime.isPrime, And.left
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
refine_2 : ∀ (i : Ideal R) (_ : i ∈ hS.toFinset (s := S)), ¬I ≤ i
⊢ ¬∃ i ∈ hS.toFinset (s := S), I ≤ i

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
K : Ideal R
hK : K ∈ hS.toFinset (s := S)
e : I ≤ K
⊢ (↑(r + 1) : ℕ∞) ≤ K.height

Tactic:
have := hr.trans (Ideal.height_mono e)
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
K : Ideal R
hK : K ∈ hS.toFinset (s := S)
e : I ≤ K
this : (↑(r + 1) : ℕ∞) ≤ K.height
⊢ K ∈ S

Tactic:
rw [Set.Finite.mem_toFinset] at hK

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
K : Ideal R
hK : K ∈ hS.toFinset (s := S)
e : I ≤ K
this : (↑(r + 1) : ℕ∞) ≤ K.height
hK₁ : K ∈ S
⊢ I ≤ K

Tactic:
rw [Set.Finite.mem_toFinset] at hK

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
K : Ideal R
hK : K ∈ hS.toFinset (s := S)
e : I ≤ K
this : (↑(r + 1) : ℕ∞) ≤ K.height
hK₁ : K ∈ S
e₁ : I ≤ K
⊢ (↑(r + 1) : ℕ∞) ≤ K.height

Tactic:
rw [Set.Finite.mem_toFinset] at hK

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
K : Ideal R
hK : K ∈ S
e : I ≤ K
this : (↑(r + 1) : ℕ∞) ≤ K.height
⊢ ¬LT.lt (α := ℕ∞) (↑r : ℕ∞) (↑(r + 1) : ℕ∞)

Tactic:
rw [hK.2, ← not_lt] at this

Premises used: not_lt, And.right
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
K : Ideal R
hK : K ∈ S
e : I ≤ K
this : ¬LT.lt (α := ℕ∞) (↑r : ℕ∞) (↑(r + 1) : ℕ∞)
⊢ ¬r < r + 1

Tactic:
norm_cast at this
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
K : Ideal R
hK : K ∈ S
e : I ≤ K
this : ¬r < r + 1
⊢ False

Tactic:
this r.lt_succ_self

Premises used: Nat.lt_succ_self
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
K : Ideal R
hK : K ∈ S
e : I ≤ K
this : ¬r < r + 1
⊢ False

Tactic:
exact this r.lt_succ_self

Premises used: Nat.lt_succ_self