[GOAL]
⊢ factors 0 = []
[PROOFSTEP]
rw [factors]
[GOAL]
⊢ factors 1 = []
[PROOFSTEP]
rw [factors]
[GOAL]
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ factors n → Prime p
[PROOFSTEP]
match n with
| 0 => simp
| 1 => simp
| k + 2 =>
  intro p h
  let m := minFac (k + 2)
  have : (k + 2) / m < (k + 2) := factors_lemma
  have h₁ : p = m ∨ p ∈ factors ((k + 2) / m) := List.mem_cons.1 (by rwa [factors] at h )
  exact Or.casesOn h₁ (fun h₂ => h₂.symm ▸ minFac_prime (by simp)) prime_of_mem_factors
[GOAL]
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ factors 0 → Prime p
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ factors 1 → Prime p
[PROOFSTEP]
simp
[GOAL]
n k : ℕ
⊢ ∀ {p : ℕ}, p ∈ factors (k + 2) → Prime p
[PROOFSTEP]
intro p h
[GOAL]
n k p : ℕ
h : p ∈ factors (k + 2)
⊢ Prime p
[PROOFSTEP]
let m := minFac (k + 2)
[GOAL]
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
⊢ Prime p
[PROOFSTEP]
have : (k + 2) / m < (k + 2) := factors_lemma
[GOAL]
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ Prime p
[PROOFSTEP]
have h₁ : p = m ∨ p ∈ factors ((k + 2) / m) := List.mem_cons.1 (by rwa [factors] at h )
[GOAL]
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ p ∈ m :: factors ((k + 2) / m)
[PROOFSTEP]
rwa [factors] at h 
[GOAL]
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
h₁ : p = m ∨ p ∈ factors ((k + 2) / m)
⊢ Prime p
[PROOFSTEP]
exact Or.casesOn h₁ (fun h₂ => h₂.symm ▸ minFac_prime (by simp)) prime_of_mem_factors
[GOAL]
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
h₁ : p = m ∨ p ∈ factors ((k + 2) / m)
h₂ : p = m
⊢ k + 2 ≠ 1
[PROOFSTEP]
simp
[GOAL]
⊢ 0 ≠ 0 → List.prod (factors 0) = 0
[PROOFSTEP]
simp
[GOAL]
⊢ 1 ≠ 0 → List.prod (factors 1) = 1
[PROOFSTEP]
simp
[GOAL]
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ List.prod (factors (k + 2)) = k + 2
[PROOFSTEP]
have h₁ : (k + 2) / m ≠ 0 := fun h =>
  by
  have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h
  rw [zero_mul] at this ; exact (show k + 2 ≠ 0 by simp) this
[GOAL]
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
h : (k + 2) / m = 0
⊢ False
[PROOFSTEP]
have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h
[GOAL]
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0 * m
⊢ False
[PROOFSTEP]
rw [zero_mul] at this 
[GOAL]
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ False
[PROOFSTEP]
exact (show k + 2 ≠ 0 by simp) this
[GOAL]
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ k + 2 ≠ 0
[PROOFSTEP]
simp
[GOAL]
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
⊢ List.prod (factors (k + 2)) = k + 2
[PROOFSTEP]
rw [factors, List.prod_cons, prod_factors h₁, Nat.mul_div_cancel' (minFac_dvd _)]
[GOAL]
p : ℕ
hp : Prime p
⊢ factors p = [p]
[PROOFSTEP]
have : p = p - 2 + 2 := (tsub_eq_iff_eq_add_of_le hp.two_le).mp rfl
[GOAL]
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ factors p = [p]
[PROOFSTEP]
rw [this, Nat.factors]
[GOAL]
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ (let m := minFac (p - 2 + 2);
    let_fun this := (_ : (p - 2 + 2) / minFac (p - 2 + 2) < p - 2 + 2);
    m :: factors ((p - 2 + 2) / m)) =
    [p - 2 + 2]
[PROOFSTEP]
simp only [Eq.symm this]
[GOAL]
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ minFac p :: factors (p / minFac p) = [p]
[PROOFSTEP]
have : Nat.minFac p = p := (Nat.prime_def_minFac.mp hp).2
[GOAL]
p : ℕ
hp : Prime p
this✝ : p = p - 2 + 2
this : minFac p = p
⊢ minFac p :: factors (p / minFac p) = [p]
[PROOFSTEP]
simp only [this, Nat.factors, Nat.div_self (Nat.Prime.pos hp)]
[GOAL]
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ n → a ≤ p) → List.Chain (fun x x_1 => x ≤ x_1) a (factors n)
[PROOFSTEP]
match n with
| 0 => simp
| 1 => simp
| k + 2 =>
  intro a h
  let m := minFac (k + 2)
  have : (k + 2) / m < (k + 2) := factors_lemma
  rw [factors]
  refine' List.Chain.cons ((le_minFac.2 h).resolve_left (by simp)) (factors_chain _)
  exact fun p pp d => minFac_le_of_dvd pp.two_le (d.trans <| div_dvd_of_dvd <| minFac_dvd _)
