R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
⊢ ∃ n, Associated x (ϖ ^ n)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
⊢ ∃ n, Associated x (ϖ ^ n)
have : WfDvdMonoid R := IsNoetherianRing.wfDvdMonoid
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
⊢ ∃ n, Associated x (ϖ ^ n)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
⊢ ∃ n, Associated x (ϖ ^ n)
cases' WfDvdMonoid.exists_factors x hx with fx hfx
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
⊢ Associated x (ϖ ^ ↑Multiset.card fx)
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
⊢ ∃ n, Associated x (ϖ ^ n)
use Multiset.card fx
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associated (Multiset.prod fx) x
⊢ Associated x (ϖ ^ ↑Multiset.card fx)
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
⊢ Associated x (ϖ ^ ↑Multiset.card fx)
have H := hfx.2
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
⊢ Associates.mk x = Associates.mk (ϖ ^ ↑Multiset.card fx)
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associated (Multiset.prod fx) x
⊢ Associated x (ϖ ^ ↑Multiset.card fx)
rw [← Associates.mk_eq_mk_iff_associated] at H⊢
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
⊢ Multiset.prod (Multiset.map Associates.mk fx) =
    Multiset.prod (Multiset.replicate (↑Multiset.card fx) (Associates.mk ϖ))
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
⊢ Associates.mk x = Associates.mk (ϖ ^ ↑Multiset.card fx)
rw [← H, ← Associates.prod_mk, Associates.mk_pow, ← Multiset.prod_replicate]
case intro.e_a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
⊢ Multiset.map Associates.mk fx = Multiset.replicate (↑Multiset.card fx) (Associates.mk ϖ)
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
⊢ Multiset.prod (Multiset.map Associates.mk fx) =
    Multiset.prod (Multiset.replicate (↑Multiset.card fx) (Associates.mk ϖ))
congr 1
case intro.e_a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
⊢ ↑Multiset.card (Multiset.map Associates.mk fx) = ↑Multiset.card fx ∧
    ∀ (b : Associates R), b ∈ Multiset.map Associates.mk fx → b = Associates.mk ϖ
case intro.e_a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
⊢ Multiset.map Associates.mk fx = Multiset.replicate (↑Multiset.card fx) (Associates.mk ϖ)
rw [Multiset.eq_replicate]
case intro.e_a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
⊢ ∀ (b : Associates R) (x : R), x ∈ fx → Associates.mk x = b → b = Associates.mk ϖ
case intro.e_a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
⊢ ↑Multiset.card (Multiset.map Associates.mk fx) = ↑Multiset.card fx ∧
    ∀ (b : Associates R), b ∈ Multiset.map Associates.mk fx → b = Associates.mk ϖ
simp only [true_and_iff, and_imp, Multiset.card_map, eq_self_iff_true, Multiset.mem_map,
  exists_imp]
case intro.e_a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
x✝ : R
a✝ : x✝ ∈ fx
⊢ Associates.mk x✝ = Associates.mk ϖ
case intro.e_a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
⊢ ∀ (b : Associates R) (x : R), x ∈ fx → Associates.mk x = b → b = Associates.mk ϖ
rintro _ _ _ rfl
case intro.e_a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
x✝ : R
a✝ : x✝ ∈ fx
⊢ Associated x✝ ϖ
case intro.e_a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
x✝ : R
a✝ : x✝ ∈ fx
⊢ Associates.mk x✝ = Associates.mk ϖ
rw [Associates.mk_eq_mk_iff_associated]
case intro.e_a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
x✝ : R
a✝ : x✝ ∈ fx
⊢ Irreducible x✝
case intro.e_a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
x✝ : R
a✝ : x✝ ∈ fx
⊢ Associated x✝ ϖ
refine' associated_of_irreducible _ _ hirr
case intro.e_a.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
x✝ : R
a✝ : x✝ ∈ fx
⊢ x✝ ∈ fx
case intro.e_a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
x✝ : R
a✝ : x✝ ∈ fx
⊢ Irreducible x✝
apply hfx.1
no goals
case intro.e_a.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
x✝ : R
a✝ : x✝ ∈ fx
⊢ x✝ ∈ fx
assumption