m : ℕ+
p : Nat.Primes
k : ℕ
⊢ Pow.pow (↑p) k ∣ m ↔ k ≤ Multiset.count p (factorMultiset m)
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ Pow.pow (↑p) k ∣ m ↔ k ≤ Multiset.count p (factorMultiset m)
intros
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ k • PrimeMultiset.ofPrime p ≤ factorMultiset m ↔ Multiset.replicate k p ≤ factorMultiset m
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ Pow.pow (↑p) k ∣ m ↔ k ≤ Multiset.count p (factorMultiset m)
rw [Multiset.le_count_iff_replicate_le, ← factorMultiset_le_iff, factorMultiset_pow,
  factorMultiset_ofPrime]
case a.h.e'_3.h
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ k • PrimeMultiset.ofPrime p = Multiset.replicate k p
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ k • PrimeMultiset.ofPrime p ≤ factorMultiset m ↔ Multiset.replicate k p ≤ factorMultiset m
congr! 2
case a.h.e'_3.h
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ ↑Multiset.card (k • PrimeMultiset.ofPrime p) = k ∧ ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p
case a.h.e'_3.h
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ k • PrimeMultiset.ofPrime p = Multiset.replicate k p
apply Multiset.eq_replicate.mpr
case a.h.e'_3.h.left
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ ↑Multiset.card (k • PrimeMultiset.ofPrime p) = k

case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p
case a.h.e'_3.h
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ ↑Multiset.card (k • PrimeMultiset.ofPrime p) = k ∧ ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p
constructor
no goals
case a.h.e'_3.h.left
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ ↑Multiset.card (k • PrimeMultiset.ofPrime p) = k
rw [Multiset.card_nsmul, PrimeMultiset.card_ofPrime, mul_one]
case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ k • PrimeMultiset.ofPrime p
⊢ q = p
case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p
intro q h
case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ Multiset.replicate k p
⊢ q = p
case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ k • PrimeMultiset.ofPrime p
⊢ q = p
rw [PrimeMultiset.ofPrime, Multiset.nsmul_singleton _ k] at h
no goals
case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ Multiset.replicate k p
⊢ q = p
exact Multiset.eq_of_mem_replicate h