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
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
⊢ ∃ (u : Rˣ), p ^ m * (↑u : R) = q ^ n

Tactic:
⟨u * v⁻¹, ?_⟩

Premises used: HMul.hMul, Inv.inv, Exists.intro
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
refine : p ^ m * (↑(u * v⁻¹) : R) = q ^ n
⊢ ∃ (u : Rˣ), p ^ m * (↑u : R) = q ^ n

Tactic:
refine ⟨u * v⁻¹, ?_⟩
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
simp : p ^ m * ((↑u : R) * (↑v⁻¹ : R)) = q ^ n
⊢ p ^ m * (↑(u * v⁻¹) : R) = q ^ n

Tactic:
simp only [Units.val_mul]

Premises used: Units.val_mul
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
rw : (↑u : R) * (p ^ m * (↑v⁻¹ : R)) = q ^ n
rw₁ : (↑u : R) * p ^ m * (↑v⁻¹ : R) = q ^ n
rw₂ : (↑v : R) * q ^ n * (↑v⁻¹ : R) = q ^ n
rw₃ : (↑v : R) * (↑v⁻¹ : R) * q ^ n = q ^ n
rw₄ : 1 * q ^ n = q ^ n
rw₅ rw₆ : q ^ n = q ^ n
⊢ p ^ m * ((↑u : R) * (↑v⁻¹ : R)) = q ^ n

Tactic:
rw [mul_left_comm, ← mul_assoc, h, mul_right_comm, Units.mul_inv, one_mul]

Premises used: mul_assoc, Units.mul_inv, mul_left_comm, mul_right_comm, one_mul
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
⊢ Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod

Tactic:
have key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod := by
    rw [Multiset.prod_replicate, Multiset.prod_replicate, Associated]
    refine ⟨u * v⁻¹, ?_⟩
    simp only [Units.val_mul]
    rw [mul_left_comm, ← mul_assoc, h, mul_right_comm, Units.mul_inv, one_mul]
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod
⊢ (Multiset.replicate m p).card = (Multiset.replicate n q).card

Tactic:
Multiset.card_eq_card_of_rel (UniqueFactorizationMonoid.factors_unique ?_ ?_ key)

Premises used: UniqueFactorizationMonoid.factors_unique, Multiset.card_eq_card_of_rel
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod
refine_1 : ∀ x ∈ Multiset.replicate m p, Irreducible x
refine_2 : ∀ x ∈ Multiset.replicate n q, Irreducible x
⊢ (Multiset.replicate m p).card = (Multiset.replicate n q).card

Tactic:
refine Multiset.card_eq_card_of_rel (UniqueFactorizationMonoid.factors_unique ?_ ?_ key)

Premises used: UniqueFactorizationMonoid.factors_unique, Multiset.card_eq_card_of_rel
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod
x : R
hx : x ∈ Multiset.replicate m p
⊢ Irreducible x

Tactic:
obtain rfl := Multiset.eq_of_mem_replicate hx

Premises used: Multiset.eq_of_mem_replicate, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod
x : R
hx : x ∈ Multiset.replicate m p
hp₁ : Irreducible x
⊢ (↑u : R) * x ^ m = (↑v : R) * q ^ n

Tactic:
obtain rfl := Multiset.eq_of_mem_replicate hx

Premises used: Multiset.eq_of_mem_replicate, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod
x : R
hx : x ∈ Multiset.replicate m p
hp₁ : Irreducible x
h₁ : (↑u : R) * x ^ m = (↑v : R) * q ^ n
⊢ Associated (Multiset.replicate m x).prod (Multiset.replicate n q).prod

Tactic:
obtain rfl := Multiset.eq_of_mem_replicate hx

Premises used: Multiset.eq_of_mem_replicate, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod
x : R
hx : x ∈ Multiset.replicate m p
hp₁ : Irreducible x
h₁ : (↑u : R) * x ^ m = (↑v : R) * q ^ n
key₁ : Associated (Multiset.replicate m x).prod (Multiset.replicate n q).prod
⊢ x ∈ Multiset.replicate m x

Tactic:
obtain rfl := Multiset.eq_of_mem_replicate hx

Premises used: Multiset.eq_of_mem_replicate, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
q : R
hq : Irreducible q
u v : Rˣ
m n : ℕ
x : R
hp : Irreducible x
h : (↑u : R) * x ^ m = (↑v : R) * q ^ n
key : Associated (Multiset.replicate m x).prod (Multiset.replicate n q).prod
hx : x ∈ Multiset.replicate m x
⊢ Irreducible x

Tactic:
assumption
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod
x : R
hx : x ∈ Multiset.replicate n q
⊢ Irreducible x

Tactic:
obtain rfl := Multiset.eq_of_mem_replicate hx

