awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
h : ¬IsField R
h' : ringKrullDim R < 1
h'' : ringKrullDim R ≤ 0
⊢ Ring.KrullDimLE 0 R

Tactic:
rw [← Nat.cast_zero, ← Ring.krullDimLE_iff] at h''

Premises used: Ring.krullDimLE_iff, Nat.cast_zero
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
h : ¬IsField R
h' : ringKrullDim R < 1
h'' : Ring.KrullDimLE 0 R
⊢ IsField R

Tactic:
Ring.KrullDimLE.isField_of_isDomain

Premises used: Ring.KrullDimLE.isField_of_isDomain
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
h : ¬IsField R
h' : ringKrullDim R < 1
h'' : Ring.KrullDimLE 0 R
⊢ IsField R

Tactic:
exact Ring.KrullDimLE.isField_of_isDomain

Premises used: Ring.KrullDimLE.isField_of_isDomain
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
m : Ideal R
inst_3 : m.IsMaximal
h : ¬IsField R
⊢ m.height = 1

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
m : Ideal R
inst_3 : m.IsMaximal
h : ¬IsField R
refine_1 : m.height ≤ 1
refine_2 : 1 ≤ m.height
⊢ m.height = 1

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
m : Ideal R
inst_3 : m.IsMaximal
h_1 : ¬IsField R
h : (↑m.height : WithBot ℕ∞) ≤ 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ∀ (h : m.height ≤ 1), m.height ≤ 1
⊢ m.height ≤ 1

Tactic:
norm_cast at h
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
m : Ideal R
inst_3 : m.IsMaximal
h : ¬IsField R
refine_1 : (↑m.height : WithBot ℕ∞) ≤ 1
⊢ m.height ≤ 1

Tactic:
suffices h : (m.height : WithBot ℕ∞) ≤ 1 by norm_cast at h
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
m : Ideal R
inst_3 : m.IsMaximal
h : ¬IsField R
refine_1 : (↑m.height : WithBot ℕ∞) ≤ ringKrullDim R
⊢ (↑m.height : WithBot ℕ∞) ≤ 1

Tactic:
rw [← IsPrincipalIdealRing.ringKrullDim_eq_one _ h]

Premises used: IsPrincipalIdealRing.ringKrullDim_eq_one
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
m : Ideal R
inst_3 : m.IsMaximal
h : ¬IsField R
⊢ (↑m.height : WithBot ℕ∞) ≤ ringKrullDim R

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.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
m : Ideal R
inst_3 : m.IsMaximal
h : ¬IsField R
⊢ (↑m.height : WithBot ℕ∞) ≤ ringKrullDim R

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.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
m : Ideal R
inst_3 : m.IsMaximal
h : ¬IsField R
apply : 1 = Ideal.height.{u_1} (R := R) ⊥ + 1
⊢ 1 ≤ m.height

Tactic:
apply le_of_eq_of_le _ (Ideal.height_add_one_le_of_lt_of_isPrime (Ideal.bot_lt_of_maximal m h))

Premises used: Ideal.bot_lt_of_maximal, le_of_eq_of_le, Ideal.height_add_one_le_of_lt_of_isPrime
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
m : Ideal R
inst_3 : m.IsMaximal
h : ¬IsField R
⊢ 1 = Ideal.height.{u_1} (R := R) ⊥ + 1

