awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vy : ℕ∞
hvy : ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y = vy
vx : ℕ
hvx : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) ((↑vx : ℕ∞) : ℕ∞)
coe :
  ∀ (hvy : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) (⊤ : ℕ∞)),
    LE.le (α := WithBot ℕ) (↑vx : ℕ∞) ⊤ ↔ x ∣ y
coe₁ :
  ∀ (vy : ℕ) (hvy : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) ((↑vy : ℕ∞) : ℕ∞)),
    LE.le (α := WithBot ℕ) (↑vx : ℕ∞) (↑vy : ℕ∞) ↔ x ∣ y
⊢ (↑vx : ℕ∞) ≤ vy ↔ x ∣ y

Tactic:
cases vy with
    | top => rw [addVal_eq_top_iff] at hvy; tauto
    | coe vy =>
      rw [← addVal_le_iff_dvd, hvx, hvy]
      exact WithBot.coe_le_coe.trans WithTop.coe_le_coe.symm

Premises used: WithBot.coe_le_coe, IsDiscreteValuationRing.addVal_eq_top_iff, Iff.trans, WithTop.coe_le_coe, IsDiscreteValuationRing.addVal_le_iff_dvd, Iff.symm
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vx : ℕ∞
hvx : ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x = vx
vy : ℕ∞
hvy : ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y = vy
top : ∀ (hvx : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (⊤ : ℕ∞)), ⊤ ≤ vy ↔ x ∣ y
coe :
  ∀ (vx : ℕ) (hvx : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) ((↑vx : ℕ∞) : ℕ∞)),
    (↑vx : ℕ∞) ≤ vy ↔ x ∣ y
⊢ vx ≤ vy ↔ x ∣ y

Tactic:
cases vx with
  | top => rw [addVal_eq_top_iff] at hvx; tauto
  | coe vx =>
    cases vy with
    | top => rw [addVal_eq_top_iff] at hvy; tauto
    | coe vy =>
      rw [← addVal_le_iff_dvd, hvx, hvy]
      exact WithBot.coe_le_coe.trans WithTop.coe_le_coe.symm

Premises used: WithBot.coe_le_coe, IsDiscreteValuationRing.addVal_eq_top_iff, Iff.trans, WithTop.coe_le_coe, IsDiscreteValuationRing.addVal_le_iff_dvd, Iff.symm
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hle : toWithBotNat x ≤ toWithBotNat y
pos : ∀ (hy : y = 0), x ∣ y
neg : ∀ (hy : ¬y = 0), x ∣ y
⊢ x ∣ y

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hle : toWithBotNat x ≤ toWithBotNat y
hy : y = 0
⊢ x ∣ y

Tactic:
simp [hy, hx] at hle
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hle : toWithBotNat x ≤ toWithBotNat y
hy : ¬y = 0
⊢ x ∣ y

Tactic:
(toWithBotNat_le_toWithBotNat_iff hx hy).mp hle

Premises used: Iff.mp, IsDiscreteValuationRing.toWithBotNat_le_toWithBotNat_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hle : toWithBotNat x ≤ toWithBotNat y
hy : ¬y = 0
⊢ x ∣ y

Tactic:
exact (toWithBotNat_le_toWithBotNat_iff hx hy).mp hle

Premises used: Iff.mp, IsDiscreteValuationRing.toWithBotNat_le_toWithBotNat_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x : R
⊢ quotient x 0 = 0

Tactic:
simp [quotient]

Premises used: IsDiscreteValuationRing.quotient
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
rw :
  ((y * if y = 0 then 0 else if h : y ∣ x then Exists.choose (p := fun (c : R) ↦ x = y * c) h else 0) +
      if y ∣ x then 0 else x) =
    x
⊢ y * quotient x y + remainder x y = x

Tactic:
rw [remainder, quotient]

Premises used: IsDiscreteValuationRing.quotient, IsDiscreteValuationRing.remainder
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
pos : ∀ (h₁ : y = 0) (h₂ : y ∣ x), y * 0 + 0 = x
neg : ∀ (h₁ : y = 0) (h₂ : ¬y ∣ x), y * 0 + x = x
pos₁ : ∀ (h₁ : ¬y = 0) (h₂ : y ∣ x), y * Exists.choose (p := fun (c : R) ↦ x = y * c) h₂ + 0 = x
neg₁ : ∀ (h₁ : ¬y = 0) (h₂ : ¬y ∣ x), y * 0 + x = x
⊢ ((y * if y = 0 then 0 else if h : y ∣ x then Exists.choose (p := fun (c : R) ↦ x = y * c) h else 0) +
      if y ∣ x then 0 else x) =
    x

Tactic:
split_ifs with h₁ h₂ h₂
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
h₁ : y = 0
h₂ : y ∣ x
⊢ x = 0

