awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose (p := Prime) ⋯)
h :
  LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞)
pos : ∀ (ha0 : a = 0), a ∣ b
neg : ∀ (ha0 : ¬a = 0), a ∣ b
⊢ a ∣ b

Tactic:
by_cases ha0 : a = 0
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose (p := Prime) ⋯)
h :
  LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞)
ha0 : a = 0
⊢ b = 0

Tactic:
rw [ha0, addVal_zero, top_le_iff, addVal_eq_top_iff] at h

Premises used: IsDiscreteValuationRing.addVal_zero, IsDiscreteValuationRing.addVal_eq_top_iff, top_le_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose (p := Prime) ⋯)
h :
  LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞)
ha0 : a = 0
h₁ : b = 0
⊢ a = 0

Tactic:
rw [ha0, addVal_zero, top_le_iff, addVal_eq_top_iff] at h

Premises used: IsDiscreteValuationRing.addVal_zero, IsDiscreteValuationRing.addVal_eq_top_iff, top_le_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose (p := Prime) ⋯)
h : b = 0
ha0 : a = 0
pos : a ∣ 0
⊢ a ∣ b

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose (p := Prime) ⋯)
h : b = 0
ha0 : a = 0
⊢ a ∣ 0

Tactic:
apply dvd_zero

Premises used: dvd_zero
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose (p := Prime) ⋯)
h :
  LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞)
ha0 : ¬a = 0
neg : ∀ (n : ℕ) (ha : Associated a (Classical.choose (p := Prime) ⋯ ^ n)), a ∣ b
⊢ a ∣ b

Tactic:
obtain ⟨n, ha⟩ := associated_pow_irreducible ha0 hp.irreducible

Premises used: Prime.irreducible, IsDiscreteValuationRing.associated_pow_irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose (p := Prime) ⋯)
h :
  LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞)
ha0 : ¬a = 0
n : ℕ
ha : Associated a (Classical.choose (p := Prime) ⋯ ^ n)
neg :
  ∀ (h : ∀ (n : ℕ), Classical.choose (p := Prime) ⋯ ^ n ∣ a → Classical.choose (p := Prime) ⋯ ^ n ∣ b) (ha0 : ¬a = 0)
    (n : ℕ) (ha : Associated a (Classical.choose (p := Prime) ⋯ ^ n)), a ∣ b
⊢ a ∣ b

Tactic:
rw [addVal, multiplicity_addValuation_apply, multiplicity_addValuation_apply,
      emultiplicity_le_emultiplicity_iff] at h

Premises used: multiplicity_addValuation_apply, emultiplicity_le_emultiplicity_iff, IsDiscreteValuationRing.addVal
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose (p := Prime) ⋯)
h : ∀ (n : ℕ), Classical.choose (p := Prime) ⋯ ^ n ∣ a → Classical.choose (p := Prime) ⋯ ^ n ∣ b
ha0 : ¬a = 0
n : ℕ
ha : Associated a (Classical.choose (p := Prime) ⋯ ^ n)
⊢ a ∣ b

Tactic:
ha.dvd.trans (h n ha.symm.dvd)

Premises used: Associated.dvd, Associated.symm, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose (p := Prime) ⋯)
h : ∀ (n : ℕ), Classical.choose (p := Prime) ⋯ ^ n ∣ a → Classical.choose (p := Prime) ⋯ ^ n ∣ b
ha0 : ¬a = 0
n : ℕ
ha : Associated a (Classical.choose (p := Prime) ⋯ ^ n)
⊢ a ∣ b

Tactic:
exact ha.dvd.trans (h n ha.symm.dvd)

Premises used: Associated.dvd, Associated.symm, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose (p := Prime) ⋯)
h : a ∣ b
⊢ emultiplicity (Classical.choose (p := Prime) ⋯) a ≤ emultiplicity (Classical.choose (p := Prime) ⋯) b

Tactic:
emultiplicity_le_emultiplicity_of_dvd_right h

Premises used: emultiplicity_le_emultiplicity_of_dvd_right
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose (p := Prime) ⋯)
h : a ∣ b
⊢ emultiplicity (Classical.choose (p := Prime) ⋯) a ≤ emultiplicity (Classical.choose (p := Prime) ⋯) b

Tactic:
exact emultiplicity_le_emultiplicity_of_dvd_right h

