awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
e : I ≤ J
inst_1 : J.IsPrime
inst_2 : J.FiniteHeight
e' : J.height ≤ I.height
p : Ideal R
h₁ : p ∈ I.minimalPrimes
h₂ : p ≤ J
⊢ J = p
have h : ∀ (h₃ : p < J), False
Tactic: refine (eq_of_le_of_not_lt h₂ fun h₃ ↦ ?_).symm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
e : I ≤ J
inst_1 : J.IsPrime
inst_2 : J.FiniteHeight
e' : J.height ≤ I.height
p : Ideal R
h₁ : p ∈ I.minimalPrimes
h₂ : p ≤ J
h₃ : p < J
⊢ False
have this : p.IsPrime
Tactic: have := h₁.isPrime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
e : I ≤ J
inst_1 : J.IsPrime
inst_2 : J.FiniteHeight
e' : J.height ≤ I.height
p : Ideal R
h₁ : p ∈ I.minimalPrimes
h₂ : p ≤ J
h₃ : p < J
this : p.IsPrime
⊢ False
have this₁ : p.FiniteHeight
Tactic: have := finiteHeight_of_le h₂ IsPrime.ne_top'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
⊢ I.height = 0 ↔ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I
have rw : IsMin { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R } ↔
  Membership.mem (γ := Set (Ideal R)) {x : Ideal R | Minimal IsPrime x} I
Tactic: rw [Ideal.height_eq_primeHeight, Ideal.primeHeight, Order.height_eq_zero,
    minimalPrimes_eq_minimals]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
⊢ IsMin { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R } ↔
    Membership.mem (γ := Set (Ideal R)) {x : Ideal R | Minimal IsPrime x} I
have refine : ∀ (h : IsMin { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R }) ⦃y : Ideal R⦄, y.IsPrime → y ≤ I → I ≤ y
Tactic: refine ⟨fun h ↦ ⟨‹_›, ?_⟩, fun ⟨hI, hI'⟩ b hb ↦ hI' b.isPrime hb⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
h : IsMin { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R }
⊢ ∀ ⦃y : Ideal R⦄, y.IsPrime → y ≤ I → I ≤ y
have by_contra! : ∀ (P : Ideal R) (hP₁ : P.IsPrime) (hP₂ : P ≤ I) (hP₃ : ¬I ≤ P), False
Tactic: by_contra! ⟨P, ⟨hP₁, ⟨hP₂, hP₃⟩⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
⊢ I.primeHeight = 0 ↔ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I
have rw : I.height = 0 ↔ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I
Tactic: rw [← Ideal.height_eq_primeHeight, Ideal.height_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
rw : I.height = 0 ↔ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I
⊢ I.primeHeight = 0 ↔ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I
have rw₁ : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I ↔ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I
Tactic: rw [← Ideal.height_eq_primeHeight, Ideal.height_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
⊢ 1 ≤ height (R := R) (span {x})
have rw : LE.le (α := ℕ∞) 1
  (⨅ (J : Ideal R), ⨅ (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) J), J.height)
Tactic: rw [Ideal.height_eq_inf_minimalPrimes]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
⊢ LE.le (α := ℕ∞) 1
    (⨅ (J : Ideal R), ⨅ (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) J), J.height)
