[GOAL]
n : ℕ
⊢ ∀ (a : ℕ), a ∈ toFinset (factors n) ↔ (fun p => if Prime p then padicValNat p n else 0) a ≠ 0
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn0)
[GOAL]
case inl
⊢ ∀ (a : ℕ), a ∈ toFinset (factors 0) ↔ (fun p => if Prime p then padicValNat p 0 else 0) a ≠ 0
[PROOFSTEP]
simp
[GOAL]
case inr
n : ℕ
hn0 : n ≠ 0
⊢ ∀ (a : ℕ), a ∈ toFinset (factors n) ↔ (fun p => if Prime p then padicValNat p n else 0) a ≠ 0
[PROOFSTEP]
simp only [mem_factors hn0, mem_toFinset, Ne.def, ite_eq_right_iff, not_forall, exists_prop, and_congr_right_iff]
[GOAL]
case inr
n : ℕ
hn0 : n ≠ 0
⊢ ∀ (a : ℕ), Prime a → (a ∣ n ↔ ¬padicValNat a n = 0)
[PROOFSTEP]
rintro p hp
[GOAL]
case inr
n : ℕ
hn0 : n ≠ 0
p : ℕ
hp : Prime p
⊢ p ∣ n ↔ ¬padicValNat p n = 0
[PROOFSTEP]
haveI := fact_iff.mpr hp
[GOAL]
case inr
n : ℕ
hn0 : n ≠ 0
p : ℕ
hp : Prime p
this : Fact (Prime p)
⊢ p ∣ n ↔ ¬padicValNat p n = 0
[PROOFSTEP]
exact dvd_iff_padicValNat_ne_zero hn0
[GOAL]
n p : ℕ
pp : Prime p
⊢ ↑(factorization n) p = padicValNat p n
[PROOFSTEP]
simpa [factorization] using absurd pp
[GOAL]
n p : ℕ
⊢ count p (factors n) = ↑(factorization n) p
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn0)
[GOAL]
case inl
p : ℕ
⊢ count p (factors 0) = ↑(factorization 0) p
[PROOFSTEP]
simp [factorization, count]
[GOAL]
case inr
n p : ℕ
hn0 : n > 0
⊢ count p (factors n) = ↑(factorization n) p
[PROOFSTEP]
by_cases pp : p.Prime
[GOAL]
case pos
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p (factors n) = ↑(factorization n) p
case neg n p : ℕ hn0 : n > 0 pp : ¬Prime p ⊢ count p (factors n) = ↑(factorization n) p
[PROOFSTEP]
case neg =>
  rw [count_eq_zero_of_not_mem (mt prime_of_mem_factors pp)]
  simp [factorization, pp]
[GOAL]
n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ count p (factors n) = ↑(factorization n) p
[PROOFSTEP]
case neg =>
  rw [count_eq_zero_of_not_mem (mt prime_of_mem_factors pp)]
  simp [factorization, pp]