Premises used: emultiplicity_le_emultiplicity_of_dvd_right
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
have have₁ have₂ :
  ∀ (hp : Prime (Classical.choose (p := Prime) ⋯)),
    LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞) ↔
      a ∣ b
mp :
  ∀ (hp : Prime (Classical.choose (p := Prime) ⋯))
    (h :
      LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞)),
    a ∣ b
mpr mpr₁ :
  ∀ (hp : Prime (Classical.choose (p := Prime) ⋯)) (h : a ∣ b),
    LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞)
⊢ LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞) ↔
    a ∣ b

Tactic:
classical
  have hp := Classical.choose_spec (exists_prime R)
  constructor <;> intro h
  · by_cases ha0 : a = 0
    · rw [ha0, addVal_zero, top_le_iff, addVal_eq_top_iff] at h
      rw [h]
      apply dvd_zero
    obtain ⟨n, ha⟩ := associated_pow_irreducible ha0 hp.irreducible
    rw [addVal, multiplicity_addValuation_apply, multiplicity_addValuation_apply,
      emultiplicity_le_emultiplicity_iff] at h
    exact ha.dvd.trans (h n ha.symm.dvd)
  · rw [addVal, multiplicity_addValuation_apply, multiplicity_addValuation_apply]
    exact emultiplicity_le_emultiplicity_of_dvd_right h

Premises used: IsDiscreteValuationRing.addVal_zero, dvd_zero, multiplicity_addValuation_apply, emultiplicity_le_emultiplicity_iff, IsDiscreteValuationRing.addVal, IsDiscreteValuationRing.addVal_eq_top_iff, top_le_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
⊢ LE.le (α := ℕ∞)
    (min (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b) : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (a + b) : ℕ∞)

Tactic:
(addVal R).map_add _ _

Premises used: IsDiscreteValuationRing.addVal, AddValuation.map_add
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
u : Rˣ
obtain :
  ∀ (ϖ : R) (hϖ : Irreducible ϖ), Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (↑u : R) : ℕ∞) (0 : ℕ∞)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (↑u : R) : ℕ∞) (0 : ℕ∞)

Tactic:
obtain ⟨ϖ, hϖ⟩ := exists_irreducible R

Premises used: IsDiscreteValuationRing.exists_irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
rw : Eq (α := ℕ∞) (↑0 : ℕ∞) 0
rw₁ : (↑u : R) = (↑u : R) * HPow.hPow (β := ℕ) ϖ 0
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (↑u : R) : ℕ∞) (0 : ℕ∞)

Tactic:
rw [addVal_def (u : R) u hϖ 0]

Premises used: Units.val, IsDiscreteValuationRing.addVal_def, OfNat.ofNat
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
⊢ Eq (α := ℕ∞) (↑0 : ℕ∞) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
⊢ (↑u : R) = (↑u : R) * HPow.hPow (β := ℕ) ϖ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
inl : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) 0 : ℕ∞) (0 : ℕ∞) ↔ IsUnit.{u_1} (M := R) 0
inr : ∀ (hx : x ≠ 0), Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (0 : ℕ∞) ↔ IsUnit x
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (0 : ℕ∞) ↔ IsUnit x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) 0 : ℕ∞) (0 : ℕ∞) ↔ IsUnit.{u_1} (M := R) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
inr :
  ∀ (ϖ : R) (hϖ : Irreducible ϖ),
    Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (0 : ℕ∞) ↔ IsUnit x
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (0 : ℕ∞) ↔ IsUnit x

Tactic:
obtain ⟨ϖ, hϖ⟩ := exists_irreducible R

Premises used: IsDiscreteValuationRing.exists_irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hϖ : Irreducible ϖ
inr :
  ∀ (n : ℕ) (u : Rˣ) (hx : (↑u : R) * ϖ ^ n ≠ 0),
    Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑u : R) * ϖ ^ n) : ℕ∞) (0 : ℕ∞) ↔
      IsUnit ((↑u : R) * ϖ ^ n)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (0 : ℕ∞) ↔ IsUnit x

Tactic:
obtain ⟨n, u, rfl⟩ := eq_unit_mul_pow_irreducible hx hϖ

Premises used: IsDiscreteValuationRing.eq_unit_mul_pow_irreducible, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
hx : (↑u : R) * ϖ ^ n ≠ 0
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑u : R) * ϖ ^ n) : ℕ∞) (0 : ℕ∞) ↔
    IsUnit ((↑u : R) * ϖ ^ n)

