-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- A `k`-smooth number can be written as a square times a product of distinct primes `< k`. -/
lemma eq_prod_primes_mul_sq_of_mem_smoothNumbers {n k : ℕ} (h : n ∈ smoothNumbers k) :
    ∃ s ∈ k.primesBelow.powerset, ∃ m, n = m ^ 2 * (s.prod id)

Proof state:
case intro.intro.intro.refine_2
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ n = m ^ 2 * l.primeFactorsList.toFinset.prod id

Tactic:
rw [← H₁]

Result:
case intro.intro.intro.refine_2
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ m ^ 2 * l = m ^ 2 * l.primeFactorsList.toFinset.prod id

Proof state:
case intro.intro.intro.refine_1
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ l.primeFactorsList.toFinset ∈ k.primesBelow.powerset

Tactic:
simp only [toFinset_factors, Finset.mem_powerset]

Result:
case intro.intro.intro.refine_1
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ l.primeFactors ⊆ k.primesBelow

Proof state:
case intro.intro.intro.refine_2
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ m ^ 2 * l = m ^ 2 * l.primeFactorsList.toFinset.prod id

Tactic:
congr

Result:
case intro.intro.intro.refine_2.e_a
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ l = l.primeFactorsList.toFinset.prod id

Proof state:
case intro.intro.intro.refine_2.e_a
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ l = l.primeFactorsList.toFinset.prod id

Tactic:
simp only [toFinset_factors]

Result:
case intro.intro.intro.refine_2.e_a
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ l = l.primeFactors.prod id

Proof state:
case intro.intro.intro.refine_2.e_a
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ l = l.primeFactors.prod id

Tactic:
exact (prod_primeFactors_of_squarefree H₂).symm

Result:
no goals

Proof state:
case intro.intro.intro.refine_1
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ l.primeFactors ⊆ k.primesBelow

Tactic:
refine fun p hp ↦ mem_primesBelow.mpr ⟨?_, (mem_primeFactors.mp hp).1⟩

Result:
case intro.intro.intro.refine_1
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
p : ℕ
hp : p ∈ l.primeFactors
⊢ p < k

Proof state:
case intro.intro.intro
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
⊢ ∃ s ∈ k.primesBelow.powerset, ∃ m, n = m ^ 2 * s.prod id

Tactic:
have hl : l ∈ smoothNumbers k := mem_smoothNumbers_of_dvd h (Dvd.intro_left (m ^ 2) H₁)

Result:
case intro.intro.intro
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ ∃ s ∈ k.primesBelow.powerset, ∃ m, n = m ^ 2 * s.prod id

Proof state:
case intro.intro.intro.refine_1
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
p : ℕ
hp : p ∈ l.primeFactors
⊢ p < k

Tactic:
rw [mem_primeFactors] at hp

Result:
case intro.intro.intro.refine_1
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
p : ℕ
hp : Prime p ∧ p ∣ l ∧ l ≠ 0
⊢ p < k

Proof state:
case intro.intro.intro
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ ∃ s ∈ k.primesBelow.powerset, ∃ m, n = m ^ 2 * s.prod id

Tactic:
refine ⟨l.primeFactorsList.toFinset, ?_,  m, ?_⟩

Result:
case intro.intro.intro.refine_1
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ l.primeFactorsList.toFinset ∈ k.primesBelow.powerset

case intro.intro.intro.refine_2
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ n = m ^ 2 * l.primeFactorsList.toFinset.prod id

Proof state:
case intro.intro.intro.refine_1
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
p : ℕ
hp : Prime p ∧ p ∣ l ∧ l ≠ 0
⊢ p < k

Tactic:
exact mem_smoothNumbers'.mp hl p hp.1 hp.2.1

Result:
no goals

Proof state:
n k : ℕ
h : n ∈ k.smoothNumbers
⊢ ∃ s ∈ k.primesBelow.powerset, ∃ m, n = m ^ 2 * s.prod id

Tactic:
obtain ⟨l, m, H₁, H₂⟩ := sq_mul_squarefree n

Result:
case intro.intro.intro
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
⊢ ∃ s ∈ k.primesBelow.powerset, ∃ m, n = m ^ 2 * s.prod id