Tactic:
rw [h₁, zero_dvd_iff] at h₂

Premises used: zero_dvd_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
h₁ : y = 0
h₂ : x = 0
pos : HMul.hMul (α := R) 0 0 + 0 = 0
⊢ y * 0 + 0 = x

Tactic:
rw [h₁, h₂]
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
h₁ : y = 0
h₂ : x = 0
⊢ HMul.hMul (α := R) 0 0 + 0 = 0

Tactic:
ring
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
h₁ : y = 0
h₂ : ¬y ∣ x
neg : HMul.hMul (α := R) 0 0 + x = x
⊢ y * 0 + x = x

Tactic:
rw [h₁]
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
h₁ : y = 0
h₂ : ¬y ∣ x
⊢ HMul.hMul (α := R) 0 0 + x = x

Tactic:
ring
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
h₁ : ¬y = 0
h₂ : y ∣ x
pos : x + 0 = x
⊢ y * Exists.choose (p := fun (c : R) ↦ x = y * c) h₂ + 0 = x

Tactic:
rw [← h₂.choose_spec]

Premises used: Exists.choose_spec
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
h₁ : ¬y = 0
h₂ : y ∣ x
⊢ x + 0 = x

Tactic:
ring
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
h₁ : ¬y = 0
h₂ : ¬y ∣ x
⊢ y * 0 + x = x

Tactic:
ring
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
pos : ∀ (hyx : y ∣ x), toWithBotNat.{u_2} (R := R) 0 < toWithBotNat y
neg : ∀ (hyx : ¬y ∣ x), toWithBotNat x < toWithBotNat y
⊢ toWithBotNat (if y ∣ x then 0 else x) < toWithBotNat y

Tactic:
split_ifs with hyx
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hyx : y ∣ x
pos : ⊥ < toWithBotNat y
pos₁ pos₂ pos₃ pos₄ : y ≠ 0
⊢ toWithBotNat.{u_2} (R := R) 0 < toWithBotNat y

Tactic:
rwa [toWithBotNat_zero, bot_lt_toWithBotNat_iff]

Premises used: IsDiscreteValuationRing.toWithBotNat_zero, IsDiscreteValuationRing.bot_lt_toWithBotNat_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hyx : ¬y ∣ x
⊢ toWithBotNat x < toWithBotNat y

Tactic:
lt_iff_not_ge.mpr (mt (dvd_of_toWithBotNat_le_toWithBotNat _ _ hy) hyx)

Premises used: Iff.mpr, lt_iff_not_ge, IsDiscreteValuationRing.dvd_of_toWithBotNat_le_toWithBotNat, mt
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hyx : ¬y ∣ x
⊢ toWithBotNat x < toWithBotNat y

Tactic:
exact lt_iff_not_ge.mpr (mt (dvd_of_toWithBotNat_le_toWithBotNat _ _ hy) hyx)

Premises used: Iff.mpr, lt_iff_not_ge, IsDiscreteValuationRing.dvd_of_toWithBotNat_le_toWithBotNat, mt
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
pos : ∀ (hx : x = 0), ¬toWithBotNat (x * y) < toWithBotNat x
neg : ∀ (hx : ¬x = 0), ¬toWithBotNat (x * y) < toWithBotNat x
⊢ ¬toWithBotNat (x * y) < toWithBotNat x

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hx : x = 0
⊢ ¬toWithBotNat (x * y) < toWithBotNat x

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hx : ¬x = 0
neg : x ∣ x * y
⊢ ¬toWithBotNat (x * y) < toWithBotNat x

Tactic:
rw [not_lt, toWithBotNat_le_toWithBotNat_iff hx (mul_ne_zero hx hy)]

Premises used: not_lt, mul_ne_zero, IsDiscreteValuationRing.toWithBotNat_le_toWithBotNat_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hx : ¬x = 0
⊢ x ∣ x * y

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x y : R
hy : y ≠ 0
hx : ¬x = 0
⊢ x ∣ x * y

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
⊢ ValuationRing A

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
K : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O K
v : Valuation K Γ₀
hv : v.Integers O
this : IsDomain O := ⋯
inst_4 : IsDiscreteValuationRing O
_ :
  ∀ {ϖ : O} (_h : Irreducible ϖ),
    (↑(maximalIdeal O) : Set O) =
      {y : O |
        LE.le.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) ((algebraMap O K : (a : O) → K) y : K) : Γ₀)
          ((v : (a : K) → Γ₀) ((algebraMap O K : (a : O) → K) ϖ : K) : Γ₀)}
⊢ ∀ {ϖ : O} (_h : Irreducible ϖ),
    (↑(maximalIdeal O) : Set O) =
      {y : O |
        LE.le.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) ((algebraMap O K : (a : O) → K) y : K) : Γ₀)
          ((v : (a : K) → Γ₀) ((algebraMap O K : (a : O) → K) ϖ : K) : Γ₀)}

