awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
n : ℕ
hn :
  comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n) ⊔ I =
    comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ) ⊔ I
y : R
hy : Membership.mem (γ := Submodule R R) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ)) y
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx :
  Membership.mem (γ := Submodule R R)
    ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
          (a : Ideal (Localization.AtPrime q)) → Ideal R)
        (HPow.hPow (α := Ideal (Localization.AtPrime q))
          (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
      Ideal R)
    (y + z • Submodule.IsPrincipal.generator I)
⊢ z * Submodule.IsPrincipal.generator I ∈
    HMul.hMul (α := Ideal R)
      ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
            (a : Ideal (Localization.AtPrime q)) → Ideal R)
          (HPow.hPow (α := Ideal (Localization.AtPrime q))
            (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
        Ideal R)
      I

Tactic:
Ideal.mul_mem_mul ?_ (Submodule.IsPrincipal.generator_mem _)

Premises used: Set.Mem, Ideal.mul_mem_mul, Submodule.IsPrincipal.generator_mem
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
n : ℕ
hn :
  comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n) ⊔ I =
    comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ) ⊔ I
y : R
hy : Membership.mem (γ := Submodule R R) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ)) y
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx :
  Membership.mem (γ := Submodule R R)
    ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
          (a : Ideal (Localization.AtPrime q)) → Ideal R)
        (HPow.hPow (α := Ideal (Localization.AtPrime q))
          (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
      Ideal R)
    (y + z • Submodule.IsPrincipal.generator I)
hIN :
  Membership.mem (γ := Ideal R)
    ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
          (a : Ideal (Localization.AtPrime q)) → Ideal R)
        (HPow.hPow (α := Ideal (Localization.AtPrime q))
          (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
      Ideal R)
    z
⊢ z * Submodule.IsPrincipal.generator I ∈
    HMul.hMul (α := Ideal R)
      ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
            (a : Ideal (Localization.AtPrime q)) → Ideal R)
          (HPow.hPow (α := Ideal (Localization.AtPrime q))
            (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
        Ideal R)
      I

Tactic:
refine Ideal.mul_mem_mul ?_ (Submodule.IsPrincipal.generator_mem _)

Premises used: Ideal.mul_mem_mul, Submodule.IsPrincipal.generator_mem
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
n : ℕ
hn :
  comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n) ⊔ I =
    comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ) ⊔ I
y : R
hy : Membership.mem (γ := Submodule R R) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ)) y
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx :
  Membership.mem (γ := Submodule R R)
    (under R
      (HPow.hPow (α := Ideal (Localization.AtPrime q))
        (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n))
    (y + z * Submodule.IsPrincipal.generator I)
hIN :
  ∀
    (hx :
      HMul.hMul (α := Localization.AtPrime q) (β := Localization.AtPrime q)
          ((f : (a : R) → Localization.AtPrime q) (Submodule.IsPrincipal.generator I) : Localization.AtPrime q)
          ((f : (a : R) → Localization.AtPrime q) z : Localization.AtPrime q) ∈
        HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n),
    IsUnit (M := Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) (Submodule.IsPrincipal.generator I) : Localization.AtPrime q)
⊢ Membership.mem (γ := Ideal R)
    ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
          (a : Ideal (Localization.AtPrime q)) → Ideal R)
        (HPow.hPow (α := Ideal (Localization.AtPrime q))
          (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
      Ideal R)
    z

Tactic:
rwa [Ideal.mem_comap, f.map_add, f.map_mul, Ideal.add_mem_iff_right _
      (Ideal.pow_le_pow_right n.le_succ hy), mul_comm, Ideal.unit_mul_mem_iff_mem] at hx

Premises used: Nat.le_succ, Ideal.pow_le_pow_right, Ideal.add_mem_iff_right, Ideal.unit_mul_mem_iff_mem, mul_comm, RingHom.map_mul, RingHom.map_add, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
n : ℕ
hn :
  comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n) ⊔ I =
    comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ) ⊔ I
y : R
hy : Membership.mem (γ := Submodule R R) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ)) y
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx :
  HMul.hMul (α := Localization.AtPrime q) (β := Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) (Submodule.IsPrincipal.generator I) : Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) z : Localization.AtPrime q) ∈
    HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n
⊢ IsUnit (M := Localization.AtPrime q)
    ((f : (a : R) → Localization.AtPrime q) (Submodule.IsPrincipal.generator I) : Localization.AtPrime q)

Tactic:
IsLocalization.map_units (M := q.primeCompl) _ ⟨_, ?_⟩

Premises used: Subtype.mk, Submodule.IsPrincipal.generator, IsLocalization.map_units, Classical.choose
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
n : ℕ
hn :
  comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n) ⊔ I =
    comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ) ⊔ I
