R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
key : Associated (Multiset.prod (Multiset.replicate m p)) (Multiset.prod (Multiset.replicate n q))
⊢ m = n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ m = n
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]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
key : Associated (Multiset.prod (Multiset.replicate m p)) (Multiset.prod (Multiset.replicate n q))
this : ↑Multiset.card (Multiset.replicate m p) = ↑Multiset.card (Multiset.replicate n q)
⊢ m = n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
key : Associated (Multiset.prod (Multiset.replicate m p)) (Multiset.prod (Multiset.replicate n q))
⊢ m = n
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
no goals
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
key : Associated (Multiset.prod (Multiset.replicate m p)) (Multiset.prod (Multiset.replicate n q))
this : ↑Multiset.card (Multiset.replicate m p) = ↑Multiset.card (Multiset.replicate n q)
⊢ m = n
simpa only [Multiset.card_replicate]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ ∃ u, p ^ m * ↑u = q ^ n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ Associated (Multiset.prod (Multiset.replicate m p)) (Multiset.prod (Multiset.replicate n q))
rw [Multiset.prod_replicate, Multiset.prod_replicate, Associated]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ p ^ m * ↑(u * v⁻¹) = q ^ n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ ∃ u, p ^ m * ↑u = q ^ n
refine' ⟨u * v⁻¹, _⟩
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ p ^ m * (↑u * ↑v⁻¹) = q ^ n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ p ^ m * ↑(u * v⁻¹) = q ^ n
simp only [Units.val_mul]
no goals
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ p ^ m * (↑u * ↑v⁻¹) = q ^ n
rw [mul_left_comm, ← mul_assoc, h, mul_right_comm, Units.mul_inv, one_mul]
case refine'_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
key : Associated (Multiset.prod (Multiset.replicate m p)) (Multiset.prod (Multiset.replicate n q))
⊢ ∀ (x : R), x ∈ Multiset.replicate m p → Irreducible x

case refine'_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
key : Associated (Multiset.prod (Multiset.replicate m p)) (Multiset.prod (Multiset.replicate n q))
⊢ ∀ (x : R), x ∈ Multiset.replicate n q → Irreducible x
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
key : Associated (Multiset.prod (Multiset.replicate m p)) (Multiset.prod (Multiset.replicate n q))
⊢ ?m.265183
refine' Multiset.card_eq_card_of_rel (UniqueFactorizationMonoid.factors_unique _ _ key)
no goals
case refine'_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
key : Associated (Multiset.prod (Multiset.replicate m p)) (Multiset.prod (Multiset.replicate n q))
⊢ ∀ (x : R), x ∈ Multiset.replicate m p → Irreducible x

case refine'_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
key : Associated (Multiset.prod (Multiset.replicate m p)) (Multiset.prod (Multiset.replicate n q))
⊢ ∀ (x : R), x ∈ Multiset.replicate n q → Irreducible x
all_goals
  intro x hx
  obtain rfl := Multiset.eq_of_mem_replicate hx
  assumption
case refine'_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
key : Associated (Multiset.prod (Multiset.replicate m p)) (Multiset.prod (Multiset.replicate n q))
x : R
hx : x ∈ Multiset.replicate n q
⊢ Irreducible x
case refine'_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
key : Associated (Multiset.prod (Multiset.replicate m p)) (Multiset.prod (Multiset.replicate n q))
⊢ ∀ (x : R), x ∈ Multiset.replicate n q → Irreducible x
intro x hx
case refine'_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p : R
hp : Irreducible p
u v : Rˣ
m n : ℕ
x : R
hq : Irreducible x
h : ↑u * p ^ m = ↑v * x ^ n
key : Associated (Multiset.prod (Multiset.replicate m p)) (Multiset.prod (Multiset.replicate n x))
hx : x ∈ Multiset.replicate n x
⊢ Irreducible x
case refine'_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
key : Associated (Multiset.prod (Multiset.replicate m p)) (Multiset.prod (Multiset.replicate n q))
x : R
hx : x ∈ Multiset.replicate n q
⊢ Irreducible x
obtain rfl := Multiset.eq_of_mem_replicate hx
no goals
case refine'_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
p : R
hp : Irreducible p
u v : Rˣ
m n : ℕ
x : R
hq : Irreducible x
h : ↑u * p ^ m = ↑v * x ^ n
key : Associated (Multiset.prod (Multiset.replicate m p)) (Multiset.prod (Multiset.replicate n x))
hx : x ∈ Multiset.replicate n x
⊢ Irreducible x
assumption