awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
e : R ≃+* S
⊢ ringKrullDim R = ringKrullDim S

Tactic:
le_antisymm (ringKrullDim_le_of_surjective e.symm e.symm.surjective)
    (ringKrullDim_le_of_surjective e e.surjective)

Premises used: RingEquiv.surjective, le_antisymm, RingHomClass.toRingHom, ringKrullDim_le_of_surjective, RingEquiv.symm
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : FiniteRingKrullDim R
⊢ ringKrullDim R ≠ ⊤

Tactic:
krullDim_ne_top_of_finiteDimensionalOrder

Premises used: ringKrullDim, Order.krullDim_ne_top_of_finiteDimensionalOrder
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : FiniteRingKrullDim R
⊢ ringKrullDim R < ⊤

Tactic:
ringKrullDim_ne_top.lt_top

Premises used: Ne.lt_top, ringKrullDim_ne_top
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : FiniteRingKrullDim R
⊢ ringKrullDim R ≠ ⊥

Tactic:
krullDim_ne_bot_of_finiteDimensionalOrder

Premises used: Order.krullDim_ne_bot_of_finiteDimensionalOrder, ringKrullDim
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
⊢ FiniteRingKrullDim R ↔ ringKrullDim R ≠ ⊥ ∧ ringKrullDim R ≠ ⊤

Tactic:
(Order.finiteDimensionalOrder_iff_krullDim_ne_bot_and_top (α := PrimeSpectrum R))

Premises used: Order.finiteDimensionalOrder_iff_krullDim_ne_bot_and_top, ringKrullDim
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : FiniteRingKrullDim R
rw : Nonempty.{u_1 + 1} (PrimeSpectrum R)
⊢ Nontrivial R

Tactic:
rw [← PrimeSpectrum.nonempty_iff_nontrivial]

Premises used: PrimeSpectrum.nonempty_iff_nontrivial
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : FiniteRingKrullDim R
⊢ Nonempty.{u_1 + 1} (PrimeSpectrum R)

Tactic:
LTSeries.nonempty_of_finiteDimensionalOrder _

Premises used: LTSeries.nonempty_of_finiteDimensionalOrder
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : FiniteRingKrullDim R
⊢ Nonempty.{u_1 + 1} (PrimeSpectrum R)

Tactic:
exact LTSeries.nonempty_of_finiteDimensionalOrder _

Premises used: LTSeries.nonempty_of_finiteDimensionalOrder
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
simp_rw :
  (∀ (a : Ideal R) (b : a.IsPrime),
      Ideal.IsMaximal.{u_1} (α := R)
        (PrimeSpectrum.asIdeal
          ((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)))) ↔
    ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
⊢ KrullDimLE 0 R ↔ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal

Tactic:
simp_rw [Ring.KrullDimLE, Order.krullDimLE_iff, Nat.cast_zero,
    Order.krullDim_nonpos_iff_forall_isMax,
    (PrimeSpectrum.equivSubtype R).forall_congr_left, Subtype.forall, PrimeSpectrum.isMax_iff]

Premises used: Order.krullDim_nonpos_iff_forall_isMax, PrimeSpectrum.isMax_iff, Equiv.forall_congr_left, PrimeSpectrum.equivSubtype, Subtype.forall, Nat.cast_zero, RelIso.toEquiv, Ring.KrullDimLE, Order.krullDimLE_iff
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      Ideal.IsMaximal.{u_1} (α := R)
        (PrimeSpectrum.asIdeal
          ((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)))) ↔
    ∀ (I : Ideal R), I.IsPrime → I.IsMaximal

Tactic:
rfl
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
H rwa rwa₁ rwa₂ rwa₃ : ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
⊢ KrullDimLE 0 R

Tactic:
rwa [Ring.krullDimLE_zero_iff]

Premises used: Ring.krullDimLE_zero_iff
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Ring.KrullDimLE 0 R
I : Ideal R
inst_2 : I.IsPrime
⊢ I.IsMaximal

Tactic:
Ring.krullDimLE_zero_iff.mp ‹_› I ‹_›

