awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact le_of_eq (IsLocalRing.eq_maximalIdeal this).symm

Premises used: le_of_eq, Eq.symm, IsLocalRing.eq_maximalIdeal
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h_2 : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
h : ringKrullDim R ≤ 0
⊢ Ring.KrullDimLE 0 R

Tactic:
have : Ring.KrullDimLE 0 R := Ring.krullDimLE_iff.mpr h
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h_2 : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
h : ringKrullDim R ≤ 0
this : Ring.KrullDimLE 0 R
⊢ False

Tactic:
hn Ring.KrullDimLE.isField_of_isDomain

Premises used: Ring.KrullDimLE.isField_of_isDomain
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h_2 : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
h : ringKrullDim R ≤ 0
this : Ring.KrullDimLE 0 R
⊢ False

Tactic:
exact hn Ring.KrullDimLE.isField_of_isDomain

Premises used: Ring.KrullDimLE.isField_of_isDomain
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬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 ≤ 0

Tactic:
have : ¬ ringKrullDim R ≤ 0 := fun h ↦ by
      have : Ring.KrullDimLE 0 R := Ring.krullDimLE_iff.mpr h
      exact hn Ring.KrullDimLE.isField_of_isDomain
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h_2 : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
this : ¬ringKrullDim R ≤ 0
h : Ring.KrullDimLE 1 R
⊢ ringKrullDim R ≤ (↑1 : WithBot ℕ∞)

Tactic:
rw [Ring.krullDimLE_iff] at h

Premises used: Ring.krullDimLE_iff
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h_2 : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
this : ¬ringKrullDim R ≤ 0
h : ringKrullDim R ≤ (↑1 : WithBot ℕ∞)
⊢ ringKrullDim R = 1

Tactic:
le_antisymm h (Order.succ_le_of_lt (lt_of_not_ge this))

Premises used: lt_of_not_ge, Order.succ_le_of_lt, le_antisymm
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h_2 : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
this : ¬ringKrullDim R ≤ 0
h : ringKrullDim R ≤ (↑1 : WithBot ℕ∞)
⊢ ringKrullDim R = 1

Tactic:
exact le_antisymm h (Order.succ_le_of_lt (lt_of_not_ge this))

Premises used: lt_of_not_ge, Order.succ_le_of_lt, le_antisymm
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬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}))
this : ¬ringKrullDim R ≤ 0
refine_3 : Ring.KrullDimLE 1 R
⊢ ringKrullDim R = 1

Tactic:
suffices h : Ring.KrullDimLE 1 R by
      rw [Ring.krullDimLE_iff] at h
      exact le_antisymm h (Order.succ_le_of_lt (lt_of_not_ge this))
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬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}))
this : ¬ringKrullDim R ≤ 0
⊢ Ring.KrullDimLE 1 R

Tactic:
Ring.krullDimLE_one_iff_of_noZeroDivisors.mpr fun I hI hI_prime ↦ ?_

Premises used: Iff.mpr, Ring.krullDimLE_one_iff_of_noZeroDivisors
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬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}))
this : ¬ringKrullDim R ≤ 0
refine_3 : ∀ (I : Ideal R) (hI : I ≠ ⊥) (hI_prime : I.IsPrime), I.IsMaximal
⊢ Ring.KrullDimLE 1 R

Tactic:
refine Ring.krullDimLE_one_iff_of_noZeroDivisors.mpr fun I hI hI_prime ↦ ?_

Premises used: Iff.mpr, Ring.krullDimLE_one_iff_of_noZeroDivisors
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬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}))
this : ¬ringKrullDim R ≤ 0
I : Ideal R
hI : I ≠ ⊥
hI_prime : I.IsPrime
apply : ∀ (h : ¬∃ x ∈ I, x ≠ 0), ∀ x ∈ I, Membership.mem (γ := Submodule R R) ⊥ x
⊢ ∃ x ∈ I, x ≠ 0

Tactic:
apply by_contradiction fun h ↦ (hI (le_antisymm (fun x ↦ ?_) bot_le))

Premises used: le_antisymm, by_contradiction, bot_le
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h_2 : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
this : ¬ringKrullDim R ≤ 0
I : Ideal R
hI : I ≠ ⊥
hI_prime : I.IsPrime
h : ¬∃ x ∈ I, x ≠ 0
x : R
⊢ ∀ x ∈ I, x = 0