Tactic:
_
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
K : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O K
v : Valuation K Γ₀
hv : v.Integers O
this : IsDomain O := ⋯
inst_4 : IsDiscreteValuationRing O
ϖ : O
h : Irreducible ϖ
rw : (↑(maximalIdeal O) : Set O) = (↑(span {ϖ}) : Set O)
rw₁ rw₂ : (↑(maximalIdeal O) : Set O) = (↑(maximalIdeal O) : Set O)
⊢ (↑(maximalIdeal O) : Set O) =
    {y : O |
      LE.le.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) ((algebraMap O K : (a : O) → K) y : K) : Γ₀)
        ((v : (a : K) → Γ₀) ((algebraMap O K : (a : O) → K) ϖ : K) : Γ₀)}

Tactic:
rw [← hv.coe_span_singleton_eq_setOf_le_v_algebraMap, ← h.maximalIdeal_eq]

Premises used: Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap, Irreducible.maximalIdeal_eq
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
K : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O K
v : Valuation K Γ₀
hv : v.Integers O
this : IsDomain O := ⋯
inst_4 : IsDiscreteValuationRing O
ϖ : O
h : Irreducible ϖ
n : ℕ
⊢ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) ((algebraMap O K : (a : O) → K) ϖ : K) : Γ₀) n =
    (v : (a : K) → Γ₀) ((algebraMap O K : (a : O) → K) (ϖ ^ n) : K)

Tactic:
simp
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
K : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O K
v : Valuation K Γ₀
hv : v.Integers O
this : IsDomain O := ⋯
inst_4 : IsDiscreteValuationRing O
ϖ : O
h : Irreducible ϖ
n : ℕ
⊢ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) ((algebraMap O K : (a : O) → K) ϖ : K) : Γ₀) n =
    (v : (a : K) → Γ₀) ((algebraMap O K : (a : O) → K) (ϖ ^ n) : K)

Tactic:
have : (v (algebraMap O K ϖ)) ^ n = v (algebraMap O K (ϖ ^ n)) := by simp
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
K : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O K
v : Valuation K Γ₀
hv : v.Integers O
this_1 : IsDomain O := ⋯
inst_4 : IsDiscreteValuationRing O
ϖ : O
h : Irreducible ϖ
n : ℕ
this :
  HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) ((algebraMap O K : (a : O) → K) ϖ : K) : Γ₀) n =
    (v : (a : K) → Γ₀) ((algebraMap O K : (a : O) → K) (ϖ ^ n) : K)
rw :
  (↑(HPow.hPow (α := Ideal O) (maximalIdeal O) n) : Set O) =
    {y : O |
      LE.le.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) ((algebraMap O K : (a : O) → K) y : K) : Γ₀)
        ((v : (a : K) → Γ₀) ((algebraMap O K : (a : O) → K) (ϖ ^ n) : K) : Γ₀)}
rw₁ : (↑(HPow.hPow (α := Ideal O) (maximalIdeal O) n) : Set O) = (↑(span {ϖ ^ n}) : Set O)
rw₂ : (↑(HPow.hPow (α := Ideal O) (maximalIdeal O) n) : Set O) = (↑(HPow.hPow (α := Ideal O) (span {ϖ}) n) : Set O)
rw₃ rw₄ :
  (↑(HPow.hPow (α := Ideal O) (maximalIdeal O) n) : Set O) = (↑(HPow.hPow (α := Ideal O) (maximalIdeal O) n) : Set O)
⊢ (↑(HPow.hPow (α := Ideal O) (maximalIdeal O) n) : Set O) =
    {y : O |
      (v : (a : K) → Γ₀) ((algebraMap O K : (a : O) → K) y : K) ≤
        HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) ((algebraMap O K : (a : O) → K) ϖ : K) : Γ₀) n}

Tactic:
rw [this, ← hv.coe_span_singleton_eq_setOf_le_v_algebraMap,
      ← Ideal.span_singleton_pow, ← h.maximalIdeal_eq]

Premises used: Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap, Irreducible.maximalIdeal_eq, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
inst_2 : IsDiscreteValuationRing.{u_1} ↥v.integer
ϖ : ↥v.integer
h : Irreducible ϖ
⊢ (↑(maximalIdeal ↥v.integer) : Set ↥v.integer) =
    {y : ↥v.integer | LE.le.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑y : K) : Γ₀) ((v : (a : K) → Γ₀) (↑ϖ : K) : Γ₀)}

Tactic:
(Valuation.integer.integers v).maximalIdeal_eq_setOf_le_v_algebraMap h