Premises used: Ring.krullDimLE_zero_iff, Iff.mp
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Ring.KrullDimLE 0 R
I : Ideal R
hI : I.IsPrime
⊢ I.IsMaximal

Tactic:
I.isMaximal_of_isPrime

Premises used: Ideal.isMaximal_of_isPrime
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal R
inst_2 : I.IsPrime
inst_3 : Ring.KrullDimLE 0 R
⊢ I.IsMaximal

Tactic:
I.isMaximal_of_isPrime

Premises used: Ideal.isMaximal_of_isPrime
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Ring.KrullDimLE 0 R
I : Ideal R
⊢ I.IsMaximal ↔ I.IsPrime

Tactic:
⟨IsMaximal.isPrime, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Ideal.IsMaximal.isPrime, Iff.intro
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Ring.KrullDimLE 0 R
I : Ideal R
inst_2 : I.IsPrime
⊢ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I

Tactic:
minimalPrimes_eq_minimals (R := R) ▸
    ⟨‹_›, fun J hJ hJI ↦ (IsMaximal.eq_of_le inferInstance IsPrime.ne_top' hJI).ge⟩

Premises used: minimalPrimes_eq_minimals, Eq.ge, Eq.rec, inferInstance, Ideal.IsMaximal.eq_of_le, And.intro, Ideal.IsPrime.ne_top', Eq.symm
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Ring.KrullDimLE 0 R
I : Ideal R
⊢ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I ↔ I.IsPrime

Tactic:
⟨(·.1.1), fun _ ↦ I.mem_minimalPrimes_of_krullDimLE_zero⟩

Premises used: And.left, Iff.intro, Ideal.mem_minimalPrimes_of_krullDimLE_zero
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_3
inst : CommRing R
⊢ LE.le (α := Ideal R) (nilradical R) (Ring.jacobson R)

Tactic:
nilradical_eq_sInf R ▸ le_sInf fun _I hI ↦ sInf_le (Ideal.IsMaximal.isPrime ⟨hI⟩)

Premises used: Eq.rec, Ideal.IsMaximal.isPrime, Ideal.IsMaximal.mk, sInf_le, le_sInf, nilradical_eq_sInf, Eq.symm
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_3
inst : CommRing R
inst_1 : KrullDimLE 0 R
⊢ Eq (α := Ideal R) (jacobson R) (nilradical R)

Tactic:
(nilradical_le_jacobson R).antisymm' <| nilradical_eq_sInf R ▸ le_sInf fun I (_ : I.IsPrime) ↦
    sInf_le Ideal.IsMaximal.out

Premises used: LE.le.antisymm', nilradical_le_jacobson, Eq.rec, Ideal.IsMaximal.out, sInf_le, le_sInf, nilradical_eq_sInf, Eq.symm
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Ring.KrullDimLE 0 R
⊢ Ring.KrullDimLE 1 R

Tactic:
.mono zero_le_one _

Premises used: Order.KrullDimLE.mono, zero_le_one
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
simp_rw :
  (∀ (a : Ideal R) (b : a.IsPrime),
      Membership.mem (γ := Set (Ideal R)) (minimalPrimes R)
          (PrimeSpectrum.asIdeal
            ((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))) ∨
        Ideal.IsMaximal.{u_1} (α := R)
          (PrimeSpectrum.asIdeal
            ((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)))) ↔
    ∀ (I : Ideal R), I.IsPrime → Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I ∨ I.IsMaximal
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I.IsPrime → Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I ∨ I.IsMaximal

Tactic:
simp_rw [Ring.KrullDimLE, Order.krullDimLE_iff, Nat.cast_one,
    Order.krullDim_le_one_iff, (PrimeSpectrum.equivSubtype R).forall_congr_left,
    Subtype.forall, PrimeSpectrum.isMax_iff, PrimeSpectrum.isMin_iff]

Premises used: Order.krullDim_le_one_iff, PrimeSpectrum.isMax_iff, Equiv.forall_congr_left, PrimeSpectrum.isMin_iff, PrimeSpectrum.equivSubtype, Subtype.forall, RelIso.toEquiv, Nat.cast_one, Ring.KrullDimLE, Order.krullDimLE_iff
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      Membership.mem (γ := Set (Ideal R)) (minimalPrimes R)
          (PrimeSpectrum.asIdeal
            ((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))) ∨
        Ideal.IsMaximal.{u_1} (α := R)
          (PrimeSpectrum.asIdeal
            ((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)))) ↔
    ∀ (I : Ideal R), I.IsPrime → Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I ∨ I.IsMaximal