[GOAL]
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ 0 → a ≤ p) → List.Chain (fun x x_1 => x ≤ x_1) a (factors 0)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ 1 → a ≤ p) → List.Chain (fun x x_1 => x ≤ x_1) a (factors 1)
[PROOFSTEP]
simp
[GOAL]
n k : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p) → List.Chain (fun x x_1 => x ≤ x_1) a (factors (k + 2))
[PROOFSTEP]
intro a h
[GOAL]
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
⊢ List.Chain (fun x x_1 => x ≤ x_1) a (factors (k + 2))
[PROOFSTEP]
let m := minFac (k + 2)
[GOAL]
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
⊢ List.Chain (fun x x_1 => x ≤ x_1) a (factors (k + 2))
[PROOFSTEP]
have : (k + 2) / m < (k + 2) := factors_lemma
[GOAL]
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ List.Chain (fun x x_1 => x ≤ x_1) a (factors (k + 2))
[PROOFSTEP]
rw [factors]
[GOAL]
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ List.Chain (fun x x_1 => x ≤ x_1) a
    (let m := minFac (k + 2);
    let_fun this := (_ : (k + 2) / minFac (k + 2) < k + 2);
    m :: factors ((k + 2) / m))
[PROOFSTEP]
refine' List.Chain.cons ((le_minFac.2 h).resolve_left (by simp)) (factors_chain _)
[GOAL]
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ ¬k + 2 = 1
[PROOFSTEP]
simp
[GOAL]
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ ∀ (p : ℕ), Prime p → p ∣ (k + 2) / minFac (k + 2) → minFac (k + 2) ≤ p
[PROOFSTEP]
exact fun p pp d => minFac_le_of_dvd pp.two_le (d.trans <| div_dvd_of_dvd <| minFac_dvd _)
[GOAL]
n : ℕ
⊢ factors (n + 2) = minFac (n + 2) :: factors ((n + 2) / minFac (n + 2))
[PROOFSTEP]
rw [factors]
[GOAL]
n : ℕ
⊢ factors n = [] ↔ n = 0 ∨ n = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
⊢ factors n = [] → n = 0 ∨ n = 1
[PROOFSTEP]
intro h
[GOAL]
case mpr
n : ℕ
⊢ n = 0 ∨ n = 1 → factors n = []
[PROOFSTEP]
intro h
[GOAL]
case mp
n : ℕ
h : factors n = []
⊢ n = 0 ∨ n = 1
[PROOFSTEP]
rcases n with (_ | _ | n)
[GOAL]
case mp.zero
h : factors zero = []
⊢ zero = 0 ∨ zero = 1
[PROOFSTEP]
exact Or.inl rfl
[GOAL]
case mp.succ.zero
h : factors (succ zero) = []
⊢ succ zero = 0 ∨ succ zero = 1
[PROOFSTEP]
exact Or.inr rfl
[GOAL]
case mp.succ.succ
n : ℕ
h : factors (succ (succ n)) = []
⊢ succ (succ n) = 0 ∨ succ (succ n) = 1
[PROOFSTEP]
rw [factors] at h 
[GOAL]
case mp.succ.succ
n : ℕ
h :
  (let m := minFac (n + 2);
    let_fun this := (_ : (n + 2) / minFac (n + 2) < n + 2);
    m :: factors ((n + 2) / m)) =
    []