y : R
hy : Membership.mem (γ := Submodule R R) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ)) y
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx :
  HMul.hMul (α := Localization.AtPrime q) (β := Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) (Submodule.IsPrincipal.generator I) : Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) z : Localization.AtPrime q) ∈
    HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n
hIN : (Classical.indefiniteDescription (fun (x : R) ↦ I = R ∙ x) ⋯).1 ∈ q.primeCompl
⊢ IsUnit (M := Localization.AtPrime q)
    ((f : (a : R) → Localization.AtPrime q) (Submodule.IsPrincipal.generator I) : Localization.AtPrime q)

Tactic:
refine IsLocalization.map_units (M := q.primeCompl) _ ⟨_, ?_⟩

Premises used: Subtype.mk, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
n : ℕ
hn :
  comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n) ⊔ I =
    comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ) ⊔ I
y : R
hy : Membership.mem (γ := Submodule R R) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ)) y
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx :
  HMul.hMul (α := Localization.AtPrime q) (β := Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) (Submodule.IsPrincipal.generator I) : Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) z : Localization.AtPrime q) ∈
    HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n
hIN : Submodule.IsPrincipal.generator I ∉ (↑q : Set R)
⊢ (Classical.indefiniteDescription (fun (x : R) ↦ I = R ∙ x) ⋯).1 ∈ q.primeCompl

Tactic:
change Submodule.IsPrincipal.generator I ∉ (↑q : Set R)

Premises used: Submodule.IsPrincipal.generator, SetLike.coe
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
n : ℕ
hn :
  comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n) ⊔ I =
    comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ) ⊔ I
y : R
hy : Membership.mem (γ := Submodule R R) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ)) y
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx :
  HMul.hMul (α := Localization.AtPrime q) (β := Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) (Submodule.IsPrincipal.generator I) : Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) z : Localization.AtPrime q) ∈
    HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n
hIN : ¬I ≤ q
⊢ Submodule.IsPrincipal.generator I ∉ (↑q : Set R)

Tactic:
rw [← Set.singleton_subset_iff, ← Ideal.span_le, Ideal.span_singleton_generator]

Premises used: Ideal.span_le, Set.singleton_subset_iff, Ideal.span_singleton_generator
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
n : ℕ
hn :
  comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n) ⊔ I =
    comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ) ⊔ I
y : R
hy : Membership.mem (γ := Submodule R R) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ)) y
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx :
  HMul.hMul (α := Localization.AtPrime q) (β := Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) (Submodule.IsPrincipal.generator I) : Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) z : Localization.AtPrime q) ∈
    HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n
⊢ ¬I ≤ q

Tactic:
fun e ↦ h₂.not_ge (hp.2 ⟨h₁, e⟩ h₂.le)

Premises used: LT.lt.le, And.right, And.intro, LT.lt.not_ge, Not
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
n : ℕ
hn :
  comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n) ⊔ I =
    comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ) ⊔ I
y : R
hy : Membership.mem (γ := Submodule R R) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ)) y
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx :
  HMul.hMul (α := Localization.AtPrime q) (β := Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) (Submodule.IsPrincipal.generator I) : Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) z : Localization.AtPrime q) ∈
    HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n
⊢ ¬I ≤ q

Tactic:
exact fun e ↦ h₂.not_ge (hp.2 ⟨h₁, e⟩ h₂.le)

Premises used: LT.lt.le, And.right, And.intro, LT.lt.not_ge
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
inst_2 : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ p.IsPrime

Tactic:
have := hp.isPrime
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
inst_2 : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
refine_2 :
  ∀ (this : height.{u_1} (R := Localization.AtPrime p) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ≤ 1),
    p.height ≤ 1
refine_1 :
  Membership.mem (γ := Set (Ideal (Localization.AtPrime p))) (Ideal.minimalPrimes (map f I))
    (IsLocalRing.maximalIdeal (Localization.AtPrime p))
⊢ p.height ≤ 1

Tactic:
have := Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing (I.map f) ?_
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
inst_2 : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this_1 : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
this : height.{u_1} (R := Localization.AtPrime p) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ≤ 1
refine_2 :
  ∀ (this : height (under R (B := Localization.AtPrime p) (IsLocalRing.maximalIdeal (Localization.AtPrime p))) ≤ 1),
    p.height ≤ 1
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : ∀ (this : p.height ≤ 1), p.height ≤ 1
⊢ p.height ≤ 1

Tactic:
rwa [← IsLocalization.height_under p.primeCompl,
      Localization.AtPrime.under_maximalIdeal] at this