Tactic:
rfl
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
H rwa rwa₁ rwa₂ rwa₃ :
  ∀ (I : Ideal R), I.IsPrime → Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I ∨ I.IsMaximal
⊢ KrullDimLE 1 R

Tactic:
rwa [Ring.krullDimLE_one_iff]

Premises used: Ring.krullDimLE_one_iff
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Ideal.IsPrime.{u_1} (α := R) ⊥
this : OrderBot (PrimeSpectrum R) := { bot := { asIdeal := ⊥, isPrime := inst_1 }, bot_le := ⋯ }
simp_rw :
  (∀ (a : Ideal R) (b : a.IsPrime),
      ¬Eq.{u_1 + 1} (α := Ideal R)
            (PrimeSpectrum.asIdeal
              ((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.asIdeal ⊥) →
        Ideal.IsMaximal.{u_1} (α := R)
          (PrimeSpectrum.asIdeal
            ((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)))) ↔
    ∀ (I : Ideal R) (b : I.IsPrime) (a : ¬I = ⊥), I.IsMaximal
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
simp_rw [Ring.KrullDimLE, Order.krullDimLE_iff, Nat.cast_one,
    Order.krullDim_le_one_iff_forall_isMax, (PrimeSpectrum.equivSubtype R).forall_congr_left,
    Subtype.forall, PrimeSpectrum.isMax_iff, forall_comm (α := _ ≠ ⊥),
    ne_eq, PrimeSpectrum.ext_iff]

Premises used: PrimeSpectrum.isMax_iff, Equiv.forall_congr_left, forall_comm, PrimeSpectrum.equivSubtype, Subtype.forall, ne_eq, PrimeSpectrum.ext_iff, Order.krullDim_le_one_iff_forall_isMax, RelIso.toEquiv, Nat.cast_one, Ring.KrullDimLE, Order.krullDimLE_iff
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Ideal.IsPrime.{u_1} (α := R) ⊥
this : OrderBot (PrimeSpectrum R) := { bot := { asIdeal := ⊥, isPrime := inst_1 }, bot_le := ⋯ }
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      ¬Eq.{u_1 + 1} (α := Ideal R)
            (PrimeSpectrum.asIdeal
              ((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.asIdeal ⊥) →
        Ideal.IsMaximal.{u_1} (α := R)
          (PrimeSpectrum.asIdeal
            ((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)))) ↔
    ∀ (I : Ideal R) (b : I.IsPrime) (a : ¬I = ⊥), I.IsMaximal

Tactic:
rfl
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inl : Subsingleton R → (KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal)
inr : Nontrivial R → (KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal)
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
h : Subsingleton R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
iff_of_true inferInstance fun I h ↦ (h <| Subsingleton.elim ..).elim

Premises used: False.elim, inferInstance, Bot.bot, iff_of_true, Subsingleton.elim
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
h : Subsingleton R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
exact iff_of_true inferInstance fun I h ↦ (h <| Subsingleton.elim ..).elim
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
h : Nontrivial R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
Ring.krullDimLE_one_iff_of_isPrime_bot

Premises used: Ring.krullDimLE_one_iff_of_isPrime_bot
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
h : Nontrivial R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
exact Ring.krullDimLE_one_iff_of_isPrime_bot

Premises used: Ring.krullDimLE_one_iff_of_isPrime_bot
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : Ring.KrullDimLE 1 R
I : Ideal R
hI : I.IsPrime
hI' : I ≠ ⊥
⊢ I.IsMaximal

Tactic:
Ring.krullDimLE_one_iff_of_noZeroDivisors.mp ‹_› _ hI' hI

Premises used: Ring.krullDimLE_one_iff_of_noZeroDivisors, Iff.mp
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : Ring.KrullDimLE 1 R
I : Ideal R
inst_3 : I.IsPrime
hI' : I ≠ ⊥
⊢ I.IsMaximal

Tactic:
Ideal.IsPrime.isMaximal_of_ne_bot ‹_› hI'

Premises used: Ideal.IsPrime.isMaximal_of_ne_bot
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
pos : ∀ (hR : Ideal.IsPrime.{u_1} (α := R) ⊥), KrullDimLE 1 R
neg : ∀ (hR : ¬Ideal.IsPrime.{u_1} (α := R) ⊥), KrullDimLE 1 R
⊢ KrullDimLE 1 R

Tactic:
by_cases hR : (⊥ : Ideal R).IsPrime

Premises used: Bot.bot, Ideal.IsPrime
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : Ideal.IsPrime.{u_1} (α := R) ⊥
pos pos₁ pos₂ pos₃ : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
⊢ KrullDimLE 1 R

Tactic:
rwa [Ring.krullDimLE_one_iff_of_isPrime_bot]

Premises used: Ring.krullDimLE_one_iff_of_isPrime_bot
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ¬Ideal.IsPrime.{u_1} (α := R) ⊥
neg : KrullDimLE 0 R
⊢ KrullDimLE 1 R

Tactic:
suffices Ring.KrullDimLE 0 R from inferInstance
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ¬Ideal.IsPrime.{u_1} (α := R) ⊥
⊢ KrullDimLE 0 R

Tactic:
.mk₀ fun I hI ↦ H I (fun e ↦ hR (e ▸ hI)) hI

Premises used: Ring.KrullDimLE.mk₀, Eq.rec
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ¬Ideal.IsPrime.{u_1} (α := R) ⊥
⊢ KrullDimLE 0 R

Tactic:
exact .mk₀ fun I hI ↦ H I (fun e ↦ hR (e ▸ hI)) hI
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : Ring.KrullDimLE 1 R
a : R
ha : Prime a
⊢ Ne (α := Ideal R) (Ideal.span {a}) ⊥

Tactic:
simpa using ha.ne_zero

Premises used: Prime.ne_zero
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : NoZeroDivisors R
inst_3 : Ring.KrullDimLE 1 R
inst_4 : Algebra R S
P : Ideal S
p : R
hP : P ≠ ⊤
hp : Prime p
⊢ Ne (α := Ideal R) (under R P) ⊤

Tactic:
have hP : P.under R ≠ ⊤ := Ideal.comap_ne_top _ hP
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : NoZeroDivisors R
inst_3 : Ring.KrullDimLE 1 R
inst_4 : Algebra R S
P : Ideal S
p : R
hP_1 : P ≠ ⊤
hp : Prime p
hP : Ne (α := Ideal R) (under R P) ⊤
⊢ P.LiesOver (A := R) (span {p}) ↔ Membership.mem (α := S) P ((algebraMap R S : (a : R) → S) p : S)

Tactic:
simp [Ideal.liesOver_iff, Ideal.IsMaximal.eq_iff_le hp.isMaximal_span_singleton hP]

Premises used: Prime.isMaximal_span_singleton, Ideal.liesOver_iff, Ideal.IsMaximal.eq_iff_le
-- Module: Mathlib.RingTheory.KrullDimension.Field
Goal:
F : Type u_1
inst : Field F
⊢ ringKrullDim F = 0

Tactic:
krullDim_eq_zero_of_unique

Premises used: Order.krullDim_eq_zero_of_unique, ringKrullDim
-- Module: Mathlib.RingTheory.KrullDimension.Field
Goal:
F : Type u_1
inst : CommRing F
hF : IsField F
⊢ ringKrullDim F = 0

Tactic:
@krullDim_eq_zero_of_unique _ _ <| @PrimeSpectrum.instUnique _ hF.toField

Premises used: Order.krullDim_eq_zero_of_unique, ringKrullDim
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
⊢ ringKrullDim R = 1 ↔
    ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))

Tactic:
⟨fun h ↦ ⟨fun h' ↦ ?_, ?_⟩, fun ⟨hn, h⟩ ↦ ?_⟩

Premises used: _private.0.ringKrullDim_eq_one_iff_of_isLocalRing_isDomain.match_1, And.intro, Iff.intro, ringKrullDim, OfNat.ofNat, Eq
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
refine_1 : ∀ (h : ringKrullDim R = 1) (h' : IsField R), False
refine_2 :
  ∀ (h : ringKrullDim R = 1) (x : R),
    x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
refine_3 :
  (¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))) →
    ∀ (hn : ¬IsField R)
      (h : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))),
      ringKrullDim R = 1