⊢ succ (succ n) = 0 ∨ succ (succ n) = 1
[PROOFSTEP]
injection h
[GOAL]
case mpr
n : ℕ
h : n = 0 ∨ n = 1
⊢ factors n = []
[PROOFSTEP]
rcases h with (rfl | rfl)
[GOAL]
case mpr.inl
⊢ factors 0 = []
[PROOFSTEP]
exact factors_zero
[GOAL]
case mpr.inr
⊢ factors 1 = []
[PROOFSTEP]
exact factors_one
[GOAL]
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : factors a ~ factors b
⊢ a = b
[PROOFSTEP]
simpa [prod_factors ha, prod_factors hb] using List.Perm.prod_eq h
[GOAL]
n p : ℕ
h : p ∈ factors n
⊢ p ∣ n
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn)
[GOAL]
case inl
p : ℕ
h : p ∈ factors 0
⊢ p ∣ 0
[PROOFSTEP]
exact dvd_zero p
[GOAL]
case inr
n p : ℕ
h : p ∈ factors n
hn : n > 0
⊢ p ∣ n
[PROOFSTEP]
rwa [← mem_factors_iff_dvd hn.ne' (prime_of_mem_factors h)]
[GOAL]
n p : ℕ
h : p ∈ factors n
⊢ p ≤ n
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn)
[GOAL]
case inl
p : ℕ
h : p ∈ factors 0
⊢ p ≤ 0
[PROOFSTEP]
rw [factors_zero] at h 
[GOAL]
case inl
p : ℕ
h : p ∈ []
⊢ p ≤ 0
[PROOFSTEP]
cases h
[GOAL]
case inr
n p : ℕ
h : p ∈ factors n
hn : n > 0
⊢ p ≤ n
[PROOFSTEP]
exact le_of_dvd hn (dvd_of_mem_factors h)
[GOAL]
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ l ~ factors n
[PROOFSTEP]
refine' perm_of_prod_eq_prod _ _ _
[GOAL]
case refine'_1
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ prod l = prod (factors n)
[PROOFSTEP]
rw [h₁]
[GOAL]
case refine'_1
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ n = prod (factors n)
[PROOFSTEP]
refine' (prod_factors _).symm
[GOAL]
case refine'_1
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ n ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : prod l = 0
⊢ False
[PROOFSTEP]
rw [prod_eq_zero_iff] at h₁ 
[GOAL]
case refine'_1
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : 0 ∈ l
⊢ False
[PROOFSTEP]
exact Prime.ne_zero (h₂ 0 h₁) rfl
[GOAL]
case refine'_2
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → _root_.Prime p
[PROOFSTEP]
simp_rw [← prime_iff]
[GOAL]
case refine'_2
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → Prime p
[PROOFSTEP]
exact h₂
[GOAL]
case refine'_3
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ factors n → _root_.Prime p
[PROOFSTEP]
simp_rw [← prime_iff]
[GOAL]
case refine'_3
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ factors n → Prime p
[PROOFSTEP]
exact fun p => prime_of_mem_factors
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ factors (p ^ n) = replicate n p
[PROOFSTEP]
symm
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p = factors (p ^ n)
[PROOFSTEP]
rw [← List.replicate_perm]
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p ~ factors (p ^ n)
[PROOFSTEP]
apply Nat.factors_unique (List.prod_replicate n p)
[GOAL]
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ (p_1 : ℕ), p_1 ∈ replicate n p → Prime p_1
[PROOFSTEP]
intro q hq
[GOAL]
p : ℕ
hp : Prime p
n q : ℕ
hq : q ∈ replicate n p
⊢ Prime q
[PROOFSTEP]
rwa [eq_of_mem_replicate hq]
[GOAL]
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
⊢ n = p ^ length (factors n)
[PROOFSTEP]
set k := n.factors.length
[GOAL]
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := length (factors n)
⊢ n = p ^ k
[PROOFSTEP]
rw [← prod_factors hpos, ← prod_replicate k p,
  eq_replicate_of_mem fun d hd => h (prime_of_mem_factors hd) (dvd_of_mem_factors hd)]
