awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_2 : ∃ (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_2 = 0
this :
  HPow.hPow (α := Ideal R) (maximalIdeal R)
      (Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this_2) ≤
    Ideal.span {a}
⊢ LE.le (α := Ideal R) ⊤ (Ideal.span {a})

Tactic:
rw [hn, pow_zero, Ideal.one_eq_top] at this

Premises used: Ideal.one_eq_top, pow_zero
-- 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_2 : ∃ (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_2 = 0
this : LE.le (α := Ideal R) ⊤ (Ideal.span {a})
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
(Ideal.IsMaximal.ne_top inferInstance (eq_top_iff.mpr <| this.trans hle)).elim

Premises used: Iff.mpr, eq_top_iff, False.elim, inferInstance, Ideal.IsMaximal.ne_top, LE.le.trans
-- 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_2 : ∃ (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_2 = 0
this : LE.le (α := Ideal R) ⊤ (Ideal.span {a})
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
exact (Ideal.IsMaximal.ne_top inferInstance (eq_top_iff.mpr <| this.trans hle)).elim

Premises used: Iff.mpr, eq_top_iff, False.elim, inferInstance, Ideal.IsMaximal.ne_top, LE.le.trans
-- 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}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
by_contra! :
  ∀
    (h' :
      ∀ (b : R) (_ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n),
        Membership.mem (γ := Ideal R) (Ideal.span {a}) b),
    False
⊢ ∃ b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n, b ∉ Ideal.span {a}

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) ⊥
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}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
h' : ∀ (b : R) (_ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n), Membership.mem (γ := Ideal R) (Ideal.span {a}) b
⊢ HPow.hPow (α := Ideal R) (maximalIdeal R) (n + 1) ≤ Ideal.span {a} ∧
    ∀ n_1 < n + 1, ¬HPow.hPow (α := Ideal R) (maximalIdeal R) n_1 ≤ Ideal.span {a}

Tactic:
rw [Nat.find_eq_iff] at hn

Premises used: Nat.find_eq_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)
this_1 : Eq (α := Ideal R) (Ideal.radical (Ideal.span {a})) (maximalIdeal R)
this : ∃ (n : ℕ), HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
h' : ∀ (b : R) (_ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n), Membership.mem (γ := Ideal R) (Ideal.span {a}) b
hn₁ :
  HPow.hPow (α := Ideal R) (maximalIdeal R) (n + 1) ≤ Ideal.span {a} ∧
    ∀ n_1 < n + 1, ¬HPow.hPow (α := Ideal R) (maximalIdeal R) n_1 ≤ Ideal.span {a}
⊢ ∀ (b : R) (_ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n), Membership.mem (γ := Ideal R) (Ideal.span {a}) b

Tactic:
rw [Nat.find_eq_iff] at hn

Premises used: Nat.find_eq_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)
this_1 : Eq (α := Ideal R) (Ideal.radical (Ideal.span {a})) (maximalIdeal R)
this : ∃ (n : ℕ), HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}
n : ℕ
hn :
  HPow.hPow (α := Ideal R) (maximalIdeal R) (n + 1) ≤ Ideal.span {a} ∧
    ∀ n_1 < n + 1, ¬HPow.hPow (α := Ideal R) (maximalIdeal R) n_1 ≤ Ideal.span {a}
h' : ∀ (b : R) (_ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n), Membership.mem (γ := Ideal R) (Ideal.span {a}) b
⊢ False

Tactic:
hn.2 n n.lt_succ_self fun x hx => h' x hx

Premises used: Nat.lt_succ_self, And.right
-- 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}
n : ℕ
hn :
  HPow.hPow (α := Ideal R) (maximalIdeal R) (n + 1) ≤ Ideal.span {a} ∧
    ∀ n_1 < n + 1, ¬HPow.hPow (α := Ideal R) (maximalIdeal R) n_1 ≤ Ideal.span {a}
h' : ∀ (b : R) (_ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n), Membership.mem (γ := Ideal R) (Ideal.span {a}) b
⊢ False

Tactic:
exact hn.2 n n.lt_succ_self fun x hx => h' x hx

Premises used: Nat.lt_succ_self, And.right
-- 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}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
neg :
  ∀ (b : R) (hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n) (hb₂ : b ∉ Ideal.span {a}),
    Submodule.IsPrincipal (maximalIdeal R)
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
obtain ⟨b, hb₁, hb₂⟩ : ∃ b ∈ maximalIdeal R ^ n, b ∉ Ideal.span {a} := by
    by_contra! h'; rw [Nat.find_eq_iff] at hn; exact hn.2 n n.lt_succ_self fun x hx => h' x hx

Premises used: IsLocalRing.maximalIdeal, Ideal.span, Singleton.singleton
-- 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}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
b : R
hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : b ∉ Ideal.span {a}
m : R
hm : Membership.mem (γ := Ideal R) (maximalIdeal R) m
rw : Membership.mem (γ := Ideal R) (Ideal.span {a}) (b * m)
⊢ ∃ (k : R), k * a = b * m

Tactic:
rw [← Ideal.mem_span_singleton']

Premises used: Ideal.mem_span_singleton'
-- 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}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
b : R
hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : b ∉ Ideal.span {a}
m : R
hm : Membership.mem (γ := Ideal R) (maximalIdeal R) m
a₁ :
  b * m ∈
    HPow.hPow (α := Ideal R) (maximalIdeal R)
      (Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this)
⊢ Membership.mem (γ := Ideal R) (Ideal.span {a}) (b * m)