Premises used: Set.Mem, setOf, Valuation.integer.integers, Valuation.Integers.maximalIdeal_eq_setOf_le_v_algebraMap
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
inst_2 : IsDiscreteValuationRing.{u_1} ↥v.integer
ϖ : ↥v.integer
h : Irreducible ϖ
n : ℕ
⊢ (↑(HPow.hPow (α := Ideal ↥v.integer) (maximalIdeal ↥v.integer) n) : Set ↥v.integer) =
    {y : ↥v.integer | (v : (a : K) → Γ₀) (↑y : K) ≤ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (↑ϖ : K) : Γ₀) n}

Tactic:
(Valuation.integer.integers v).maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow h _

Premises used: Set.Mem, setOf, Valuation.integer.integers, Valuation.Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_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
h' : Submodule.IsPrincipal (maximalIdeal R)
I : Ideal R
hI : I ≠ ⊥
pos : ∀ (h : IsField R), ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
neg : ∀ (h : ¬IsField R), ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
⊢ ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n

Tactic:
by_cases h : IsField R

Premises used: IsField
-- 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
h' : Submodule.IsPrincipal (maximalIdeal R)
I : Ideal R
hI : I ≠ ⊥
h : IsField R
x : Field R := h.toField
⊢ I = HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 0

Tactic:
simp [(eq_bot_or_eq_top I).resolve_left hI]

Premises used: Or.resolve_left, IsSimpleOrder.eq_bot_or_eq_top
-- 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
h' : Submodule.IsPrincipal (maximalIdeal R)
I : Ideal R
hI : I ≠ ⊥
h : IsField R
x : Field R := h.toField
⊢ ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n

Tactic:
exact ⟨0, by simp [(eq_bot_or_eq_top I).resolve_left hI]⟩
-- 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
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
⊢ ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n

Tactic:
obtain ⟨x, hx : _ = Ideal.span _⟩ := h'

Premises used: Ideal.span
-- 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})
pos : ∀ (hI' : I = ⊤), ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
neg : ∀ (hI' : ¬I = ⊤), ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n
⊢ ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n

Tactic:
by_cases hI' : I = ⊤
-- 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₁ : I = HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 0
⊢ ∃ (n : ℕ), I = HPow.hPow (α := Ideal R) (maximalIdeal R) n

Tactic:
use 0
-- 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₁ : I = 1
h₂ : Eq.{u_1 + 1} (α := Ideal R) ⊤ 1
h₃ h₄ : Eq.{u_1 + 1} (α := Ideal R) ⊤ ⊤
⊢ I = HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 0

Tactic:
rw [pow_zero, hI', Ideal.one_eq_top]

Premises used: Ideal.one_eq_top, pow_zero
-- 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 = ⊤
⊢ ∀ (r : R), ¬IsUnit r ↔ x ∣ r

Tactic:
have H : ∀ r : R, ¬IsUnit r ↔ x ∣ r := fun r =>
    (SetLike.ext_iff.mp hx r).trans Ideal.mem_span_singleton
-- 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
hI' : ¬I = ⊤
hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {0})
H : ∀ (r : R), ¬IsUnit r ↔ 0 ∣ r
apply : Eq (α := Ideal R) (maximalIdeal R) ⊥
⊢ False

Tactic:
apply Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal R) h

Premises used: Ring.ne_bot_of_isMaximal_of_not_isField, IsLocalRing.maximalIdeal.isMaximal
-- 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
hI' : ¬I = ⊤
hx : Eq (α := Ideal R) (maximalIdeal R) (Ideal.span {0})
H : ∀ (r : R), ¬IsUnit r ↔ 0 ∣ r
⊢ Eq (α := Ideal R) (maximalIdeal R) ⊥

Tactic:
simp [hx]
-- 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
⊢ x ≠ 0

Tactic:
have : x ≠ 0 := by
    rintro rfl
    apply Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal R) h
    simp [hx]
-- 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 : x ≠ 0
⊢ Irreducible x

Tactic:
have hx' := IsDiscreteValuationRing.irreducible_of_span_eq_maximalIdeal x this hx
-- 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 : x ≠ 0
hx' : Irreducible x
r : R
hr₁ : r ≠ 0
hr₂ : r ∈ nonunits R
obtain :
  ∀ (f : Multiset R) (hf₁ : ∀ b ∈ f, Irreducible b) (hf₂ : f ≠ ∅) (hr₁ : f.prod ≠ 0) (hr₂ : f.prod ∈ nonunits R),
    ∃ (n : ℕ), Associated (x ^ n) f.prod
⊢ ∃ (n : ℕ), Associated (x ^ n) r

Tactic:
obtain ⟨f, hf₁, rfl, hf₂⟩ := (WfDvdMonoid.not_unit_iff_exists_factors_eq r hr₁).mp hr₂

Premises used: WfDvdMonoid.not_unit_iff_exists_factors_eq, Iff.mp, rfl