-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- The set of `k`-smooth numbers `≤ N` is contained in the set of numbers of the form `m^2 * P`,
where `m ≤ √N` and `P` is a product of distinct primes `< k`. -/
lemma smoothNumbersUpTo_subset_image (N k : ℕ) :
    smoothNumbersUpTo N k ⊆ Finset.image (fun (s, m) ↦ m ^ 2 * (s.prod id))
      (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).erase 0)

Proof state:
case intro.intro.intro.intro.refine_2
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m ^ 2 * 1 ≤ m ^ 2 * s.prod id

Tactic:
exact mul_le_mul_left' (Finset.one_le_prod' fun p hp ↦
  (prime_of_mem_primesBelow <| Finset.mem_powerset.mp hs hp).one_lt.le) _

Result:
no goals

Proof state:
case intro
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
⊢ n ∈
    Finset.image
      (fun x =>
        match x with
        | (s, m) => m ^ 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).erase 0)

Tactic:
obtain ⟨s, hs, m, hm⟩ := eq_prod_primes_mul_sq_of_mem_smoothNumbers hn₂

Result:
case intro.intro.intro.intro
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ n ∈
    Finset.image
      (fun x =>
        match x with
        | (s, m) => m ^ 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).erase 0)

Proof state:
case intro.intro.intro.intro
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ ∃ a b, (a ⊆ k.primesBelow ∧ b ≠ 0 ∧ b < N.sqrt.succ) ∧ b ^ 2 * ∏ x ∈ a, x = n

Tactic:
refine ⟨s, m, ⟨Finset.mem_powerset.mp hs, ?_, ?_⟩, hm.symm⟩

Result:
case intro.intro.intro.intro.refine_1
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m ≠ 0

case intro.intro.intro.intro.refine_2
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m < N.sqrt.succ

Proof state:
case intro.intro.intro.intro.refine_2
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m ^ 2 ≤ N

Tactic:
refine LE.le.trans ?_ (hm ▸ hn₁)

Result:
case intro.intro.intro.intro.refine_2
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m ^ 2 ≤ m ^ 2 * s.prod id

Proof state:
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
⊢ n ∈
    Finset.image
      (fun x =>
        match x with
        | (s, m) => m ^ 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).erase 0)

Tactic:
obtain ⟨hn₁, hn₂⟩ := mem_smoothNumbersUpTo.mp hn

Result:
case intro
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
⊢ n ∈
    Finset.image
      (fun x =>
        match x with
        | (s, m) => m ^ 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).erase 0)

Proof state:
N k : ℕ
⊢ N.smoothNumbersUpTo k ⊆
    Finset.image
      (fun x =>
        match x with
        | (s, m) => m ^ 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).erase 0)

Tactic:
intro n hn

Result:
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
⊢ n ∈
    Finset.image
      (fun x =>
        match x with
        | (s, m) => m ^ 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).erase 0)

Proof state:
case intro.intro.intro.intro.refine_1
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
this : ¬m = 0 ∧ ¬s.prod id = 0
⊢ m ≠ 0

Tactic:
exact this.1

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_2
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m < N.sqrt.succ

Tactic:
rw [lt_succ, le_sqrt']

Result:
case intro.intro.intro.intro.refine_2
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m ^ 2 ≤ N

Proof state:
case intro.intro.intro.intro
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ n ∈
    Finset.image
      (fun x =>
        match x with
        | (s, m) => m ^ 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).erase 0)

Tactic:
simp only [id_eq, Finset.mem_range, zero_lt_succ, not_true_eq_false, Finset.mem_image,
  Finset.mem_product, Finset.mem_powerset, Finset.mem_erase, Prod.exists]

Result:
case intro.intro.intro.intro
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ ∃ a b, (a ⊆ k.primesBelow ∧ b ≠ 0 ∧ b < N.sqrt.succ) ∧ b ^ 2 * ∏ x ∈ a, x = n

Proof state:
case intro.intro.intro.intro.refine_2
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m ^ 2 ≤ m ^ 2 * s.prod id

Tactic:
nth_rw 1 [← mul_one (m ^ 2)]

Result:
case intro.intro.intro.intro.refine_2
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m ^ 2 * 1 ≤ m ^ 2 * s.prod id

Proof state:
case intro.intro.intro.intro.refine_1
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m ≠ 0

Tactic:
have := hm ▸ ne_zero_of_mem_smoothNumbers hn₂

Result:
case intro.intro.intro.intro.refine_1
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
this : m ^ 2 * s.prod id ≠ 0
⊢ m ≠ 0

Proof state:
case intro.intro.intro.intro.refine_1
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
this : m ^ 2 * s.prod id ≠ 0
⊢ m ≠ 0

Tactic:
simp only [ne_eq, _root_.mul_eq_zero, sq_eq_zero_iff, not_or] at this

Result:
case intro.intro.intro.intro.refine_1
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
this : ¬m = 0 ∧ ¬s.prod id = 0
⊢ m ≠ 0