[GOAL]
n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ count p (factors n) = ↑(factorization n) p
[PROOFSTEP]
rw [count_eq_zero_of_not_mem (mt prime_of_mem_factors pp)]
[GOAL]
n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ 0 = ↑(factorization n) p
[PROOFSTEP]
simp [factorization, pp]
[GOAL]
case pos
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p (factors n) = ↑(factorization n) p
[PROOFSTEP]
simp only [factorization, coe_mk, pp, if_true]
[GOAL]
case pos
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p (factors n) = padicValNat p n
[PROOFSTEP]
rw [← PartENat.natCast_inj, padicValNat_def' pp.ne_one hn0,
  UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors pp hn0.ne']
[GOAL]
case pos
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ ↑(count p (factors n)) = ↑(Multiset.count (↑normalize p) (UniqueFactorizationMonoid.normalizedFactors n))
[PROOFSTEP]
simp [factors_eq]
[GOAL]
n : ℕ
⊢ factorization n = ↑Multiset.toFinsupp ↑(factors n)
[PROOFSTEP]
ext p
[GOAL]
case h
n p : ℕ
⊢ ↑(factorization n) p = ↑(↑Multiset.toFinsupp ↑(factors n)) p
[PROOFSTEP]
simp
[GOAL]
n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ multiplicity p n = ↑(↑(factorization n) p)
[PROOFSTEP]
simp [factorization, pp, padicValNat_def' pp.ne_one hn.bot_lt]
[GOAL]
n : ℕ
hn : n ≠ 0
⊢ (Finsupp.prod (factorization n) fun x x_1 => x ^ x_1) = n
[PROOFSTEP]
rw [factorization_eq_factors_multiset n]
[GOAL]
n : ℕ
hn : n ≠ 0
⊢ (Finsupp.prod (↑Multiset.toFinsupp ↑(factors n)) fun x x_1 => x ^ x_1) = n
[PROOFSTEP]
simp only [← prod_toMultiset, factorization, Multiset.coe_prod, Multiset.toFinsupp_toMultiset]
[GOAL]
n : ℕ
hn : n ≠ 0
⊢ List.prod (factors n) = n
[PROOFSTEP]
exact prod_factors hn
[GOAL]
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), ↑(factorization a) p = ↑(factorization b) p
⊢ factors a ~ factors b
[PROOFSTEP]
simpa only [List.perm_iff_count, factors_count_eq] using h
[GOAL]
a : ℕ
ha : a ∈ {x | x ≠ 0}
b : ℕ
hb : b ∈ {x | x ≠ 0}
h : factorization a = factorization b
p : ℕ
⊢ ↑(factorization a) p = ↑(factorization b) p
[PROOFSTEP]
simp [h]
[GOAL]
⊢ factorization 0 = 0
[PROOFSTEP]
simp [factorization]
[GOAL]
⊢ factorization 1 = 0
[PROOFSTEP]
simp [factorization]
[GOAL]
n : ℕ
⊢ (factorization n).support = toFinset (factors n)
[PROOFSTEP]
simp [factorization]
[GOAL]
n p : ℕ
⊢ p ∈ (factorization n).support ↔ p ∈ factors n
[PROOFSTEP]
simp only [support_factorization, List.mem_toFinset]
[GOAL]
n p : ℕ
⊢ ↑(factorization n) p = 0 ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
[PROOFSTEP]
rw [← not_mem_support_iff, support_factorization, mem_toFinset]
[GOAL]
n p : ℕ
⊢ ¬p ∈ factors n ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
p : ℕ
⊢ ¬p ∈ factors 0 ↔ ¬Prime p ∨ ¬p ∣ 0 ∨ 0 = 0
[PROOFSTEP]
simp
[GOAL]
case inr
n p : ℕ
hn : n ≠ 0
⊢ ¬p ∈ factors n ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
[PROOFSTEP]
simp [hn, Nat.mem_factors, not_and_or, -not_and]
[GOAL]
n p : ℕ
hp : ¬Prime p
⊢ ↑(factorization n) p = 0
[PROOFSTEP]
simp [factorization_eq_zero_iff, hp]
[GOAL]
n p : ℕ
h : ¬p ∣ n
⊢ ↑(factorization n) p = 0
[PROOFSTEP]
simp [factorization_eq_zero_iff, h]
[GOAL]
n p : ℕ
hp : Prime p
hn : n ≠ 0
h : p ∣ n
⊢ 0 < ↑(factorization n) p
[PROOFSTEP]
rwa [← factors_count_eq, count_pos, mem_factors_iff_dvd hn hp]
[GOAL]
p r i : ℕ
hr : ¬p ∣ r
⊢ ↑(factorization (p * i + r)) p = 0
[PROOFSTEP]
apply factorization_eq_zero_of_not_dvd
[GOAL]
case h
p r i : ℕ
hr : ¬p ∣ r
⊢ ¬p ∣ p * i + r
[PROOFSTEP]
rwa [← Nat.dvd_add_iff_right (Dvd.intro i rfl)]
[GOAL]
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
⊢ ¬p ∣ r ↔ ↑(factorization (p * i + r)) p = 0
[PROOFSTEP]
refine' ⟨factorization_eq_zero_of_remainder i, fun h => _⟩
[GOAL]
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : ↑(factorization (p * i + r)) p = 0
⊢ ¬p ∣ r
[PROOFSTEP]
rw [factorization_eq_zero_iff] at h 
[GOAL]
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : ¬Prime p ∨ ¬p ∣ p * i + r ∨ p * i + r = 0
⊢ ¬p ∣ r
[PROOFSTEP]
contrapose! h
[GOAL]
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ Prime p ∧ p ∣ p * i + r ∧ p * i + r ≠ 0
[PROOFSTEP]
refine' ⟨pp, _, _⟩
[GOAL]
case refine'_1
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p ∣ p * i + r
[PROOFSTEP]
rwa [← Nat.dvd_add_iff_right (dvd_mul_right p i)]
[GOAL]
case refine'_2
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p * i + r ≠ 0
[PROOFSTEP]
contrapose! hr0
[GOAL]
case refine'_2
p r i : ℕ
pp : Prime p
h : p ∣ r
hr0 : p * i + r = 0
⊢ r = 0
[PROOFSTEP]
exact (add_eq_zero_iff.mp hr0).2
[GOAL]
n : ℕ
⊢ factorization n = 0 ↔ n = 0 ∨ n = 1
[PROOFSTEP]
rw [factorization_eq_factors_multiset n]
[GOAL]
n : ℕ
⊢ ↑Multiset.toFinsupp ↑(factors n) = 0 ↔ n = 0 ∨ n = 1
[PROOFSTEP]
simp [factorization, AddEquiv.map_eq_zero_iff, Multiset.coe_eq_zero]
[GOAL]
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ factorization (a * b) = factorization a + factorization b
[PROOFSTEP]
ext p
[GOAL]
case h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ ↑(factorization (a * b)) p = ↑(factorization a + factorization b) p
[PROOFSTEP]
simp only [add_apply, ← factors_count_eq, perm_iff_count.mp (perm_factors_mul ha hb) p, count_append]
[GOAL]
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (factorization (a * b)).support = (factorization a).support ∪ (factorization b).support
[PROOFSTEP]
ext q
[GOAL]
case a
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
q : ℕ
⊢ q ∈ (factorization (a * b)).support ↔ q ∈ (factorization a).support ∪ (factorization b).support
[PROOFSTEP]
simp only [Finset.mem_union, factor_iff_mem_factorization]
[GOAL]
case a
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
q : ℕ
⊢ q ∈ factors (a * b) ↔ q ∈ factors a ∨ q ∈ factors b
[PROOFSTEP]
exact mem_factors_mul ha hb
[GOAL]
n : ℕ
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
⊢ (Finsupp.prod (factorization n) fun p x => f p) = ∏ p in toFinset (factors n), f p
[PROOFSTEP]
apply prod_congr support_factorization
[GOAL]
n : ℕ
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
⊢ ∀ (x : ℕ), x ∈ toFinset (factors n) → (fun p x => f p) x (↑(factorization n) x) = f x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
⊢ factorization (Finset.prod S g) = ∑ x in S, factorization (g x)
[PROOFSTEP]
classical
ext p
refine' Finset.induction_on' S ?_ ?_
· simp
· intro x T hxS hTS hxT IH
  have hT : T.prod g ≠ 0 := prod_ne_zero_iff.mpr fun x hx => hS x (hTS hx)
  simp [prod_insert hxT, sum_insert hxT, ← IH, factorization_mul (hS x hxS) hT]
[GOAL]
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
⊢ factorization (Finset.prod S g) = ∑ x in S, factorization (g x)
[PROOFSTEP]
ext p
[GOAL]
case h
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
p : ℕ
⊢ ↑(factorization (Finset.prod S g)) p = ↑(∑ x in S, factorization (g x)) p
[PROOFSTEP]
refine' Finset.induction_on' S ?_ ?_
[GOAL]
case h.refine'_1
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
p : ℕ
⊢ ↑(factorization (Finset.prod ∅ g)) p = ↑(∑ x in ∅, factorization (g x)) p
[PROOFSTEP]
simp
[GOAL]
case h.refine'_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
p : ℕ
⊢ ∀ {a : α} {s : Finset α},
    a ∈ S →
      s ⊆ S →
        ¬a ∈ s →
          ↑(factorization (Finset.prod s g)) p = ↑(∑ x in s, factorization (g x)) p →
            ↑(factorization (Finset.prod (insert a s) g)) p = ↑(∑ x in insert a s, factorization (g x)) p
[PROOFSTEP]
intro x T hxS hTS hxT IH
[GOAL]
case h.refine'_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
p : ℕ
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
hxT : ¬x ∈ T
IH : ↑(factorization (Finset.prod T g)) p = ↑(∑ x in T, factorization (g x)) p
⊢ ↑(factorization (Finset.prod (insert x T) g)) p = ↑(∑ x in insert x T, factorization (g x)) p
[PROOFSTEP]
have hT : T.prod g ≠ 0 := prod_ne_zero_iff.mpr fun x hx => hS x (hTS hx)
[GOAL]
case h.refine'_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ (x : α), x ∈ S → g x ≠ 0
p : ℕ
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
hxT : ¬x ∈ T
IH : ↑(factorization (Finset.prod T g)) p = ↑(∑ x in T, factorization (g x)) p
hT : Finset.prod T g ≠ 0
⊢ ↑(factorization (Finset.prod (insert x T) g)) p = ↑(∑ x in insert x T, factorization (g x)) p
[PROOFSTEP]
simp [prod_insert hxT, sum_insert hxT, ← IH, factorization_mul (hS x hxS) hT]
[GOAL]
n k : ℕ
⊢ factorization (n ^ k) = k • factorization n
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
n : ℕ
⊢ factorization (n ^ zero) = zero • factorization n
[PROOFSTEP]
simp
[GOAL]
case succ
n k : ℕ
ih : factorization (n ^ k) = k • factorization n
⊢ factorization (n ^ succ k) = succ k • factorization n
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case succ.inl
k : ℕ
ih : factorization (0 ^ k) = k • factorization 0
⊢ factorization (0 ^ succ k) = succ k • factorization 0
[PROOFSTEP]
simp
[GOAL]
case succ.inr
n k : ℕ
ih : factorization (n ^ k) = k • factorization n
hn : n ≠ 0
⊢ factorization (n ^ succ k) = succ k • factorization n
[PROOFSTEP]
rw [pow_succ, mul_comm, factorization_mul hn (pow_ne_zero _ hn), ih, succ_eq_one_add, add_smul, one_smul]
[GOAL]
p : ℕ
hp : Prime p
⊢ Nat.factorization p = single p 1
[PROOFSTEP]
ext q
[GOAL]
case h
p : ℕ
hp : Prime p
q : ℕ
⊢ ↑(Nat.factorization p) q = ↑(single p 1) q
[PROOFSTEP]
rw [← factors_count_eq, factors_prime hp, single_apply, count_singleton', if_congr eq_comm]
[GOAL]
case h.h_t
p : ℕ
hp : Prime p
q : ℕ
⊢ 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case h.h_e
p : ℕ
hp : Prime p
q : ℕ
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp : Prime p
⊢ ↑(Nat.factorization p) p = 1
[PROOFSTEP]
simp [hp]
[GOAL]
p k : ℕ
hp : Prime p
⊢ Nat.factorization (p ^ k) = single p k
[PROOFSTEP]
simp [hp]
[GOAL]
n p k : ℕ
hn : n ≠ 0
h : factorization n = single p k
⊢ n = p ^ k
[PROOFSTEP]
rw [← Nat.factorization_prod_pow_eq_self hn, h, Finsupp.prod_single_index]
[GOAL]
n p k : ℕ
hn : n ≠ 0
h : factorization n = single p k
⊢ p ^ 0 = 1
[PROOFSTEP]
simp
[GOAL]
p q : ℕ
hp : Prime p
h : ↑(Nat.factorization p) q ≠ 0
⊢ p = q
[PROOFSTEP]
simpa [hp.factorization, single_apply] using h
[GOAL]
f : ℕ →₀ ℕ
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
⊢ factorization (Finsupp.prod f fun x x_1 => x ^ x_1) = f
[PROOFSTEP]
have h : ∀ x : ℕ, x ∈ f.support → x ^ f x ≠ 0 := fun p hp => pow_ne_zero _ (Prime.ne_zero (hf p hp))
[GOAL]
f : ℕ →₀ ℕ
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : ∀ (x : ℕ), x ∈ f.support → x ^ ↑f x ≠ 0
⊢ factorization (Finsupp.prod f fun x x_1 => x ^ x_1) = f
[PROOFSTEP]
simp only [Finsupp.prod, factorization_prod h]
[GOAL]
f : ℕ →₀ ℕ
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : ∀ (x : ℕ), x ∈ f.support → x ^ ↑f x ≠ 0
⊢ ∑ x in f.support, factorization (x ^ ↑f x) = f
[PROOFSTEP]
conv =>
  rhs
  rw [(sum_single f).symm]
[GOAL]
f : ℕ →₀ ℕ
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : ∀ (x : ℕ), x ∈ f.support → x ^ ↑f x ≠ 0
| ∑ x in f.support, factorization (x ^ ↑f x) = f
[PROOFSTEP]
  rhs
  rw [(sum_single f).symm]
[GOAL]
f : ℕ →₀ ℕ
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : ∀ (x : ℕ), x ∈ f.support → x ^ ↑f x ≠ 0
| ∑ x in f.support, factorization (x ^ ↑f x) = f
[PROOFSTEP]
  rhs
  rw [(sum_single f).symm]
[GOAL]
f : ℕ →₀ ℕ
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : ∀ (x : ℕ), x ∈ f.support → x ^ ↑f x ≠ 0
| ∑ x in f.support, factorization (x ^ ↑f x) = f
[PROOFSTEP]
rhs
[GOAL]
f : ℕ →₀ ℕ
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : ∀ (x : ℕ), x ∈ f.support → x ^ ↑f x ≠ 0
| f
[PROOFSTEP]
rw [(sum_single f).symm]
[GOAL]
f : ℕ →₀ ℕ
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : ∀ (x : ℕ), x ∈ f.support → x ^ ↑f x ≠ 0
⊢ ∑ x in f.support, factorization (x ^ ↑f x) = Finsupp.sum f single
[PROOFSTEP]
exact sum_congr rfl fun p hp => Prime.factorization_pow (hf p hp)
[GOAL]
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : f = factorization n
⊢ (Finsupp.prod f fun x x_1 => x ^ x_1) = n
[PROOFSTEP]
rw [h, factorization_prod_pow_eq_self hn]
[GOAL]
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : (Finsupp.prod f fun x x_1 => x ^ x_1) = n
⊢ f = factorization n
[PROOFSTEP]
rw [← h, prod_pow_factorization_eq_self hf]
[GOAL]
n : ℕ+
⊢ ↑(↑factorizationEquiv n) = factorization ↑n
[PROOFSTEP]
cases n
[GOAL]
case mk
val✝ : ℕ
property✝ : 0 < val✝
⊢ ↑(↑factorizationEquiv { val := val✝, property := property✝ }) = factorization ↑{ val := val✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
n p : ℕ
hp : ¬Prime p
⊢ p ^ ↑(factorization n) p = 1
[PROOFSTEP]
simp [factorization_eq_zero_of_non_prime n hp]
[GOAL]
n p : ℕ
hp : ¬Prime p
⊢ n / p ^ ↑(factorization n) p = n
[PROOFSTEP]
simp [factorization_eq_zero_of_non_prime n hp]
[GOAL]
n p : ℕ
⊢ p ^ ↑(factorization n) p ∣ n
[PROOFSTEP]
by_cases hp : p.Prime
[GOAL]
case pos
n p : ℕ
hp : Prime p
⊢ p ^ ↑(factorization n) p ∣ n
case neg n p : ℕ hp : ¬Prime p ⊢ p ^ ↑(factorization n) p ∣ n
[PROOFSTEP]
case neg => simp [hp]
[GOAL]
n p : ℕ
hp : ¬Prime p
⊢ p ^ ↑(factorization n) p ∣ n
[PROOFSTEP]
case neg => simp [hp]
[GOAL]
n p : ℕ
hp : ¬Prime p
⊢ p ^ ↑(factorization n) p ∣ n
[PROOFSTEP]
simp [hp]
[GOAL]
case pos
n p : ℕ
hp : Prime p
⊢ p ^ ↑(factorization n) p ∣ n
[PROOFSTEP]
rw [← factors_count_eq]
[GOAL]
case pos
n p : ℕ
hp : Prime p
⊢ p ^ count p (factors n) ∣ n
[PROOFSTEP]
apply dvd_of_factors_subperm (pow_ne_zero _ hp.ne_zero)
[GOAL]
case pos
n p : ℕ
hp : Prime p
⊢ factors (p ^ count p (factors n)) <+~ factors n
[PROOFSTEP]
rw [hp.factors_pow, List.subperm_ext_iff]
[GOAL]
case pos
n p : ℕ
hp : Prime p
⊢ ∀ (x : ℕ), x ∈ replicate (count p (factors n)) p → count x (replicate (count p (factors n)) p) ≤ count x (factors n)
[PROOFSTEP]
intro q hq
[GOAL]
case pos
n p : ℕ
hp : Prime p
q : ℕ
hq : q ∈ replicate (count p (factors n)) p
⊢ count q (replicate (count p (factors n)) p) ≤ count q (factors n)
[PROOFSTEP]
simp [List.eq_of_mem_replicate hq]
[GOAL]
n p : ℕ
⊢ 0 < p ^ ↑(factorization n) p
[PROOFSTEP]
by_cases pp : p.Prime
[GOAL]
case pos
n p : ℕ
pp : Prime p
⊢ 0 < p ^ ↑(factorization n) p
[PROOFSTEP]
simp [pow_pos pp.pos]
[GOAL]
case neg
n p : ℕ
pp : ¬Prime p
⊢ 0 < p ^ ↑(factorization n) p
[PROOFSTEP]
simp [pp]
[GOAL]
n p : ℕ
hn : n ≠ 0
⊢ 0 < n / p ^ ↑(factorization n) p
[PROOFSTEP]
cases' em' p.Prime with pp pp
[GOAL]
case inl
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ 0 < n / p ^ ↑(factorization n) p
[PROOFSTEP]
simpa [Nat.factorization_eq_zero_of_non_prime n pp] using hn.bot_lt
[GOAL]
case inr
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ 0 < n / p ^ ↑(factorization n) p
[PROOFSTEP]
exact Nat.div_pos (ord_proj_le p hn) (ord_proj_pos n p)
[GOAL]
a b p : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ p ^ ↑(factorization (a * b)) p = p ^ ↑(factorization a) p * p ^ ↑(factorization b) p
[PROOFSTEP]
simp [factorization_mul ha hb, pow_add]
[GOAL]
a b p : ℕ
⊢ a * b / p ^ ↑(factorization (a * b)) p = a / p ^ ↑(factorization a) p * (b / p ^ ↑(factorization b) p)
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
b p : ℕ
⊢ 0 * b / p ^ ↑(factorization (0 * b)) p = 0 / p ^ ↑(factorization 0) p * (b / p ^ ↑(factorization b) p)
[PROOFSTEP]
simp
[GOAL]
case inr
a b p : ℕ
ha : a ≠ 0
⊢ a * b / p ^ ↑(factorization (a * b)) p = a / p ^ ↑(factorization a) p * (b / p ^ ↑(factorization b) p)
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | hb)
[GOAL]
case inr.inl
a p : ℕ
ha : a ≠ 0
⊢ a * 0 / p ^ ↑(factorization (a * 0)) p = a / p ^ ↑(factorization a) p * (0 / p ^ ↑(factorization 0) p)
[PROOFSTEP]
simp
[GOAL]
case inr.inr
a b p : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b / p ^ ↑(factorization (a * b)) p = a / p ^ ↑(factorization a) p * (b / p ^ ↑(factorization b) p)
[PROOFSTEP]
simp only [ord_proj_mul p ha hb]
[GOAL]
case inr.inr
a b p : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b / (p ^ ↑(factorization a) p * p ^ ↑(factorization b) p) =
    a / p ^ ↑(factorization a) p * (b / p ^ ↑(factorization b) p)
[PROOFSTEP]
rw [mul_div_mul_comm_of_dvd_dvd (ord_proj_dvd a p) (ord_proj_dvd b p)]
[GOAL]
n p : ℕ
h : p ∈ (factorization n).support
⊢ p ∣ n
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
p : ℕ
h : p ∈ (factorization 0).support
⊢ p ∣ 0
[PROOFSTEP]
simp
[GOAL]
case inr
n p : ℕ
h : p ∈ (factorization n).support
hn : n ≠ 0
⊢ p ∣ n
[PROOFSTEP]
simp [← mem_factors_iff_dvd hn (prime_of_mem_factorization h), factor_iff_mem_factorization.mp h]
[GOAL]
n p : ℕ
hn : n ≠ 0
⊢ ↑(factorization n) p < n
[PROOFSTEP]
by_cases pp : p.Prime
[GOAL]
case pos
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ ↑(factorization n) p < n
case neg n p : ℕ hn : n ≠ 0 pp : ¬Prime p ⊢ ↑(factorization n) p < n
[PROOFSTEP]
case neg =>
  simp [factorization_eq_zero_of_non_prime n pp]
  exact hn.bot_lt
[GOAL]
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ ↑(factorization n) p < n
[PROOFSTEP]
case neg =>
  simp [factorization_eq_zero_of_non_prime n pp]
  exact hn.bot_lt
[GOAL]
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ ↑(factorization n) p < n
[PROOFSTEP]
simp [factorization_eq_zero_of_non_prime n pp]
[GOAL]
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ 0 < n
[PROOFSTEP]
exact hn.bot_lt
[GOAL]
case pos
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ ↑(factorization n) p < n
[PROOFSTEP]
rw [← pow_lt_iff_lt_right pp.two_le]
[GOAL]
case pos
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ p ^ ↑(factorization n) p < p ^ n
[PROOFSTEP]
apply lt_of_le_of_lt (ord_proj_le p hn)
[GOAL]
case pos
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ n < p ^ n
[PROOFSTEP]
exact lt_of_lt_of_le (lt_two_pow n) (pow_le_pow_of_le_left pp.two_le n)
[GOAL]
n p b : ℕ
hb : n ≤ p ^ b
⊢ ↑(factorization n) p ≤ b
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
p b : ℕ
hb : 0 ≤ p ^ b
⊢ ↑(factorization 0) p ≤ b
[PROOFSTEP]
simp
[GOAL]
case inr
n p b : ℕ
hb : n ≤ p ^ b
hn : n ≠ 0
⊢ ↑(factorization n) p ≤ b
[PROOFSTEP]
by_cases pp : p.Prime
[GOAL]
case pos
n p b : ℕ
hb : n ≤ p ^ b
hn : n ≠ 0
pp : Prime p
⊢ ↑(factorization n) p ≤ b
[PROOFSTEP]
exact (pow_le_iff_le_right pp.two_le).1 (le_trans (ord_proj_le p hn) hb)
[GOAL]
case neg
n p b : ℕ
hb : n ≤ p ^ b
hn : n ≠ 0
pp : ¬Prime p
⊢ ↑(factorization n) p ≤ b
[PROOFSTEP]
simp [factorization_eq_zero_of_non_prime n pp]
[GOAL]
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ factorization d ≤ factorization n ↔ d ∣ n
[PROOFSTEP]
constructor
[GOAL]
case mp
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ factorization d ≤ factorization n → d ∣ n
[PROOFSTEP]
intro hdn
[GOAL]
case mp
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : factorization d ≤ factorization n
⊢ d ∣ n
[PROOFSTEP]
set K := n.factorization - d.factorization with hK
[GOAL]
case mp
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : factorization d ≤ factorization n
K : ℕ →₀ ℕ := factorization n - factorization d
hK : K = factorization n - factorization d
⊢ d ∣ n
[PROOFSTEP]
use K.prod (· ^ ·)
[GOAL]
case h
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : factorization d ≤ factorization n
K : ℕ →₀ ℕ := factorization n - factorization d
hK : K = factorization n - factorization d
⊢ n = d * Finsupp.prod K fun x x_1 => x ^ x_1
[PROOFSTEP]
rw [← factorization_prod_pow_eq_self hn, ← factorization_prod_pow_eq_self hd, ←
  Finsupp.prod_add_index' pow_zero pow_add, hK, add_tsub_cancel_of_le hdn]
[GOAL]
case mpr
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d ∣ n → factorization d ≤ factorization n
[PROOFSTEP]
rintro ⟨c, rfl⟩
[GOAL]
case mpr.intro
d : ℕ
hd : d ≠ 0
c : ℕ
hn : d * c ≠ 0
⊢ factorization d ≤ factorization (d * c)
[PROOFSTEP]
rw [factorization_mul hd (right_ne_zero_of_mul hn)]
[GOAL]
case mpr.intro
d : ℕ
hd : d ≠ 0
c : ℕ
hn : d * c ≠ 0
⊢ factorization d ≤ factorization d + factorization c
[PROOFSTEP]
simp
[GOAL]
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ (∀ (p : ℕ), Prime p → ↑(factorization d) p ≤ ↑(factorization n) p) ↔ d ∣ n
[PROOFSTEP]
rw [← factorization_le_iff_dvd hd hn]
[GOAL]
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ (∀ (p : ℕ), Prime p → ↑(factorization d) p ≤ ↑(factorization n) p) ↔ factorization d ≤ factorization n
[PROOFSTEP]
refine' ⟨fun h p => (em p.Prime).elim (h p) fun hp => _, fun h p _ => h p⟩
[GOAL]
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
h : ∀ (p : ℕ), Prime p → ↑(factorization d) p ≤ ↑(factorization n) p
p : ℕ
hp : ¬Prime p
⊢ ↑(factorization d) p ≤ ↑(factorization n) p
[PROOFSTEP]
simp_rw [factorization_eq_zero_of_non_prime _ hp, le_refl]
[GOAL]
n p : ℕ
hn : n ≠ 0
hp : Prime p
⊢ ¬p ^ (↑(factorization n) p + 1) ∣ n
[PROOFSTEP]
intro h
[GOAL]
n p : ℕ
hn : n ≠ 0
hp : Prime p
h : p ^ (↑(factorization n) p + 1) ∣ n
⊢ False
[PROOFSTEP]
rw [← factorization_le_iff_dvd (pow_pos hp.pos _).ne' hn] at h 
[GOAL]
n p : ℕ
hn : n ≠ 0
hp : Prime p
h : factorization (p ^ (↑(factorization n) p + 1)) ≤ factorization n
⊢ False
[PROOFSTEP]
simpa [hp.factorization] using h p
[GOAL]
a b : ℕ
hb : b ≠ 0
⊢ factorization a ≤ factorization (a * b)
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
b : ℕ
hb : b ≠ 0
⊢ factorization 0 ≤ factorization (0 * b)
[PROOFSTEP]
simp
[GOAL]
case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ factorization a ≤ factorization (a * b)
[PROOFSTEP]
rw [factorization_le_iff_dvd ha <| mul_ne_zero ha hb]
[GOAL]
case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a ∣ a * b
[PROOFSTEP]
exact Dvd.intro b rfl
[GOAL]
a b : ℕ
ha : a ≠ 0
⊢ factorization b ≤ factorization (a * b)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
a b : ℕ
ha : a ≠ 0
⊢ factorization b ≤ factorization (b * a)
[PROOFSTEP]
apply factorization_le_factorization_mul_left ha
[GOAL]
p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ^ k ∣ n ↔ k ≤ ↑(Nat.factorization n) p
[PROOFSTEP]
rw [← factorization_le_iff_dvd (pow_pos pp.pos k).ne' hn, pp.factorization_pow, single_le_iff]
[GOAL]
p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ^ k ∣ n ↔ p ^ k ∣ p ^ ↑(Nat.factorization n) p
[PROOFSTEP]
rw [pow_dvd_pow_iff_le_right pp.one_lt, pp.pow_dvd_iff_le_factorization hn]
[GOAL]
p n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ∣ n ↔ p ^ 1 ∣ n
[PROOFSTEP]
simp
[GOAL]
a b : ℕ
ha : a ≠ 0
hab : a < b
⊢ ∃ p, ↑(factorization a) p < ↑(factorization b) p
[PROOFSTEP]
have hb : b ≠ 0 := (ha.bot_lt.trans hab).ne'
[GOAL]
a b : ℕ
ha : a ≠ 0
hab : a < b
hb : b ≠ 0
⊢ ∃ p, ↑(factorization a) p < ↑(factorization b) p
[PROOFSTEP]
contrapose! hab
[GOAL]
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (p : ℕ), ↑(factorization b) p ≤ ↑(factorization a) p
⊢ b ≤ a
[PROOFSTEP]
rw [← Finsupp.le_def, factorization_le_iff_dvd hb ha] at hab 
[GOAL]
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : b ∣ a
⊢ b ≤ a
[PROOFSTEP]
exact le_of_dvd ha.bot_lt hab
[GOAL]
d n : ℕ
h : d ∣ n
⊢ factorization (n / d) = factorization n - factorization d
[PROOFSTEP]
rcases eq_or_ne d 0 with (rfl | hd)
[GOAL]
case inl
n : ℕ
h : 0 ∣ n
⊢ factorization (n / 0) = factorization n - factorization 0
[PROOFSTEP]
simp [zero_dvd_iff.mp h]
[GOAL]
case inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
⊢ factorization (n / d) = factorization n - factorization d
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inr.inl
d : ℕ
hd : d ≠ 0
h : d ∣ 0
⊢ factorization (0 / d) = factorization 0 - factorization d
[PROOFSTEP]
simp
[GOAL]
case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ factorization (n / d) = factorization n - factorization d
[PROOFSTEP]
apply add_left_injective d.factorization
[GOAL]
case inr.inr.a
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (fun x => x + factorization d) (factorization (n / d)) =
    (fun x => x + factorization d) (factorization n - factorization d)
[PROOFSTEP]
simp only
[GOAL]
case inr.inr.a
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ factorization (n / d) + factorization d = factorization n - factorization d + factorization d
[PROOFSTEP]
rw [tsub_add_cancel_of_le <| (Nat.factorization_le_iff_dvd hd hn).mpr h, ←
  Nat.factorization_mul (Nat.div_pos (Nat.le_of_dvd hn.bot_lt h) hd.bot_lt).ne' hd, Nat.div_mul_cancel h]
[GOAL]
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬p ∣ n / p ^ ↑(factorization n) p
[PROOFSTEP]
rw [Nat.Prime.dvd_iff_one_le_factorization hp (ord_compl_pos p hn).ne']
[GOAL]
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ ↑(factorization (n / p ^ ↑(factorization n) p)) p
[PROOFSTEP]
rw [Nat.factorization_div (Nat.ord_proj_dvd n p)]
[GOAL]
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ ↑(factorization n - factorization (p ^ ↑(factorization n) p)) p
[PROOFSTEP]
simp [hp.factorization]
[GOAL]
n p : ℕ
⊢ factorization (n / p ^ ↑(factorization n) p) = Finsupp.erase p (factorization n)
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
p : ℕ
⊢ factorization (0 / p ^ ↑(factorization 0) p) = Finsupp.erase p (factorization 0)
[PROOFSTEP]
simp
[GOAL]
case inr
n p : ℕ
hn : n ≠ 0
⊢ factorization (n / p ^ ↑(factorization n) p) = Finsupp.erase p (factorization n)
[PROOFSTEP]
by_cases pp : p.Prime
[GOAL]
case pos
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ factorization (n / p ^ ↑(factorization n) p) = Finsupp.erase p (factorization n)
case neg
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ factorization (n / p ^ ↑(factorization n) p) = Finsupp.erase p (factorization n)
[PROOFSTEP]
case neg =>
  -- porting note: needed to solve side goal explicitly
  rw [Finsupp.erase_of_not_mem_support]
  · simp [pp]
  · simp [mt prime_of_mem_factors pp]
[GOAL]
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ factorization (n / p ^ ↑(factorization n) p) = Finsupp.erase p (factorization n)
[PROOFSTEP]
case neg =>
  -- porting note: needed to solve side goal explicitly
  rw [Finsupp.erase_of_not_mem_support]
  · simp [pp]
  · simp [mt prime_of_mem_factors pp]
[GOAL]
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ factorization (n / p ^ ↑(factorization n) p) = Finsupp.erase p (factorization n)
[PROOFSTEP]
rw [Finsupp.erase_of_not_mem_support]
[GOAL]
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ factorization (n / p ^ ↑(factorization n) p) = factorization n
[PROOFSTEP]
simp [pp]
[GOAL]
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ ¬p ∈ (factorization n).support
[PROOFSTEP]
simp [mt prime_of_mem_factors pp]
[GOAL]
case pos
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ factorization (n / p ^ ↑(factorization n) p) = Finsupp.erase p (factorization n)
[PROOFSTEP]
ext q
[GOAL]
case pos.h
n p : ℕ
hn : n ≠ 0
pp : Prime p
q : ℕ
⊢ ↑(factorization (n / p ^ ↑(factorization n) p)) q = ↑(Finsupp.erase p (factorization n)) q
[PROOFSTEP]
rcases eq_or_ne q p with (rfl | hqp)
[GOAL]
case pos.h.inl
n : ℕ
hn : n ≠ 0
q : ℕ
pp : Prime q
⊢ ↑(factorization (n / q ^ ↑(factorization n) q)) q = ↑(Finsupp.erase q (factorization n)) q
[PROOFSTEP]
simp only [Finsupp.erase_same, factorization_eq_zero_iff, not_dvd_ord_compl pp hn]
[GOAL]
case pos.h.inl
n : ℕ
hn : n ≠ 0
q : ℕ
pp : Prime q
⊢ ¬Prime q ∨ True ∨ n / q ^ ↑(factorization n) q = 0
[PROOFSTEP]
simp
[GOAL]
case pos.h.inr
n p : ℕ
hn : n ≠ 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ ↑(factorization (n / p ^ ↑(factorization n) p)) q = ↑(Finsupp.erase p (factorization n)) q
[PROOFSTEP]
rw [Finsupp.erase_ne hqp, factorization_div (ord_proj_dvd n p)]
[GOAL]
case pos.h.inr
n p : ℕ
hn : n ≠ 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ ↑(factorization n - factorization (p ^ ↑(factorization n) p)) q = ↑(factorization n) q
[PROOFSTEP]
simp [pp.factorization, hqp.symm]
[GOAL]
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
⊢ d ∣ n / p ^ ↑(factorization n) p
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn0)
[GOAL]
case inl
p d : ℕ
hpd : ¬p ∣ d
hdn : d ∣ 0
⊢ d ∣ 0 / p ^ ↑(factorization 0) p
[PROOFSTEP]
simp
[GOAL]
case inr
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n ≠ 0
⊢ d ∣ n / p ^ ↑(factorization n) p
[PROOFSTEP]
rcases eq_or_ne d 0 with (rfl | hd0)
[GOAL]
case inr.inl
p n : ℕ
hn0 : n ≠ 0
hdn : 0 ∣ n
hpd : ¬p ∣ 0
⊢ 0 ∣ n / p ^ ↑(factorization n) p
[PROOFSTEP]
simp at hpd 
[GOAL]
case inr.inr
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n ≠ 0
hd0 : d ≠ 0
⊢ d ∣ n / p ^ ↑(factorization n) p
[PROOFSTEP]
rw [← factorization_le_iff_dvd hd0 (ord_compl_pos p hn0).ne', factorization_ord_compl]
[GOAL]
case inr.inr
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n ≠ 0
hd0 : d ≠ 0
⊢ factorization d ≤ Finsupp.erase p (factorization n)
[PROOFSTEP]
intro q
[GOAL]
case inr.inr
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n ≠ 0
hd0 : d ≠ 0
q : ℕ
⊢ ↑(factorization d) q ≤ ↑(Finsupp.erase p (factorization n)) q
[PROOFSTEP]
rcases eq_or_ne q p with (rfl | hqp)
[GOAL]
case inr.inr.inl
d n : ℕ
hdn : d ∣ n
hn0 : n ≠ 0
hd0 : d ≠ 0
q : ℕ
hpd : ¬q ∣ d
⊢ ↑(factorization d) q ≤ ↑(Finsupp.erase q (factorization n)) q
[PROOFSTEP]
simp [factorization_eq_zero_iff, hpd]
[GOAL]
case inr.inr.inr
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n ≠ 0
hd0 : d ≠ 0
q : ℕ
hqp : q ≠ p
⊢ ↑(factorization d) q ≤ ↑(Finsupp.erase p (factorization n)) q
[PROOFSTEP]
simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q]
[GOAL]
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
⊢ d ∣ n ↔ factorization (n / d) = factorization n - factorization d
[PROOFSTEP]
refine' ⟨factorization_div, _⟩
[GOAL]
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
⊢ factorization (n / d) = factorization n - factorization d → d ∣ n
[PROOFSTEP]
rcases eq_or_lt_of_le hdn with (rfl | hd_lt_n)
[GOAL]
case inl
d : ℕ
hd : d ≠ 0
hdn : d ≤ d
⊢ factorization (d / d) = factorization d - factorization d → d ∣ d
[PROOFSTEP]
simp
[GOAL]
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
⊢ factorization (n / d) = factorization n - factorization d → d ∣ n
[PROOFSTEP]
have h1 : n / d ≠ 0 := fun H => Nat.lt_asymm hd_lt_n ((Nat.div_eq_zero_iff hd.bot_lt).mp H)
[GOAL]
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
⊢ factorization (n / d) = factorization n - factorization d → d ∣ n
[PROOFSTEP]
intro h
[GOAL]
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : factorization (n / d) = factorization n - factorization d
⊢ d ∣ n
[PROOFSTEP]
rw [dvd_iff_le_div_mul n d]
[GOAL]
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : factorization (n / d) = factorization n - factorization d
⊢ n ≤ n / d * d
[PROOFSTEP]
by_contra h2
[GOAL]
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : factorization (n / d) = factorization n - factorization d
h2 : ¬n ≤ n / d * d
⊢ False
[PROOFSTEP]
cases' exists_factorization_lt_of_lt (mul_ne_zero h1 hd) (not_le.mp h2) with p hp
[GOAL]
case inr.intro
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : factorization (n / d) = factorization n - factorization d
h2 : ¬n ≤ n / d * d
p : ℕ
hp : ↑(factorization (n / d * d)) p < ↑(factorization n) p
⊢ False
[PROOFSTEP]
rwa [factorization_mul h1 hd, add_apply, ← lt_tsub_iff_right, h, tsub_apply, lt_self_iff_false] at hp 
[GOAL]
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
⊢ p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
[PROOFSTEP]
rcases em' p.Prime with (pp | pp)
[GOAL]
case inl
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
[PROOFSTEP]
simp [pp]
[GOAL]
case inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha0)
[GOAL]
case inr.inl
b : ℕ
hb0 : b ≠ 0
p : ℕ
pp : Prime p
hab : 0 ∣ b
⊢ p ^ ↑(factorization 0) p ∣ p ^ ↑(factorization b) p
[PROOFSTEP]
simp
[GOAL]
case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
[PROOFSTEP]
rw [pow_dvd_pow_iff_le_right pp.one_lt]
[GOAL]
case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ ↑(factorization a) p ≤ ↑(factorization b) p
[PROOFSTEP]
exact (factorization_le_iff_dvd ha0 hb0).2 hab p
[GOAL]
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ (∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p) ↔ a ∣ b
[PROOFSTEP]
refine' ⟨fun h => _, fun hab p => ord_proj_dvd_ord_proj_of_dvd hb0 hab p⟩
[GOAL]
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
⊢ a ∣ b
[PROOFSTEP]
rw [← factorization_le_iff_dvd ha0 hb0]
[GOAL]
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
⊢ factorization a ≤ factorization b
[PROOFSTEP]
intro q
[GOAL]
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
q : ℕ
⊢ ↑(factorization a) q ≤ ↑(factorization b) q
[PROOFSTEP]
rcases le_or_lt q 1 with (hq_le | hq1)
[GOAL]
case inl
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
q : ℕ
hq_le : q ≤ 1
⊢ ↑(factorization a) q ≤ ↑(factorization b) q
[PROOFSTEP]
interval_cases q
[GOAL]
case inl.«0»
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
q : ℕ
hq_le : 0 ≤ 1
⊢ ↑(factorization a) 0 ≤ ↑(factorization b) 0
[PROOFSTEP]
simp
[GOAL]
case inl.«1»
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
q : ℕ
hq_le : 1 ≤ 1
⊢ ↑(factorization a) 1 ≤ ↑(factorization b) 1
[PROOFSTEP]
simp
[GOAL]
case inr
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
q : ℕ
hq1 : 1 < q
⊢ ↑(factorization a) q ≤ ↑(factorization b) q
[PROOFSTEP]
exact (pow_dvd_pow_iff_le_right hq1).1 (h q)
[GOAL]
a b : ℕ
hab : a ∣ b
p : ℕ
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
[PROOFSTEP]
rcases em' p.Prime with (pp | pp)
[GOAL]
case inl
a b : ℕ
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
[PROOFSTEP]
simp [pp, hab]
[GOAL]
case inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | hb0)
[GOAL]
case inr.inl
a p : ℕ
pp : Prime p
hab : a ∣ 0
⊢ a / p ^ ↑(factorization a) p ∣ 0 / p ^ ↑(factorization 0) p
[PROOFSTEP]
simp
[GOAL]
case inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha0)
[GOAL]
case inr.inr.inl
b p : ℕ
pp : Prime p
hb0 : b ≠ 0
hab : 0 ∣ b
⊢ 0 / p ^ ↑(factorization 0) p ∣ b / p ^ ↑(factorization b) p
[PROOFSTEP]
cases hb0 (zero_dvd_iff.1 hab)
[GOAL]
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
[PROOFSTEP]
have ha := (Nat.div_pos (ord_proj_le p ha0) (ord_proj_pos a p)).ne'
[GOAL]
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
[PROOFSTEP]
have hb := (Nat.div_pos (ord_proj_le p hb0) (ord_proj_pos b p)).ne'
[GOAL]
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
hb : b / p ^ ↑(factorization b) p ≠ 0
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
[PROOFSTEP]
rw [← factorization_le_iff_dvd ha hb, factorization_ord_compl a p, factorization_ord_compl b p]
[GOAL]
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
hb : b / p ^ ↑(factorization b) p ≠ 0
⊢ Finsupp.erase p (factorization a) ≤ Finsupp.erase p (factorization b)
[PROOFSTEP]
intro q
[GOAL]
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
hb : b / p ^ ↑(factorization b) p ≠ 0
q : ℕ
⊢ ↑(Finsupp.erase p (factorization a)) q ≤ ↑(Finsupp.erase p (factorization b)) q
[PROOFSTEP]
rcases eq_or_ne q p with (rfl | hqp)
[GOAL]
case inr.inr.inr.inl
a b : ℕ
hab : a ∣ b
hb0 : b ≠ 0
ha0 : a ≠ 0
q : ℕ
pp : Prime q
ha : a / q ^ ↑(factorization a) q ≠ 0
hb : b / q ^ ↑(factorization b) q ≠ 0
⊢ ↑(Finsupp.erase q (factorization a)) q ≤ ↑(Finsupp.erase q (factorization b)) q
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
hb : b / p ^ ↑(factorization b) p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ ↑(Finsupp.erase p (factorization a)) q ≤ ↑(Finsupp.erase p (factorization b)) q
[PROOFSTEP]
simp_rw [erase_ne hqp]
[GOAL]
case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
hb : b / p ^ ↑(factorization b) p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ ↑(factorization a) q ≤ ↑(factorization b) q
[PROOFSTEP]
exact (factorization_le_iff_dvd ha0 hb0).2 hab q
[GOAL]
a b : ℕ
⊢ (∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p) ↔ a ∣ b
[PROOFSTEP]
refine' ⟨fun h => _, fun hab p => ord_compl_dvd_ord_compl_of_dvd hab p⟩
[GOAL]
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
⊢ a ∣ b
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | hb0)
[GOAL]
case inl
a : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ 0 / p ^ ↑(factorization 0) p
⊢ a ∣ 0
[PROOFSTEP]
simp
[GOAL]
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
⊢ a ∣ b
[PROOFSTEP]
by_cases pa : a.Prime
[GOAL]
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
⊢ a ∣ b
case neg
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : ¬Prime a
⊢ a ∣ b
[PROOFSTEP]
case neg => simpa [pa] using h a
[GOAL]
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : ¬Prime a
⊢ a ∣ b
[PROOFSTEP]
case neg => simpa [pa] using h a
[GOAL]
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : ¬Prime a
⊢ a ∣ b
[PROOFSTEP]
simpa [pa] using h a
[GOAL]
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
⊢ a ∣ b
[PROOFSTEP]
by_cases pb : b.Prime
[GOAL]
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a ∣ b
case neg
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : ¬Prime b
⊢ a ∣ b
[PROOFSTEP]
case neg => simpa [pb] using h b
[GOAL]
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : ¬Prime b
⊢ a ∣ b
[PROOFSTEP]
case neg => simpa [pb] using h b
[GOAL]
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : ¬Prime b
⊢ a ∣ b
[PROOFSTEP]
simpa [pb] using h b
[GOAL]
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a ∣ b
[PROOFSTEP]
rw [prime_dvd_prime_iff_eq pa pb]
[GOAL]
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a = b
[PROOFSTEP]
by_contra hab
[GOAL]
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ False
[PROOFSTEP]
apply pa.ne_one
[GOAL]
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ a = 1
[PROOFSTEP]
rw [← Nat.dvd_one, ← Nat.mul_dvd_mul_iff_left hb0.bot_lt, mul_one]
[GOAL]
case pos
a b : ℕ
h : ∀ (p : ℕ), a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ b * a ∣ b
[PROOFSTEP]
simpa [Prime.factorization_self pb, Prime.factorization pa, hab] using h b
[GOAL]
n d : ℕ
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
d : ℕ
⊢ d ∣ 0 ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ 0
[PROOFSTEP]
simp
[GOAL]
case inr
n d : ℕ
hn : n ≠ 0
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
[PROOFSTEP]
rcases eq_or_ne d 0 with (rfl | hd)
[GOAL]
case inr.inl
n : ℕ
hn : n ≠ 0
⊢ 0 ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ 0 → p ^ k ∣ n
[PROOFSTEP]
simp only [zero_dvd_iff, hn, false_iff_iff, not_forall]
[GOAL]
case inr.inl
n : ℕ
hn : n ≠ 0
⊢ ∃ x x_1 h x_2, ¬x ^ x_1 ∣ n
[PROOFSTEP]
exact ⟨2, n, prime_two, dvd_zero _, mt (le_of_dvd hn.bot_lt) (lt_two_pow n).not_le⟩
[GOAL]
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
[PROOFSTEP]
refine' ⟨fun h p k _ hpkd => dvd_trans hpkd h, _⟩
[GOAL]
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ (∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) → d ∣ n
[PROOFSTEP]
rw [← factorization_prime_le_iff_dvd hd hn]
[GOAL]
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ (∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) → ∀ (p : ℕ), Prime p → ↑(factorization d) p ≤ ↑(factorization n) p
[PROOFSTEP]
intro h p pp
[GOAL]
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
h : ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
p : ℕ
pp : Prime p
⊢ ↑(factorization d) p ≤ ↑(factorization n) p
[PROOFSTEP]
simp_rw [← pp.pow_dvd_iff_le_factorization hn]
[GOAL]
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
h : ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
p : ℕ
pp : Prime p
⊢ p ^ ↑(factorization d) p ∣ n
[PROOFSTEP]
exact h p _ pp (ord_proj_dvd _ _)
[GOAL]
n : ℕ
⊢ ∏ p in toFinset (factors n), p ∣ n
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
n : ℕ
hn : n = 0
⊢ ∏ p in toFinset (factors n), p ∣ n
[PROOFSTEP]
subst hn
[GOAL]
case pos
⊢ ∏ p in toFinset (factors 0), p ∣ 0
[PROOFSTEP]
simp
[GOAL]
case neg
n : ℕ
hn : ¬n = 0
⊢ ∏ p in toFinset (factors n), p ∣ n
[PROOFSTEP]
simpa [prod_factors hn] using Multiset.toFinset_prod_dvd_prod (n.factors : Multiset ℕ)
[GOAL]
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
[PROOFSTEP]
let dfac := a.factorization ⊓ b.factorization
[GOAL]
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
[PROOFSTEP]
let d := dfac.prod Nat.pow
[GOAL]
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
[PROOFSTEP]
have dfac_prime : ∀ p : ℕ, p ∈ dfac.support → Prime p :=
  by
  intro p hp
  have : p ∈ a.factors ∧ p ∈ b.factors := by simpa using hp
  exact prime_of_mem_factors this.1
[GOAL]
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
⊢ ∀ (p : ℕ), p ∈ dfac.support → Prime p
[PROOFSTEP]
intro p hp
[GOAL]
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
p : ℕ
hp : p ∈ dfac.support
⊢ Prime p
[PROOFSTEP]
have : p ∈ a.factors ∧ p ∈ b.factors := by simpa using hp
[GOAL]
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
p : ℕ
hp : p ∈ dfac.support
⊢ p ∈ factors a ∧ p ∈ factors b
[PROOFSTEP]
simpa using hp
[GOAL]
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
p : ℕ
hp : p ∈ dfac.support
this : p ∈ factors a ∧ p ∈ factors b
⊢ Prime p
[PROOFSTEP]
exact prime_of_mem_factors this.1
[GOAL]
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
[PROOFSTEP]
have h1 : d.factorization = dfac := prod_pow_factorization_eq_self dfac_prime
[GOAL]
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
[PROOFSTEP]
have hd_pos : d ≠ 0 := (factorizationEquiv.invFun ⟨dfac, dfac_prime⟩).2.ne'
[GOAL]
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
[PROOFSTEP]
suffices d = gcd a b by rwa [← this]
[GOAL]
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
this : d = gcd a b
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
[PROOFSTEP]
rwa [← this]
[GOAL]
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ d = gcd a b
[PROOFSTEP]
apply gcd_greatest
[GOAL]
case hda
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ d ∣ a
[PROOFSTEP]
rw [← factorization_le_iff_dvd hd_pos ha_pos, h1]
[GOAL]
case hda
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ dfac ≤ factorization a
[PROOFSTEP]
exact inf_le_left
[GOAL]
case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ d ∣ b
[PROOFSTEP]
rw [← factorization_le_iff_dvd hd_pos hb_pos, h1]
[GOAL]
case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ dfac ≤ factorization b
[PROOFSTEP]
exact inf_le_right
[GOAL]
case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ d
[PROOFSTEP]
intro e hea heb
[GOAL]
case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
⊢ e ∣ d
[PROOFSTEP]
rcases Decidable.eq_or_ne e 0 with (rfl | he_pos)
[GOAL]
case hd.inl
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
hea : 0 ∣ a
heb : 0 ∣ b
⊢ 0 ∣ d
[PROOFSTEP]
simp only [zero_dvd_iff] at hea 
[GOAL]
case hd.inl
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
heb : 0 ∣ b
hea : a = 0
⊢ 0 ∣ d
[PROOFSTEP]
contradiction
[GOAL]
case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
⊢ e ∣ d
[PROOFSTEP]
have hea' := (factorization_le_iff_dvd he_pos ha_pos).mpr hea
[GOAL]
case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
hea' : factorization e ≤ factorization a
⊢ e ∣ d
[PROOFSTEP]
have heb' := (factorization_le_iff_dvd he_pos hb_pos).mpr heb
[GOAL]
case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
hea' : factorization e ≤ factorization a
heb' : factorization e ≤ factorization b
⊢ e ∣ d
[PROOFSTEP]
simp [← factorization_le_iff_dvd he_pos hd_pos, h1, hea', heb']
[GOAL]
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ factorization (lcm a b) = factorization a ⊔ factorization b
[PROOFSTEP]
rw [← add_right_inj (a.gcd b).factorization, ←
  factorization_mul (mt gcd_eq_zero_iff.1 fun h => ha h.1) (lcm_ne_zero ha hb), gcd_mul_lcm, factorization_gcd ha hb,
  factorization_mul ha hb]
[GOAL]
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ factorization a + factorization b = factorization a ⊓ factorization b + factorization a ⊔ factorization b
[PROOFSTEP]
ext1
[GOAL]
case h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ ↑(factorization a + factorization b) a✝ = ↑(factorization a ⊓ factorization b + factorization a ⊔ factorization b) a✝
[PROOFSTEP]
exact (min_add_max _ _).symm
[GOAL]
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
⊢ Finset.prod (toFinset (factors (gcd m n))) f * Finset.prod (toFinset (factors (m * n))) f =
    Finset.prod (toFinset (factors m)) f * Finset.prod (toFinset (factors n)) f
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hm0)
[GOAL]
case inl
β : Type u_1
inst✝ : CommMonoid β
m : ℕ
f : ℕ → β
⊢ Finset.prod (toFinset (factors (gcd m 0))) f * Finset.prod (toFinset (factors (m * 0))) f =
    Finset.prod (toFinset (factors m)) f * Finset.prod (toFinset (factors 0)) f
[PROOFSTEP]
simp
[GOAL]
case inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
⊢ Finset.prod (toFinset (factors (gcd m n))) f * Finset.prod (toFinset (factors (m * n))) f =
    Finset.prod (toFinset (factors m)) f * Finset.prod (toFinset (factors n)) f
[PROOFSTEP]
rcases eq_or_ne m 0 with (rfl | hn0)
[GOAL]
case inr.inl
β : Type u_1
inst✝ : CommMonoid β
n : ℕ
f : ℕ → β
hm0 : n ≠ 0
⊢ Finset.prod (toFinset (factors (gcd 0 n))) f * Finset.prod (toFinset (factors (0 * n))) f =
    Finset.prod (toFinset (factors 0)) f * Finset.prod (toFinset (factors n)) f
[PROOFSTEP]
simp
[GOAL]
case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
hn0 : m ≠ 0
⊢ Finset.prod (toFinset (factors (gcd m n))) f * Finset.prod (toFinset (factors (m * n))) f =
    Finset.prod (toFinset (factors m)) f * Finset.prod (toFinset (factors n)) f
[PROOFSTEP]
rw [← @Finset.prod_union_inter _ _ m.factors.toFinset n.factors.toFinset, mul_comm]
[GOAL]
case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
hn0 : m ≠ 0
⊢ Finset.prod (toFinset (factors (m * n))) f * Finset.prod (toFinset (factors (gcd m n))) f =
    (∏ x in toFinset (factors m) ∪ toFinset (factors n), f x) * ∏ x in toFinset (factors m) ∩ toFinset (factors n), f x
[PROOFSTEP]
congr
[GOAL]
case inr.inr.e_a.e_s
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
hn0 : m ≠ 0
⊢ toFinset (factors (m * n)) = toFinset (factors m) ∪ toFinset (factors n)
[PROOFSTEP]
apply factors_mul_toFinset
[GOAL]
case inr.inr.e_a.e_s.ha
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
hn0 : m ≠ 0
⊢ m ≠ 0
[PROOFSTEP]
assumption
[GOAL]
case inr.inr.e_a.e_s.hb
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
hn0 : m ≠ 0
⊢ n ≠ 0
[PROOFSTEP]
assumption
[GOAL]
case inr.inr.e_a.e_s
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm0 : n ≠ 0
hn0 : m ≠ 0
⊢ toFinset (factors (gcd m n)) = toFinset (factors m) ∩ toFinset (factors n)
[PROOFSTEP]
simp only [← support_factorization, factorization_gcd hn0 hm0, Finsupp.support_inf]
[GOAL]
n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ {i | i ≠ 0 ∧ p ^ i ∣ n} = Set.Icc 1 (↑(factorization n) p)
[PROOFSTEP]
ext
[GOAL]
case h
n p : ℕ
pp : Prime p
hn : n ≠ 0
x✝ : ℕ
⊢ x✝ ∈ {i | i ≠ 0 ∧ p ^ i ∣ n} ↔ x✝ ∈ Set.Icc 1 (↑(factorization n) p)
[PROOFSTEP]
simp [lt_succ_iff, one_le_iff_ne_zero, pp.pow_dvd_iff_le_factorization hn]
[GOAL]
n p : ℕ
pp : Prime p
⊢ Icc 1 (↑(factorization n) p) = Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
p : ℕ
pp : Prime p
⊢ Icc 1 (↑(factorization 0) p) = Finset.filter (fun i => p ^ i ∣ 0) (Ico 1 0)
[PROOFSTEP]
simp
[GOAL]
case inr
n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ Icc 1 (↑(factorization n) p) = Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)
[PROOFSTEP]
ext x
[GOAL]
case inr.a
n p : ℕ
pp : Prime p
hn : n ≠ 0
x : (fun x => ℕ) p
⊢ x ∈ Icc 1 (↑(factorization n) p) ↔ x ∈ Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)
[PROOFSTEP]
simp only [mem_Icc, Finset.mem_filter, mem_Ico, and_assoc, and_congr_right_iff, pp.pow_dvd_iff_le_factorization hn,
  iff_and_self]
