awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
h' : Submodule.IsPrincipal (maximalIdeal R)
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
neg :
  ∀ (x : R) (hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})),
    ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
pos :
  ∀ (x : R) (hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})) (hI' : I = ⊤),
    ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
⊢ ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
have neg₁ : ∀ (x : R) (hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})) (hI' : ¬I = ⊤),
  ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
Tactic: classical
  obtain ⟨x, hx : _ = Ideal.span _⟩ := h'
  by_cases hI' : I = ⊤
  · use 0; rw [pow_zero, hI', Ideal.one_eq_top]
  have H : ∀ r : R, ¬IsUnit r ↔ x ∣ r := fun r =>
    (SetLike.ext_iff.mp hx r).trans Ideal.mem_span_singleton
  have : x ≠ 0 := by
    rintro rfl
    apply Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal R) h
    simp [hx]
  have hx' := IsDiscreteValuationRing.irreducible_of_span_eq_maximalIdeal x this hx
  have H' : ∀ r : R, r ≠ 0 → r ∈ nonunits R → ∃ n : ℕ, Associated (x ^ n) r := by
    intro r hr₁ hr₂
    obtain ⟨f, hf₁, rfl, hf₂⟩ := (WfDvdMonoid.not_unit_iff_exists_factors_eq r hr₁).mp hr₂
    have : ∀ b ∈ f, Associated x b := by
      intro b hb
      exact Irreducible.associated_of_dvd hx' (hf₁ b hb) ((H b).mp (hf₁ b hb).1)
    clear hr₁ hr₂ hf₁
    induction f using Multiset.induction with
    | empty => exact (hf₂ rfl).elim
    | cons fa fs fh => ?_
    rcases eq_or_ne fs ∅ with (rfl | hf')
    · use 1
      rw [pow_one, Multiset.prod_cons, Multiset.empty_eq_zero, Multiset.prod_zero, mul_one]
      exact this _ (Multiset.mem_cons_self _ _)
    · obtain ⟨n, hn⟩ := fh hf' fun b hb => this _ (Multiset.mem_cons_of_mem hb)
      use n + 1
      rw [pow_add, Multiset.prod_cons, mul_comm, pow_one]
      exact Associated.mul_mul (this _ (Multiset.mem_cons_self _ _)) hn
  have : ∃ n : ℕ, x ^ n ∈ I := by
    obtain ⟨r, hr₁, hr₂⟩ : ∃ r : R, r ∈ I ∧ r ≠ 0 := by
      by_contra! h; apply hI; rw [eq_bot_iff]; exact h
    obtain ⟨n, u, rfl⟩ := H' r hr₂ (le_maximalIdeal hI' hr₁)
    use n
    rwa [← I.unit_mul_mem_iff_mem u.isUnit, mul_comm]
  use Nat.find this
  apply le_antisymm
  · change ∀ s ∈ I, s ∈ _
    by_contra! ⟨s, hs₁, hs₂⟩
    apply hs₂
    by_cases hs₃ : s = 0; · rw [hs₃]; exact zero_mem _
    obtain ⟨n, u, rfl⟩ := H' s hs₃ (le_maximalIdeal hI' hs₁)
    rw [mul_comm, Ideal.unit_mul_mem_iff_mem _ u.isUnit] at hs₁ ⊢
    apply Ideal.pow_le_pow_right (Nat.find_min' this hs₁)
    apply Ideal.pow_mem_pow
    exact (H _).mpr (dvd_refl _)
  · rw [hx, Ideal.span_singleton_pow, Ideal.span_le, Set.singleton_subset_iff]
    exact Nat.find_spec this
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
inst_3 : IsDomain R
h' : Submodule.IsPrincipal (maximalIdeal R)
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
neg :
  ∀ (x : R) (hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})),
    ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