Tactic:
apply 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
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}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
b : R
hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : b ∉ Ideal.span {a}
m : R
hm : Membership.mem (γ := Ideal R) (maximalIdeal R) m
a₁ : b * m ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n * maximalIdeal R
⊢ b * m ∈
    HPow.hPow (α := Ideal R) (maximalIdeal R)
      (Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this)

Tactic:
rw [hn, pow_succ]

Premises used: pow_succ
-- 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}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
b : R
hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : b ∉ Ideal.span {a}
m : R
hm : Membership.mem (γ := Ideal R) (maximalIdeal R) m
⊢ b * m ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n * maximalIdeal R

Tactic:
Ideal.mul_mem_mul hb₁ hm

Premises used: Set.Mem, Ideal.mul_mem_mul
-- 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}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
b : R
hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : b ∉ Ideal.span {a}
m : R
hm : Membership.mem (γ := Ideal R) (maximalIdeal R) m
⊢ b * m ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n * maximalIdeal R

Tactic:
exact Ideal.mul_mem_mul hb₁ hm

Premises used: Ideal.mul_mem_mul
-- 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}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
b : R
hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : b ∉ Ideal.span {a}
⊢ ∀ (m : R), Membership.mem (γ := Ideal R) (maximalIdeal R) m → ∃ (k : R), k * a = b * m

Tactic:
have hb₃ : ∀ m ∈ maximalIdeal R, ∃ k : R, k * a = b * m := by
    intro m hm; rw [← Ideal.mem_span_singleton']; apply Nat.find_spec this
    rw [hn, pow_succ]; exact Ideal.mul_mem_mul hb₁ hm
-- 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}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
hb₁ : 0 ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : 0 ∉ Ideal.span {a}
hb₃ : ∀ (m : R), Membership.mem (γ := Ideal R) (maximalIdeal R) m → ∃ (k : R), k * a = 0 * m
apply : Membership.mem (γ := Ideal R) (Ideal.span {a}) 0
⊢ False

Tactic:
apply hb₂
-- 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}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
hb₁ : 0 ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : 0 ∉ Ideal.span {a}
hb₃ : ∀ (m : R), Membership.mem (γ := Ideal R) (maximalIdeal R) m → ∃ (k : R), k * a = 0 * m
⊢ Membership.mem (γ := Ideal R) (Ideal.span {a}) 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- 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}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
hb₁ : 0 ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : 0 ∉ Ideal.span {a}
hb₃ : ∀ (m : R), Membership.mem (γ := Ideal R) (maximalIdeal R) m → ∃ (k : R), k * a = 0 * m
⊢ Membership.mem (γ := Ideal R) (Ideal.span {a}) 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- 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}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
b : R
hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ (m : R), Membership.mem (γ := Ideal R) (maximalIdeal R) m → ∃ (k : R), k * a = b * m
⊢ b ≠ 0

Tactic:
have hb₄ : b ≠ 0 := by rintro rfl; apply hb₂; exact zero_mem _
-- 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}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
b : R
hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ (m : R), Membership.mem (γ := Ideal R) (maximalIdeal R) m → ∃ (k : R), k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
⊢ Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)

Tactic:
have ha₃ : algebraMap R K a ≠ 0 := IsFractionRing.to_map_eq_zero_iff.not.mpr ha₂
-- 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}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
b : R
hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ (m : R), Membership.mem (γ := Ideal R) (maximalIdeal R) m → ∃ (k : R), k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
pos : ∀ (hx : ∀ y ∈ M, x * y ∈ M), Submodule.IsPrincipal (maximalIdeal R)
neg : ∀ (hx : ¬∀ y ∈ M, x * y ∈ M), Submodule.IsPrincipal (maximalIdeal R)
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
by_cases hx : ∀ y ∈ M, x * y ∈ M
-- 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}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1
b : R
hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ (m : R), Membership.mem (γ := Ideal R) (maximalIdeal R) m → ∃ (k : R), k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
hx : ∀ y ∈ M, x * y ∈ M
pos : ∀ (this : IsIntegral R x), Submodule.IsPrincipal (maximalIdeal R)
pos₁ : M ≠ ⊥
pos₂ : M.FG
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
have := isIntegral_of_smul_mem_submodule M ?_ ?_ x hx
-- 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_2 : ∃ (n : ℕ), HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this_2 = n + 1
b : R
hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ (m : R), Membership.mem (γ := Ideal R) (maximalIdeal R) m → ∃ (k : R), k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
hx : ∀ y ∈ M, x * y ∈ M
this : IsIntegral R x
pos : ∀ (y : R) (e : (algebraMap R K : (a : R) → K) y = x), Submodule.IsPrincipal (maximalIdeal R)
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
obtain ⟨y, e⟩ := IsIntegrallyClosed.algebraMap_eq_of_integral this

Premises used: IsIntegrallyClosed.algebraMap_eq_of_integral
-- 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_2 : ∃ (n : ℕ), HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this_2 = n + 1
b : R
hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ (m : R), Membership.mem (γ := Ideal R) (maximalIdeal R) m → ∃ (k : R), k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
hx : ∀ y ∈ M, x * y ∈ M
this : IsIntegral R x
y : R
e : (algebraMap R K : (a : R) → K) y = x
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
(hb₂ (Ideal.mem_span_singleton'.mpr ⟨y, ?_⟩)).elim

Premises used: Iff.mpr, Ideal.mem_span_singleton', False.elim, Exists.intro