Tactic:
simp only [ne_eq, not_exists, not_and, not_not] at h

Premises used: Classical.not_not, not_exists, ne_eq, not_and
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h_2 : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
this : ¬ringKrullDim R ≤ 0
I : Ideal R
hI : I ≠ ⊥
hI_prime : I.IsPrime
x : R
h : ∀ x ∈ I, x = 0
⊢ x ∈ I → Membership.mem (γ := Submodule R R) ⊥ x

Tactic:
fun hx ↦ h x hx

Premises used: Set.Mem, setOf, Set.singleton
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h_2 : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
this : ¬ringKrullDim R ≤ 0
I : Ideal R
hI : I ≠ ⊥
hI_prime : I.IsPrime
x : R
h : ∀ x ∈ I, x = 0
⊢ x ∈ I → Membership.mem (γ := Submodule R R) ⊥ x

Tactic:
exact fun hx ↦ h x hx
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬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}))
this : ¬ringKrullDim R ≤ 0
I : Ideal R
hI : I ≠ ⊥
hI_prime : I.IsPrime
refine_3 : ∀ (x : R) (hI : x ∈ I) (hx : x ≠ 0), I.IsMaximal
⊢ I.IsMaximal

Tactic:
obtain ⟨x, hI, hx⟩ : ∃ (x : R), x ∈ I ∧ x ≠ 0 := by
      apply by_contradiction fun h ↦ (hI (le_antisymm (fun x ↦ ?_) bot_le))
      simp only [ne_eq, not_exists, not_and, not_not] at h
      exact fun hx ↦ h x hx
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬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}))
this : ¬ringKrullDim R ≤ 0
I : Ideal R
hI_1 : I ≠ ⊥
hI_prime : I.IsPrime
x : R
hI : x ∈ I
hx : x ≠ 0
⊢ IsLocalRing.maximalIdeal R ≤ I

Tactic:
have : IsLocalRing.maximalIdeal R ≤ I := le_trans (h x hx)
      ((Ideal.IsRadical.radical_le_iff hI_prime.isRadical).mpr
        ((Ideal.span_singleton_le_iff_mem I).mpr hI))
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬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}))
this_1 : ¬ringKrullDim R ≤ 0
I : Ideal R
hI_1 : I ≠ ⊥
hI_prime : I.IsPrime
x : R
hI : x ∈ I
hx : x ≠ 0
this : IsLocalRing.maximalIdeal R ≤ I
⊢ IsLocalRing.maximalIdeal R = I

Tactic:
have := Ideal.IsMaximal.eq_of_le (IsLocalRing.maximalIdeal.isMaximal R) hI_prime.ne_top this
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬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}))
this_1 : ¬ringKrullDim R ≤ 0
I : Ideal R
hI_1 : I ≠ ⊥
hI_prime : I.IsPrime
x : R
hI : x ∈ I
hx : x ≠ 0
this_2 : IsLocalRing.maximalIdeal R ≤ I
this : IsLocalRing.maximalIdeal R = I
⊢ I.IsMaximal

Tactic:
this ▸ (IsLocalRing.maximalIdeal.isMaximal R)

Premises used: Eq.rec, IsLocalRing.maximalIdeal.isMaximal
-- Module: Mathlib.RingTheory.KrullDimension.LocalRing
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬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}))
this_1 : ¬ringKrullDim R ≤ 0
I : Ideal R
hI_1 : I ≠ ⊥
hI_prime : I.IsPrime
x : R
hI : x ∈ I
hx : x ≠ 0
this_2 : IsLocalRing.maximalIdeal R ≤ I
this : IsLocalRing.maximalIdeal R = I
⊢ I.IsMaximal

Tactic:
exact this ▸ (IsLocalRing.maximalIdeal.isMaximal R)
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Subsingleton M
⊢ supportDim R M = ⊥

Tactic:
simpa [supportDim, support_eq_empty_iff]

Premises used: Module.support_eq_empty_iff, Module.supportDim
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
⊢ Nonempty.{u_1 + 1} (↑(support R M) : Type u_1)

Tactic:
have : Nonempty (Module.support R M) := nonempty_support_of_nontrivial.to_subtype
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
this : Nonempty.{u_1 + 1} (↑(support R M) : Type u_1)
⊢ supportDim R M ≠ ⊥

