awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this_1 : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ (n : ℕ), Associated (x ^ n) r
this : ∃ (n : ℕ), x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : s ∉ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)
hs₃ : s = 0
pos : 0 ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)
⊢ s ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)

Tactic:
rw [hs₃]
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this_1 : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ (n : ℕ), Associated (x ^ n) r
this : ∃ (n : ℕ), x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : s ∉ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)
hs₃ : s = 0
⊢ 0 ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this_1 : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ (n : ℕ), Associated (x ^ n) r
this : ∃ (n : ℕ), x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : s ∉ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)
hs₃ : s = 0
⊢ 0 ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this_1 : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ (n : ℕ), Associated (x ^ n) r
this : ∃ (n : ℕ), x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : s ∉ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)
hs₃ : ¬s = 0
neg :
  ∀ (n : ℕ) (u : Rˣ) (hs₁ : x ^ n * (↑u : R) ∈ I)
    (hs₂ : x ^ n * (↑u : R) ∉ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this))
    (hs₃ : ¬x ^ n * (↑u : R) = 0),
    x ^ n * (↑u : R) ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)
⊢ s ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)

Tactic:
obtain ⟨n, u, rfl⟩ := H' s hs₃ (le_maximalIdeal hI' hs₁)

Premises used: IsLocalRing.le_maximalIdeal, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this_1 : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ (n : ℕ), Associated (x ^ n) r
this : ∃ (n : ℕ), x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n * (↑u : R) ∈ I
hs₂ : x ^ n * (↑u : R) ∉ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)
hs₃ : ¬x ^ n * (↑u : R) = 0
neg :
  ∀ (hs₁ : x ^ n ∈ I)
    (hs₂ : x ^ n * (↑u : R) ∉ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this))
    (hs₃ : ¬x ^ n * (↑u : R) = 0),
    x ^ n ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)
⊢ x ^ n * (↑u : R) ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)

Tactic:
rw [mul_comm, Ideal.unit_mul_mem_iff_mem _ u.isUnit] at hs₁ ⊢

Premises used: Ideal.unit_mul_mem_iff_mem, mul_comm, Units.isUnit
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this_1 : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ (n : ℕ), Associated (x ^ n) r
this : ∃ (n : ℕ), x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n ∈ I
hs₂ : x ^ n * (↑u : R) ∉ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)
hs₃ : ¬x ^ n * (↑u : R) = 0
neg : x ^ n ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
⊢ x ^ n ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)

Tactic:
apply Ideal.pow_le_pow_right (Nat.find_min' this hs₁)

Premises used: Ideal.pow_le_pow_right, Nat.find_min'
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this_1 : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ (n : ℕ), Associated (x ^ n) r
this : ∃ (n : ℕ), x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n ∈ I
hs₂ : x ^ n * (↑u : R) ∉ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)
hs₃ : ¬x ^ n * (↑u : R) = 0
neg : Membership.mem (γ := Ideal R) (maximalIdeal R) x
⊢ x ^ n ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n

Tactic:
apply Ideal.pow_mem_pow

Premises used: Ideal.pow_mem_pow
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this_1 : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ (n : ℕ), Associated (x ^ n) r
this : ∃ (n : ℕ), x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n ∈ I
hs₂ : x ^ n * (↑u : R) ∉ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)
hs₃ : ¬x ^ n * (↑u : R) = 0
⊢ Membership.mem (γ := Ideal R) (maximalIdeal R) x

Tactic:
(H _).mpr (dvd_refl _)

Premises used: Iff.mpr, Set.Mem, setOf, nonunits, dvd_refl, Not
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this_1 : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ (n : ℕ), Associated (x ^ n) r
this : ∃ (n : ℕ), x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n ∈ I
hs₂ : x ^ n * (↑u : R) ∉ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this)
hs₃ : ¬x ^ n * (↑u : R) = 0
⊢ Membership.mem (γ := Ideal R) (maximalIdeal R) x

Tactic:
exact (H _).mpr (dvd_refl _)

Premises used: Iff.mpr, dvd_refl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this_1 : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ (n : ℕ), Associated (x ^ n) r
this : ∃ (n : ℕ), x ^ n ∈ I
h₁ : x ^ Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this ∈ (↑I : Set R)
⊢ HPow.hPow (α := Ideal R) (maximalIdeal R) (Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this) ≤ I

Tactic:
rw [hx, Ideal.span_singleton_pow, Ideal.span_le, Set.singleton_subset_iff]