pos :
  ∀ (x : R) (hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})) (hI' : I = ⊤),
    ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
neg₁ neg₂ :
  ∀ (x : R) (hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})) (hI' : ¬I = ⊤),
    ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
⊢ ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
have neg₃ : ∀ (x : R) (hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {x})) (hI' : ¬I = ⊤) (H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r),
  ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
Tactic: classical
  obtain ⟨x, hx : _ = Ideal.span _⟩ := h'
  by_cases hI' : I = ⊤
  · use 0; rw [pow_zero, hI', Ideal.one_eq_top]
  have H : ∀ r : R, ¬IsUnit r ↔ x ∣ r := fun r =>
    (SetLike.ext_iff.mp hx r).trans Ideal.mem_span_singleton
  have : x ≠ 0 := by
    rintro rfl
    apply Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal R) h
    simp [hx]
  have hx' := IsDiscreteValuationRing.irreducible_of_span_eq_maximalIdeal x this hx
  have H' : ∀ r : R, r ≠ 0 → r ∈ nonunits R → ∃ n : ℕ, Associated (x ^ n) r := by
    intro r hr₁ hr₂
    obtain ⟨f, hf₁, rfl, hf₂⟩ := (WfDvdMonoid.not_unit_iff_exists_factors_eq r hr₁).mp hr₂
    have : ∀ b ∈ f, Associated x b := by
      intro b hb
      exact Irreducible.associated_of_dvd hx' (hf₁ b hb) ((H b).mp (hf₁ b hb).1)
    clear hr₁ hr₂ hf₁
    induction f using Multiset.induction with
    | empty => exact (hf₂ rfl).elim
    | cons fa fs fh => ?_
    rcases eq_or_ne fs ∅ with (rfl | hf')
    · use 1
      rw [pow_one, Multiset.prod_cons, Multiset.empty_eq_zero, Multiset.prod_zero, mul_one]
      exact this _ (Multiset.mem_cons_self _ _)
    · obtain ⟨n, hn⟩ := fh hf' fun b hb => this _ (Multiset.mem_cons_of_mem hb)
      use n + 1
      rw [pow_add, Multiset.prod_cons, mul_comm, pow_one]
      exact Associated.mul_mul (this _ (Multiset.mem_cons_self _ _)) hn
  have : ∃ n : ℕ, x ^ n ∈ I := by
    obtain ⟨r, hr₁, hr₂⟩ : ∃ r : R, r ∈ I ∧ r ≠ 0 := by
      by_contra! h; apply hI; rw [eq_bot_iff]; exact h
    obtain ⟨n, u, rfl⟩ := H' r hr₂ (le_maximalIdeal hI' hr₁)
    use n
    rwa [← I.unit_mul_mem_iff_mem u.isUnit, mul_comm]
  use Nat.find this
  apply le_antisymm
  · change ∀ s ∈ I, s ∈ _
    by_contra! ⟨s, hs₁, hs₂⟩
    apply hs₂
    by_cases hs₃ : s = 0; · rw [hs₃]; exact zero_mem _
    obtain ⟨n, u, rfl⟩ := H' s hs₃ (le_maximalIdeal hI' hs₁)
    rw [mul_comm, Ideal.unit_mul_mem_iff_mem _ u.isUnit] at hs₁ ⊢
    apply Ideal.pow_le_pow_right (Nat.find_min' this hs₁)
    apply Ideal.pow_mem_pow
    exact (H _).mpr (dvd_refl _)
  · rw [hx, Ideal.span_singleton_pow, Ideal.span_le, Set.singleton_subset_iff]
    exact Nat.find_spec this
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
⊢ Submodule.IsPrincipal (maximalIdeal R)
have pos : ∀ (ne_bot : Eq (α := Ideal R) (maximalIdeal R) ⊥), Submodule.IsPrincipal (maximalIdeal R)
Tactic: by_cases ne_bot : maximalIdeal R = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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)
⊢ Submodule.IsPrincipal (maximalIdeal R)
have neg : ∀ (ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥), Submodule.IsPrincipal (maximalIdeal R)
Tactic: by_cases ne_bot : maximalIdeal R = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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 (maximalIdeal R)
have pos : Submodule.IsPrincipal.{u_1, u_1} (R := R) (M := R) ⊥
Tactic: rw [ne_bot]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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), Membership.mem (γ := Ideal R) (maximalIdeal R) a ∧ a ≠ 0
have by_contra! : ∀ (h' : ∀ (a : R) (_ : Membership.mem (γ := Ideal R) (maximalIdeal R) a), a = 0), False
Tactic: by_contra! h'
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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
⊢ False
have apply : Eq (α := Ideal R) (maximalIdeal R) ⊥
Tactic: apply ne_bot
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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
⊢ Eq (α := Ideal R) (maximalIdeal R) ⊥
have rwa : LE.le (α := Ideal R) (maximalIdeal R) ⊥
Tactic: rwa [eq_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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 (maximalIdeal R)
have neg : ∀ (a : R) (ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a) (ha₂ : a ≠ 0), 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]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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)
have rwa : {a} ⊆ (↑(maximalIdeal R) : Set R)
Tactic: rwa [Ideal.span_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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)
⊢ LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)
have rwa₁ : a ∈ (↑(maximalIdeal R) : Set R)
Tactic: rwa [Ideal.span_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (hypothesis)
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
⊢ Submodule.IsPrincipal (maximalIdeal R)
have hle : 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]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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)
have rw : Eq (α := Ideal R) (sInf {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime}) (maximalIdeal R)
Tactic: rw [Ideal.radical_eq_sInf]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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) (sInf {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime}) (maximalIdeal R)
have a₁ : LE.le (α := Ideal R) (sInf {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime}) (maximalIdeal R)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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)
⊢ Eq (α := Ideal R) (sInf {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime}) (maximalIdeal R)
have a₂ : LE.le (α := Ideal R) (maximalIdeal R) (sInf {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime})
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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})
have a₁ : ∀ (I : Ideal R) (hI : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.span {a} ≤ J ∧ J.IsPrime} I) (e : I = ⊥),
  a = 0