[GOAL]
case inr.a
n p : ℕ
pp : Prime p
hn : n ≠ 0
x : (fun x => ℕ) p
⊢ 1 ≤ x → x ≤ ↑(factorization n) p → x < n
[PROOFSTEP]
exact fun _ H => lt_of_le_of_lt H (factorization_lt p hn)
[GOAL]
n p : ℕ
pp : Prime p
⊢ ↑(factorization n) p = card (Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n))
[PROOFSTEP]
simp [← Icc_factorization_eq_pow_dvd n pp]
[GOAL]
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
⊢ Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n) = Finset.filter (fun i => p ^ i ∣ n) (Icc 1 b)
[PROOFSTEP]
ext x
[GOAL]
case a
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
⊢ x ∈ Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n) ↔ x ∈ Finset.filter (fun i => p ^ i ∣ n) (Icc 1 b)
[PROOFSTEP]
simp only [Finset.mem_filter, mem_Ico, mem_Icc, and_congr_left_iff, and_congr_right_iff]
[GOAL]
case a
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
⊢ p ^ x ∣ n → 1 ≤ x → (x < n ↔ x ≤ b)
[PROOFSTEP]
rintro h1 -
[GOAL]
case a
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
h1 : p ^ x ∣ n
⊢ x < n ↔ x ≤ b
[PROOFSTEP]
simp [lt_of_pow_dvd_right hn pp.two_le h1, (pow_le_iff_le_right pp.two_le).1 ((le_of_dvd hn.bot_lt h1).trans hb)]
[GOAL]
p a b : ℕ
hab : coprime a b
⊢ ↑(factorization (a * b)) p = ↑(factorization a) p + ↑(factorization b) p
[PROOFSTEP]
simp only [← factors_count_eq, perm_iff_count.mp (perm_factors_mul_of_coprime hab), count_append]
[GOAL]
a b : ℕ
hab : coprime a b
⊢ factorization (a * b) = factorization a + factorization b
[PROOFSTEP]
ext q
[GOAL]
case h
a b : ℕ
hab : coprime a b
q : ℕ
⊢ ↑(factorization (a * b)) q = ↑(factorization a + factorization b) q
[PROOFSTEP]
rw [Finsupp.add_apply, factorization_mul_apply_of_coprime hab]
[GOAL]
p a b : ℕ
hab : coprime a b
hpa : p ∈ factors a
⊢ ↑(factorization (a * b)) p = ↑(factorization a) p
[PROOFSTEP]
rw [factorization_mul_apply_of_coprime hab, ← factors_count_eq, ← factors_count_eq,
  count_eq_zero_of_not_mem (coprime_factors_disjoint hab hpa), add_zero]