Premises used: Multiset.eq_of_mem_replicate, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod
x : R
hx : x ∈ Multiset.replicate n q
hq₁ : Irreducible x
⊢ (↑u : R) * p ^ m = (↑v : R) * x ^ n

Tactic:
obtain rfl := Multiset.eq_of_mem_replicate hx

Premises used: Multiset.eq_of_mem_replicate, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod
x : R
hx : x ∈ Multiset.replicate n q
hq₁ : Irreducible x
h₁ : (↑u : R) * p ^ m = (↑v : R) * x ^ n
⊢ Associated (Multiset.replicate m p).prod (Multiset.replicate n x).prod

Tactic:
obtain rfl := Multiset.eq_of_mem_replicate hx

Premises used: Multiset.eq_of_mem_replicate, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod
x : R
hx : x ∈ Multiset.replicate n q
hq₁ : Irreducible x
h₁ : (↑u : R) * p ^ m = (↑v : R) * x ^ n
key₁ : Associated (Multiset.replicate m p).prod (Multiset.replicate n x).prod
⊢ x ∈ Multiset.replicate n x

Tactic:
obtain rfl := Multiset.eq_of_mem_replicate hx

Premises used: Multiset.eq_of_mem_replicate, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p : R
hp : Irreducible p
u v : Rˣ
m n : ℕ
x : R
hq : Irreducible x
h : (↑u : R) * p ^ m = (↑v : R) * x ^ n
key : Associated (Multiset.replicate m p).prod (Multiset.replicate n x).prod
hx : x ∈ Multiset.replicate n x
⊢ Irreducible x

Tactic:
assumption
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod
⊢ (Multiset.replicate m p).card = (Multiset.replicate n q).card

Tactic:
have := by
    refine Multiset.card_eq_card_of_rel (UniqueFactorizationMonoid.factors_unique ?_ ?_ key)
    all_goals
      intro x hx
      obtain rfl := Multiset.eq_of_mem_replicate hx
      assumption
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : (↑u : R) * p ^ m = (↑v : R) * q ^ n
key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod
this : (Multiset.replicate m p).card = (Multiset.replicate n q).card
⊢ m = n

Tactic:
simpa only [Multiset.card_replicate]

Premises used: Multiset.card_replicate
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m n : ℕ
h : (↑u : R) * ϖ ^ m = (↑v : R) * ϖ ^ n
⊢ m = n

Tactic:
unit_mul_pow_congr_pow hirr hirr u v m n h

Premises used: IsDiscreteValuationRing.unit_mul_pow_congr_pow
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m n : ℕ
h : (↑u : R) * ϖ ^ m = (↑v : R) * ϖ ^ n
⊢ (↑u : R) * ϖ ^ m = (↑v : R) * ϖ ^ m

Tactic:
obtain rfl : m = n := unit_mul_pow_congr_pow hirr hirr u v m n h

Premises used: IsDiscreteValuationRing.unit_mul_pow_congr_pow, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : (↑u : R) * ϖ ^ m = (↑v : R) * ϖ ^ m
⊢ (↑u : R) * ϖ ^ m - (↑v : R) * ϖ ^ m = 0

Tactic:
rw [← sub_eq_zero] at h

Premises used: sub_eq_zero
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : (↑u : R) * ϖ ^ m - (↑v : R) * ϖ ^ m = 0
⊢ (↑u : R) - (↑v : R) = 0 ∨ ϖ ^ m = 0

Tactic:
rw [← sub_mul, mul_eq_zero] at h

Premises used: mul_eq_zero, sub_mul
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : (↑u : R) - (↑v : R) = 0 ∨ ϖ ^ m = 0
inl : ∀ (h : (↑u : R) - (↑v : R) = 0), u = v
inr : ∀ (h : ϖ ^ m = 0), u = v
⊢ u = v

Tactic:
rcases h with h | h
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : (↑u : R) - (↑v : R) = 0
⊢ (↑u : R) = (↑v : R)

Tactic:
rw [sub_eq_zero] at h

Premises used: sub_eq_zero
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : (↑u : R) = (↑v : R)
⊢ u = v

Tactic:
mod_cast h

Premises used: cast, Units.val_inj._simp_2
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : (↑u : R) = (↑v : R)
⊢ u = v

Tactic:
exact mod_cast h
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ϖ ^ m = 0
⊢ u = v

Tactic:
apply (hirr.ne_zero (eq_zero_of_pow_eq_zero h)).elim

Premises used: False.elim, Irreducible.ne_zero, eq_zero_of_pow_eq_zero
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
r : R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
hr : r = (↑u : R) * ϖ ^ n
rw :
  Eq (α := ℕ∞)
    (((multiplicity_addValuation (p := Classical.choose (p := Prime) ⋯) ⋯ : AddValuation R ℕ∞) : (a : R) → ℕ∞) r : ℕ∞)
    ((↑n : ℕ∞) : ℕ∞)
