[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
hn : IsPrimePow n
⊢ Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
[PROOFSTEP]
obtain ⟨p, k, hp, hk, rfl⟩ := hn
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Prime p
hk : 0 < k
⊢ Nat.minFac (p ^ k) ^ ↑(Nat.factorization (p ^ k)) (Nat.minFac (p ^ k)) = p ^ k
[PROOFSTEP]
rw [← Nat.prime_iff] at hp 
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ Nat.minFac (p ^ k) ^ ↑(Nat.factorization (p ^ k)) (Nat.minFac (p ^ k)) = p ^ k
[PROOFSTEP]
rw [hp.pow_minFac hk.ne', hp.factorization_pow, Finsupp.single_eq_same]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
hn : n ≠ 1
⊢ IsPrimePow n
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn')
[GOAL]
case inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k : ℕ
h : Nat.minFac 0 ^ ↑(Nat.factorization 0) (Nat.minFac 0) = 0
hn : 0 ≠ 1
⊢ IsPrimePow 0
[PROOFSTEP]
simp_all
[GOAL]
case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ IsPrimePow n
[PROOFSTEP]
refine' ⟨_, _, (Nat.minFac_prime hn).prime, _, h⟩
[GOAL]
case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ 0 < ↑(Nat.factorization n) (Nat.minFac n)
[PROOFSTEP]
rw [pos_iff_ne_zero, ← Finsupp.mem_support_iff, Nat.factor_iff_mem_factorization,
  Nat.mem_factors_iff_dvd hn' (Nat.minFac_prime hn)]
[GOAL]
case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ Nat.minFac n ∣ n
[PROOFSTEP]
apply Nat.minFac_dvd
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ IsPrimePow n ↔ ∃ p k, 0 < k ∧ Nat.factorization n = Finsupp.single p k
[PROOFSTEP]
rw [isPrimePow_nat_iff]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p k, 0 < k ∧ Nat.factorization n = Finsupp.single p k
[PROOFSTEP]
refine' exists₂_congr fun p k => _
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n ↔ 0 < k ∧ Nat.factorization n = Finsupp.single p k
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n → 0 < k ∧ Nat.factorization n = Finsupp.single p k
[PROOFSTEP]
rintro ⟨hp, hk, hn⟩
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : p ^ k = n
⊢ 0 < k ∧ Nat.factorization n = Finsupp.single p k
[PROOFSTEP]
exact ⟨hk, by rw [← hn, Nat.Prime.factorization_pow hp]⟩
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : p ^ k = n
⊢ Nat.factorization n = Finsupp.single p k
[PROOFSTEP]
rw [← hn, Nat.Prime.factorization_pow hp]
[GOAL]
case mpr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
⊢ 0 < k ∧ Nat.factorization n = Finsupp.single p k → Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rintro ⟨hk, hn⟩
[GOAL]
case mpr.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
hk : 0 < k
hn : Nat.factorization n = Finsupp.single p k
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
have hn0 : n ≠ 0 := by
  rintro rfl
  simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
hk : 0 < k
hn : Nat.factorization n = Finsupp.single p k
⊢ n ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hk : 0 < k
hn : Nat.factorization 0 = Finsupp.single p k
⊢ False
[PROOFSTEP]
simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']
[GOAL]
case mpr.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
hk : 0 < k
hn : Nat.factorization n = Finsupp.single p k
hn0 : n ≠ 0
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rw [Nat.eq_pow_of_factorization_eq_single hn0 hn]
[GOAL]
case mpr.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
hk : 0 < k
hn : Nat.factorization n = Finsupp.single p k
hn0 : n ≠ 0
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = p ^ k
[PROOFSTEP]
exact ⟨Nat.prime_of_mem_factorization (by simp [hn, hk.ne'] : p ∈ n.factorization.support), hk, rfl⟩
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
hk : 0 < k
hn : Nat.factorization n = Finsupp.single p k
hn0 : n ≠ 0
⊢ p ∈ (Nat.factorization n).support
[PROOFSTEP]
simp [hn, hk.ne']
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ IsPrimePow n ↔ Finset.card (Nat.factorization n).support = 1
[PROOFSTEP]
simp_rw [isPrimePow_iff_factorization_eq_single, Finsupp.card_support_eq_one', exists_prop, pos_iff_ne_zero]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : IsPrimePow n
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn0)
[GOAL]
case inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k : ℕ
h : IsPrimePow 0
⊢ ∃ p, Nat.Prime p ∧ 0 / p ^ ↑(Nat.factorization 0) p = 1
[PROOFSTEP]
cases not_isPrimePow_zero h
[GOAL]
case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
[PROOFSTEP]
rcases isPrimePow_iff_factorization_eq_single.mp h with ⟨p, k, hk0, h1⟩
[GOAL]
case inr.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
[PROOFSTEP]
rcases em' p.Prime with (pp | pp)
[GOAL]
case inr.intro.intro.intro.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
[PROOFSTEP]
refine' absurd _ hk0.ne'
[GOAL]
case inr.intro.intro.intro.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ k = 0
[PROOFSTEP]
simp [← Nat.factorization_eq_zero_of_non_prime n pp, h1]
[GOAL]
case inr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
[PROOFSTEP]
refine' ⟨p, pp, _⟩
[GOAL]
case inr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
⊢ n / p ^ ↑(Nat.factorization n) p = 1
[PROOFSTEP]
refine' Nat.eq_of_factorization_eq (Nat.ord_compl_pos p hn0).ne' (by simp) fun q => _
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
⊢ 1 ≠ 0
[PROOFSTEP]
simp
[GOAL]
case inr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
q : ℕ
⊢ ↑(Nat.factorization (n / p ^ ↑(Nat.factorization n) p)) q = ↑(Nat.factorization 1) q
[PROOFSTEP]
rw [Nat.factorization_ord_compl n p, h1]
[GOAL]
case inr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : Nat.factorization n = Finsupp.single p k
pp : Nat.Prime p
q : ℕ
⊢ ↑(Finsupp.erase p (Finsupp.single p k)) q = ↑(Nat.factorization 1) q
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
hn : n ≠ 1
⊢ IsPrimePow n ↔ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
[PROOFSTEP]
refine' ⟨fun h => IsPrimePow.exists_ord_compl_eq_one h, fun h => _⟩
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
hn : n ≠ 1
h : ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
⊢ IsPrimePow n
[PROOFSTEP]
rcases h with ⟨p, pp, h⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ IsPrimePow n
[PROOFSTEP]
rw [isPrimePow_nat_iff]
[GOAL]
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rw [← Nat.eq_of_dvd_of_div_eq_one (Nat.ord_proj_dvd n p) h] at hn ⊢
[GOAL]
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hn : p ^ ↑(Nat.factorization n) p ≠ 1
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ ∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ ↑(Nat.factorization n) p
[PROOFSTEP]
refine' ⟨p, n.factorization p, pp, _, by simp⟩
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hn : p ^ ↑(Nat.factorization n) p ≠ 1
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ p ^ ↑(Nat.factorization n) p = p ^ ↑(Nat.factorization n) p
[PROOFSTEP]
simp
[GOAL]
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hn : p ^ ↑(Nat.factorization n) p ≠ 1
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ 0 < ↑(Nat.factorization n) p
[PROOFSTEP]
contrapose! hn
[GOAL]
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
hn : ↑(Nat.factorization n) p ≤ 0
⊢ p ^ ↑(Nat.factorization n) p = 1
[PROOFSTEP]
simp [le_zero_iff.1 hn]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ IsPrimePow n ↔ ∃! p, Nat.Prime p ∧ p ∣ n
[PROOFSTEP]
rw [isPrimePow_nat_iff]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃! p, Nat.Prime p ∧ p ∣ n
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃! p, Nat.Prime p ∧ p ∣ n
[PROOFSTEP]
rintro ⟨p, k, hp, hk, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ∃! p_1, Nat.Prime p_1 ∧ p_1 ∣ p ^ k
[PROOFSTEP]
refine' ⟨p, ⟨hp, dvd_pow_self _ hk.ne'⟩, _⟩
[GOAL]
case mp.intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ∀ (y : ℕ), (fun p_1 => Nat.Prime p_1 ∧ p_1 ∣ p ^ k) y → y = p
[PROOFSTEP]
rintro q ⟨hq, hq'⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
q : ℕ
hq : Nat.Prime q
hq' : q ∣ p ^ k
⊢ q = p
[PROOFSTEP]
exact (Nat.prime_dvd_prime_iff_eq hq hp).1 (hq.dvd_of_dvd_pow hq')
[GOAL]
case mpr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ (∃! p, Nat.Prime p ∧ p ∣ n) → ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rintro ⟨p, ⟨hp, hn⟩, hq⟩
[GOAL]
case mpr.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn₀)
[GOAL]
case mpr.intro.intro.intro.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k p : ℕ
hp : Nat.Prime p
hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ 0) y → y = p
hn : p ∣ 0
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = 0
[PROOFSTEP]
cases (hq 2 ⟨Nat.prime_two, dvd_zero 2⟩).trans (hq 3 ⟨Nat.prime_three, dvd_zero 3⟩).symm
[GOAL]
case mpr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
refine' ⟨p, n.factorization p, hp, hp.factorization_pos_of_dvd hn₀ hn, _⟩
[GOAL]
case mpr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hq : ∀ (y : ℕ), (fun p => Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
⊢ p ^ ↑(Nat.factorization n) p = n
[PROOFSTEP]
simp only [and_imp] at hq 
[GOAL]
case mpr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ p ^ ↑(Nat.factorization n) p = n
[PROOFSTEP]
apply
  Nat.dvd_antisymm
    (Nat.ord_proj_dvd _ _)
      -- We need to show n ∣ p ^ n.factorization p
[GOAL]
case mpr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ n ∣ p ^ ↑(Nat.factorization n) p
[PROOFSTEP]
apply Nat.dvd_of_factors_subperm hn₀
[GOAL]
case mpr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ Nat.factors n <+~ Nat.factors (p ^ ↑(Nat.factorization n) p)
[PROOFSTEP]
rw [hp.factors_pow, List.subperm_ext_iff]
[GOAL]
case mpr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ ∀ (x : ℕ),
    x ∈ Nat.factors n → List.count x (Nat.factors n) ≤ List.count x (List.replicate (↑(Nat.factorization n) p) p)
[PROOFSTEP]
intro q hq'
[GOAL]
case mpr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : q ∈ Nat.factors n
⊢ List.count q (Nat.factors n) ≤ List.count q (List.replicate (↑(Nat.factorization n) p) p)
[PROOFSTEP]
rw [Nat.mem_factors hn₀] at hq' 
[GOAL]
case mpr.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : Nat.Prime q ∧ q ∣ n
⊢ List.count q (Nat.factors n) ≤ List.count q (List.replicate (↑(Nat.factorization n) p) p)
[PROOFSTEP]
cases hq _ hq'.1 hq'.2
[GOAL]
case mpr.intro.intro.intro.inr.refl
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
hq' : Nat.Prime p ∧ p ∣ n
⊢ List.count p (Nat.factors n) ≤ List.count p (List.replicate (↑(Nat.factorization n) p) p)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k✝ n k : ℕ
hk : k ≠ 0
⊢ IsPrimePow (n ^ k) ↔ IsPrimePow n
[PROOFSTEP]
simp only [isPrimePow_iff_unique_prime_dvd]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k✝ n k : ℕ
hk : k ≠ 0
⊢ (∃! p, Nat.Prime p ∧ p ∣ n ^ k) ↔ ∃! p, Nat.Prime p ∧ p ∣ n
[PROOFSTEP]
apply exists_unique_congr
[GOAL]
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k✝ n k : ℕ
hk : k ≠ 0
⊢ ∀ (a : ℕ), Nat.Prime a ∧ a ∣ n ^ k ↔ Nat.Prime a ∧ a ∣ n
[PROOFSTEP]
simp only [and_congr_right_iff]
[GOAL]
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k✝ n k : ℕ
hk : k ≠ 0
⊢ ∀ (a : ℕ), Nat.Prime a → (a ∣ n ^ k ↔ a ∣ n)
[PROOFSTEP]
intro p hp
[GOAL]
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n k : ℕ
hk : k ≠ 0
p : ℕ
hp : Nat.Prime p
⊢ p ∣ n ^ k ↔ p ∣ n
[PROOFSTEP]
exact ⟨hp.dvd_of_dvd_pow, fun t => t.trans (dvd_pow_self _ hk)⟩
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a b : ℕ
hab : coprime a b
hn : IsPrimePow n
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n b : ℕ
hn : IsPrimePow n
hab : coprime 0 b
⊢ n ∣ 0 * b ↔ n ∣ 0 ∨ n ∣ b
[PROOFSTEP]
simp only [Nat.coprime_zero_left] at hab 
[GOAL]
case inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n b : ℕ
hn : IsPrimePow n
hab : b = 1
⊢ n ∣ 0 * b ↔ n ∣ 0 ∨ n ∣ b
[PROOFSTEP]
simp [hab, Finset.filter_singleton, not_isPrimePow_one]
[GOAL]
case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a b : ℕ
hab : coprime a b
hn : IsPrimePow n
ha : a ≠ 0
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | hb)
[GOAL]
case inr.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a : ℕ
hn : IsPrimePow n
ha : a ≠ 0
hab : coprime a 0
⊢ n ∣ a * 0 ↔ n ∣ a ∨ n ∣ 0
[PROOFSTEP]
simp only [Nat.coprime_zero_right] at hab 
[GOAL]
case inr.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a : ℕ
hn : IsPrimePow n
ha : a ≠ 0
hab : a = 1
⊢ n ∣ a * 0 ↔ n ∣ a ∨ n ∣ 0
[PROOFSTEP]
simp [hab, Finset.filter_singleton, not_isPrimePow_one]
[GOAL]
case inr.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a b : ℕ
hab : coprime a b
hn : IsPrimePow n
ha : a ≠ 0
hb : b ≠ 0
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
[PROOFSTEP]
refine'
  ⟨_, fun h =>
    Or.elim h (fun i => i.trans ((@dvd_mul_right a b a hab).mpr (dvd_refl a))) fun i =>
      i.trans ((@dvd_mul_left a b b hab.symm).mpr (dvd_refl b))⟩
[GOAL]
case inr.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n a b : ℕ
hab : coprime a b
hn : IsPrimePow n
ha : a ≠ 0
hb : b ≠ 0
⊢ n ∣ a * b → n ∣ a ∨ n ∣ b
[PROOFSTEP]
obtain ⟨p, k, hp, _, rfl⟩ := (isPrimePow_nat_iff _).1 hn
[GOAL]
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ p ^ k ∣ a * b → p ^ k ∣ a ∨ p ^ k ∣ b
[PROOFSTEP]
simp only [hp.pow_dvd_iff_le_factorization (mul_ne_zero ha hb), Nat.factorization_mul ha hb,
  hp.pow_dvd_iff_le_factorization ha, hp.pow_dvd_iff_le_factorization hb, Pi.add_apply, Finsupp.coe_add]
[GOAL]
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ k ≤ ↑(factorization a) p + ↑(factorization b) p → k ≤ ↑(factorization a) p ∨ k ≤ ↑(factorization b) p
[PROOFSTEP]
have : a.factorization p = 0 ∨ b.factorization p = 0 :=
  by
  rw [← Finsupp.not_mem_support_iff, ← Finsupp.not_mem_support_iff, ← not_and_or, ← Finset.mem_inter]
  intro t
  simpa using (Nat.factorization_disjoint_of_coprime hab).le_bot t
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ ↑(factorization a) p = 0 ∨ ↑(factorization b) p = 0
[PROOFSTEP]
rw [← Finsupp.not_mem_support_iff, ← Finsupp.not_mem_support_iff, ← not_and_or, ← Finset.mem_inter]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ ¬p ∈ (factorization a).support ∩ (factorization b).support
[PROOFSTEP]
intro t
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
t : p ∈ (factorization a).support ∩ (factorization b).support
⊢ False
[PROOFSTEP]
simpa using (Nat.factorization_disjoint_of_coprime hab).le_bot t
[GOAL]
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
this : ↑(factorization a) p = 0 ∨ ↑(factorization b) p = 0
⊢ k ≤ ↑(factorization a) p + ↑(factorization b) p → k ≤ ↑(factorization a) p ∨ k ≤ ↑(factorization b) p
[PROOFSTEP]
cases' this with h h
[GOAL]
case inr.inr.intro.intro.intro.intro.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
h : ↑(factorization a) p = 0
⊢ k ≤ ↑(factorization a) p + ↑(factorization b) p → k ≤ ↑(factorization a) p ∨ k ≤ ↑(factorization b) p
[PROOFSTEP]
simp [h, imp_or]
[GOAL]
case inr.inr.intro.intro.intro.intro.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
h : ↑(factorization b) p = 0
⊢ k ≤ ↑(factorization a) p + ↑(factorization b) p → k ≤ ↑(factorization a) p ∨ k ≤ ↑(factorization b) p
[PROOFSTEP]
simp [h, imp_or]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
⊢ Finset.filter IsPrimePow (divisors (a * b)) = Finset.filter IsPrimePow (divisors a ∪ divisors b)
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k b : ℕ
hab : coprime 0 b
⊢ Finset.filter IsPrimePow (divisors (0 * b)) = Finset.filter IsPrimePow (divisors 0 ∪ divisors b)
[PROOFSTEP]
simp only [Nat.coprime_zero_left] at hab 
[GOAL]
case inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k b : ℕ
hab : b = 1
⊢ Finset.filter IsPrimePow (divisors (0 * b)) = Finset.filter IsPrimePow (divisors 0 ∪ divisors b)
[PROOFSTEP]
simp [hab, Finset.filter_singleton, not_isPrimePow_one]
[GOAL]
case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
ha : a ≠ 0
⊢ Finset.filter IsPrimePow (divisors (a * b)) = Finset.filter IsPrimePow (divisors a ∪ divisors b)
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | hb)
[GOAL]
case inr.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k a : ℕ
ha : a ≠ 0
hab : coprime a 0
⊢ Finset.filter IsPrimePow (divisors (a * 0)) = Finset.filter IsPrimePow (divisors a ∪ divisors 0)
[PROOFSTEP]
simp only [Nat.coprime_zero_right] at hab 
[GOAL]
case inr.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k a : ℕ
ha : a ≠ 0
hab : a = 1
⊢ Finset.filter IsPrimePow (divisors (a * 0)) = Finset.filter IsPrimePow (divisors a ∪ divisors 0)
[PROOFSTEP]
simp [hab, Finset.filter_singleton, not_isPrimePow_one]
[GOAL]
case inr.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
⊢ Finset.filter IsPrimePow (divisors (a * b)) = Finset.filter IsPrimePow (divisors a ∪ divisors b)
[PROOFSTEP]
ext n
[GOAL]
case inr.inr.a
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
n : ℕ
⊢ n ∈ Finset.filter IsPrimePow (divisors (a * b)) ↔ n ∈ Finset.filter IsPrimePow (divisors a ∪ divisors b)
[PROOFSTEP]
simp only [ha, hb, Finset.mem_union, Finset.mem_filter, Nat.mul_eq_zero, and_true_iff, Ne.def, and_congr_left_iff,
  not_false_iff, Nat.mem_divisors, or_self_iff]
[GOAL]
case inr.inr.a
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k a b : ℕ
hab : coprime a b
ha : a ≠ 0
hb : b ≠ 0
n : ℕ
⊢ IsPrimePow n → (n ∣ a * b ↔ n ∣ a ∨ n ∣ b)
[PROOFSTEP]
apply hab.isPrimePow_dvd_mul