Premises used: Ideal.span_le, Set.singleton_subset_iff, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this_1 : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ (n : ℕ), Associated (x ^ n) r
this : ∃ (n : ℕ), x ^ n ∈ I
⊢ x ^ Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this ∈ (↑I : Set R)

Tactic:
Nat.find_spec this

Premises used: Nat.find_spec
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this_1 : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ (n : ℕ), Associated (x ^ n) r
this : ∃ (n : ℕ), x ^ n ∈ I
⊢ x ^ Nat.find (p := fun (n : ℕ) ↦ x ^ n ∈ I) this ∈ (↑I : Set R)

Tactic:
exact Nat.find_spec this

Premises used: Nat.find_spec
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
pos : ∀ (ne_bot : Eq (α := Ideal R) (maximalIdeal R) ⊥), Submodule.IsPrincipal (maximalIdeal R)
neg : ∀ (ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥), Submodule.IsPrincipal (maximalIdeal R)
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
by_cases ne_bot : maximalIdeal R = ⊥

Premises used: IsLocalRing.maximalIdeal
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : Eq (α := Ideal R) (maximalIdeal R) ⊥
pos : Submodule.IsPrincipal.{u_1, u_1} (R := R) (M := R) ⊥
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
rw [ne_bot]
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : Eq (α := Ideal R) (maximalIdeal R) ⊥
⊢ Submodule.IsPrincipal.{u_1, u_1} (R := R) (M := R) ⊥

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
by_contra! : ∀ (h' : ∀ (a : R) (_ : Membership.mem (γ := Ideal R) (maximalIdeal R) a), a = 0), False
⊢ ∃ (a : R), Membership.mem (γ := Ideal R) (maximalIdeal R) a ∧ a ≠ 0

Tactic:
by_contra! h'
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
h' : ∀ (a : R) (_ : Membership.mem (γ := Ideal R) (maximalIdeal R) a), a = 0
apply : Eq (α := Ideal R) (maximalIdeal R) ⊥
⊢ False

Tactic:
apply ne_bot
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
h' : ∀ (a : R) (_ : Membership.mem (γ := Ideal R) (maximalIdeal R) a), a = 0
rwa rwa₁ rwa₂ rwa₃ : LE.le (α := Ideal R) (maximalIdeal R) ⊥
⊢ Eq (α := Ideal R) (maximalIdeal R) ⊥

Tactic:
rwa [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
neg :
  ∀ (a : R) (ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a) (ha₂ : a ≠ 0),
    Submodule.IsPrincipal (maximalIdeal R)
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
obtain ⟨a, ha₁, ha₂⟩ : ∃ a ∈ maximalIdeal R, a ≠ (0 : R) := by
    by_contra! h'; apply ne_bot; rwa [eq_bot_iff]

Premises used: IsLocalRing.maximalIdeal, OfNat.ofNat
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
rwa : {a} ⊆ (↑(maximalIdeal R) : Set R)
rwa₁ rwa₂ rwa₃ rwa₄ : a ∈ (↑(maximalIdeal R) : Set R)
⊢ LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)

Tactic:
rwa [Ideal.span_le, Set.singleton_subset_iff]

Premises used: Ideal.span_le, Set.singleton_subset_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
⊢ LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)

Tactic:
have hle : Ideal.span {a} ≤ maximalIdeal R := by rwa [Ideal.span_le, Set.singleton_subset_iff]
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
rw : Eq (α := Ideal R) (sInf {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime}) (maximalIdeal R)
⊢ Eq (α := Ideal R) (Ideal.radical (Ideal.span {a})) (maximalIdeal R)

Tactic:
rw [Ideal.radical_eq_sInf]

Premises used: Ideal.radical_eq_sInf
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
a₁ : LE.le (α := Ideal R) (sInf {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime}) (maximalIdeal R)
a₂ : LE.le (α := Ideal R) (maximalIdeal R) (sInf {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime})
⊢ Eq (α := Ideal R) (sInf {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime}) (maximalIdeal R)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
⊢ LE.le (α := Ideal R) (sInf {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime}) (maximalIdeal R)

Tactic:
sInf_le ⟨hle, inferInstance⟩

Premises used: Set.Mem, inferInstance, sInf_le, And.intro
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
⊢ LE.le (α := Ideal R) (sInf {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime}) (maximalIdeal R)

Tactic:
exact sInf_le ⟨hle, inferInstance⟩
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
⊢ LE.le (α := Ideal R) (maximalIdeal R) (sInf {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime})

Tactic:
le_sInf fun I hI =>
          (eq_maximalIdeal <| hI.2.isMaximal (fun e => ha₂ ?_)).ge