[GOAL]
p a b : ℕ
hab : coprime a b
hpb : p ∈ factors b
⊢ ↑(factorization (a * b)) p = ↑(factorization b) p
[PROOFSTEP]
rw [mul_comm]
[GOAL]
p a b : ℕ
hab : coprime a b
hpb : p ∈ factors b
⊢ ↑(factorization (b * a)) p = ↑(factorization b) p
[PROOFSTEP]
exact factorization_eq_of_coprime_left (coprime_comm.mp hab) hpb
[GOAL]
a b : ℕ
hab : coprime a b
⊢ _root_.Disjoint (factorization a).support (factorization b).support
[PROOFSTEP]
simpa only [support_factorization] using disjoint_toFinset_iff_disjoint.mpr (coprime_factors_disjoint hab)
[GOAL]
a b : ℕ
hab : coprime a b
⊢ (factorization (a * b)).support = (factorization a).support ∪ (factorization b).support
[PROOFSTEP]
rw [factorization_mul_of_coprime hab]
[GOAL]
a b : ℕ
hab : coprime a b
⊢ (factorization a + factorization b).support = (factorization a).support ∪ (factorization b).support
[PROOFSTEP]
exact support_add_eq (factorization_disjoint_of_coprime hab)
[GOAL]
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
⊢ P (k + 2)
[PROOFSTEP]
let p := (k + 2).minFac
[GOAL]
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
⊢ P (k + 2)
[PROOFSTEP]
have hp : Prime p :=
  minFac_prime
    (succ_succ_ne_one k)
      -- the awkward `let` stuff here is because `factorization` is noncomputable (Finsupp);
            -- we get around this by using the computable `factors.count`, and rewriting when we want
            -- to use the `factorization` API
