awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) r : ℕ∞) ((↑n : ℕ∞) : ℕ∞)
have rw₅ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑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ϖ)]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) r : ℕ∞) ((↑n : ℕ∞) : ℕ∞)
have rw : Eq (α := ℕ∞)
  (((multiplicity_addValuation (p := Classical.choose (p := Prime) sorry) sorry : 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ϖ)]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞) : ℕ∞)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) r : ℕ∞) ((↑n : ℕ∞) : ℕ∞)
have rw₁ : emultiplicity (Classical.choose (p := Prime) sorry) 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ϖ)]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) r : ℕ∞) ((↑n : ℕ∞) : ℕ∞)
have rw₂ : emultiplicity (Classical.choose (p := Prime) sorry) ((↑u : R) * ϖ ^ n) = (↑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ϖ)]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) r : ℕ∞) ((↑n : ℕ∞) : ℕ∞)
have rw₃ : emultiplicity ϖ ((↑u : R) * ϖ ^ n) = (↑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ϖ)]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) r : ℕ∞) ((↑n : ℕ∞) : ℕ∞)
have rw₄ : emultiplicity ϖ (ϖ ^ n) = (↑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ϖ)]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) r : ℕ∞) ((↑n : ℕ∞) : ℕ∞)
have rw₅ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑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ϖ)]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
ϖ : R
h : Irreducible ϖ
n : ℕ
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (ϖ ^ n) : ℕ∞) ((↑n : ℕ∞) : ℕ∞)
have rw : HSMul.hSMul (β := ℕ∞) n (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ϖ : ℕ∞) = (↑n : ℕ∞)
Tactic: rw [addVal_pow, addVal_uniformizer h, nsmul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (ϖ ^ n) : ℕ∞) ((↑n : ℕ∞) : ℕ∞)
have rw₁ : HSMul.hSMul (β := ℕ∞) n 1 = (↑n : ℕ∞)
Tactic: rw [addVal_pow, addVal_uniformizer h, nsmul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (ϖ ^ n) : ℕ∞) ((↑n : ℕ∞) : ℕ∞)
have rw₂ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
Tactic: rw [addVal_pow, addVal_uniformizer h, nsmul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a : R
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞) ↔ a = 0
have hi : Irreducible (Classical.choose (p := Prime) sorry)
Tactic: have hi := (Classical.choose_spec (exists_prime R)).irreducible
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a : R
hi : Irreducible (Classical.choose (p := Prime) ⋯)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞) ↔ a = 0
have mp : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞) → a = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞) ↔ a = 0
have mpr : a = 0 → Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a : R
hi : Irreducible (Classical.choose (p := Prime) ⋯)
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞) → a = 0
have mp : ¬a = 0 → ¬Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞)
Tactic: contrapose
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ ¬Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞)
have mp : ∀ (n : ℕ) (ha : Associated a (Classical.choose (p := Prime) sorry ^ n)),
  ¬Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞)
Tactic: obtain ⟨n, ha⟩ := associated_pow_irreducible h hi
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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)
⊢ ¬Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞) (⊤ : ℕ∞)
have mp : ∀ (u : Rˣ) (h : ¬Classical.choose (p := Prime) sorry ^ n * (↑u : R) = 0)
  (ha : Associated (Classical.choose (p := Prime) sorry ^ n * (↑u : R)) (Classical.choose (p := Prime) sorry ^ n)),
  ¬Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (Classical.choose (p := Prime) sorry ^ n * (↑u : R)) : ℕ∞)
      (⊤ : ℕ∞)
Tactic: obtain ⟨u, rfl⟩ := ha.symm
Cleared hypotheses: a, h, ha
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (Classical.choose (p := Prime) ⋯ ^ n * (↑u : R)) : ℕ∞)
      (⊤ : ℕ∞)
have mp : ¬Eq (α := ℕ∞) (↑n : ℕ∞) ⊤
Tactic: rw [mul_comm, addVal_def' u hi n]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
⊢ LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞) ↔
    a ∣ b
have hp : Prime (Classical.choose (p := Prime) sorry)
Tactic: have hp := Classical.choose_spec (exists_prime R)
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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) ⋯)
⊢ LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞) ↔
    a ∣ b
have mp : LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞) →
  a ∣ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞) ↔
    a ∣ b
have mpr : a ∣ b →
  LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞)
⊢ a ∣ b
have pos : ∀ (ha0 : a = 0), a ∣ b
Tactic: by_cases ha0 : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ a ∣ b
have neg : ∀ (ha0 : ¬a = 0), a ∣ b
Tactic: by_cases ha0 : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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
⊢ a ∣ b
have h₁ : b = 0
Tactic: rw [ha0, addVal_zero, top_le_iff, addVal_eq_top_iff] at h
Cleared hypotheses: h, ha0
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 ∣ b
have pos : a ∣ 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ a ∣ b
have neg : ∀ (n : ℕ) (ha : Associated a (Classical.choose (p := Prime) sorry ^ n)), a ∣ b
Tactic: obtain ⟨n, ha⟩ := associated_pow_irreducible ha0 hp.irreducible
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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)
⊢ a ∣ b
have neg : ∀ (h : ∀ (n : ℕ), Classical.choose (p := Prime) sorry ^ n ∣ a → Classical.choose (p := Prime) sorry ^ n ∣ b) (ha0 : ¬a = 0)
  (n : ℕ) (ha : Associated a (Classical.choose (p := Prime) sorry ^ n)), a ∣ b
Tactic: rw [addVal, multiplicity_addValuation_apply, multiplicity_addValuation_apply,
      emultiplicity_le_emultiplicity_iff] at h
Cleared hypotheses: h, ha0, n, ha
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
a b : R
⊢ LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞) ↔
    a ∣ b
have have : ∀ (hp : Prime (Classical.choose (p := Prime) sorry)),
  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
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞) ↔
    a ∣ b
have mp : ∀ (hp : Prime (Classical.choose (p := Prime) sorry))
  (h :
    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
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) b : ℕ∞) ↔
    a ∣ b
have mpr : ∀ (hp : Prime (Classical.choose (p := Prime) sorry)) (h : a ∣ b),
  LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) a : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) 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
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
u : Rˣ
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (↑u : R) : ℕ∞) (0 : ℕ∞)
have obtain : ∀ (ϖ : R) (hϖ : Irreducible ϖ), Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (↑u : R) : ℕ∞) (0 : ℕ∞)
Tactic: obtain ⟨ϖ, hϖ⟩ := exists_irreducible R
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (↑u : R) : ℕ∞) (0 : ℕ∞)
have rw : Eq (α := ℕ∞) (↑0 : ℕ∞) 0
Tactic: rw [addVal_def (u : R) u hϖ 0]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (↑u : R) : ℕ∞) (0 : ℕ∞)
have rw₁ : (↑u : R) = (↑u : R) * HPow.hPow (β := ℕ) ϖ 0
Tactic: rw [addVal_def (u : R) u hϖ 0]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (0 : ℕ∞) ↔ IsUnit x
have inl : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) 0 : ℕ∞) (0 : ℕ∞) ↔ IsUnit.{u_1} (M := R) 0
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (0 : ℕ∞) ↔ IsUnit x
have inr : ∀ (hx : x ≠ 0), Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (0 : ℕ∞) ↔ IsUnit x
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
⊢ Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (0 : ℕ∞) ↔ IsUnit x
have inr : ∀ (ϖ : R) (hϖ : Irreducible ϖ),
  Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (0 : ℕ∞) ↔ IsUnit x
Tactic: obtain ⟨ϖ, hϖ⟩ := exists_irreducible R