rw₁ : emultiplicity (Classical.choose (p := Prime) ⋯) r = (↑n : ℕ∞)
rw₂ : emultiplicity (Classical.choose (p := Prime) ⋯) ((↑u : R) * ϖ ^ n) = (↑n : ℕ∞)
rw₃ : emultiplicity ϖ ((↑u : R) * ϖ ^ n) = (↑n : ℕ∞)
rw₄ : emultiplicity ϖ (ϖ ^ n) = (↑n : ℕ∞)
rw₅ rw₆ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) r : ℕ∞) ((↑n : ℕ∞) : ℕ∞)

Tactic:
rw [addVal, multiplicity_addValuation_apply, hr, emultiplicity_eq_of_associated_left
      (associated_of_irreducible R hϖ (Classical.choose_spec (exists_prime R)).irreducible),
    emultiplicity_eq_of_associated_right (Associated.symm ⟨u, mul_comm _ _⟩),
    emultiplicity_pow_self_of_prime (irreducible_iff_prime.1 hϖ)]

Premises used: Prime.irreducible, emultiplicity_eq_of_associated_right, multiplicity_addValuation_apply, emultiplicity_eq_of_associated_left, IsDiscreteValuationRing.exists_prime, IsDiscreteValuationRing.associated_of_irreducible, Classical.choose_spec, IsDiscreteValuationRing.addVal, Associated.symm, Exists.intro, Iff.mp, mul_comm, irreducible_iff_prime, emultiplicity_pow_self_of_prime
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
r : R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
hr : r = (↑u : R) * ϖ ^ n
rw :
  Eq (α := ℕ∞)
    (((multiplicity_addValuation (p := Classical.choose (p := Prime) ⋯) ⋯ : AddValuation R ℕ∞) : (a : R) → ℕ∞) r : ℕ∞)
    ((↑n : ℕ∞) : ℕ∞)
rw₁ : emultiplicity (Classical.choose (p := Prime) ⋯) r = (↑n : ℕ∞)
rw₂ : emultiplicity (Classical.choose (p := Prime) ⋯) ((↑u : R) * ϖ ^ n) = (↑n : ℕ∞)
rw₃ : emultiplicity ϖ ((↑u : R) * ϖ ^ n) = (↑n : ℕ∞)
rw₄ : emultiplicity ϖ (ϖ ^ n) = (↑n : ℕ∞)
rw₅ rw₆ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) r : ℕ∞) ((↑n : ℕ∞) : ℕ∞)

Tactic:
classical
  rw [addVal, multiplicity_addValuation_apply, hr, emultiplicity_eq_of_associated_left
      (associated_of_irreducible R hϖ (Classical.choose_spec (exists_prime R)).irreducible),
    emultiplicity_eq_of_associated_right (Associated.symm ⟨u, mul_comm _ _⟩),
    emultiplicity_pow_self_of_prime (irreducible_iff_prime.1 hϖ)]

Premises used: Prime.irreducible, emultiplicity_eq_of_associated_right, multiplicity_addValuation_apply, emultiplicity_eq_of_associated_left, IsDiscreteValuationRing.exists_prime, IsDiscreteValuationRing.associated_of_irreducible, Classical.choose_spec, IsDiscreteValuationRing.addVal, Associated.symm, Exists.intro, Iff.mp, mul_comm, irreducible_iff_prime, emultiplicity_pow_self_of_prime
-- 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 ϖ
n : ℕ
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑u : R) * ϖ ^ n) : ℕ∞) ((↑n : ℕ∞) : ℕ∞)

Tactic:
addVal_def _ u hϖ n rfl

Premises used: IsDiscreteValuationRing.addVal_def, 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 : ℕ∞) (⊤ : ℕ∞)

Tactic:
(addVal R).map_zero

Premises used: AddValuation.map_zero, IsDiscreteValuationRing.addVal
-- 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) → ℕ∞) 1 : ℕ∞) (0 : ℕ∞)

Tactic:
(addVal R).map_one

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

Tactic:
simpa only [one_mul, eq_self_iff_true, Units.val_one, pow_one, forall_true_left, Nat.cast_one]
    using addVal_def ϖ 1 hϖ 1

Premises used: forall_true_left, pow_one, Units.val_one, IsDiscreteValuationRing.addVal_def, OfNat.ofNat, Nat.cast_one, eq_self_iff_true, one_mul
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
⊢ ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (a * b) =
    HAdd.hAdd (α := ℕ∞) (β := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞)