Premises used: Eq.ge, Set.Mem, Ideal.IsPrime.isMaximal, And.right, le_sInf, IsLocalRing.eq_maximalIdeal
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
a₁ :
  ∀ (I : Ideal R) (hI : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime} I)
    (e : I = ⊥), a = 0
⊢ LE.le (α := Ideal R) (maximalIdeal R) (sInf {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime})

Tactic:
refine
        le_sInf fun I hI =>
          (eq_maximalIdeal <| hI.2.isMaximal (fun e => ha₂ ?_)).ge

Premises used: Eq.ge, le_sInf, IsLocalRing.eq_maximalIdeal
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
I : Ideal R
hI : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime} I
e : I = ⊥
a₁ : Ideal.span {a} ≤ I
⊢ a = 0

Tactic:
rw [← Ideal.span_singleton_eq_bot, eq_bot_iff, ← e]

Premises used: Ideal.span_singleton_eq_bot, eq_bot_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
I : Ideal R
hI : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime} I
e : I = ⊥
⊢ Ideal.span {a} ≤ I

Tactic:
hI.1

Premises used: And.left
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
I : Ideal R
hI : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime} I
e : I = ⊥
⊢ Ideal.span {a} ≤ I

Tactic:
exact hI.1

Premises used: And.left
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
⊢ Eq (α := Ideal R) (Ideal.radical (Ideal.span {a})) (maximalIdeal R)

Tactic:
have : (Ideal.span {a}).radical = maximalIdeal R := by
    rw [Ideal.radical_eq_sInf]
    apply le_antisymm
    · exact sInf_le ⟨hle, inferInstance⟩
    · refine
        le_sInf fun I hI =>
          (eq_maximalIdeal <| hI.2.isMaximal (fun e => ha₂ ?_)).ge
      rw [← Ideal.span_singleton_eq_bot, eq_bot_iff, ← e]; exact hI.1
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
this : Eq (α := Ideal R) (Ideal.radical (Ideal.span {a})) (maximalIdeal R)
rw : ∃ (n : ℕ), HPow.hPow (α := Ideal R) (Ideal.radical (Ideal.span {a})) n ≤ Ideal.span {a}
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}

Tactic:
rw [← this]
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
this : Eq (α := Ideal R) (Ideal.radical (Ideal.span {a})) (maximalIdeal R)
h : Ideal.FG (R := R) (Ideal.radical (Ideal.span {a}))
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) (Ideal.radical (Ideal.span {a})) n ≤ Ideal.span {a}

Tactic:
apply Ideal.exists_radical_pow_le_of_fg

Premises used: Ideal.exists_radical_pow_le_of_fg
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
this : Eq (α := Ideal R) (Ideal.radical (Ideal.span {a})) (maximalIdeal R)
⊢ Ideal.FG (R := R) (Ideal.radical (Ideal.span {a}))

Tactic:
IsNoetherian.noetherian _

Premises used: IsNoetherian.noetherian, Submodule.FG, Ideal.FG
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
this : Eq (α := Ideal R) (Ideal.radical (Ideal.span {a})) (maximalIdeal R)
⊢ Ideal.FG (R := R) (Ideal.radical (Ideal.span {a}))

Tactic:
exact IsNoetherian.noetherian _

Premises used: IsNoetherian.noetherian
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
this : Eq (α := Ideal R) (Ideal.radical (Ideal.span {a})) (maximalIdeal R)
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}

Tactic:
have : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a} := by
    rw [← this]; apply Ideal.exists_radical_pow_le_of_fg; exact IsNoetherian.noetherian _
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
this_1 : Eq (α := Ideal R) (Ideal.radical (Ideal.span {a})) (maximalIdeal R)
this : ∃ (n : ℕ), HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}
neg :
  ∀ (hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = 0),
    Submodule.IsPrincipal (maximalIdeal R)
neg₁ :
  ∀ (n : ℕ)
    (hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1),
    Submodule.IsPrincipal (maximalIdeal R)
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
rcases hn : Nat.find this with - | n

Premises used: Nat.find
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
a : R
ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a
ha₂ : a ≠ 0
hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
this_1 : Eq (α := Ideal R) (Ideal.radical (Ideal.span {a})) (maximalIdeal R)
this : ∃ (n : ℕ), HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = 0
⊢ HPow.hPow (α := Ideal R) (maximalIdeal R)
      (Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this) ≤
    Ideal.span {a}

Tactic:
have := Nat.find_spec this