Tactic:
simp [supportDim]

Premises used: Module.supportDim
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ supportDim R M = ⊥ ↔ Subsingleton M

Tactic:
simp [supportDim, krullDim_eq_bot_iff, support_eq_empty_iff]

Premises used: Order.krullDim_eq_bot_iff, Module.support_eq_empty_iff, Module.supportDim
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ supportDim R M ≠ ⊥ ↔ Nontrivial M

Tactic:
simp [supportDim, krullDim_eq_bot_iff, support_eq_empty_iff, not_subsingleton_iff_nontrivial]

Premises used: Order.krullDim_eq_bot_iff, Module.support_eq_empty_iff, Module.supportDim, not_subsingleton_iff_nontrivial
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
rw :
  krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑(annihilator R M) : Set R)) : Type u_1) =
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := _root_.Ideal R) (annihilator R M))
rw₁ rw₂ :
  krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑(annihilator R M) : Set R)) : Type u_1) =
    krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑(annihilator R M) : Set R)) : Type u_1)
⊢ krullDim.{u_1} (↑(support R M) : Type u_1) =
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := _root_.Ideal R) (annihilator R M))

Tactic:
rw [support_eq_zeroLocus, ringKrullDim_quotient]

Premises used: ringKrullDim_quotient, Module.support_eq_zeroLocus
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := _root_.Ideal R) (annihilator R R) ⊥

Tactic:
have : annihilator R R = ⊥ :=
    annihilator_eq_bot.mpr ((faithfulSMul_iff_algebraMap_injective R R).mpr fun {a₁ a₂} a ↦ a)
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
this : Eq (α := _root_.Ideal R) (annihilator R R) ⊥
rw : ringKrullDim.{u_1} (HasQuotient.Quotient R (B := _root_.Ideal R) ⊥) = ringKrullDim R
⊢ supportDim R R = ringKrullDim R

Tactic:
rw [supportDim_eq_ringKrullDim_quotient_annihilator, this]

Premises used: Module.supportDim_eq_ringKrullDim_quotient_annihilator
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
this : Eq (α := _root_.Ideal R) (annihilator R R) ⊥
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := _root_.Ideal R) ⊥) = ringKrullDim R

Tactic:
(RingEquiv.ringKrullDim (RingEquiv.quotientBot R))

Premises used: RingEquiv.ringKrullDim, RingEquiv.quotientBot
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
this : Eq (α := _root_.Ideal R) (annihilator R R) ⊥
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := _root_.Ideal R) ⊥) = ringKrullDim R

Tactic:
exact (RingEquiv.ringKrullDim (RingEquiv.quotientBot R))

Premises used: RingEquiv.ringKrullDim, RingEquiv.quotientBot
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ supportDim R M ≤ ringKrullDim R

Tactic:
krullDim_le_of_strictMono (fun a ↦ a) fun {_ _} lt ↦ lt

Premises used: Order.krullDim_le_of_strictMono, Module.supportDim, ringKrullDim, Subtype.val
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
I : _root_.Ideal R
rw :
  ringKrullDim.{u_1} (HasQuotient.Quotient R (B := _root_.Ideal R) (annihilator R (R ⧸ I))) = ringKrullDim.{u_1} (R ⧸ I)
rw₁ rw₂ : ringKrullDim.{u_1} (R ⧸ I) = ringKrullDim.{u_1} (R ⧸ I)
⊢ supportDim R (R ⧸ I) = ringKrullDim.{u_1} (R ⧸ I)

Tactic:
rw [supportDim_eq_ringKrullDim_quotient_annihilator, Ideal.annihilator_quotient]

Premises used: Module.supportDim_eq_ringKrullDim_quotient_annihilator, Ideal.annihilator_quotient
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ supportDim R M ≤ supportDim R N

Tactic:
krullDim_le_of_strictMono (fun a ↦ ⟨a.1, Module.support_subset_of_injective f h a.2⟩)
    (fun {_ _} lt ↦ lt)

Premises used: Subtype.mk, Order.krullDim_le_of_strictMono, Module.support_subset_of_injective, Module.supportDim, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ supportDim R N ≤ supportDim R M

Tactic:
krullDim_le_of_strictMono (fun a ↦ ⟨a.1, Module.support_subset_of_surjective f h a.2⟩)
    (fun {_ _} lt ↦ lt)

