R : Type ?u.1643
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
R : Type ?u.1643
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ IsPrimePow n ↔ ∃ p k, 0 < k ∧ Nat.factorization n = Finsupp.single p k
rw [isPrimePow_nat_iff]
R : Type ?u.1643
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
R : Type ?u.1643
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
refine' exists₂_congr fun p k => _
case mp
R : Type ?u.1643
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

case mpr
R : Type ?u.1643
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
R : Type ?u.1643
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
constructor
case mp.intro.intro
R : Type ?u.1643
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
case mp
R : Type ?u.1643
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
rintro ⟨hp, hk, hn⟩
no goals
case mp.intro.intro
R : Type ?u.1643
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
exact ⟨hk, by rw [← hn, Nat.Prime.factorization_pow hp]⟩
no goals
R : Type ?u.1643
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
rw [← hn, Nat.Prime.factorization_pow hp]
case mpr.intro
R : Type ?u.1643
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
case mpr
R : Type ?u.1643
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
rintro ⟨hk, hn⟩
case mpr.intro
R : Type ?u.1643
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
case mpr.intro
R : Type ?u.1643
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
have hn0 : n ≠ 0 := by
  rintro rfl
  simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']
case mpr.intro
R : Type ?u.1643
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
case mpr.intro
R : Type ?u.1643
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
rw [Nat.eq_pow_of_factorization_eq_single hn0 hn]
no goals
case mpr.intro
R : Type ?u.1643
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
exact
  ⟨Nat.prime_of_mem_factorization (by simp [hn, hk.ne'] : p ∈ n.factorization.support), hk, rfl⟩
R : Type ?u.1643
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hk : 0 < k
hn : Nat.factorization 0 = Finsupp.single p k
⊢ False
R : Type ?u.1643
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n p k : ℕ
hk : 0 < k
hn : Nat.factorization n = Finsupp.single p k
⊢ n ≠ 0
rintro rfl
no goals
R : Type ?u.1643
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hk : 0 < k
hn : Nat.factorization 0 = Finsupp.single p k
⊢ False
simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']
no goals
R : Type ?u.1643
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
simp [hn, hk.ne']