[GOAL]
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
hp : Prime p
⊢ P (k + 2)
[PROOFSTEP]
let t := (k + 2).factors.count p
[GOAL]
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
hp : Prime p
t : ℕ := count p (factors (k + 2))
⊢ P (k + 2)
[PROOFSTEP]
have ht : t = (k + 2).factorization p := factors_count_eq
[GOAL]
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
hp : Prime p
t : ℕ := count p (factors (k + 2))
ht : t = ↑(factorization (k + 2)) p
⊢ P (k + 2)
[PROOFSTEP]
have hpt : p ^ t ∣ k + 2 := by
  rw [ht]
  exact ord_proj_dvd _ _
[GOAL]
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
hp : Prime p
t : ℕ := count p (factors (k + 2))
ht : t = ↑(factorization (k + 2)) p
⊢ p ^ t ∣ k + 2
[PROOFSTEP]
rw [ht]
[GOAL]
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
hp : Prime p
t : ℕ := count p (factors (k + 2))
ht : t = ↑(factorization (k + 2)) p
⊢ p ^ ↑(factorization (k + 2)) p ∣ k + 2
[PROOFSTEP]
exact ord_proj_dvd _ _
[GOAL]
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
hp : Prime p
t : ℕ := count p (factors (k + 2))
ht : t = ↑(factorization (k + 2)) p
hpt : p ^ t ∣ k + 2
⊢ P (k + 2)
[PROOFSTEP]
have htp : 0 < t := by
  rw [ht]
  exact hp.factorization_pos_of_dvd (Nat.succ_ne_zero _) (minFac_dvd _)
