awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
⊢ HPow.hPow (β := ℕ) p ((m.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList).prod =
    m
have rw : (replicate (List.count p m.primeFactorsList) p ++ List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList).prod =
  m
Tactic: rw [← primeFactorsList_count_eq, ← prod_replicate, ← prod_append]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
⊢ (replicate (List.count p m.primeFactorsList) p ++
        List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList).prod =
    m
have nth_rewrite : (replicate (List.count p m.primeFactorsList) p ++ List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList).prod =
  m.primeFactorsList.prod
Tactic: nth_rewrite 3 [← prod_primeFactorsList hm₀]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
⊢ List.filter (fun (x : ℕ) ↦ decide (x = p)) m.primeFactorsList =
    List.filter (fun (x : ℕ) ↦ decide (x ∉ s)) m.primeFactorsList
have refine : ∀ (q : ℕ) (hq : q ∈ m.primeFactorsList), decide (q ∉ s) = decide (q = p)
Tactic: refine (filter_congr fun q hq ↦ ?_).symm
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
q : ℕ
hq : q ∈ m.primeFactorsList
⊢ decide (q ∉ s) = decide (q = p)
have simp : (!decide (q ∈ s)) = decide (q = p)
Tactic: simp only [decide_not]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
q : ℕ
hq : q ∈ m.primeFactorsList
⊢ (!decide (q ∈ s)) = decide (q = p)
have inl : ∀ (h : q = p), (!decide (q ∈ s)) = decide (q = p)
Tactic: rcases Finset.mem_insert.mp <| hm _ hq with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
q : ℕ
hq : q ∈ m.primeFactorsList
inl : ∀ (h : q = p), (!decide (q ∈ s)) = decide (q = p)
⊢ (!decide (q ∈ s)) = decide (q = p)
have inr : ∀ (h : q ∈ s), (!decide (q ∈ s)) = decide (q = p)
Tactic: rcases Finset.mem_insert.mp <| hm _ hq with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
q : ℕ
hq : q ∈ m.primeFactorsList
h : q ∈ s
⊢ (!decide (q ∈ s)) = decide (q = p)
have inr : ¬q = p
Tactic: simp only [h, decide_true, Bool.not_true, false_eq_decide_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
⊢ (replicate (List.count p m.primeFactorsList) p ++
        List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList).prod =
    m.primeFactorsList.prod
have this : List.filter (fun (x : ℕ) ↦ decide (x = p)) m.primeFactorsList =
  List.filter (fun (x : ℕ) ↦ decide (x ∉ s)) m.primeFactorsList
Tactic: have : m.primeFactorsList.filter (· = p) = m.primeFactorsList.filter (· ∉ s) := by
      refine (filter_congr fun q hq ↦ ?_).symm
      simp only [decide_not]
      rcases Finset.mem_insert.mp <| hm _ hq with h | h
      · simp only [h, hs, decide_false, Bool.not_false, decide_true]
      · simp only [h, decide_true, Bool.not_true, false_eq_decide_iff]
        exact fun H ↦ hs <| H ▸ h
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
this :
  List.filter (fun (x : ℕ) ↦ decide (x = p)) m.primeFactorsList =
    List.filter (fun (x : ℕ) ↦ decide (x ∉ s)) m.primeFactorsList
⊢ (replicate (List.count p m.primeFactorsList) p ++
        List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList).prod =
    m.primeFactorsList.prod
have refine : List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ++
    List.filter (fun (x : ℕ) ↦ decide (x ∉ s)) m.primeFactorsList ~
  m.primeFactorsList
Tactic: refine prod_eq <| (filter_eq p).symm ▸ this ▸ perm_append_comm.trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
this :
  List.filter (fun (x : ℕ) ↦ decide (x = p)) m.primeFactorsList =
    List.filter (fun (x : ℕ) ↦ decide (x ∉ s)) m.primeFactorsList
⊢ List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ++
      List.filter (fun (x : ℕ) ↦ decide (x ∉ s)) m.primeFactorsList ~
    m.primeFactorsList
have simp : List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ++
    List.filter (fun (x : ℕ) ↦ !decide (x ∈ s)) m.primeFactorsList ~
  m.primeFactorsList
Tactic: simp only [decide_not]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
n : ℕ
⊢ n.smoothNumbers = factoredNumbers n.primesBelow
have rw : factoredNumbers (Finset.range n) = factoredNumbers n.primesBelow
Tactic: rw [smoothNumbers_eq_factoredNumbers]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
n : ℕ
⊢ factoredNumbers (Finset.range n) = factoredNumbers n.primesBelow
have refine : ∀ (m : ℕ) (hm : m ∈ factoredNumbers (Finset.range n)), m ∈ factoredNumbers n.primesBelow
Tactic: refine Set.Subset.antisymm (fun m hm ↦ ?_) <| factoredNumbers_mono Finset.mem_of_mem_filter
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
n m : ℕ
hm : m ∈ factoredNumbers (Finset.range n)
⊢ m ∈ factoredNumbers n.primesBelow
have simp_rw : ∀ (hm : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ Finset.range n) (p : ℕ), Prime p → p ∣ m → p ∈ n.primesBelow
Tactic: simp_rw [mem_factoredNumbers'] at hm ⊢
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
n m k : ℕ
h : m ∈ n.smoothNumbers
h' : k ∣ m
⊢ k ∈ n.smoothNumbers
have simp : ∀ (h : m ∈ factoredNumbers (Finset.range n)), k ∈ factoredNumbers (Finset.range n)
Tactic: simp only [smoothNumbers_eq_factoredNumbers] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
m₁ m₂ n : ℕ
hm1 : m₁ ∈ n.smoothNumbers
hm2 : m₂ ∈ n.smoothNumbers
⊢ m₁ * m₂ ∈ n.smoothNumbers
have rw : ∀ (hm1 : m₁ ∈ factoredNumbers (Finset.range n)) (hm2 : m₂ ∈ factoredNumbers (Finset.range n)),
  m₁ * m₂ ∈ factoredNumbers (Finset.range n)
Tactic: rw [smoothNumbers_eq_factoredNumbers] at hm1 hm2 ⊢
Cleared hypotheses: hm1, hm2
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
⊢ p ^ e * n ∈ p.succ.smoothNumbers
have this : NoZeroDivisors ℕ
Tactic: have : NoZeroDivisors ℕ := inferInstance
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
⊢ p ^ e * n ∈ p.succ.smoothNumbers
have hp' : p ^ e ≠ 0
Tactic: have hp' := pow_ne_zero e hp
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
⊢ p ^ e * n ∈ p.succ.smoothNumbers
have refine : ∀ (q : ℕ) (hq : q ∈ (p ^ e * n).primeFactorsList), q < p.succ
Tactic: refine ⟨mul_ne_zero hp' hn.1, fun q hq ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
⊢ q < p.succ
have inl : ∀ (H : q ∈ (p ^ e).primeFactorsList), q < p.succ
Tactic: rcases (mem_primeFactorsList_mul hp' hn.1).mp hq with H | H
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
inl : ∀ (H : q ∈ (p ^ e).primeFactorsList), q < p.succ
⊢ q < p.succ
have inr : ∀ (H : q ∈ n.primeFactorsList), q < p.succ
Tactic: rcases (mem_primeFactorsList_mul hp' hn.1).mp hq with H | H
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : q ∈ (p ^ e).primeFactorsList
⊢ q < p.succ
have H₁ : Prime q ∧ q ∣ p ^ e
Tactic: rw [mem_primeFactorsList hp'] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
p n : ℕ
hp : Prime p
hn : n ∈ p.smoothNumbers
⊢ p.Coprime n
have hn₁ : n ∈ factoredNumbers (Finset.range p)
Tactic: simp only [smoothNumbers_eq_factoredNumbers] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k : ℕ
⊢ #(N.smoothNumbersUpTo k) + #(N.roughNumbersUpTo k) = N
have rw : #({x ∈ Finset.range (N + 1) | x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers}) = N
Tactic: rw [smoothNumbersUpTo, roughNumbersUpTo,
    ← Finset.card_union_of_disjoint <| Finset.disjoint_filter.mpr fun n _ hn₂ h ↦ h.2 hn₂,
    Finset.filter_union_right]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
N k : ℕ
this : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
n : ℕ
⊢ n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0
have this₁ : n ∈ k.smoothNumbers → n ≠ 0
Tactic: have : n ∈ smoothNumbers k → n ≠ 0 := ne_zero_of_mem_smoothNumbers
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k : ℕ
this_1 : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
n : ℕ
this : n ∈ k.smoothNumbers → n ≠ 0
⊢ n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0
have refine : ∀ (H : n ≠ 0), n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers
Tactic: refine ⟨fun H ↦ Or.elim H this fun H ↦ H.1, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
N k : ℕ
this : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
⊢ #({x ∈ Finset.range (N + 1) | x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers}) = N
have hn' : ∀ (n : ℕ), n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0
Tactic: have hn' (n) : n ∈ smoothNumbers k ∨ n ≠ 0 ∧ n ∉ smoothNumbers k ↔ n ≠ 0 := by
      have : n ∈ smoothNumbers k → n ≠ 0 := ne_zero_of_mem_smoothNumbers
      refine ⟨fun H ↦ Or.elim H this fun H ↦ H.1, fun H ↦ ?_⟩
      simp only [ne_eq, H, not_false_eq_true, true_and, or_not]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k : ℕ
⊢ #({x ∈ Finset.range (N + 1) | x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers}) = N
have suffices : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
Tactic: suffices #{x ∈ Finset.range (N + 1) | x ≠ 0} = N by
    have hn' (n) : n ∈ smoothNumbers k ∨ n ≠ 0 ∧ n ∉ smoothNumbers k ↔ n ≠ 0 := by
      have : n ∈ smoothNumbers k → n ≠ 0 := ne_zero_of_mem_smoothNumbers
      refine ⟨fun H ↦ Or.elim H this fun H ↦ H.1, fun H ↦ ?_⟩
      simp only [ne_eq, H, not_false_eq_true, true_and, or_not]
    rwa [Finset.filter_congr (s := Finset.range (succ N)) fun n _ ↦ hn' n]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k : ℕ
⊢ #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
have rw : #(Finset.range N.succ) - 1 = N
Tactic: rw [Finset.filter_ne', Finset.card_erase_of_mem <| Finset.mem_range_succ_iff.mpr <| zero_le N]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
n k : ℕ
h : n ∈ k.smoothNumbers
⊢ ∃ s ∈ k.primesBelow.powerset, ∃ (m : ℕ), n = HPow.hPow (β := ℕ) m 2 * s.prod id
have obtain : ∀ (l m : ℕ) (H₁ : HPow.hPow (β := ℕ) m 2 * l = n) (H₂ : Squarefree l),
  ∃ s ∈ k.primesBelow.powerset, ∃ (m : ℕ), n = HPow.hPow (β := ℕ) m 2 * s.prod id
Tactic: obtain ⟨l, m, H₁, H₂⟩ := sq_mul_squarefree n
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : HPow.hPow (β := ℕ) m 2 * l = n
H₂ : Squarefree l
⊢ ∃ s ∈ k.primesBelow.powerset, ∃ (m : ℕ), n = HPow.hPow (β := ℕ) m 2 * s.prod id
have hl : l ∈ k.smoothNumbers
Tactic: have hl : l ∈ smoothNumbers k := mem_smoothNumbers_of_dvd h (Dvd.intro_left (m ^ 2) H₁)
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : HPow.hPow (β := ℕ) m 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ ∃ s ∈ k.primesBelow.powerset, ∃ (m : ℕ), n = HPow.hPow (β := ℕ) m 2 * s.prod id
have refine_1 : l.primeFactorsList.toFinset ∈ k.primesBelow.powerset
Tactic: refine ⟨l.primeFactorsList.toFinset, ?_, m, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : HPow.hPow (β := ℕ) m 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
refine_1 : l.primeFactorsList.toFinset ∈ k.primesBelow.powerset
⊢ ∃ s ∈ k.primesBelow.powerset, ∃ (m : ℕ), n = HPow.hPow (β := ℕ) m 2 * s.prod id
have refine_2 : n = HPow.hPow (β := ℕ) m 2 * l.primeFactorsList.toFinset.prod id
Tactic: refine ⟨l.primeFactorsList.toFinset, ?_, m, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : HPow.hPow (β := ℕ) m 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ l.primeFactorsList.toFinset ∈ k.primesBelow.powerset
have refine_1 : l.primeFactors ⊆ k.primesBelow
Tactic: simp only [toFinset_factors, Finset.mem_powerset]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : HPow.hPow (β := ℕ) m 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ l.primeFactors ⊆ k.primesBelow
have refine_1 : ∀ (p : ℕ) (hp : p ∈ l.primeFactors), p < k
Tactic: refine fun p hp ↦ mem_primesBelow.mpr ⟨?_, (mem_primeFactors.mp hp).1⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : HPow.hPow (β := ℕ) m 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
p : ℕ
hp : p ∈ l.primeFactors
⊢ p < k
have hp₁ : Prime p ∧ p ∣ l ∧ l ≠ 0
Tactic: rw [mem_primeFactors] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : HPow.hPow (β := ℕ) m 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ n = HPow.hPow (β := ℕ) m 2 * l.primeFactorsList.toFinset.prod id
have refine_2 : HPow.hPow (β := ℕ) m 2 * l = HPow.hPow (β := ℕ) m 2 * l.primeFactorsList.toFinset.prod id
Tactic: rw [← H₁]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : HPow.hPow (β := ℕ) m 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ HPow.hPow (β := ℕ) m 2 * l = HPow.hPow (β := ℕ) m 2 * l.primeFactorsList.toFinset.prod id
have refine_2 : l = l.primeFactorsList.toFinset.prod id
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
⊢ Membership.mem (γ := Finset ℕ)
    (Finset.image
      (fun (x : Finset ℕ × ℕ) ↦
        match (motive := Finset ℕ × ℕ → ℕ) x with
        | (s, m) => HPow.hPow (β := ℕ) m 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0))
    n
have hn₁ : n ≤ N
Tactic: obtain ⟨hn₁, hn₂⟩ := mem_smoothNumbersUpTo.mp hn
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
⊢ Membership.mem (γ := Finset ℕ)
    (Finset.image
      (fun (x : Finset ℕ × ℕ) ↦
        match (motive := Finset ℕ × ℕ → ℕ) x with
        | (s, m) => HPow.hPow (β := ℕ) m 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0))
    n
have hn₂ : n ∈ k.smoothNumbers
Tactic: obtain ⟨hn₁, hn₂⟩ := mem_smoothNumbersUpTo.mp hn
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
⊢ Membership.mem (γ := Finset ℕ)
    (Finset.image
      (fun (x : Finset ℕ × ℕ) ↦
        match (motive := Finset ℕ × ℕ → ℕ) x with
        | (s, m) => HPow.hPow (β := ℕ) m 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0))
    n
have obtain : ∀ (s : Finset ℕ) (hs : s ∈ k.primesBelow.powerset) (m : ℕ) (hm : n = HPow.hPow (β := ℕ) m 2 * s.prod id),
  Membership.mem (γ := Finset ℕ)
    (Finset.image
      (fun (x : Finset ℕ × ℕ) ↦
        match (motive := Finset ℕ × ℕ → ℕ) x with
        | (s, m) => HPow.hPow (β := ℕ) m 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0))
    n
Tactic: obtain ⟨s, hs, m, hm⟩ := eq_prod_primes_mul_sq_of_mem_smoothNumbers hn₂
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
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 = HPow.hPow (β := ℕ) m 2 * s.prod id
⊢ Membership.mem (γ := Finset ℕ)
    (Finset.image
      (fun (x : Finset ℕ × ℕ) ↦
        match (motive := Finset ℕ × ℕ → ℕ) x with
        | (s, m) => HPow.hPow (β := ℕ) m 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0))
    n
have simp : ∃ (a : Finset ℕ) (b : ℕ), (a ⊆ k.primesBelow ∧ b ≠ 0 ∧ b < N.sqrt + 1) ∧ HPow.hPow (β := ℕ) b 2 * ∏ x ∈ a, x = n
Tactic: simp only [id_eq, Finset.mem_range, Finset.mem_image,
    Finset.mem_product, Finset.mem_powerset, Finset.mem_erase, Prod.exists]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
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 = HPow.hPow (β := ℕ) m 2 * s.prod id
⊢ ∃ (a : Finset ℕ) (b : ℕ), (a ⊆ k.primesBelow ∧ b ≠ 0 ∧ b < N.sqrt + 1) ∧ HPow.hPow (β := ℕ) b 2 * ∏ x ∈ a, x = n
have refine_1 : m ≠ 0
Tactic: refine ⟨s, m, ⟨Finset.mem_powerset.mp hs, ?_, ?_⟩, hm.symm⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
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 = HPow.hPow (β := ℕ) m 2 * s.prod id
refine_1 : m ≠ 0
⊢ ∃ (a : Finset ℕ) (b : ℕ), (a ⊆ k.primesBelow ∧ b ≠ 0 ∧ b < N.sqrt + 1) ∧ HPow.hPow (β := ℕ) b 2 * ∏ x ∈ a, x = n
have refine_2 : m < N.sqrt + 1
Tactic: refine ⟨s, m, ⟨Finset.mem_powerset.mp hs, ?_, ?_⟩, hm.symm⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
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 = HPow.hPow (β := ℕ) m 2 * s.prod id
⊢ m ≠ 0
have this : HPow.hPow (β := ℕ) m 2 * s.prod id ≠ 0
Tactic: have := hm ▸ ne_zero_of_mem_smoothNumbers hn₂
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
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 = HPow.hPow (β := ℕ) m 2 * s.prod id
this : HPow.hPow (β := ℕ) m 2 * s.prod id ≠ 0
⊢ m ≠ 0
have this₁ : ¬m = 0 ∧ ¬s.prod id = 0
Tactic: simp only [ne_eq, _root_.mul_eq_zero, sq_eq_zero_iff, not_or] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
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 = HPow.hPow (β := ℕ) m 2 * s.prod id
⊢ m < N.sqrt + 1
have refine_2 : HPow.hPow (β := ℕ) m 2 ≤ N
Tactic: rw [Nat.lt_succ_iff, le_sqrt']
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
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 = HPow.hPow (β := ℕ) m 2 * s.prod id
⊢ HPow.hPow (β := ℕ) m 2 ≤ N
have refine_2 : HPow.hPow (β := ℕ) m 2 ≤ HPow.hPow (β := ℕ) m 2 * s.prod id
Tactic: refine LE.le.trans ?_ (hm ▸ hn₁)
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
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 = HPow.hPow (β := ℕ) m 2 * s.prod id
⊢ HPow.hPow (β := ℕ) m 2 ≤ HPow.hPow (β := ℕ) m 2 * s.prod id
have refine_2 : HPow.hPow (β := ℕ) m 2 * 1 ≤ HPow.hPow (β := ℕ) m 2 * s.prod id
Tactic: nth_rw 1 [← mul_one (m ^ 2)]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
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 = HPow.hPow (β := ℕ) m 2 * s.prod id
⊢ HPow.hPow (β := ℕ) m 2 * 1 ≤ HPow.hPow (β := ℕ) m 2 * s.prod id
have refine_2 : 1 ≤ s.prod id
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k : ℕ
⊢ #(N.smoothNumbersUpTo k) ≤ HPow.hPow (α := ℕ) 2 #k.primesBelow * N.sqrt
have h : HPow.hPow (α := ℕ) 2 #k.primesBelow * N.sqrt = #(k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0)
Tactic: convert! (Finset.card_le_card <| smoothNumbersUpTo_subset_image N k).trans <| Finset.card_image_le
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k : ℕ
⊢ N.roughNumbersUpTo k =
    ((N + 1).primesBelow \ k.primesBelow).biUnion fun (p : ℕ) ↦ {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m}
have h : ∀ (m : ℕ),
  m ∈ N.roughNumbersUpTo k ↔
    Membership.mem (γ := Finset ℕ)
      (((N + 1).primesBelow \ k.primesBelow).biUnion fun (p : ℕ) ↦ {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m}) m
Tactic: ext m
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k m : ℕ
tauto tauto₁ : ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
⊢ ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
have mp : ∀ (P Q : Prop), P ∧ (P → Q) → P ∧ Q
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k m : ℕ
tauto tauto₁ : ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
mp : ∀ (P Q : Prop), P ∧ (P → Q) → P ∧ Q
⊢ ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
have mpr : ∀ (P Q : Prop), P ∧ Q → P ∧ (P → Q)
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k m : ℕ
tauto tauto₁ : ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
mp : ∀ (P Q : Prop), P ∧ (P → Q) → P ∧ Q
mpr : ∀ (P Q : Prop), P ∧ Q → P ∧ (P → Q)
⊢ ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
have mp₁ : ∀ (P Q : Prop), P → (P → Q) → P ∧ Q
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k m : ℕ
tauto tauto₁ : ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
mp : ∀ (P Q : Prop), P ∧ (P → Q) → P ∧ Q
mpr : ∀ (P Q : Prop), P ∧ Q → P ∧ (P → Q)
mp₁ mp₂ : ∀ (P Q : Prop), P → (P → Q) → P ∧ Q
⊢ ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
have mp₃ : ∀ (P Q : Prop), P → (P → Q) → P
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k m : ℕ
tauto tauto₁ : ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
mp : ∀ (P Q : Prop), P ∧ (P → Q) → P ∧ Q
mpr : ∀ (P Q : Prop), P ∧ Q → P ∧ (P → Q)
mp₁ mp₂ : ∀ (P Q : Prop), P → (P → Q) → P ∧ Q
mp₃ : ∀ (P Q : Prop), P → (P → Q) → P
⊢ ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
have mp₄ : ∀ (P Q : Prop), P → (P → Q) → Q
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k m : ℕ
tauto tauto₁ : ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
mp : ∀ (P Q : Prop), P ∧ (P → Q) → P ∧ Q
mpr : ∀ (P Q : Prop), P ∧ Q → P ∧ (P → Q)
mp₁ mp₂ : ∀ (P Q : Prop), P → (P → Q) → P ∧ Q
mp₃ : ∀ (P Q : Prop), P → (P → Q) → P
mp₄ : ∀ (P Q : Prop), P → (P → Q) → Q
⊢ ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
have mpr₁ : ∀ (P Q : Prop), P → Q → P ∧ (P → Q)
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N k m : ℕ
tauto tauto₁ : ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
mp : ∀ (P Q : Prop), P ∧ (P → Q) → P ∧ Q
mpr : ∀ (P Q : Prop), P ∧ Q → P ∧ (P → Q)
mp₁ mp₂ : ∀ (P Q : Prop), P → (P → Q) → P ∧ Q
mp₃ : ∀ (P Q : Prop), P → (P → Q) → P
mp₄ : ∀ (P Q : Prop), P → (P → Q) → Q
mpr₁ mpr₂ : ∀ (P Q : Prop), P → Q → P ∧ (P → Q)
⊢ ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q
have mpr₃ : ∀ (P Q : Prop), P → Q → P
Tactic: tauto