Premises used: Subtype.mk, Order.krullDim_le_of_strictMono, Module.supportDim, Subtype.val, Module.support_subset_of_surjective, Subtype.property
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
⊢ supportDim R M = supportDim R N

Tactic:
le_antisymm (supportDim_le_of_injective e e.injective)
    (supportDim_le_of_surjective e e.surjective)

Premises used: Module.supportDim_le_of_injective, LinearEquiv.surjective, le_antisymm, LinearEquiv.toLinearMap, LinearEquiv.injective, Module.supportDim_le_of_surjective
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
⊢ Nontrivial N

Tactic:
simp [← Module.supportDim_ne_bot_iff_nontrivial R, dim]

Premises used: Module.supportDim_ne_bot_iff_nontrivial
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
rw : Eq (α := Set (PrimeSpectrum R)) (Module.support R N) {{ asIdeal := maximalIdeal R, isPrime := ⋯ }}
⊢ Eq (α := Set (PrimeSpectrum R)) (Module.support R N) (PrimeSpectrum.zeroLocus (↑(maximalIdeal R) : Set R))

Tactic:
rw [PrimeSpectrum.zeroLocus_eq_singleton]

Premises used: PrimeSpectrum.zeroLocus_eq_singleton
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
a : LE.le (α := Set (PrimeSpectrum R)) (Module.support R N) {{ asIdeal := maximalIdeal R, isPrime := ⋯ }}
a₁ : LE.le (α := Set (PrimeSpectrum R)) {{ asIdeal := maximalIdeal R, isPrime := ⋯ }} (Module.support R N)
⊢ Eq (α := Set (PrimeSpectrum R)) (Module.support R N) {{ asIdeal := maximalIdeal R, isPrime := ⋯ }}

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p
a : ∀ (nmem : p ∉ {{ asIdeal := maximalIdeal R, isPrime := ⋯ }}), False
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) {{ asIdeal := maximalIdeal R, isPrime := ⋯ }} p

Tactic:
by_contra nmem
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p
nmem : p ∉ {{ asIdeal := maximalIdeal R, isPrime := ⋯ }}
⊢ ¬p = { asIdeal := maximalIdeal R, isPrime := ⋯ }

Tactic:
push _ ∈ _ at nmem
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p
nmem : ¬p = { asIdeal := maximalIdeal R, isPrime := ⋯ }
⊢ p < { asIdeal := maximalIdeal R, isPrime := ⋯ }

Tactic:
have : p < ⟨maximalIdeal R, IsMaximal.isPrime' (maximalIdeal R)⟩ :=
      lt_of_le_of_ne (IsLocalRing.le_maximalIdeal IsPrime.ne_top') nmem
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p
nmem : ¬p = { asIdeal := maximalIdeal R, isPrime := ⋯ }
this : p < { asIdeal := maximalIdeal R, isPrime := ⋯ }
simp :
  ∃ (a : PrimeSpectrum R),
    Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) a ∧
      ∃ (a_1 : PrimeSpectrum R), Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) a_1 ∧ a < a_1
⊢ Module.supportDim R N > 0

Tactic:
simp only [Module.supportDim, gt_iff_lt, Order.krullDim_pos_iff, Subtype.exists,
        Subtype.mk_lt_mk, exists_prop]

Premises used: Order.krullDim_pos_iff, Subtype.mk_lt_mk, Subtype.exists, exists_prop, gt_iff_lt, Module.supportDim
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h_1 : Nontrivial N := ⋯
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p
nmem : ¬p = { asIdeal := maximalIdeal R, isPrime := ⋯ }
this : p < { asIdeal := maximalIdeal R, isPrime := ⋯ }
h :
  Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p ∧
    ∃ (a : PrimeSpectrum R), Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) a ∧ p < a
⊢ ∃ (a : PrimeSpectrum R),
    Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) a ∧
      ∃ (a_1 : PrimeSpectrum R), Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) a_1 ∧ a < a_1

Tactic:
use p
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p
nmem : ¬p = { asIdeal := maximalIdeal R, isPrime := ⋯ }
this : p < { asIdeal := maximalIdeal R, isPrime := ⋯ }
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p ∧
    ∃ (a : PrimeSpectrum R), Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) a ∧ p < a

Tactic:
simpa [hp] using ⟨_, IsLocalRing.closedPoint_mem_support R N, this⟩