Tactic:
simp [isUnit_pow_iff_of_not_isUnit hϖ.not_isUnit, hϖ]

Premises used: Irreducible.not_isUnit, isUnit_pow_iff_of_not_isUnit
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
mp :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) →
    Associated x y
mpr :
  Associated x y →
    Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) ↔
    Associated x y

Tactic:
constructor
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
pos : ∀ (hx : x = 0), Associated x y
neg : ∀ (hx : ¬x = 0), Associated x y
⊢ Associated x y

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : x = 0
pos :
  ∀ (h : Eq (α := ℕ∞) (⊤ : ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)) (hx : x = 0), Associated 0 y
⊢ Associated x y

Tactic:
simp_all only [AddValuation.map_zero]

Premises used: AddValuation.map_zero
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h : Eq (α := ℕ∞) (⊤ : ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : x = 0
pos pos₁ : Associated.{u_1} (M := R) 0 0
⊢ Associated 0 y

Tactic:
rw [addVal_eq_top_iff.mp h.symm]

Premises used: IsDiscreteValuationRing.addVal_eq_top_iff, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : ¬x = 0
pos : ∀ (hy : y = 0), Associated x y
neg : ∀ (hy : ¬y = 0), Associated x y
⊢ Associated x y

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : ¬x = 0
hy : y = 0
pos :
  ∀ (h : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (⊤ : ℕ∞)) (hx : ¬x = 0) (hy : y = 0),
    False
⊢ Associated x y

Tactic:
simp_all only [AddValuation.map_zero, associated_zero_iff_eq_zero]

Premises used: associated_zero_iff_eq_zero, AddValuation.map_zero
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (⊤ : ℕ∞)
hx : ¬x = 0
hy : y = 0
⊢ False

Tactic:
hx (addVal_eq_top_iff.mp h)

Premises used: IsDiscreteValuationRing.addVal_eq_top_iff, Iff.mp
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (⊤ : ℕ∞)
hx : ¬x = 0
hy : y = 0
⊢ False

Tactic:
exact hx (addVal_eq_top_iff.mp h)

Premises used: IsDiscreteValuationRing.addVal_eq_top_iff, Iff.mp
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : ¬x = 0
hy : ¬y = 0
neg : ∀ (ϖ : R) (hϖ : Irreducible ϖ), Associated x y
⊢ Associated x y

Tactic:
obtain ⟨ϖ, hϖ⟩ := exists_irreducible R

Premises used: IsDiscreteValuationRing.exists_irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : ¬x = 0
hy : ¬y = 0
ϖ : R
hϖ : Irreducible ϖ
neg : ∀ (m : ℕ) (α : Rˣ) (hx' : x = (↑α : R) * ϖ ^ m), Associated x y
⊢ Associated x y

Tactic:
obtain ⟨m, α, hx'⟩ := eq_unit_mul_pow_irreducible hx hϖ

Premises used: IsDiscreteValuationRing.eq_unit_mul_pow_irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : ¬x = 0
hy : ¬y = 0
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx' : x = (↑α : R) * ϖ ^ m
neg : ∀ (n : ℕ) (β : Rˣ) (hy' : y = (↑β : R) * ϖ ^ n), Associated x y
⊢ Associated x y

Tactic:
obtain ⟨n, β, hy'⟩ := eq_unit_mul_pow_irreducible hy hϖ

Premises used: IsDiscreteValuationRing.eq_unit_mul_pow_irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
h :
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞)
hx : ¬x = 0
hy : ¬y = 0
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx' : x = (↑α : R) * ϖ ^ m
n : ℕ
β : Rˣ
hy' : y = (↑β : R) * ϖ ^ n
neg :
  ∀
    (h :
      HMul.hMul (α := ℕ∞) (β := ℕ∞) ((↑m : ℕ∞) : ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ϖ : ℕ∞) =
        HMul.hMul (α := ℕ∞) (β := ℕ∞) ((↑n : ℕ∞) : ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ϖ : ℕ∞)),
    Associated (ϖ ^ m) (ϖ ^ n)
⊢ Associated x y

Tactic:
simp only [hx', AddValuation.map_mul, addVal_eq_zero_of_unit, AddValuation.map_pow,
      nsmul_eq_mul, zero_add, hy', associated_unit_mul_right_iff,
      associated_unit_mul_left_iff] at h ⊢

Premises used: AddValuation.map_pow, associated_unit_mul_right_iff, zero_add, AddValuation.map_mul, associated_unit_mul_left_iff, IsDiscreteValuationRing.addVal_eq_zero_of_unit, nsmul_eq_mul
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : ¬x = 0
hy : ¬y = 0
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx' : x = (↑α : R) * ϖ ^ m
n : ℕ
β : Rˣ
hy' : y = (↑β : R) * ϖ ^ n
h :
  HMul.hMul (α := ℕ∞) (β := ℕ∞) ((↑m : ℕ∞) : ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ϖ : ℕ∞) =
    HMul.hMul (α := ℕ∞) (β := ℕ∞) ((↑n : ℕ∞) : ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ϖ : ℕ∞)
⊢ m = n

Tactic:
simp only [addVal_uniformizer hϖ, mul_one, ENat.coe_inj] at h

Premises used: IsDiscreteValuationRing.addVal_uniformizer, ENat.coe_inj, mul_one
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : ¬x = 0
hy : ¬y = 0
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx' : x = (↑α : R) * ϖ ^ m
n : ℕ
β : Rˣ
hy' : y = (↑β : R) * ϖ ^ n
h : m = n
neg : Associated (ϖ ^ n) (ϖ ^ n)
⊢ Associated (ϖ ^ m) (ϖ ^ n)

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : ¬x = 0
hy : ¬y = 0
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx' : x = (↑α : R) * ϖ ^ m
n : ℕ
β : Rˣ
hy' : y = (↑β : R) * ϖ ^ n
h : m = n
⊢ Associated (ϖ ^ n) (ϖ ^ n)

Tactic:
Associates.mk_eq_mk_iff_associated.mp rfl

Premises used: Associates.mk_eq_mk_iff_associated, Iff.mp, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : ¬x = 0
hy : ¬y = 0
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx' : x = (↑α : R) * ϖ ^ m
n : ℕ
β : Rˣ
hy' : y = (↑β : R) * ϖ ^ n
h : m = n
⊢ Associated (ϖ ^ n) (ϖ ^ n)

Tactic:
exact Associates.mk_eq_mk_iff_associated.mp rfl

Premises used: Associates.mk_eq_mk_iff_associated, Iff.mp, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
u : Rˣ
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (x * (↑u : R)) : ℕ∞)

Tactic:
simp_all
-- 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 : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
this :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
          (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) =
        I),
    (fun (n : ℕ∞ᵒᵈ) ↦
          (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
              ((OrderDual.ofDual : (a : ℕ∞ᵒᵈ) → ℕ∞) n) :
            Ideal R))
        ((fun (I : Ideal R) ↦
            ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (generator I) : ℕ∞) :
              ℕ∞ᵒᵈ))
          I) =
      I