⊢ ringKrullDim R = 1 ↔
    ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))

Tactic:
refine ⟨fun h ↦ ⟨fun h' ↦ ?_, ?_⟩, fun ⟨hn, h⟩ ↦ ?_⟩
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h : ringKrullDim R = 1
h' : IsField R
⊢ False

Tactic:
zero_ne_one ((ringKrullDim_eq_zero_of_isField h') ▸ h)

Premises used: zero_ne_one
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h : ringKrullDim R = 1
h' : IsField R
⊢ False

Tactic:
exact zero_ne_one ((ringKrullDim_eq_zero_of_isField h') ▸ h)

Premises used: zero_ne_one
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h : ringKrullDim R = 1
x : R
hx : x ≠ 0
refine_2 : LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (sInf {J : Ideal R | Ideal.span {x} ≤ J ∧ J.IsPrime})
⊢ LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))

Tactic:
rw [Ideal.radical_eq_sInf]

Premises used: Ideal.radical_eq_sInf
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h : ringKrullDim R = 1
x : R
hx : x ≠ 0
⊢ LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (sInf {J : Ideal R | Ideal.span {x} ≤ J ∧ J.IsPrime})

Tactic:
le_sInf (fun J ⟨hJ1, hJ2⟩ ↦ ?_)

Premises used: Set.Mem, IsLocalRing.maximalIdeal, _private.0.ringKrullDim_eq_one_iff_of_isLocalRing_isDomain.match_2, LE.le, le_sInf
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h : ringKrullDim R = 1
x : R
hx : x ≠ 0
refine_2 :
  ∀ (J : Ideal R),
    Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.span {x} ≤ J ∧ J.IsPrime} J →
      ∀ (hJ1 : Ideal.span {x} ≤ J) (hJ2 : J.IsPrime), IsLocalRing.maximalIdeal R ≤ J
⊢ LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (sInf {J : Ideal R | Ideal.span {x} ≤ J ∧ J.IsPrime})

Tactic:
refine le_sInf (fun J ⟨hJ1, hJ2⟩ ↦ ?_)
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h : ringKrullDim R = 1
x : R
hx : x ≠ 0
J : Ideal R
h_1 : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.span {x} ≤ J ∧ J.IsPrime} J
hJ1 : Ideal.span {x} ≤ J
hJ2 : J.IsPrime
⊢ ringKrullDim R ≤ (↑1 : WithBot ℕ∞)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h : ringKrullDim R = 1
x : R
hx : x ≠ 0
J : Ideal R
h_1 : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.span {x} ≤ J ∧ J.IsPrime} J
hJ1 : Ideal.span {x} ≤ J
hJ2 : J.IsPrime
hJ3 : J = ⊥
⊢ x = 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h : ringKrullDim R = 1
x : R
hx : x ≠ 0
J : Ideal R
h_1 : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.span {x} ≤ J ∧ J.IsPrime} J
hJ1 : Ideal.span {x} ≤ J
hJ2 : J.IsPrime
⊢ J.IsMaximal

Tactic:
have : J.IsMaximal :=
      Ring.krullDimLE_one_iff_of_noZeroDivisors.mp (Ring.krullDimLE_iff.mpr (by simp [h]))
        J (fun hJ3 ↦ hx (by simp_all)) hJ2
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h : ringKrullDim R = 1
x : R
hx : x ≠ 0
J : Ideal R
h_1 : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.span {x} ≤ J ∧ J.IsPrime} J
hJ1 : Ideal.span {x} ≤ J
hJ2 : J.IsPrime
this : J.IsMaximal
⊢ IsLocalRing.maximalIdeal R ≤ J

Tactic:
le_of_eq (IsLocalRing.eq_maximalIdeal this).symm

Premises used: le_of_eq, Eq.symm, IsLocalRing.eq_maximalIdeal