R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u * ϖ ^ m = ↑v * ϖ ^ m
⊢ u = v
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m n : ℕ
h : ↑u * ϖ ^ m = ↑v * ϖ ^ n
⊢ u = v
obtain rfl : m = n := unit_mul_pow_congr_pow hirr hirr u v m n h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h✝ : ↑u * ϖ ^ m = ↑v * ϖ ^ m
h : ↑u * ϖ ^ m - ↑v * ϖ ^ m = 0
⊢ u = v
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u * ϖ ^ m = ↑v * ϖ ^ m
⊢ u = v
rw [← sub_eq_zero] at h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h✝ : ↑u * ϖ ^ m = ↑v * ϖ ^ m
h : ↑u - ↑v = 0 ∨ ϖ ^ m = 0
⊢ u = v
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h✝ : ↑u * ϖ ^ m = ↑v * ϖ ^ m
h : ↑u * ϖ ^ m - ↑v * ϖ ^ m = 0
⊢ u = v
rw [← sub_mul, mul_eq_zero] at h
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h✝ : ↑u * ϖ ^ m = ↑v * ϖ ^ m
h : ↑u - ↑v = 0
⊢ u = v

case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h✝ : ↑u * ϖ ^ m = ↑v * ϖ ^ m
h : ϖ ^ m = 0
⊢ u = v
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h✝ : ↑u * ϖ ^ m = ↑v * ϖ ^ m
h : ↑u - ↑v = 0 ∨ ϖ ^ m = 0
⊢ u = v
cases' h with h h
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h✝ : ↑u * ϖ ^ m = ↑v * ϖ ^ m
h : ↑u = ↑v
⊢ u = v
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h✝ : ↑u * ϖ ^ m = ↑v * ϖ ^ m
h : ↑u - ↑v = 0
⊢ u = v
rw [sub_eq_zero] at h
no goals
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h✝ : ↑u * ϖ ^ m = ↑v * ϖ ^ m
h : ↑u = ↑v
⊢ u = v
exact_mod_cast h
no goals
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h✝ : ↑u * ϖ ^ m = ↑v * ϖ ^ m
h : ϖ ^ m = 0
⊢ u = v
apply (hirr.ne_zero (pow_eq_zero h)).elim