have refine : ∀ (q : Ideal R) (hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) q), 1 ≤ q.height
Tactic: refine le_iInf₂ fun q hq => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
q : Ideal R
hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) q
⊢ 1 ≤ q.height
have this : q.IsPrime
Tactic: have : q.IsPrime := hq.isPrime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
q : Ideal R
hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) q
this : q.IsPrime
⊢ 1 ≤ q.height
have rw : q ∉ minimalPrimes R
Tactic: rw [ENat.one_le_iff_ne_zero, Ne, height_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ height.{u_1} (R := R) ⊥ = 0
have obtain : ∀ (p : Ideal R) (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p), height.{u_1} (R := R) ⊥ = 0
Tactic: obtain ⟨p, hp⟩ := Ideal.nonempty_minimalPrimes (R := R) (I := ⊥) top_ne_bot.symm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p
⊢ height.{u_1} (R := R) ⊥ = 0
have rw : Eq (α := ℕ∞) (⨅ (J : Ideal R), ⨅ (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) J), J.height) 0
Tactic: rw [Ideal.height_eq_inf_minimalPrimes]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p
⊢ Eq (α := ℕ∞) (⨅ (J : Ideal R), ⨅ (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) J), J.height) 0
have simp : ∃ (i : Ideal R) (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) i), i.height = 0
Tactic: simp only [ENat.iInf_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : Subsingleton R
⊢ I.height = ⊤
have rw : height.{u_1} (R := R) ⊤ = ⊤
Tactic: rw [Subsingleton.elim I ⊤, Ideal.height_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : Subsingleton R
rw : height.{u_1} (R := R) ⊤ = ⊤
⊢ I.height = ⊤
have rw₁ : Eq (α := ℕ∞) ⊤ ⊤
Tactic: rw [Subsingleton.elim I ⊤, Ideal.height_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
inst_2 : FiniteRingKrullDim R
e : (↑I.height : WithBot ℕ∞) = ringKrullDim R
⊢ I.IsMaximal
have h : I ≠ ⊤
Tactic: have h : I ≠ ⊤ := Ideal.IsPrime.ne_top'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
inst_2 : FiniteRingKrullDim R
e : (↑I.height : WithBot ℕ∞) = ringKrullDim R
h : I ≠ ⊤
⊢ I.IsMaximal
have obtain : ∀ (M : Ideal R) (hM : M.IsMaximal) (hM' : I ≤ M), I.IsMaximal
Tactic: obtain ⟨M, hM, hM'⟩ := Ideal.exists_le_maximal I h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
inst_2 : FiniteRingKrullDim R
e : (↑I.height : WithBot ℕ∞) = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
⊢ I.IsMaximal
have inl : ∀ (hM' : I < M), I.IsMaximal
Tactic: rcases lt_or_eq_of_le hM' with (hM' | hM')
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
inst_2 : FiniteRingKrullDim R
e : (↑I.height : WithBot ℕ∞) = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
inl : ∀ (hM' : I < M), I.IsMaximal
⊢ I.IsMaximal
have inr : ∀ (hM' : I = M), I.IsMaximal
Tactic: rcases lt_or_eq_of_le hM' with (hM' | hM')
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
inst_2 : FiniteRingKrullDim R
e : (↑I.height : WithBot ℕ∞) = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'_1 : I ≤ M
hM' : I < M
⊢ I.IsMaximal
have h1 : I.height < M.height
Tactic: have h1 := Ideal.height_strict_mono_of_isPrime hM'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
inst_2 : FiniteRingKrullDim R
e : (↑I.height : WithBot ℕ∞) = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'_1 : I ≤ M
hM' : I < M
h1 : I.height < M.height
⊢ I.IsMaximal
have h2 : (↑M.height : WithBot ℕ∞) ≤ (↑I.height : WithBot ℕ∞)
Tactic: have h2 := e ▸ M.height_le_ringKrullDim_of_ne_top hM.ne_top
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
⊢ (↑(height (maximalIdeal R)) : WithBot ℕ∞) = ringKrullDim R
have rw : (↑(Order.height (α := PrimeSpectrum R) { asIdeal := maximalIdeal R, isPrime := sorry : PrimeSpectrum R }) : WithBot ℕ∞) =
  ringKrullDim R
Tactic: rw [Ideal.height_eq_primeHeight, Ideal.primeHeight]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : FiniteRingKrullDim R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : I.IsPrime
⊢ (↑I.height : WithBot ℕ∞) = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R
have mp : (↑I.height : WithBot ℕ∞) = ringKrullDim R → I = IsLocalRing.maximalIdeal R
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : FiniteRingKrullDim R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : I.IsPrime
mp : (↑I.height : WithBot ℕ∞) = ringKrullDim R → I = IsLocalRing.maximalIdeal R
⊢ (↑I.height : WithBot ℕ∞) = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R
have mpr : I = IsLocalRing.maximalIdeal R → (↑I.height : WithBot ℕ∞) = ringKrullDim R
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : FiniteRingKrullDim R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : I.IsPrime
⊢ (↑I.primeHeight : WithBot ℕ∞) = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R
have rw : (↑I.height : WithBot ℕ∞) = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R
Tactic: rw [← Ideal.height_eq_primeHeight, Ideal.height_eq_ringKrullDim_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : FiniteRingKrullDim R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : I.IsPrime
rw : (↑I.height : WithBot ℕ∞) = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R
⊢ (↑I.primeHeight : WithBot ℕ∞) = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R
have rw₁ : I = IsLocalRing.maximalIdeal R ↔ I = IsLocalRing.maximalIdeal R
Tactic: rw [← Ideal.height_eq_primeHeight, Ideal.height_eq_ringKrullDim_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
⊢ p.height ≤ (↑n : ℕ∞) ↔ ∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)
have rw : (∀ (a : Ideal R) (b : a.IsPrime),
    (Equiv.symm
              (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
            (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
          (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a b) <
        { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } →
      Order.height (α := PrimeSpectrum R)
          ((Equiv.symm
                  (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
              (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a b) :
            PrimeSpectrum R) <
        (↑n : ℕ∞)) ↔
  ∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)
Tactic: rw [height_eq_primeHeight, primeHeight, Order.height_le_coe_iff,
    (PrimeSpectrum.equivSubtype R).forall_congr_left, Subtype.forall]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      (Equiv.symm
                (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                  fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
              (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
            (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a b) <
          { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } →
        Order.height (α := PrimeSpectrum R)
            ((Equiv.symm
                    (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                  (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
                (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a b) :
              PrimeSpectrum R) <
          (↑n : ℕ∞)) ↔
    ∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)
have a : ∀ (a : Ideal R) (a_1 : a.IsPrime),
  (Equiv.symm
              (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
            (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
          (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a a_1) <
        { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } →
      Order.height (α := PrimeSpectrum R)
          ((Equiv.symm
                  (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
              (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a a_1) :
            PrimeSpectrum R) <
        (↑n : ℕ∞) ↔
    a < p → a.height < (↑n : ℕ∞)
Tactic: congr!
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
a : Ideal R
h : a.IsPrime
⊢ (Equiv.symm
              (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
            (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
          (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a h) <
        { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } →
      Order.height (α := PrimeSpectrum R)
          ((Equiv.symm
                  (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
              (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a h) :
            PrimeSpectrum R) <
        (↑n : ℕ∞) ↔
    a < p → a.height < (↑n : ℕ∞)
have a : (Equiv.symm
            (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
          (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
        (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a h) <
      { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } →
    Order.height (α := PrimeSpectrum R)
        ((Equiv.symm
                (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                  fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
              (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
            (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a h) :
          PrimeSpectrum R) <
      (↑n : ℕ∞) ↔
  a < p → Order.height { asIdeal := a, isPrime := h : PrimeSpectrum R } < (↑n : ℕ∞)
Tactic: rw [height_eq_primeHeight, primeHeight]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
inst_2 : IsNoetherianRing R
⊢ p.height ≤ (↑n : ℕ∞) ↔
    ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)
have rw : (∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)) ↔
  ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)
Tactic: rw [Ideal.height_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
inst_2 : IsNoetherianRing R
⊢ (∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)) ↔
    ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)
have mp : (∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)) →
  ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
inst_2 : IsNoetherianRing R
mp :
  (∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)) →
    ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)
⊢ (∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)) ↔
    ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)
have mpr : (∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)) →
  ∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
inst_2 : IsNoetherianRing R
H : ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)
q : Ideal R
hq : q.IsPrime
e : q < p
⊢ q.height < (↑n : ℕ∞)
have mpr : ∀ (x : Ideal R) (hx : x.IsPrime)
  (hqx : Subtype.mk (p := fun (I : Ideal R) ↦ I.IsPrime) q hq ≤ Subtype.mk (p := fun (I : Ideal R) ↦ I.IsPrime) x hx)
  (hxp :
    Subtype.mk (p := fun (I : Ideal R) ↦ I.IsPrime) x hx ⋖ Subtype.mk (p := fun (I : Ideal R) ↦ I.IsPrime) p inst_1),
  q.height < (↑n : ℕ∞)
Tactic: obtain ⟨⟨x, hx⟩, hqx, hxp⟩ :=
      @exists_le_covBy_of_lt { I : Ideal R // I.IsPrime } ⟨q, hq⟩ ⟨p, ‹_›⟩ _ _ e
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
p : Ideal S
inst_2 : p.IsPrime
⊢ height (comap e p) = p.height
have rw : Order.height (α := PrimeSpectrum R) { asIdeal := comap e p, isPrime := sorry : PrimeSpectrum R } =
  Order.height.{u_1} (α := PrimeSpectrum R)
    ((PrimeSpectrum.comapEquiv e.symm : (a : PrimeSpectrum S) → PrimeSpectrum R) { asIdeal := p, isPrime := inst_2 } :
      PrimeSpectrum R)
Tactic: rw [height_eq_primeHeight, height_eq_primeHeight, primeHeight, primeHeight,
    ← Order.height_orderIso (PrimeSpectrum.comapEquiv e.symm) ⟨p, ‹_›⟩]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
p : Ideal S
inst_2 : p.IsPrime
⊢ Order.height (α := PrimeSpectrum R) { asIdeal := comap e p, isPrime := ⋯ : PrimeSpectrum R } =
    Order.height.{u_1} (α := PrimeSpectrum R)
      ((PrimeSpectrum.comapEquiv e.symm : (a : PrimeSpectrum S) → PrimeSpectrum R) { asIdeal := p, isPrime := inst_2 } :
        PrimeSpectrum R)
have this : Eq (α := Ideal R) (map (F := S →+* R) (↑e.symm : S →+* R) p) (comap e.symm.symm p)
Tactic: have := p.map_comap_of_equiv e.symm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
I : Ideal S
⊢ height (comap e I) = I.height
have refine_1 : (J : Ideal S) →
  J ∈ I.minimalPrimes ≃
    Membership.mem (α := Ideal R) (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap e I))
      (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J : Ideal R)
Tactic: refine (Equiv.iInf_congr e.idealComapOrderIso fun J ↦ (Equiv.iInf_congr ?_ fun h ↦ ?_).symm).symm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
I : Ideal S
refine_1 :
  (J : Ideal S) →
    J ∈ I.minimalPrimes ≃
      Membership.mem (α := Ideal R) (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap e I))
        (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J : Ideal R)
⊢ height (comap e I) = I.height
have refine_2 : ∀ (J : Ideal S) (h : J ∈ I.minimalPrimes),
  primeHeight.{u_1} (R := R) (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J) = J.primeHeight
Tactic: refine (Equiv.iInf_congr e.idealComapOrderIso fun J ↦ (Equiv.iInf_congr ?_ fun h ↦ ?_).symm).symm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
I J : Ideal S
⊢ J ∈ I.minimalPrimes ≃
    Membership.mem (α := Ideal R) (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap e I))
      (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J : Ideal R)
have refine_1 : J ∈ I.minimalPrimes ↔
  Membership.mem (α := Ideal R) (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap e I))
    (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J : Ideal R)
Tactic: refine .ofIff ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
I J : Ideal S
⊢ J ∈ I.minimalPrimes ↔
    Membership.mem (α := Ideal R) (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap e I))
      (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J : Ideal R)
have refine_1 : J ∈ I.minimalPrimes ↔
  Membership.mem (α := Ideal R) (γ := Set (Ideal R)) (comap (F := R →+* S) (↑e : R →+* S) '' I.minimalPrimes)
    (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J : Ideal R)
Tactic: rw [← Ideal.comap_coe,
      Ideal.comap_minimalPrimes_eq_of_surjective (f := (↑e : R →+* S)) e.surjective]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
I J : Ideal S
h : J ∈ I.minimalPrimes
⊢ primeHeight.{u_1} (R := R) (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J) = J.primeHeight
have this : J.IsPrime
Tactic: have : J.IsPrime := h.isPrime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
I : Ideal R
⊢ height.{u_2} (R := S) (map e I) = I.height
have rw : height (comap e.symm I) = I.height
Tactic: rw [← Ideal.comap_symm e, height_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
I : Ideal R
rw : height (comap e.symm I) = I.height
⊢ height.{u_2} (R := S) (map e I) = I.height
have rw₁ : I.height = I.height
Tactic: rw [← Ideal.comap_symm e, height_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
⊢ ringKrullDim R ≤ n ↔ ∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n
have rw : (∀ (i : PrimeSpectrum R), (↑(Order.height i) : WithBot ℕ∞) ≤ n) ↔
  ∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n
Tactic: rw [ringKrullDim, Order.krullDim_eq_iSup_height, iSup_le_iff]