⊢ (fun (n : ℕ∞ᵒᵈ) ↦
        (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
            ((OrderDual.ofDual : (a : ℕ∞ᵒᵈ) → ℕ∞) n) :
          Ideal R))
      ((fun (I : Ideal R) ↦
          ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (generator I) : ℕ∞) :
            ℕ∞ᵒᵈ))
        I) =
    I

Tactic:
rwa [Ideal.span_singleton_generator] at this

Premises used: Ideal.span_singleton_generator
-- 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 : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
suffices :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)
⊢ (fun (n : ℕ∞ᵒᵈ) ↦
        (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
            ((OrderDual.ofDual : (a : ℕ∞ᵒᵈ) → ℕ∞) n) :
          Ideal R))
      ((fun (I : Ideal R) ↦
          ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (generator I) : ℕ∞) :
            ℕ∞ᵒᵈ))
        I) =
    I

Tactic:
suffices (addVal R x).recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) = span {x} by
      rwa [Ideal.span_singleton_generator] at this
-- 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 : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
pos :
  ∀ (hx0 : x = 0),
    Eq.{u_1 + 1} (α := Ideal R)
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
          (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
        Ideal R)
      (span {x} : Ideal R)
neg :
  ∀ (hx0 : ¬x = 0),
    Eq.{u_1 + 1} (α := Ideal R)
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
          (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
        Ideal R)
      (span {x} : Ideal R)
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)

Tactic:
by_cases hx0 : x = 0