awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x y : R
hy : x = ϖ * y
h₁ : ϖ ∣ x
⊢ x ∈ I

Tactic:
rw [hI, Ideal.mem_span_singleton]

Premises used: Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x y : R
hy : x = ϖ * y
⊢ ϖ ∣ x

Tactic:
⟨y, hy⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x y : R
hy : x = ϖ * y
⊢ ϖ ∣ x

Tactic:
exact ⟨y, hy⟩
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)
contrapose : ∀ (h' : ϖ = 0), I = ⊥
⊢ ϖ ≠ 0

Tactic:
contrapose h'
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)
h' : ϖ = 0
rw : Eq (α := Ideal R) (span {ϖ}) ⊥
rw₁ : Eq (α := Ideal R) (span {0}) ⊥
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ I = ⊥

Tactic:
rw [hI, h', Ideal.span_singleton_eq_bot]

Premises used: Ideal.span_singleton_eq_bot
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
⊢ I = (f ∘ₗ g).ker

Tactic:
have : I = LinearMap.ker (f.comp g) := by
    ext x
    simp only [LinearMap.codRestrict, LinearMap.pow_mulRight, LinearMap.mulRight_apply,
      LinearMap.mem_ker, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
      Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero, Submodule.mem_smul_top_iff, smul_eq_mul,
      f, g]
    constructor <;> intro hx
    · exact Submodule.mul_mem_mul hx hϖ
    · rw [← pow_succ', hI, Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hx
      obtain ⟨y, hy⟩ := hx
      rw [mul_comm, pow_succ, mul_assoc, mul_right_inj' (pow_ne_zero _ _)] at hy
      · rw [hI, Ideal.mem_span_singleton]
        exact ⟨y, hy⟩
      · contrapose h'
        rw [hI, h', Ideal.span_singleton_eq_bot]
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
refine :
  Function.Surjective (α := R) (β := ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤)
    (⇑(f ∘ₗ g) : (a : R) → ↥(I ^ n) ⧸ I • ⊤)
⊢ (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤

Tactic:
refine e.trans ((f.comp g).quotKerEquivOfSurjective ?_)

Premises used: LinearMap.comp, LinearMap.quotKerEquivOfSurjective, LinearEquiv.trans
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
⊢ Function.Surjective (α := R) (β := ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤)
    (⇑(f ∘ₗ g) : (a : R) → ↥(I ^ n) ⧸ I • ⊤)

Tactic:
(Submodule.mkQ_surjective _).comp ?_

Premises used: Submodule.Quotient.mk, Function.Surjective.comp, Submodule.mkQ_surjective
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
refine : Function.Surjective (α := R) (β := ↥(I ^ n)) (⇑g : (a : R) → ↥(I ^ n))
⊢ Function.Surjective (α := R) (β := ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤)
    (⇑(f ∘ₗ g) : (a : R) → ↥(I ^ n) ⧸ I • ⊤)

Tactic:
refine (Submodule.mkQ_surjective _).comp ?_

Premises used: Function.Surjective.comp, Submodule.mkQ_surjective
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
x : R
hx : x ∈ I ^ n
⊢ ϖ ^ n ∣ x

Tactic:
rw [hI, Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hx

Premises used: Ideal.mem_span_singleton, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
x : R
hx_1 : x ∈ I ^ n
hx : ϖ ^ n ∣ x
⊢ ∃ (a : R), (g : (a : R) → ↥(I ^ n)) a = Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) x hx_1

Tactic:
hx.imp ?_

Premises used: Exists.imp
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
x : R
hx_1 : x ∈ I ^ n
hx : ϖ ^ n ∣ x
refine : ∀ (a : R), x = ϖ ^ n * a → (g : (a : R) → ↥(I ^ n)) a = Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) x hx_1
⊢ ∃ (a : R), (g : (a : R) → ↥(I ^ n)) a = Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) x hx_1

Tactic:
refine hx.imp ?_

Premises used: Exists.imp
-- Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤ :=
  (HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mkQ
ϖ : R := ⋯.choose (p := fun (a : R) ↦ I = R ∙ a)
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (HPow.hPow (α := R →ₗ[R] R) (LinearMap.mulRight R ϖ) n) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
x : R
hx_1 : x ∈ I ^ n
hx : ϖ ^ n ∣ x
⊢ ∀ (a : R), x = ϖ ^ n * a → (g : (a : R) → ↥(I ^ n)) a = Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) x hx_1

Tactic:
simp [g, LinearMap.codRestrict, eq_comm, mul_comm]

Premises used: eq_comm, mul_comm, LinearMap.codRestrict
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
hp : maximalIdeal R ∈ I.minimalPrimes
J : Ideal (R ⧸ I)
prime : J.IsPrime
⊢ Ideal.IsMaximal (maximalIdeal R)

Tactic:
IsLocalRing.maximalIdeal.isMaximal R

Premises used: IsLocalRing.maximalIdeal.isMaximal
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
hp : maximalIdeal R ∈ I.minimalPrimes
J : Ideal (R ⧸ I)
prime : J.IsPrime
h : Eq (α := Ideal R) (Ideal.comap (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) J) (maximalIdeal R)
⊢ Ideal.IsMaximal (Ideal.comap (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) J)

Tactic:
convert! IsLocalRing.maximalIdeal.isMaximal R

Premises used: IsLocalRing.maximalIdeal.isMaximal
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
hp : maximalIdeal R ∈ I.minimalPrimes
J : Ideal (R ⧸ I)
prime : J.IsPrime
h :
  ∀ (hp : I.IsMinimalPrime (maximalIdeal R)) (J : Ideal (R ⧸ I)) (prime : J.IsPrime),
    Eq (α := Ideal R) (Ideal.comap (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) J) (maximalIdeal R)
⊢ Eq (α := Ideal R) (Ideal.comap (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) J) (maximalIdeal R)

Tactic:
rw [Ideal.minimalPrimes, Set.mem_setOf] at hp

Premises used: Ideal.minimalPrimes, Set.mem_setOf
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
hp_1 : maximalIdeal R ∈ I.minimalPrimes
hp : I.IsMinimalPrime (maximalIdeal R)
J : Ideal (R ⧸ I)
prime : J.IsPrime
⊢ Ideal.IsPrime (Ideal.comap (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)

Tactic:
have := prime.comap (Ideal.Quotient.mk I)
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
hp_1 : maximalIdeal R ∈ I.minimalPrimes
hp : I.IsMinimalPrime (maximalIdeal R)
J : Ideal (R ⧸ I)
prime : J.IsPrime
this : Ideal.IsPrime (Ideal.comap (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)
⊢ I ≤ RingHom.ker (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I))

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
hp_1 : maximalIdeal R ∈ I.minimalPrimes
hp : I.IsMinimalPrime (maximalIdeal R)
J : Ideal (R ⧸ I)
prime : J.IsPrime
this : Ideal.IsPrime (Ideal.comap (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) J)
⊢ Eq (α := Ideal R) (Ideal.comap (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) J) (maximalIdeal R)

Tactic:
exact hp.eq_of_le ⟨this, .trans (by simp) (Ideal.ker_le_comap _)⟩ (le_maximalIdeal this.1)

Premises used: Ideal.ker_le_comap, Minimal.eq_of_le, And.intro, IsLocalRing.le_maximalIdeal, LE.le.trans, Ideal.IsPrime.ne_top'
-- 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
⊢ height (IsLocalRing.maximalIdeal R) ≤ 1

Tactic:
Ideal.height_le_iff.mpr fun q h₁ h₂ ↦ ?_

Premises used: Iff.mpr, Ideal.height_le_iff, WithTop.some
-- 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
refine : ∀ (q : Ideal R) (h₁ : q.IsPrime) (h₂ : q < IsLocalRing.maximalIdeal R), q.height < (↑1 : ℕ∞)
⊢ height (IsLocalRing.maximalIdeal R) ≤ 1

Tactic:
refine Ideal.height_le_iff.mpr fun q h₁ h₂ ↦ ?_

Premises used: Iff.mpr, Ideal.height_le_iff
-- 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 : q.height = 0
rw : LT.lt (α := ℕ∞) 0 (↑1 : ℕ∞)
⊢ q.height < (↑1 : ℕ∞)

Tactic:
rw [this]
-- 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 : q.height = 0
⊢ LT.lt (α := ℕ∞) 0 (↑1 : ℕ∞)

Tactic:
zero_lt_one

Premises used: WithTop.some, zero_lt_one
-- 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 : q.height = 0
⊢ LT.lt (α := ℕ∞) 0 (↑1 : ℕ∞)

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- 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
suffices : q.height = 0
⊢ q.height < (↑1 : ℕ∞)

Tactic:
suffices q.height = 0 by rw [this]; exact zero_lt_one
-- 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
rw :
  IsNilpotent (R := Ideal (Localization.AtPrime q))
    (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q)
⊢ q.height = 0

Tactic:
rw [← WithBot.coe_inj,
    ← IsLocalization.AtPrime.ringKrullDim_eq_height q (Localization.AtPrime q),
    WithBot.coe_zero, ← ringKrullDimZero_iff_ringKrullDim_eq_zero,
    ← isArtinianRing_iff_krullDimLE_zero, isArtinianRing_iff_isNilpotent_maximalIdeal,
    ← Localization.AtPrime.map_eq_maximalIdeal]

Premises used: Localization.AtPrime, ringKrullDimZero_iff_ringKrullDim_eq_zero, IsLocalization.AtPrime.ringKrullDim_eq_height, isArtinianRing_iff_isNilpotent_maximalIdeal, WithBot.coe_inj, Localization.AtPrime.map_eq_maximalIdeal, isArtinianRing_iff_krullDimLE_zero, WithBot.coe_zero
-- 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
⊢ IsArtinianRing.{u_1} (R ⧸ I)

Tactic:
have : IsArtinianRing (R ⧸ I) :=
    IsLocalRing.quotient_artinian_of_mem_minimalPrimes_of_isLocalRing I hp
-- 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' := ⋯ }
obtain :
  ∀ (n : ℕ)
    (hn :
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
            ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
            ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) m : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)),
    IsNilpotent (R := Ideal (Localization.AtPrime q))
      (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q)
⊢ IsNilpotent (R := Ideal (Localization.AtPrime q))
    (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q)

Tactic:
obtain ⟨n, hn⟩ := IsArtinian.monotone_stabilizes qs

Premises used: IsArtinian.monotone_stabilizes
-- 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 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) m : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
⊢ IsNilpotent (R := Ideal (Localization.AtPrime q))
    (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q)

Tactic:
⟨n, ?_⟩

Premises used: Exists.intro, IsNilpotent
-- 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 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) m : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
refine :
  HPow.hPow (α := Ideal (Localization.AtPrime q))
      (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n =
    0
⊢ IsNilpotent (R := Ideal (Localization.AtPrime q))
    (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q)

Tactic:
refine ⟨n, ?_⟩
-- 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 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) m : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
hIN :
  HPow.hPow (α := Ideal (Localization.AtPrime q))
      (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n ≤
    HSMul.hSMul (α := Ideal (Localization.AtPrime q)) (map f q)
      (HPow.hPow (α := Ideal (Localization.AtPrime q))
        (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n)
hIjac : LE.le (α := Ideal (Localization.AtPrime q)) (map f q) (jacobson ⊥)
⊢ HPow.hPow (α := Ideal (Localization.AtPrime q))
      (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n =
    0

Tactic:
apply Submodule.eq_bot_of_le_smul_of_le_jacobson_bot (q.map f) _ (IsNoetherian.noetherian _)

Premises used: Ideal.map, IsNoetherian.noetherian, Submodule.eq_bot_of_le_smul_of_le_jacobson_bot
-- 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 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) m : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
hIjac : Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime q)) ⊥ ⊤
⊢ LE.le (α := Ideal (Localization.AtPrime q)) (map f q) (jacobson ⊥)

Tactic:
rw [IsLocalRing.jacobson_eq_maximalIdeal, Localization.AtPrime.map_eq_maximalIdeal]

Premises used: IsLocalRing.jacobson_eq_maximalIdeal, Localization.AtPrime.map_eq_maximalIdeal