Premises used: IsLocalization.height_under, Localization.AtPrime.under_maximalIdeal, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
inst_2 : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
refine_1 :
  Membership.mem (γ := Set (Ideal (Localization.AtPrime p))) (under R ⁻¹' I.minimalPrimes)
    (IsLocalRing.maximalIdeal (Localization.AtPrime p))
refine_1₁ : under R (B := Localization.AtPrime p) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ∈ I.minimalPrimes
refine_1₂ refine_1₃ refine_1₄ refine_1₅ : p ∈ I.minimalPrimes
⊢ Membership.mem (γ := Set (Ideal (Localization.AtPrime p))) (Ideal.minimalPrimes (map f I))
    (IsLocalRing.maximalIdeal (Localization.AtPrime p))

Tactic:
rwa [IsLocalization.minimalPrimes_map p.primeCompl (Localization.AtPrime p) I,
      Set.mem_preimage, Localization.AtPrime.under_maximalIdeal]

Premises used: IsLocalization.minimalPrimes_map, Localization.AtPrime, Localization.AtPrime.under_maximalIdeal, Ideal.primeCompl, Set.mem_preimage
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
x : R
hp : p ∈ (I ⊔ span {x}).minimalPrimes
⊢ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) ≤ 1

Tactic:
let f := Ideal.Quotient.mk I
  have : p.IsPrime := hp.isPrime
  have hfp : RingHom.ker f ≤ p := I.mk_ker.trans_le (le_sup_left.trans hp.le)
  height_le_one_of_isPrincipal_of_mem_minimalPrimes ((span {x}).map f) (p.map f)
    ⟨⟨map_isPrime_of_surjective Quotient.mk_surjective hfp,
      map_mono (le_sup_right.trans hp.le)⟩,
        fun _ ⟨hr, hxr⟩ hrp ↦ map_le_iff_le_comap.mpr <| hp.2 ⟨hr.comap f, sup_le_iff.mpr
          ⟨I.mk_ker.symm.trans_le <| ker_le_comap (Ideal.Quotient.mk I), le_comap_of_map_le hxr⟩⟩ <|
            (comap_mono hrp).trans <| Eq.le <|
              (p.comap_map_of_surjective _ Quotient.mk_surjective).trans <| sup_eq_left.mpr hfp⟩

Premises used: Iff.mpr, Ideal.le_comap_of_map_le, le_sup_left, Ideal.Quotient.mk, Ideal.IsMinimalPrime.le, Ideal.IsPrime.comap, Ideal.map, sup_eq_left, Eq.le, le_sup_right, Eq.trans_le, _private.0.Ideal.map_height_le_one_of_mem_minimalPrimes.match_1, LE.le, Ideal.comap_mono, Ideal.IsMinimalPrime.isPrime, Ideal.Quotient.mk_surjective, Ideal.ker_le_comap, Ideal.map_le_iff_le_comap, Ideal.comap_map_of_surjective, sup_le_iff, And.right, And.intro, Ideal.map_isPrime_of_surjective, Ideal.map_mono, Ideal.span, LE.le.trans, Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes, Ideal.mk_ker, Singleton.singleton, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
hx' : ¬IsUnit x
⊢ Ne (α := Ideal R) (span {x}) ⊤

Tactic:
simpa
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
hx' : ¬IsUnit x
obtain :
  ∀ (p : Ideal R) (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) p),
    height (R := R) (span {x}) ≤ 1
⊢ height (R := R) (span {x}) ≤ 1

Tactic:
obtain ⟨p, hp⟩ := (span {x}).nonempty_minimalPrimes (by simpa)

Premises used: Ideal.nonempty_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
hx' : ¬IsUnit x
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) p
⊢ height (R := R) (span {x}) ≤ 1

Tactic:
le_trans (height_mono hp.1.2) ?_

Premises used: Ideal.height_mono, And.right, And.left, le_trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
hx' : ¬IsUnit x
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) p
refine : p.height ≤ 1
⊢ height (R := R) (span {x}) ≤ 1

Tactic:
refine le_trans (height_mono hp.1.2) ?_

Premises used: Ideal.height_mono, And.right, And.left, le_trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
hx' : ¬IsUnit x
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) p
⊢ p.height ≤ 1

Tactic:
Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes (span {x}) _ hp

Premises used: Ideal.span, Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes, Singleton.singleton
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
hx' : ¬IsUnit x
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) p
⊢ p.height ≤ 1

Tactic:
exact Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes (span {x}) _ hp

Premises used: Ideal.span, Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes, Singleton.singleton
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
hx' : ¬IsUnit x
⊢ height (R := R) (span {x}) = 1

Tactic:
le_antisymm (height_span_singleton_le_one hx')
    (one_le_height_span_singleton_of_mem_nonZeroDivisors hx)

Premises used: Ideal.height_span_singleton_le_one, Ideal.one_le_height_span_singleton_of_mem_nonZeroDivisors, le_antisymm
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
⊢ Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)

Tactic:
have hf : Function.Surjective f := Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
⊢ span t ≤ q

Tactic:
have hI'q : span t ≤ q := span_le.mpr htq