awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
h : ¬IsField R
apply : ringKrullDim R ≤ 1
⊢ ringKrullDim R = 1
have apply₁ : ∀ (h' : ringKrullDim R < 1), IsField R
Tactic: apply eq_of_le_of_not_lt ?_ fun h' ↦ h ?_
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
h : ¬IsField R
⊢ ringKrullDim R ≤ 1
have rw : Ring.KrullDimLE 1 R
Tactic: rw [← Nat.cast_one, ← Ring.krullDimLE_iff]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
h : ¬IsField R
h' : ringKrullDim R < 1
⊢ IsField R
have h'' : ringKrullDim R ≤ 0
Tactic: have h'' : ringKrullDim R ≤ 0 := Order.le_of_lt_succ h'
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (hypothesis)
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
⊢ IsField R
have h''₁ : Ring.KrullDimLE 0 R
Tactic: rw [← Nat.cast_zero, ← Ring.krullDimLE_iff] at h''
Cleared hypotheses: h''
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (goal)
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
have refine_1 : m.height ≤ 1
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (goal)
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
⊢ m.height = 1
have refine_2 : 1 ≤ m.height
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (goal)
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
⊢ m.height ≤ 1
have norm_cast : ∀ (h : m.height ≤ 1), m.height ≤ 1
Tactic: norm_cast at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (goal)
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
have refine_1 : (↑m.height : WithBot ℕ∞) ≤ 1
Tactic: suffices h : (m.height : WithBot ℕ∞) ≤ 1 by norm_cast at h
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (goal)
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 ℕ∞) ≤ 1
have refine_1 : (↑m.height : WithBot ℕ∞) ≤ ringKrullDim R
Tactic: rw [← IsPrincipalIdealRing.ringKrullDim_eq_one _ h]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (goal)
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 ≤ m.height
have apply : 1 = Ideal.height.{u_1} (R := R) ⊥ + 1
Tactic: apply le_of_eq_of_le _ (Ideal.height_add_one_le_of_lt_of_isPrime (Ideal.bot_lt_of_maximal m h))
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ Order.krullDim.{u_1} (PrimeSpectrum R[X]) ≤ 2 * Order.krullDim.{u_1} (PrimeSpectrum R) + 1
have apply : Monotone.{u_1, u_1} (α := PrimeSpectrum R[X]) (PrimeSpectrum.comap C)
Tactic: apply Order.krullDim_le_of_krullDim_preimage_le' (PrimeSpectrum.comap C) ?_ (fun p ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
apply : Monotone.{u_1, u_1} (α := PrimeSpectrum R[X]) (PrimeSpectrum.comap C)
⊢ Order.krullDim.{u_1} (PrimeSpectrum R[X]) ≤ 2 * Order.krullDim.{u_1} (PrimeSpectrum R) + 1
have apply₁ : ∀ (p : PrimeSpectrum R), Order.krullDim.{u_1} (↑(PrimeSpectrum.comap C ⁻¹' {p}) : Type u_1) ≤ (↑1 : WithBot ℕ∞)
Tactic: apply Order.krullDim_le_of_krullDim_preimage_le' (PrimeSpectrum.comap C) ?_ (fun p ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
p : PrimeSpectrum R
⊢ Order.krullDim.{u_1} (↑(PrimeSpectrum.comap C ⁻¹' {p}) : Type u_1) ≤ (↑1 : WithBot ℕ∞)
have rw : Ring.KrullDimLE.{u_1} 1 p.asIdeal.ResidueField[X]
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]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
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
⊢ P.height = p.height + 1
have 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
Tactic: rw [height_eq_height_add_of_liesOver_of_hasGoingDown p, h]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
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
⊢ P.height = p.height + 1
have rw₁ : p.height + 1 = p.height + 1
Tactic: rw [height_eq_height_add_of_liesOver_of_hasGoingDown p, h]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
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
⊢ P.height = p.height + 1
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
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)
have 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
Tactic: refine .map_of_surjective_of_ker_le Quotient.mk_surjective ?_
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
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)
⊢ 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
have rw : Ideal.map (F := R →+* R[X]) (algebraMap R R[X]) (under R P) ≤ P
Tactic: rw [mk_ker, LiesOver.over (P := P) (p := p)]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (hypothesis)
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)
⊢ 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
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (hypothesis)
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)
⊢ 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
have this₁ : P'.IsMaximal
Tactic: have : P'.IsMaximal := map_isMaximal_of_equiv e
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (hypothesis)
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
⊢ 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
have this₁ : P'.height = 1
Tactic: have : P'.height = 1 := IsPrincipalIdealRing.height_eq_one_of_isMaximal P' polynomial_not_isField
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsMaximal
⊢ height (R := R[X]) (Ideal.map (F := R →+* R[X]) C p) = p.height
have this : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
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
have rw : IsPrime (under R P)
Tactic: rw [P.over_def p]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (hypothesis)
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.height = p.height + 1
have this : p.IsPrime
Tactic: have : p.IsPrime := by rw [P.over_def p]; infer_instance
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (hypothesis)
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.height = p.height + 1
have p'_def : 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
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
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
have rw : IsMaximal.{u_1} (α := Rₚ) (IsLocalRing.maximalIdeal (Localization (M := R) p.primeCompl))
Tactic: rw [p'_def, Localization.AtPrime.map_eq_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (hypothesis)
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.height = p.height + 1
have this₁ : p'.IsMaximal
Tactic: have : p'.IsMaximal := by
    rw [p'_def, Localization.AtPrime.map_eq_maximalIdeal]
    exact IsLocalRing.maximalIdeal.isMaximal Rₚ
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
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_1 : 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
this : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P
⊢ Disjoint (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X]) (↑P : Set R[X])
have refine : ∀ a ∈ (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X]),
  ∀ (ha : a ∈ (↑P : Set R[X])) (b : R) (hb : b ∈ (↑p.primeCompl : Set R) ∧ (C : (a : R) → R[X]) b = a), b ∈ (↑p : Set R)