Tactic:
(addVal R).map_mul _ _

Premises used: AddValuation.map_mul, IsDiscreteValuationRing.addVal
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a : R
n : ℕ
⊢ ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (a ^ n) =
    HSMul.hSMul (β := ℕ∞) n (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)

Tactic:
(addVal R).map_pow _ _

Premises used: AddValuation.map_pow, IsDiscreteValuationRing.addVal
-- 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 : ℕ
rw : HSMul.hSMul (β := ℕ∞) n (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ϖ : ℕ∞) = (↑n : ℕ∞)
rw₁ : HSMul.hSMul (β := ℕ∞) n 1 = (↑n : ℕ∞)
rw₂ rw₃ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (ϖ ^ n) : ℕ∞) ((↑n : ℕ∞) : ℕ∞)

Tactic:
rw [addVal_pow, addVal_uniformizer h, nsmul_one]

Premises used: IsDiscreteValuationRing.addVal_uniformizer, IsDiscreteValuationRing.addVal_pow, nsmul_one
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a : R
⊢ Irreducible (Classical.choose (p := Prime) ⋯)

Tactic:
have hi := (Classical.choose_spec (exists_prime R)).irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a : R
hi : Irreducible (Classical.choose (p := Prime) ⋯)
mp : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞) → a = 0
mpr : a = 0 → Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞) ↔ a = 0

Tactic:
constructor
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a : R
hi : Irreducible (Classical.choose (p := Prime) ⋯)
mp : ¬a = 0 → ¬Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞) → a = 0

Tactic:
contrapose
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a : R
hi : Irreducible (Classical.choose (p := Prime) ⋯)
h : ¬a = 0
mp :
  ∀ (n : ℕ) (ha : Associated a (Classical.choose (p := Prime) ⋯ ^ n)),
    ¬Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞)
⊢ ¬Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞)

Tactic:
obtain ⟨n, ha⟩ := associated_pow_irreducible h hi

Premises used: 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 : R
hi : Irreducible (Classical.choose (p := Prime) ⋯)
h : ¬a = 0
n : ℕ
ha : Associated a (Classical.choose (p := Prime) ⋯ ^ n)
mp :
  ∀ (u : Rˣ) (h : ¬Classical.choose (p := Prime) ⋯ ^ n * (↑u : R) = 0)
    (ha : Associated (Classical.choose (p := Prime) ⋯ ^ n * (↑u : R)) (Classical.choose (p := Prime) ⋯ ^ n)),
    ¬Eq (α := ℕ∞)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (Classical.choose (p := Prime) ⋯ ^ n * (↑u : R)) : ℕ∞) (⊤ : ℕ∞)
⊢ ¬Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞)

Tactic:
obtain ⟨u, rfl⟩ := ha.symm

Premises used: Associated.symm, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
hi : Irreducible (Classical.choose (p := Prime) ⋯)
n : ℕ
u : Rˣ
h : ¬Classical.choose (p := Prime) ⋯ ^ n * (↑u : R) = 0
ha : Associated (Classical.choose (p := Prime) ⋯ ^ n * (↑u : R)) (Classical.choose (p := Prime) ⋯ ^ n)
mp : ¬Eq (α := ℕ∞) (↑n : ℕ∞) ⊤
⊢ ¬Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (Classical.choose (p := Prime) ⋯ ^ n * (↑u : R)) : ℕ∞)
      (⊤ : ℕ∞)

Tactic:
rw [mul_comm, addVal_def' u hi n]

Premises used: IsDiscreteValuationRing.addVal_def', mul_comm
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
hi : Irreducible (Classical.choose (p := Prime) ⋯)
n : ℕ
u : Rˣ
h : ¬Classical.choose (p := Prime) ⋯ ^ n * (↑u : R) = 0
ha : Associated (Classical.choose (p := Prime) ⋯ ^ n * (↑u : R)) (Classical.choose (p := Prime) ⋯ ^ n)
⊢ ¬Eq (α := ℕ∞) (↑n : ℕ∞) ⊤

Tactic:
nofun
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
hi : Irreducible (Classical.choose (p := Prime) ⋯)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) 0 : ℕ∞) (⊤ : ℕ∞)

Tactic:
addVal_zero

Premises used: IsDiscreteValuationRing.addVal_zero
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
hi : Irreducible (Classical.choose (p := Prime) ⋯)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) 0 : ℕ∞) (⊤ : ℕ∞)

Tactic:
exact addVal_zero

Premises used: IsDiscreteValuationRing.addVal_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
⊢ Prime (Classical.choose (p := Prime) ⋯)

Tactic:
have hp := Classical.choose_spec (exists_prime R)
-- 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) ⋯)
mp :
  LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞) →
    a ∣ b
mpr :
  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:
constructor