case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p (factors (Associates.mk a0))
⊢ ∃ b, Associates.mk a0 = b ^ k
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
k : ℕ
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p (factors a)
⊢ ∃ b, a = b ^ k
obtain ⟨a0, hz, rfl⟩ := exists_non_zero_rep ha
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
⊢ ∃ b, Associates.mk a0 = b ^ k
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p (factors (Associates.mk a0))
⊢ ∃ b, Associates.mk a0 = b ^ k
rw [factors_mk a0 hz] at hk
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
hk' : ∀ (p : { a // Irreducible a }), p ∈ factors' a0 → k ∣ Multiset.count p (factors' a0)
⊢ ∃ b, Associates.mk a0 = b ^ k
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
⊢ ∃ b, Associates.mk a0 = b ^ k
have hk' : ∀ p, p ∈ factors' a0 → k ∣ (factors' a0).count p := by
  rintro p -
  have pp : p = ⟨p.val, p.2⟩ := by simp only [Subtype.coe_eta]
  rw [pp, ← count_some p.2]
  exact hk p.val p.2
case intro.intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
hk' : ∀ (p : { a // Irreducible a }), p ∈ factors' a0 → k ∣ Multiset.count p (factors' a0)
u : Multiset { a // Irreducible a }
hu : factors' a0 = k • u
⊢ ∃ b, Associates.mk a0 = b ^ k
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
hk' : ∀ (p : { a // Irreducible a }), p ∈ factors' a0 → k ∣ Multiset.count p (factors' a0)
⊢ ∃ b, Associates.mk a0 = b ^ k
obtain ⟨u, hu⟩ := Multiset.exists_smul_of_dvd_count _ hk'
case intro.intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
hk' : ∀ (p : { a // Irreducible a }), p ∈ factors' a0 → k ∣ Multiset.count p (factors' a0)
u : Multiset { a // Irreducible a }
hu : factors' a0 = k • u
⊢ Associates.mk a0 = FactorSet.prod ↑u ^ k
case intro.intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
hk' : ∀ (p : { a // Irreducible a }), p ∈ factors' a0 → k ∣ Multiset.count p (factors' a0)
u : Multiset { a // Irreducible a }
hu : factors' a0 = k • u
⊢ ∃ b, Associates.mk a0 = b ^ k
use FactorSet.prod (u : FactorSet α)
case intro.intro.intro.h
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
hk' : ∀ (p : { a // Irreducible a }), p ∈ factors' a0 → k ∣ Multiset.count p (factors' a0)
u : Multiset { a // Irreducible a }
hu : factors' a0 = k • u
⊢ factors (Associates.mk a0) = factors (FactorSet.prod ↑u ^ k)
case intro.intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
hk' : ∀ (p : { a // Irreducible a }), p ∈ factors' a0 → k ∣ Multiset.count p (factors' a0)
u : Multiset { a // Irreducible a }
hu : factors' a0 = k • u
⊢ Associates.mk a0 = FactorSet.prod ↑u ^ k
apply eq_of_factors_eq_factors
case intro.intro.intro.h
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
hk' : ∀ (p : { a // Irreducible a }), p ∈ factors' a0 → k ∣ Multiset.count p (factors' a0)
u : Multiset { a // Irreducible a }
hu : factors' a0 = k • u
⊢ some (k • u) = k • ↑u
case intro.intro.intro.h
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
hk' : ∀ (p : { a // Irreducible a }), p ∈ factors' a0 → k ∣ Multiset.count p (factors' a0)
u : Multiset { a // Irreducible a }
hu : factors' a0 = k • u
⊢ factors (Associates.mk a0) = factors (FactorSet.prod ↑u ^ k)
rw [pow_factors, prod_factors, factors_mk a0 hz, ← WithTop.some_eq_coe, hu]
no goals
case intro.intro.intro.h
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
hk' : ∀ (p : { a // Irreducible a }), p ∈ factors' a0 → k ∣ Multiset.count p (factors' a0)
u : Multiset { a // Irreducible a }
hu : factors' a0 = k • u
⊢ some (k • u) = k • ↑u
exact WithBot.coe_nsmul u k
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
p : { a // Irreducible a }
⊢ k ∣ Multiset.count p (factors' a0)
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
⊢ ∀ (p : { a // Irreducible a }), p ∈ factors' a0 → k ∣ Multiset.count p (factors' a0)
rintro p -
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
p : { a // Irreducible a }
pp : p = { val := ↑p, property := (_ : Irreducible ↑p) }
⊢ k ∣ Multiset.count p (factors' a0)
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
p : { a // Irreducible a }
⊢ k ∣ Multiset.count p (factors' a0)
have pp : p = ⟨p.val, p.2⟩ := by simp only [Subtype.coe_eta]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
p : { a // Irreducible a }
pp : p = { val := ↑p, property := (_ : Irreducible ↑p) }
⊢ k ∣ count (↑p) (some (factors' a0))
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
p : { a // Irreducible a }
pp : p = { val := ↑p, property := (_ : Irreducible ↑p) }
⊢ k ∣ Multiset.count p (factors' a0)
rw [pp, ← count_some p.2]
no goals
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
p : { a // Irreducible a }
pp : p = { val := ↑p, property := (_ : Irreducible ↑p) }
⊢ k ∣ count (↑p) (some (factors' a0))
exact hk p.val p.2
no goals
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
k : ℕ
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ count p ↑(factors' a0)
p : { a // Irreducible a }
⊢ p = { val := ↑p, property := (_ : Irreducible ↑p) }
simp only [Subtype.coe_eta]