Tactic: refine
        le_sInf fun I hI =>
          (eq_maximalIdeal <| hI.2.isMaximal (fun e => ha₂ ?_)).ge
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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 = 0
have a₁ : Ideal.span {a} ≤ I
Tactic: rw [← Ideal.span_singleton_eq_bot, eq_bot_iff, ← e]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (hypothesis)
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)
⊢ Submodule.IsPrincipal (maximalIdeal R)
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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}
have rw : ∃ (n : ℕ), HPow.hPow (α := Ideal R) (Ideal.radical (Ideal.span {a})) n ≤ Ideal.span {a}
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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) (Ideal.radical (Ideal.span {a})) n ≤ Ideal.span {a}
have h : Ideal.FG (R := R) (Ideal.radical (Ideal.span {a}))
Tactic: apply Ideal.exists_radical_pow_le_of_fg
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (hypothesis)
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)
⊢ Submodule.IsPrincipal (maximalIdeal R)
have this₁ : ∃ (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 _
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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}
⊢ Submodule.IsPrincipal (maximalIdeal R)
have neg : ∀ (hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = 0),
  Submodule.IsPrincipal (maximalIdeal R)
Tactic: rcases hn : Nat.find this with - | n
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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)
⊢ Submodule.IsPrincipal (maximalIdeal R)
have 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)
Tactic: rcases hn : Nat.find this with - | n
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (hypothesis)
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
⊢ Submodule.IsPrincipal (maximalIdeal R)
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (hypothesis)
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}
⊢ Submodule.IsPrincipal (maximalIdeal R)
have this₁ : LE.le (α := Ideal R) ⊤ (Ideal.span {a})
Tactic: rw [hn, pow_zero, Ideal.one_eq_top] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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 ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n, b ∉ Ideal.span {a}
have by_contra! : ∀
  (h' :
    ∀ (b : R) (_ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n), Membership.mem (γ := Ideal R) (Ideal.span {a}) b),
  False
Tactic: by_contra! h'
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (hypothesis)
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
⊢ False
have 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}
Tactic: rw [Nat.find_eq_iff] at hn
Cleared hypotheses: hn, h'
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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
⊢ Submodule.IsPrincipal (maximalIdeal R)
have neg : ∀ (b : R) (hb₁ : b ∈ HPow.hPow (α := Ideal R) (maximalIdeal R) n) (hb₂ : b ∉ Ideal.span {a}),
  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
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
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
⊢ ∃ (k : R), k * a = b * m
have rw : Membership.mem (γ := Ideal R) (Ideal.span {a}) (b * m)
Tactic: rw [← Ideal.mem_span_singleton']