case intro
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
⊢ HasUnitMulPowIrreducibleFactorization R
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
⊢ HasUnitMulPowIrreducibleFactorization R
obtain ⟨p, hp⟩ := h₁
case intro
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
⊢ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
case intro
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
⊢ HasUnitMulPowIrreducibleFactorization R
refine' ⟨p, hp, _⟩
case intro
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
⊢ ∃ n, Associated (p ^ n) x
case intro
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
⊢ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
intro x hx
case intro.intro
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
⊢ ∃ n, Associated (p ^ n) x
case intro
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
⊢ ∃ n, Associated (p ^ n) x
cases' WfDvdMonoid.exists_factors x hx with fx hfx
case intro.intro
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
⊢ Associated (p ^ ↑Multiset.card fx) x
case intro.intro
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
⊢ ∃ n, Associated (p ^ n) x
refine' ⟨Multiset.card fx, _⟩
case intro.intro
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associated (Multiset.prod fx) x
⊢ Associated (p ^ ↑Multiset.card fx) x
case intro.intro
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
⊢ Associated (p ^ ↑Multiset.card fx) x
have H := hfx.2
case intro.intro
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
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 (p ^ ↑Multiset.card fx) = Associates.mk x
case intro.intro
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associated (Multiset.prod fx) x
⊢ Associated (p ^ ↑Multiset.card fx) x
rw [← Associates.mk_eq_mk_iff_associated] at H⊢
case intro.intro
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
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.replicate (↑Multiset.card fx) (Associates.mk p)) =
    Multiset.prod (Multiset.map Associates.mk fx)
case intro.intro
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
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 (p ^ ↑Multiset.card fx) = Associates.mk x
rw [← H, ← Associates.prod_mk, Associates.mk_pow, ← Multiset.prod_replicate]
case intro.intro.e_a
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
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.replicate (↑Multiset.card fx) (Associates.mk p) = Multiset.map Associates.mk fx
case intro.intro
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
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.replicate (↑Multiset.card fx) (Associates.mk p)) =
    Multiset.prod (Multiset.map Associates.mk fx)
congr 1
case intro.intro.e_a
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
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 p)
case intro.intro.e_a
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
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.replicate (↑Multiset.card fx) (Associates.mk p) = Multiset.map Associates.mk fx
symm
case intro.intro.e_a
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
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 p
case intro.intro.e_a
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
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 p)
rw [Multiset.eq_replicate]
case intro.intro.e_a
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
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 p
case intro.intro.e_a
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
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 p
simp only [true_and_iff, and_imp, Multiset.card_map, eq_self_iff_true, Multiset.mem_map,
  exists_imp]
case intro.intro.e_a
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
q : R
hq : q ∈ fx
⊢ Associates.mk q = Associates.mk p
case intro.intro.e_a
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
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 p
rintro _ q hq rfl
case intro.intro.e_a
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
q : R
hq : q ∈ fx
⊢ Associated q p
case intro.intro.e_a
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
q : R
hq : q ∈ fx
⊢ Associates.mk q = Associates.mk p
rw [Associates.mk_eq_mk_iff_associated]
no goals
case intro.intro.e_a
R : Type u_1
inst✝² : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ (b : R), b ∈ fx → Irreducible b) ∧ Associated (Multiset.prod fx) x
H : Associates.mk (Multiset.prod fx) = Associates.mk x
q : R
hq : q ∈ fx
⊢ Associated q p
apply h₂ (hfx.1 _ hq) hp