-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem toUniqueFactorizationMonoid (hR : HasUnitMulPowIrreducibleFactorization R) :
    UniqueFactorizationMonoid R :=
  let p := Classical.choose hR
  let spec := Classical.choose_spec hR
  UniqueFactorizationMonoid.of_exists_prime_factors fun x hx => by
    use Multiset.replicate (Classical.choose (spec.2 hx)) p
    constructor
    · intro q hq
      have hpq := Multiset.eq_of_mem_replicate hq
      rw [hpq]
      refine ⟨spec.1.ne_zero, spec.1.not_unit, ?_⟩
      intro a b h
      by_cases ha : a = 0
      · rw [ha]
        simp only [true_or, dvd_zero]
      obtain ⟨m, u, rfl⟩ := spec.2 ha
      rw [mul_assoc, mul_left_comm, Units.dvd_mul_left] at h
      rw [Units.dvd_mul_right]
      by_cases hm : m = 0
      · simp only [hm, one_mul, pow_zero] at h ⊢
        right
        exact h
      left
      obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hm
      rw [pow_succ']
      apply dvd_mul_of_dvd_left dvd_rfl _
    · rw [Multiset.prod_replicate]
      exact Classical.choose_spec (spec.2 hx)

Proof state:
case h.right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
⊢ Associated (Multiset.replicate (Classical.choose ⋯) p).prod x

Tactic:
rw [Multiset.prod_replicate]

Result:
case h.right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
⊢ Associated (p ^ Classical.choose ⋯) x

Proof state:
case h.left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
⊢ ∀ (a b : R), p ∣ a * b → p ∣ a ∨ p ∣ b

Tactic:
intro a b h

Result:
case h.left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
a b : R
h : p ∣ a * b
⊢ p ∣ a ∨ p ∣ b

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h : p ∣ Classical.choose hR ^ m * b
ha : ¬Classical.choose hR ^ m * ↑u = 0
hm : ¬m = 0
⊢ p ∣ Classical.choose hR ^ m ∨ p ∣ b

Tactic:
left

Result:
case neg.h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h : p ∣ Classical.choose hR ^ m * b
ha : ¬Classical.choose hR ^ m * ↑u = 0
hm : ¬m = 0
⊢ p ∣ Classical.choose hR ^ m

Proof state:
case neg.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h : p ∣ Classical.choose hR ^ m * b
ha : ¬Classical.choose hR ^ m * ↑u = 0
⊢ p ∣ Classical.choose hR ^ m * ↑u ∨ p ∣ b

Tactic:
rw [Units.dvd_mul_right]

Result:
case neg.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h : p ∣ Classical.choose hR ^ m * b
ha : ¬Classical.choose hR ^ m * ↑u = 0
⊢ p ∣ Classical.choose hR ^ m ∨ p ∣ b

Proof state:
case neg.h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h : p ∣ Classical.choose hR ^ m * b
ha : ¬Classical.choose hR ^ m * ↑u = 0
hm : ¬m = 0
⊢ p ∣ Classical.choose hR ^ m

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hm

Result:
case neg.h.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
u : Rˣ
m : ℕ
h : p ∣ Classical.choose hR ^ m.succ * b
ha : ¬Classical.choose hR ^ m.succ * ↑u = 0
hm : ¬m.succ = 0
⊢ p ∣ Classical.choose hR ^ m.succ

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod x

Tactic:
use Multiset.replicate (Classical.choose (spec.2 hx)) p

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
⊢ (∀ b ∈ Multiset.replicate (Classical.choose ⋯) p, Prime b) ∧
    Associated (Multiset.replicate (Classical.choose ⋯) p).prod x

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
a b : R
h : p ∣ a * b
ha : a = 0
⊢ p ∣ 0 ∨ p ∣ b

Tactic:
simp only [true_or, dvd_zero]

Result:
no goals

Proof state:
case h.left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
⊢ Prime q

Tactic:
have hpq := Multiset.eq_of_mem_replicate hq

Result:
case h.left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
⊢ Prime q