[GOAL]
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
hp : Prime p
t : ℕ := count p (factors (k + 2))
ht : t = ↑(factorization (k + 2)) p
hpt : p ^ t ∣ k + 2
⊢ 0 < t
[PROOFSTEP]
rw [ht]
[GOAL]
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
hp : Prime p
t : ℕ := count p (factors (k + 2))
ht : t = ↑(factorization (k + 2)) p
hpt : p ^ t ∣ k + 2
⊢ 0 < ↑(factorization (k + 2)) p
[PROOFSTEP]
exact hp.factorization_pos_of_dvd (Nat.succ_ne_zero _) (minFac_dvd _)
[GOAL]
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
hp : Prime p
t : ℕ := count p (factors (k + 2))
ht : t = ↑(factorization (k + 2)) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ P (k + 2)
[PROOFSTEP]
convert h ((k + 2) / p ^ t) p t hp _ _ _ using 1
[GOAL]
case h.e'_1
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
hp : Prime p
t : ℕ := count p (factors (k + 2))
ht : t = ↑(factorization (k + 2)) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ k + 2 = p ^ t * ((k + 2) / p ^ t)
[PROOFSTEP]
rw [Nat.mul_div_cancel' hpt]
[GOAL]
case convert_1
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
hp : Prime p
t : ℕ := count p (factors (k + 2))
ht : t = ↑(factorization (k + 2)) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ ¬p ∣ (k + 2) / p ^ t
[PROOFSTEP]
rw [Nat.dvd_div_iff hpt, ← pow_succ, ht]
[GOAL]
case convert_1
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
hp : Prime p
t : ℕ := count p (factors (k + 2))
ht : t = ↑(factorization (k + 2)) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ ¬p ^ succ (↑(factorization (k + 2)) p) ∣ k + 2
[PROOFSTEP]
exact pow_succ_factorization_not_dvd (k + 1).succ_ne_zero hp
[GOAL]
case convert_2
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
hp : Prime p
t : ℕ := count p (factors (k + 2))
ht : t = ↑(factorization (k + 2)) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ 0 < t
[PROOFSTEP]
exact htp
[GOAL]
case convert_3
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
hp : Prime p
t : ℕ := count p (factors (k + 2))
ht : t = ↑(factorization (k + 2)) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ P ((k + 2) / p ^ t)
[PROOFSTEP]
apply hk _ (Nat.div_lt_of_lt_mul _)
[GOAL]
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
hp : Prime p
t : ℕ := count p (factors (k + 2))
ht : t = ↑(factorization (k + 2)) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ k + 2 < p ^ t * (k + 2)
[PROOFSTEP]
rw [lt_mul_iff_one_lt_left Nat.succ_pos', one_lt_pow_iff htp.ne]
[GOAL]
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
h : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → P m
p : ℕ := minFac (k + 2)
hp : Prime p
t : ℕ := count p (factors (k + 2))
ht : t = ↑(factorization (k + 2)) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ 1 < p
[PROOFSTEP]
exact hp.one_lt
[GOAL]
P : ℕ → Sort u_1
hp : (p n : ℕ) → Prime p → 0 < n → P (p ^ n)
h0 : P 0
h1 : P 1
h : (a b : ℕ) → 1 < a → 1 < b → coprime a b → P a → P b → P (a * b)
⊢ (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
[PROOFSTEP]
intro a p n hp' hpa hn hPa
[GOAL]
P : ℕ → Sort u_1
hp : (p n : ℕ) → Prime p → 0 < n → P (p ^ n)
h0 : P 0
h1 : P 1
h : (a b : ℕ) → 1 < a → 1 < b → coprime a b → P a → P b → P (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : P a
⊢ P (p ^ n * a)
[PROOFSTEP]
by_cases ha1 : a = 1
[GOAL]
case pos
P : ℕ → Sort u_1
hp : (p n : ℕ) → Prime p → 0 < n → P (p ^ n)
h0 : P 0
h1 : P 1
h : (a b : ℕ) → 1 < a → 1 < b → coprime a b → P a → P b → P (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : P a
ha1 : a = 1
⊢ P (p ^ n * a)
[PROOFSTEP]
rw [ha1, mul_one]
[GOAL]
case pos
P : ℕ → Sort u_1
hp : (p n : ℕ) → Prime p → 0 < n → P (p ^ n)
h0 : P 0
h1 : P 1
h : (a b : ℕ) → 1 < a → 1 < b → coprime a b → P a → P b → P (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : P a
ha1 : a = 1
⊢ P (p ^ n)
[PROOFSTEP]
exact hp p n hp' hn
[GOAL]
case neg
P : ℕ → Sort u_1
hp : (p n : ℕ) → Prime p → 0 < n → P (p ^ n)
h0 : P 0
h1 : P 1
h : (a b : ℕ) → 1 < a → 1 < b → coprime a b → P a → P b → P (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : P a
ha1 : ¬a = 1
⊢ P (p ^ n * a)
[PROOFSTEP]
refine' h (p ^ n) a (hp'.one_lt.trans_le (le_self_pow hn.ne' _)) _ _ (hp _ _ hp' hn) hPa
[GOAL]
case neg.refine'_1
P : ℕ → Sort u_1
hp : (p n : ℕ) → Prime p → 0 < n → P (p ^ n)
h0 : P 0
h1 : P 1
h : (a b : ℕ) → 1 < a → 1 < b → coprime a b → P a → P b → P (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : P a
ha1 : ¬a = 1
⊢ 1 < a
[PROOFSTEP]
contrapose! hpa
[GOAL]
case neg.refine'_1
P : ℕ → Sort u_1
hp : (p n : ℕ) → Prime p → 0 < n → P (p ^ n)
h0 : P 0
h1 : P 1
h : (a b : ℕ) → 1 < a → 1 < b → coprime a b → P a → P b → P (a * b)
a p n : ℕ
hp' : Prime p
hn : 0 < n
hPa : P a
ha1 : ¬a = 1
hpa : a ≤ 1
⊢ p ∣ a
[PROOFSTEP]
simp [lt_one_iff.1 (lt_of_le_of_ne hpa ha1)]
[GOAL]
case neg.refine'_2
P : ℕ → Sort u_1
hp : (p n : ℕ) → Prime p → 0 < n → P (p ^ n)
h0 : P 0
h1 : P 1
h : (a b : ℕ) → 1 < a → 1 < b → coprime a b → P a → P b → P (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : P a
ha1 : ¬a = 1
⊢ coprime (p ^ n) a
[PROOFSTEP]
simpa [hn, Prime.coprime_iff_not_dvd hp']
[GOAL]
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
hp : (p : ℕ) → Prime p → P p
h : (a b : ℕ) → P a → P b → P (a * b)
p n✝ : ℕ
hp' : Prime p
n : ℕ
hn : P (p ^ n)
⊢ P (p ^ succ n)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
P : ℕ → Sort u_1
h0 : P 0
h1 : P 1
hp : (p : ℕ) → Prime p → P p
h : (a b : ℕ) → P a → P b → P (a * b)
p n✝ : ℕ
hp' : Prime p
n : ℕ
hn : P (p ^ n)
⊢ P (p ^ n * p)
[PROOFSTEP]
apply h _ _ hn (hp p hp')
[GOAL]
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ ∀ {n : ℕ}, n ≠ 0 → f n = Finsupp.prod (factorization n) fun p k => f (p ^ k)
[PROOFSTEP]
apply Nat.recOnPosPrimePosCoprime
[GOAL]
case hp
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ ∀ (p n : ℕ), Prime p → 0 < n → p ^ n ≠ 0 → f (p ^ n) = Finsupp.prod (factorization (p ^ n)) fun p k => f (p ^ k)
[PROOFSTEP]
rintro p k hp -
  -
      -- Porting note: replaced `simp` with `rw`
[GOAL]
case hp
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ k) = Finsupp.prod (factorization (p ^ k)) fun p k => f (p ^ k)
[PROOFSTEP]
rw [Prime.factorization_pow hp, Finsupp.prod_single_index _]
[GOAL]
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ 0) = 1
[PROOFSTEP]
rwa [pow_zero]
[GOAL]
case h0
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ 0 ≠ 0 → f 0 = Finsupp.prod (factorization 0) fun p k => f (p ^ k)
[PROOFSTEP]
simp
[GOAL]
case h1
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ 1 ≠ 0 → f 1 = Finsupp.prod (factorization 1) fun p k => f (p ^ k)
[PROOFSTEP]
rintro -
[GOAL]
case h1
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ f 1 = Finsupp.prod (factorization 1) fun p k => f (p ^ k)
[PROOFSTEP]
rw [factorization_one, hf]
[GOAL]
case h1
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ 1 = Finsupp.prod 0 fun p k => f (p ^ k)
[PROOFSTEP]
simp
[GOAL]
case h
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        coprime a b →
          (a ≠ 0 → f a = Finsupp.prod (factorization a) fun p k => f (p ^ k)) →
            (b ≠ 0 → f b = Finsupp.prod (factorization b) fun p k => f (p ^ k)) →
              a * b ≠ 0 → f (a * b) = Finsupp.prod (factorization (a * b)) fun p k => f (p ^ k)
[PROOFSTEP]
intro a b _ _ hab ha hb hab_pos
[GOAL]
case h
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : coprime a b
ha : a ≠ 0 → f a = Finsupp.prod (factorization a) fun p k => f (p ^ k)
hb : b ≠ 0 → f b = Finsupp.prod (factorization b) fun p k => f (p ^ k)
hab_pos : a * b ≠ 0
⊢ f (a * b) = Finsupp.prod (factorization (a * b)) fun p k => f (p ^ k)
[PROOFSTEP]
rw [h_mult a b hab, ha (left_ne_zero_of_mul hab_pos), hb (right_ne_zero_of_mul hab_pos),
  factorization_mul_of_coprime hab, ← prod_add_index_of_disjoint]
[GOAL]
case h.hd
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : coprime a b
ha : a ≠ 0 → f a = Finsupp.prod (factorization a) fun p k => f (p ^ k)
hb : b ≠ 0 → f b = Finsupp.prod (factorization b) fun p k => f (p ^ k)
hab_pos : a * b ≠ 0
⊢ _root_.Disjoint (factorization a).support (factorization b).support
[PROOFSTEP]
convert factorization_disjoint_of_coprime hab
[GOAL]
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ ∀ {n : ℕ}, f n = Finsupp.prod (factorization n) fun p k => f (p ^ k)
[PROOFSTEP]
apply Nat.recOnPosPrimePosCoprime
[GOAL]
case hp
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ ∀ (p n : ℕ), Prime p → 0 < n → f (p ^ n) = Finsupp.prod (factorization (p ^ n)) fun p k => f (p ^ k)
[PROOFSTEP]
rintro p k hp -
[GOAL]
case hp
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ k) = Finsupp.prod (factorization (p ^ k)) fun p k => f (p ^ k)
[PROOFSTEP]
simp only [hp.factorization_pow]
[GOAL]
case hp
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ k) = Finsupp.prod (single p k) fun p k => f (p ^ k)
[PROOFSTEP]
rw [prod_single_index _]
[GOAL]
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ 0) = 1
[PROOFSTEP]
simp [hf1]
[GOAL]
case h0
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ f 0 = Finsupp.prod (factorization 0) fun p k => f (p ^ k)
[PROOFSTEP]
simp [hf0]
[GOAL]
case h1
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ f 1 = Finsupp.prod (factorization 1) fun p k => f (p ^ k)
[PROOFSTEP]
rw [factorization_one, hf1]
[GOAL]
case h1
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ 1 = Finsupp.prod 0 fun p k => f (p ^ k)
[PROOFSTEP]
simp
[GOAL]
case h
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        coprime a b →
          (f a = Finsupp.prod (factorization a) fun p k => f (p ^ k)) →
            (f b = Finsupp.prod (factorization b) fun p k => f (p ^ k)) →
              f (a * b) = Finsupp.prod (factorization (a * b)) fun p k => f (p ^ k)
[PROOFSTEP]
intro a b _ _ hab ha hb
[GOAL]
case h
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : coprime a b
ha : f a = Finsupp.prod (factorization a) fun p k => f (p ^ k)
hb : f b = Finsupp.prod (factorization b) fun p k => f (p ^ k)
⊢ f (a * b) = Finsupp.prod (factorization (a * b)) fun p k => f (p ^ k)
[PROOFSTEP]
rw [h_mult a b hab, ha, hb, factorization_mul_of_coprime hab, ← prod_add_index_of_disjoint]
[GOAL]
case h.hd
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : coprime a b
ha : f a = Finsupp.prod (factorization a) fun p k => f (p ^ k)
hb : f b = Finsupp.prod (factorization b) fun p k => f (p ^ k)
⊢ _root_.Disjoint (factorization a).support (factorization b).support
[PROOFSTEP]
exact factorization_disjoint_of_coprime hab
[GOAL]
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b ↔ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
[PROOFSTEP]
constructor
[GOAL]
case mp
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b → ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
a : ℕ
ha hb : a ≠ 0
⊢ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p a
[PROOFSTEP]
simp
[GOAL]
case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b) → a = b
[PROOFSTEP]
intro h
[GOAL]
case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
⊢ a = b
[PROOFSTEP]
refine' eq_of_factorization_eq ha hb fun p => _
[GOAL]
case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
⊢ ↑(factorization a) p = ↑(factorization b) p
[PROOFSTEP]
by_cases pp : p.Prime
[GOAL]
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : Prime p
⊢ ↑(factorization a) p = ↑(factorization b) p
[PROOFSTEP]
simp [factorization_def, pp, h p pp]
[GOAL]
case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : ¬Prime p
⊢ ↑(factorization a) p = ↑(factorization b) p
[PROOFSTEP]
simp [factorization_eq_zero_of_non_prime, pp]
[GOAL]
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∏ p in Finset.filter Prime (Finset.range m), p ^ padicValNat p n = n
[PROOFSTEP]
conv =>
  rhs
  rw [← factorization_prod_pow_eq_self hn]
[GOAL]
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
| ∏ p in Finset.filter Prime (Finset.range m), p ^ padicValNat p n = n
[PROOFSTEP]
  rhs
  rw [← factorization_prod_pow_eq_self hn]
[GOAL]
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
| ∏ p in Finset.filter Prime (Finset.range m), p ^ padicValNat p n = n
[PROOFSTEP]
  rhs
  rw [← factorization_prod_pow_eq_self hn]
[GOAL]
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
| ∏ p in Finset.filter Prime (Finset.range m), p ^ padicValNat p n = n
[PROOFSTEP]
rhs
[GOAL]
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
| n
[PROOFSTEP]
rw [← factorization_prod_pow_eq_self hn]
[GOAL]
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∏ p in Finset.filter Prime (Finset.range m), p ^ padicValNat p n = Finsupp.prod (factorization n) fun x x_1 => x ^ x_1
[PROOFSTEP]
rw [eq_comm]
[GOAL]
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ (Finsupp.prod (factorization n) fun x x_1 => x ^ x_1) =
    ∏ p in Finset.filter Prime (Finset.range m), p ^ padicValNat p n
[PROOFSTEP]
apply Finset.prod_subset_one_on_sdiff
[GOAL]
case h
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ (factorization n).support ⊆ Finset.filter Prime (Finset.range m)
[PROOFSTEP]
exact fun p hp =>
  Finset.mem_filter.mpr
    ⟨Finset.mem_range.mpr (gt_of_gt_of_ge pr (le_of_mem_factorization hp)), prime_of_mem_factorization hp⟩
[GOAL]
case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ (x : ℕ), x ∈ Finset.filter Prime (Finset.range m) \ (factorization n).support → x ^ padicValNat x n = 1
[PROOFSTEP]
intro p hp
[GOAL]
case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ Finset.filter Prime (Finset.range m) \ (factorization n).support
⊢ p ^ padicValNat p n = 1
[PROOFSTEP]
cases' Finset.mem_sdiff.mp hp with hp1 hp2
[GOAL]
case hg.intro
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ Finset.filter Prime (Finset.range m) \ (factorization n).support
hp1 : p ∈ Finset.filter Prime (Finset.range m)
hp2 : ¬p ∈ (factorization n).support
⊢ p ^ padicValNat p n = 1
[PROOFSTEP]
rw [← factorization_def n (Finset.mem_filter.mp hp1).2]
[GOAL]
case hg.intro
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ Finset.filter Prime (Finset.range m) \ (factorization n).support
hp1 : p ∈ Finset.filter Prime (Finset.range m)
hp2 : ¬p ∈ (factorization n).support
⊢ p ^ ↑(factorization n) p = 1
[PROOFSTEP]
simp [Finsupp.not_mem_support_iff.mp hp2]
[GOAL]
case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ (x : ℕ), x ∈ (factorization n).support → (fun x x_1 => x ^ x_1) x (↑(factorization n) x) = x ^ padicValNat x n
[PROOFSTEP]
intro p hp
[GOAL]
case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ (factorization n).support
⊢ (fun x x_1 => x ^ x_1) p (↑(factorization n) p) = p ^ padicValNat p n
[PROOFSTEP]
simp [factorization_def n (prime_of_mem_factorization hp)]
[GOAL]
n p : ℕ
⊢ card (Finset.filter (fun e => p ∣ e + 1) (Finset.range n)) = n / p
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
p : ℕ
⊢ card (Finset.filter (fun e => p ∣ e + 1) (Finset.range zero)) = zero / p
[PROOFSTEP]
simp
[GOAL]
case succ
p n : ℕ
hn : card (Finset.filter (fun e => p ∣ e + 1) (Finset.range n)) = n / p
⊢ card (Finset.filter (fun e => p ∣ e + 1) (Finset.range (succ n))) = succ n / p
[PROOFSTEP]
simp [Nat.succ_div, add_ite, add_zero, Finset.range_succ, filter_insert, apply_ite card, card_insert_of_not_mem, hn]
[GOAL]
n p : ℕ
⊢ card (Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
p : ℕ
⊢ card (Finset.filter (fun x => p ∣ x) (Ioc 0 zero)) = zero / p
[PROOFSTEP]
simp
  -- TODO: Golf away `h1` after Yaël PRs a lemma asserting this
[GOAL]
case succ
p n : ℕ
IH : card (Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p
⊢ card (Finset.filter (fun x => p ∣ x) (Ioc 0 (succ n))) = succ n / p
[PROOFSTEP]
have h1 : Ioc 0 n.succ = insert n.succ (Ioc 0 n) :=
  by
  rcases n.eq_zero_or_pos with (rfl | hn)
  · simp
  simp_rw [← Ico_succ_succ, Ico_insert_right (succ_le_succ hn.le), Ico_succ_right]
[GOAL]
p n : ℕ
IH : card (Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p
⊢ Ioc 0 (succ n) = insert (succ n) (Ioc 0 n)
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn)
[GOAL]
case inl
p : ℕ
IH : card (Finset.filter (fun x => p ∣ x) (Ioc 0 0)) = 0 / p
⊢ Ioc 0 (succ 0) = insert (succ 0) (Ioc 0 0)
[PROOFSTEP]
simp
[GOAL]
case inr
p n : ℕ
IH : card (Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p
hn : n > 0
⊢ Ioc 0 (succ n) = insert (succ n) (Ioc 0 n)
[PROOFSTEP]
simp_rw [← Ico_succ_succ, Ico_insert_right (succ_le_succ hn.le), Ico_succ_right]
[GOAL]
case succ
p n : ℕ
IH : card (Finset.filter (fun x => p ∣ x) (Ioc 0 n)) = n / p
h1 : Ioc 0 (succ n) = insert (succ n) (Ioc 0 n)
⊢ card (Finset.filter (fun x => p ∣ x) (Ioc 0 (succ n))) = succ n / p
[PROOFSTEP]
simp [Nat.succ_div, add_ite, add_zero, h1, filter_insert, apply_ite card, card_insert_eq_ite, IH, Finset.mem_filter,
  mem_Ioc, not_le.2 (lt_add_one n), Nat.succ_eq_add_one]