[GOAL]
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ factors (a * b) ~ factors a ++ factors b
[PROOFSTEP]
refine' (factors_unique _ _).symm
[GOAL]
case refine'_1
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ prod (factors a ++ factors b) = a * b
[PROOFSTEP]
rw [List.prod_append, prod_factors ha, prod_factors hb]
[GOAL]
case refine'_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ (p : ℕ), p ∈ factors a ++ factors b → Prime p
[PROOFSTEP]
intro p hp
[GOAL]
case refine'_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ factors a ++ factors b
⊢ Prime p
[PROOFSTEP]
rw [List.mem_append] at hp 
[GOAL]
case refine'_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ factors a ∨ p ∈ factors b
⊢ Prime p
[PROOFSTEP]
cases' hp with hp' hp'
[GOAL]
case refine'_2.inl
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp' : p ∈ factors a
⊢ Prime p
[PROOFSTEP]
exact prime_of_mem_factors hp'
[GOAL]
case refine'_2.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp' : p ∈ factors b
⊢ Prime p
[PROOFSTEP]
exact prime_of_mem_factors hp'
[GOAL]
a b : ℕ
hab : coprime a b
⊢ factors (a * b) ~ factors a ++ factors b
[PROOFSTEP]
rcases a.eq_zero_or_pos with (rfl | ha)
[GOAL]
case inl
b : ℕ
hab : coprime 0 b
⊢ factors (0 * b) ~ factors 0 ++ factors b
[PROOFSTEP]
simp [(coprime_zero_left _).mp hab]
[GOAL]
case inr
a b : ℕ
hab : coprime a b
ha : a > 0
⊢ factors (a * b) ~ factors a ++ factors b
[PROOFSTEP]
rcases b.eq_zero_or_pos with (rfl | hb)
[GOAL]
case inr.inl
a : ℕ
ha : a > 0
hab : coprime a 0
⊢ factors (a * 0) ~ factors a ++ factors 0
[PROOFSTEP]
simp [(coprime_zero_right _).mp hab]
[GOAL]
case inr.inr
a b : ℕ
hab : coprime a b
ha : a > 0
hb : b > 0
⊢ factors (a * b) ~ factors a ++ factors b
[PROOFSTEP]
exact perm_factors_mul ha.ne' hb.ne'
[GOAL]
n k : ℕ
h : k ≠ 0
⊢ factors n <+ factors (n * k)
[PROOFSTEP]
cases' n with hn
[GOAL]
case zero
k : ℕ
h : k ≠ 0
⊢ factors zero <+ factors (zero * k)
[PROOFSTEP]
simp [zero_mul]
[GOAL]
case succ
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ factors (succ hn) <+ factors (succ hn * k)
[PROOFSTEP]
apply sublist_of_subperm_of_sorted _ (factors_sorted _) (factors_sorted _)
[GOAL]
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ factors (succ hn) <+~ factors (succ hn * k)
[PROOFSTEP]
simp [(perm_factors_mul (Nat.succ_ne_zero _) h).subperm_left]
[GOAL]
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ factors (succ hn) <+~ factors (succ hn) ++ factors k
[PROOFSTEP]
exact (sublist_append_left _ _).subperm
[GOAL]
n k : ℕ
h : n ∣ k
h' : k ≠ 0
⊢ factors n <+ factors k
[PROOFSTEP]
obtain ⟨a, rfl⟩ := h
[GOAL]
case intro
n a : ℕ
h' : n * a ≠ 0
⊢ factors n <+ factors (n * a)
[PROOFSTEP]
exact factors_sublist_right (right_ne_zero_of_mul h')
[GOAL]
a b : ℕ
ha : a ≠ 0
h : factors a <+~ factors b
⊢ a ∣ b
[PROOFSTEP]
rcases b.eq_zero_or_pos with (rfl | hb)
[GOAL]
case inl
a : ℕ
ha : a ≠ 0
h : factors a <+~ factors 0
⊢ a ∣ 0
[PROOFSTEP]
exact dvd_zero _
[GOAL]
case inr
a b : ℕ
ha : a ≠ 0
h : factors a <+~ factors b
hb : b > 0
⊢ a ∣ b
[PROOFSTEP]
rcases a with (_ | _ | a)
[GOAL]
case inr.zero
b : ℕ
hb : b > 0
ha : zero ≠ 0
h : factors zero <+~ factors b
⊢ zero ∣ b
[PROOFSTEP]
exact (ha rfl).elim
[GOAL]
case inr.succ.zero
b : ℕ
hb : b > 0
ha : succ zero ≠ 0
h : factors (succ zero) <+~ factors b
⊢ succ zero ∣ b
[PROOFSTEP]
exact
  one_dvd
    _
      --Porting note: previous proof
        --use (b.factors.diff a.succ.succ.factors).prod
[GOAL]
case inr.succ.succ
b : ℕ
hb : b > 0
a : ℕ
ha : succ (succ a) ≠ 0
h : factors (succ (succ a)) <+~ factors b
⊢ succ (succ a) ∣ b
[PROOFSTEP]
use(@List.diff _ instBEq b.factors a.succ.succ.factors).prod
[GOAL]
case h
b : ℕ
hb : b > 0
a : ℕ
ha : succ (succ a) ≠ 0
h : factors (succ (succ a)) <+~ factors b
⊢ b = succ (succ a) * prod (List.diff (factors b) (factors (succ (succ a))))
[PROOFSTEP]
nth_rw 1 [← Nat.prod_factors ha]
[GOAL]
case h
b : ℕ
hb : b > 0
a : ℕ
ha : succ (succ a) ≠ 0
h : factors (succ (succ a)) <+~ factors b
⊢ b = prod (factors (succ (succ a))) * prod (List.diff (factors b) (factors (succ (succ a))))
[PROOFSTEP]
rw [← List.prod_append, List.Perm.prod_eq <| List.subperm_append_diff_self_of_count_le <| List.subperm_ext_iff.mp h,
  Nat.prod_factors hb.ne']
[GOAL]
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ p ∈ factors (a * b) ↔ p ∈ factors a ∨ p ∈ factors b
[PROOFSTEP]
rw [mem_factors (mul_ne_zero ha hb), mem_factors ha, mem_factors hb, ← and_or_left]
[GOAL]
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ Prime p ∧ p ∣ a * b ↔ Prime p ∧ (p ∣ a ∨ p ∣ b)
[PROOFSTEP]
simpa only [and_congr_right_iff] using Prime.dvd_mul
[GOAL]
a b : ℕ
hab : coprime a b
⊢ List.Disjoint (factors a) (factors b)
[PROOFSTEP]
intro q hqa hqb
[GOAL]
a b : ℕ
hab : coprime a b
q : ℕ
hqa : q ∈ factors a
hqb : q ∈ factors b
⊢ False
[PROOFSTEP]
apply not_prime_one
[GOAL]
a b : ℕ
hab : coprime a b
q : ℕ
hqa : q ∈ factors a
hqb : q ∈ factors b
⊢ Prime 1
[PROOFSTEP]
rw [← eq_one_of_dvd_coprimes hab (dvd_of_mem_factors hqa) (dvd_of_mem_factors hqb)]
[GOAL]
a b : ℕ
hab : coprime a b
q : ℕ
hqa : q ∈ factors a
hqb : q ∈ factors b
⊢ Prime q
[PROOFSTEP]
exact prime_of_mem_factors hqa
[GOAL]
a b : ℕ
hab : coprime a b
p : ℕ
⊢ p ∈ factors (a * b) ↔ p ∈ factors a ∪ factors b
[PROOFSTEP]
rcases a.eq_zero_or_pos with (rfl | ha)
[GOAL]
case inl
b p : ℕ
hab : coprime 0 b
⊢ p ∈ factors (0 * b) ↔ p ∈ factors 0 ∪ factors b
[PROOFSTEP]
simp [(coprime_zero_left _).mp hab]
[GOAL]
case inr
a b : ℕ
hab : coprime a b
p : ℕ
ha : a > 0
⊢ p ∈ factors (a * b) ↔ p ∈ factors a ∪ factors b
[PROOFSTEP]
rcases b.eq_zero_or_pos with (rfl | hb)
[GOAL]
case inr.inl
a p : ℕ
ha : a > 0
hab : coprime a 0
⊢ p ∈ factors (a * 0) ↔ p ∈ factors a ∪ factors 0
[PROOFSTEP]
simp [(coprime_zero_right _).mp hab]
[GOAL]
case inr.inr
a b : ℕ
hab : coprime a b
p : ℕ
ha : a > 0
hb : b > 0
⊢ p ∈ factors (a * b) ↔ p ∈ factors a ∪ factors b
[PROOFSTEP]
rw [mem_factors_mul ha.ne' hb.ne', List.mem_union_iff]
[GOAL]
p a b : ℕ
hpa : p ∈ factors a
hb : b ≠ 0
⊢ p ∈ factors (a * b)
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
p b : ℕ
hb : b ≠ 0
hpa : p ∈ factors 0
⊢ p ∈ factors (0 * b)
[PROOFSTEP]
simp at hpa 
[GOAL]
case inr
p a b : ℕ
hpa : p ∈ factors a
hb : b ≠ 0
ha : a ≠ 0
⊢ p ∈ factors (a * b)
[PROOFSTEP]
apply (mem_factors_mul ha hb).2 (Or.inl hpa)
[GOAL]
p a b : ℕ
hpb : p ∈ factors b
ha : a ≠ 0
⊢ p ∈ factors (a * b)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
p a b : ℕ
hpb : p ∈ factors b
ha : a ≠ 0
⊢ p ∈ factors (b * a)
[PROOFSTEP]
exact mem_factors_mul_left hpb ha