Tactic:
simp
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
apply : Monotone.{u_1, u_1} (α := PrimeSpectrum R[X]) (PrimeSpectrum.comap C)
apply₁ : ∀ (p : PrimeSpectrum R), Order.krullDim.{u_1} (↑(PrimeSpectrum.comap C ⁻¹' {p}) : Type u_1) ≤ (↑1 : WithBot ℕ∞)
⊢ Order.krullDim.{u_1} (PrimeSpectrum R[X]) ≤ 2 * Order.krullDim.{u_1} (PrimeSpectrum R) + 1

Tactic:
apply Order.krullDim_le_of_krullDim_preimage_le' (PrimeSpectrum.comap C) ?_ (fun p ↦ ?_)

Premises used: Polynomial.C, PrimeSpectrum.comap, Order.krullDim_le_of_krullDim_preimage_le'
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
⊢ Monotone.{u_1, u_1} (α := PrimeSpectrum R[X]) (PrimeSpectrum.comap C)

Tactic:
fun {a b} h ↦ Ideal.comap_mono h

Premises used: Set.Mem, Monotone, Ideal.comap_mono
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
⊢ Monotone.{u_1, u_1} (α := PrimeSpectrum R[X]) (PrimeSpectrum.comap C)

Tactic:
exact fun {a b} h ↦ Ideal.comap_mono h

Premises used: Ideal.comap_mono
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
p : PrimeSpectrum R
rw : Ring.KrullDimLE.{u_1} 1 p.asIdeal.ResidueField[X]
⊢ Order.krullDim.{u_1} (↑(PrimeSpectrum.comap C ⁻¹' {p}) : Type u_1) ≤ (↑1 : WithBot ℕ∞)

Tactic:
rw [show C = (algebraMap R (Polynomial R)) from rfl, Order.krullDim_eq_of_orderIso
      (PrimeSpectrum.preimageOrderIsoFiber R (Polynomial R) p), ← ringKrullDim,
      ← ringKrullDim_eq_of_ringEquiv (polyEquivTensor R (p.asIdeal.ResidueField)).toRingEquiv,
      ← Ring.krullDimLE_iff]

Premises used: Ring.krullDimLE_iff, ringKrullDim_eq_of_ringEquiv, polyEquivTensor, Ideal.ResidueField, Order.krullDim_eq_of_orderIso, Polynomial, AlgEquiv.toRingEquiv, ringKrullDim, PrimeSpectrum.preimageOrderIsoFiber, PrimeSpectrum.asIdeal, rfl
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
p : PrimeSpectrum R
⊢ Ring.KrullDimLE.{u_1} 1 p.asIdeal.ResidueField[X]

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsMaximal
P : Ideal R[X]
inst_3 : P.IsMaximal
inst_4 : P.LiesOver p
x : Field (R ⧸ p) := Quotient.field p
h :
  height (R := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.map (F :=
        R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
        (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P) =
    1
rw :
  p.height +
      height (R := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
        (Ideal.map (F :=
          R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
          (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P) =
    p.height + 1
rw₁ rw₂ : p.height + 1 = p.height + 1
⊢ P.height = p.height + 1

Tactic:
rw [height_eq_height_add_of_liesOver_of_hasGoingDown p, h]

Premises used: Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsMaximal
P : Ideal R[X]
inst_3 : P.IsMaximal
inst_4 : P.LiesOver p
x : Field (R ⧸ p) := Quotient.field p
suffices :
  height (R := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.map (F :=
        R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
        (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P) =
    1
⊢ P.height = p.height + 1

Tactic:
suffices h : (P.map (Ideal.Quotient.mk (Ideal.map (algebraMap R R[X]) p))).height = 1 by
    rw [height_eq_height_add_of_liesOver_of_hasGoingDown p, h]
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsMaximal
P : Ideal R[X]
inst_3 : P.IsMaximal
inst_4 : P.LiesOver p
x : Field (R ⧸ p) := Quotient.field p
e : HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p) ≃+* (R ⧸ p)[X] :=
  p.polynomialQuotientEquivQuotientPolynomial.symm
P' : Ideal (R ⧸ p)[X] :=
  Ideal.map (R := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) e
    (Ideal.map (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P)
⊢ IsMaximal (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
    (Ideal.map (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P)

Tactic:
.map_of_surjective_of_ker_le Quotient.mk_surjective ?_

Premises used: Ideal.IsMaximal.map_of_surjective_of_ker_le
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsMaximal
P : Ideal R[X]
inst_3 : P.IsMaximal
inst_4 : P.LiesOver p
x : Field (R ⧸ p) := Quotient.field p
e : HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p) ≃+* (R ⧸ p)[X] :=
  p.polynomialQuotientEquivQuotientPolynomial.symm
P' : Ideal (R ⧸ p)[X] :=
  Ideal.map (R := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) e
    (Ideal.map (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P)
refine :
  RingHom.ker (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) ≤
    P
⊢ IsMaximal (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
    (Ideal.map (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P)

Tactic:
refine .map_of_surjective_of_ker_le Quotient.mk_surjective ?_
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsMaximal
P : Ideal R[X]
inst_3 : P.IsMaximal
inst_4 : P.LiesOver p
x : Field (R ⧸ p) := Quotient.field p
e : HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p) ≃+* (R ⧸ p)[X] :=
  p.polynomialQuotientEquivQuotientPolynomial.symm
P' : Ideal (R ⧸ p)[X] :=
  Ideal.map (R := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) e
    (Ideal.map (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P)
rw : Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) (under R P) ≤ P
⊢ RingHom.ker (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) ≤
    P

Tactic:
rw [mk_ker, LiesOver.over (P := P) (p := p)]

Premises used: Ideal.LiesOver.over, Ideal.mk_ker
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsMaximal
P : Ideal R[X]
inst_3 : P.IsMaximal
inst_4 : P.LiesOver p
x : Field (R ⧸ p) := Quotient.field p
e : HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p) ≃+* (R ⧸ p)[X] :=
  p.polynomialQuotientEquivQuotientPolynomial.symm
P' : Ideal (R ⧸ p)[X] :=
  Ideal.map (R := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) e
    (Ideal.map (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P)
⊢ Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) (under R P) ≤ P

Tactic:
map_comap_le

Premises used: Set.Mem, setOf, Ideal.map_comap_le
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsMaximal
P : Ideal R[X]
inst_3 : P.IsMaximal
inst_4 : P.LiesOver p
x : Field (R ⧸ p) := Quotient.field p
e : HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p) ≃+* (R ⧸ p)[X] :=
  p.polynomialQuotientEquivQuotientPolynomial.symm
P' : Ideal (R ⧸ p)[X] :=
  Ideal.map (R := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) e
    (Ideal.map (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P)
⊢ Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) (under R P) ≤ P

Tactic:
exact map_comap_le

Premises used: Ideal.map_comap_le
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsMaximal
P : Ideal R[X]
inst_3 : P.IsMaximal
inst_4 : P.LiesOver p
x : Field (R ⧸ p) := Quotient.field p
e : HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p) ≃+* (R ⧸ p)[X] :=
  p.polynomialQuotientEquivQuotientPolynomial.symm
P' : Ideal (R ⧸ p)[X] :=
  Ideal.map (R := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) e
    (Ideal.map (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P)
⊢ IsMaximal (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
    (Ideal.map (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P)

Tactic:
have : (P.map (Ideal.Quotient.mk <| p.map (algebraMap R R[X]))).IsMaximal := by
    refine .map_of_surjective_of_ker_le Quotient.mk_surjective ?_
    rw [mk_ker, LiesOver.over (P := P) (p := p)]
    exact map_comap_le
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsMaximal
P : Ideal R[X]
inst_3 : P.IsMaximal
inst_4 : P.LiesOver p
x : Field (R ⧸ p) := Quotient.field p
e : HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p) ≃+* (R ⧸ p)[X] :=
  p.polynomialQuotientEquivQuotientPolynomial.symm
P' : Ideal (R ⧸ p)[X] :=
  Ideal.map (R := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) e
    (Ideal.map (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P)
this :
  IsMaximal (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
    (Ideal.map (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P)
⊢ P'.IsMaximal

Tactic:
have : P'.IsMaximal := map_isMaximal_of_equiv e
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsMaximal
P : Ideal R[X]
inst_3 : P.IsMaximal
inst_4 : P.LiesOver p
x : Field (R ⧸ p) := Quotient.field p
e : HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p) ≃+* (R ⧸ p)[X] :=
  p.polynomialQuotientEquivQuotientPolynomial.symm
P' : Ideal (R ⧸ p)[X] :=
  Ideal.map (R := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) e
    (Ideal.map (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P)
this_1 :
  IsMaximal (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
    (Ideal.map (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P)
this : P'.IsMaximal
⊢ P'.height = 1

Tactic:
have : P'.height = 1 := IsPrincipalIdealRing.height_eq_one_of_isMaximal P' polynomial_not_isField
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsMaximal
P : Ideal R[X]
inst_3 : P.IsMaximal
inst_4 : P.LiesOver p
x : Field (R ⧸ p) := Quotient.field p
e : HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p) ≃+* (R ⧸ p)[X] :=
  p.polynomialQuotientEquivQuotientPolynomial.symm
P' : Ideal (R ⧸ p)[X] :=
  Ideal.map (R := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) e
    (Ideal.map (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P)
this_1 :
  IsMaximal (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
    (Ideal.map (F :=
      R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P)
this_2 : P'.IsMaximal
this : P'.height = 1
rwa rwa₁ rwa₂ rwa₃ :
  height (R := (R ⧸ p)[X])
      (Ideal.map (R := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
        e
        (Ideal.map (F :=
          R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
          (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P)) =
    1
⊢ height (R := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
      (Ideal.map (F :=
        R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p))
        (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) p)) P) =
    1

Tactic:
rwa [← e.height_map <| P.map (Ideal.Quotient.mk <| p.map (algebraMap R R[X]))]

Premises used: Algebra.algebraMap, Ideal.Quotient.mk, Ideal.map, Polynomial, RingEquiv.height_map
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsMaximal
⊢ LiesOver (B := R[X]) (Ideal.map (F := R →+* R[X]) C p) p

Tactic:
have : (p.map C).LiesOver p := ⟨IsMaximal.eq_of_le inferInstance IsPrime.ne_top' le_comap_map⟩
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsMaximal
this : LiesOver (B := R[X]) (Ideal.map (F := R →+* R[X]) C p) p
⊢ height (R := R[X]) (Ideal.map (F := R →+* R[X]) C p) = p.height

Tactic:
simp [height_eq_height_add_of_liesOver_of_hasGoingDown p]

Premises used: Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
rw : IsPrime (under R P)
⊢ p.IsPrime

Tactic:
rw [P.over_def p]

Premises used: Ideal.over_def
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
⊢ IsPrime (under R P)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
⊢ p.IsPrime

Tactic:
have : p.IsPrime := by rw [P.over_def p]; infer_instance
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
this : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
⊢ let p' : Ideal Rₚ := Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p;
  p' = Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p

Tactic:
set p' : Ideal Rₚ := p.map (algebraMap R Rₚ) with p'_def

Premises used: Algebra.algebraMap, Ideal.map, Ideal
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
this : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
rw : IsMaximal.{u_1} (α := Rₚ) (IsLocalRing.maximalIdeal (Localization (M := R) p.primeCompl))
⊢ p'.IsMaximal

Tactic:
rw [p'_def, Localization.AtPrime.map_eq_maximalIdeal]

Premises used: Localization.AtPrime.map_eq_maximalIdeal
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
this : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
⊢ IsMaximal.{u_1} (α := Rₚ) (IsLocalRing.maximalIdeal (Localization (M := R) p.primeCompl))

Tactic:
IsLocalRing.maximalIdeal.isMaximal Rₚ

Premises used: IsLocalRing.maximalIdeal.isMaximal
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
this : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
⊢ IsMaximal.{u_1} (α := Rₚ) (IsLocalRing.maximalIdeal (Localization (M := R) p.primeCompl))

Tactic:
exact IsLocalRing.maximalIdeal.isMaximal Rₚ

Premises used: IsLocalRing.maximalIdeal.isMaximal
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
this : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
⊢ p'.IsMaximal

Tactic:
have : p'.IsMaximal := by
    rw [p'_def, Localization.AtPrime.map_eq_maximalIdeal]
    exact IsLocalRing.maximalIdeal.isMaximal Rₚ