Tactic: refine Set.disjoint_left.mpr fun a ⟨b, hb⟩ ha ↦ hb.1 ?_
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
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_1 : 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
this : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P
a : R[X]
h : a ∈ (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X])
ha : a ∈ (↑P : Set R[X])
b : R
hb : b ∈ (↑p.primeCompl : Set R) ∧ (C : (a : R) → R[X]) b = a
⊢ b ∈ (↑p : Set R)
have rwa : b ∈ p
Tactic: rwa [SetLike.mem_coe, LiesOver.over (P := P) (p := p), mem_comap, algebraMap_eq, hb.2]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
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_1 : 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
this : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P
a : R[X]
h : a ∈ (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X])
ha : a ∈ (↑P : Set R[X])
b : R
hb : b ∈ (↑p.primeCompl : Set R) ∧ (C : (a : R) → R[X]) b = a
rwa : b ∈ p
⊢ b ∈ (↑p : Set R)
have rwa₁ : Membership.mem (γ := Ideal R) (under R P) b
Tactic: rwa [SetLike.mem_coe, LiesOver.over (P := P) (p := p), mem_comap, algebraMap_eq, hb.2]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
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_1 : 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
this : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P
a : R[X]
h : a ∈ (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X])
ha : a ∈ (↑P : Set R[X])
b : R
hb : b ∈ (↑p.primeCompl : Set R) ∧ (C : (a : R) → R[X]) b = a
rwa : b ∈ p
rwa₁ : Membership.mem (γ := Ideal R) (under R P) b
⊢ b ∈ (↑p : Set R)
have rwa₂ : Membership.mem (α := R[X]) P ((algebraMap R R[X] : (a : R) → R[X]) b : R[X])
Tactic: rwa [SetLike.mem_coe, LiesOver.over (P := P) (p := p), mem_comap, algebraMap_eq, hb.2]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
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_1 : 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
this : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P
a : R[X]
h : a ∈ (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X])
ha : a ∈ (↑P : Set R[X])
b : R
hb : b ∈ (↑p.primeCompl : Set R) ∧ (C : (a : R) → R[X]) b = a
rwa : b ∈ p
rwa₁ : Membership.mem (γ := Ideal R) (under R P) b
rwa₂ : Membership.mem (α := R[X]) P ((algebraMap R R[X] : (a : R) → R[X]) b : R[X])
⊢ b ∈ (↑p : Set R)
have rwa₃ : Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) b : R[X])
Tactic: rwa [SetLike.mem_coe, LiesOver.over (P := P) (p := p), mem_comap, algebraMap_eq, hb.2]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
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_1 : 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
this : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P
a : R[X]
h : a ∈ (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X])
ha : a ∈ (↑P : Set R[X])
b : R
hb : b ∈ (↑p.primeCompl : Set R) ∧ (C : (a : R) → R[X]) b = a
rwa : b ∈ p
rwa₁ : Membership.mem (γ := Ideal R) (under R P) b
rwa₂ : Membership.mem (α := R[X]) P ((algebraMap R R[X] : (a : R) → R[X]) b : R[X])
rwa₃ : Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) b : R[X])
⊢ b ∈ (↑p : Set R)
have rwa₄ : a ∈ P
Tactic: rwa [SetLike.mem_coe, LiesOver.over (P := P) (p := p), mem_comap, algebraMap_eq, hb.2]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (hypothesis)
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_1 : 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
this : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P
⊢ P.height = p.height + 1
have disj : Disjoint (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X]) (↑P : Set R[X])
Tactic: have disj : Disjoint (p.primeCompl.map C : Set R[X]) P := by
    refine Set.disjoint_left.mpr fun a ⟨b, hb⟩ ha ↦ hb.1 ?_
    rwa [SetLike.mem_coe, LiesOver.over (P := P) (p := p), mem_comap, algebraMap_eq, hb.2]