awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
p e m : ℕ
hp : Prime p
hm : m ∈ p.smoothNumbers
⊢ (↑((equivProdNatSmoothNumbers hp : (a : ℕ × (↑p.smoothNumbers : Type)) → (↑(p + 1).smoothNumbers : Type))
          (e, Subtype.mk (p := fun (x : ℕ) ↦ x ∈ p.smoothNumbers) m hm)) :
      ℕ) =
    p ^ e * m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
p : ℕ
hp : Prime p
x : ℕ × (↑p.smoothNumbers : Type)
⊢ (↑((equivProdNatSmoothNumbers hp : (a : ℕ × (↑p.smoothNumbers : Type)) → (↑(p + 1).smoothNumbers : Type)) x) : ℕ) =
    p ^ x.1 * (↑x.2 : ℕ)

Tactic:
rfl

Premises used: Set.Mem, setOf, Multiset.Mem, Nat.smoothNumbers, Nat.lt, rfl
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k n : ℕ
⊢ n ∈ N.smoothNumbersUpTo k ↔ n ≤ N ∧ n ∈ k.smoothNumbers

Tactic:
simp [smoothNumbersUpTo]

Premises used: Nat.smoothNumbersUpTo
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k : ℕ
rw : #({x ∈ Finset.range (N + 1) | x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers}) = N
⊢ #(N.smoothNumbersUpTo k) + #(N.roughNumbersUpTo k) = 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]

Premises used: Iff.mpr, Nat.roughNumbersUpTo, Finset.disjoint_filter, Finset.filter_union_right, Nat.smoothNumbersUpTo, Finset.card_union_of_disjoint
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k : ℕ
this : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
n : ℕ
⊢ n ∈ k.smoothNumbers → n ≠ 0

Tactic:
have : n ∈ smoothNumbers k → n ≠ 0 := ne_zero_of_mem_smoothNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
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

Tactic:
⟨fun H ↦ Or.elim H this fun H ↦ H.1, fun H ↦ ?_⟩

Premises used: And.left, Iff.intro, Or.elim
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k : ℕ
this_1 : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
n : ℕ
this : n ∈ k.smoothNumbers → n ≠ 0
refine : ∀ (H : n ≠ 0), n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers
⊢ n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0

Tactic:
refine ⟨fun H ↦ Or.elim H this fun H ↦ H.1, fun H ↦ ?_⟩
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k : ℕ
this_1 : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
n : ℕ
this : n ∈ k.smoothNumbers → n ≠ 0
H : n ≠ 0
⊢ n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers

Tactic:
simp only [ne_eq, H, not_false_eq_true, true_and, or_not]

Premises used: ne_eq, or_not, not_false_eq_true, true_and
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k : ℕ
this : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
⊢ ∀ (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]
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k : ℕ
this : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
hn' : ∀ (n : ℕ), n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0
rwa rwa₁ rwa₂ rwa₃ : #({n ∈ Finset.range N.succ | n ≠ 0}) = N
⊢ #({x ∈ Finset.range (N + 1) | x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers}) = N

Tactic:
rwa [Finset.filter_congr (s := Finset.range (succ N)) fun n _ ↦ hn' n]

Premises used: Finset.filter_congr
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k : ℕ
suffices : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
⊢ #({x ∈ Finset.range (N + 1) | x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers}) = 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]
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k : ℕ
rw : #(Finset.range N.succ) - 1 = N
⊢ #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N

Tactic:
rw [Finset.filter_ne', Finset.card_erase_of_mem <| Finset.mem_range_succ_iff.mpr <| zero_le N]

Premises used: Iff.mpr, Nat.zero_le, Finset.mem_range_succ_iff, Finset.card_erase_of_mem, Finset.filter_ne'
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k : ℕ
⊢ #(Finset.range N.succ) - 1 = N

Tactic:
simp only [Finset.card_range, succ_sub_succ_eq_sub, Nat.sub_zero]

Premises used: Finset.card_range, Nat.sub_zero, Nat.succ_sub_succ_eq_sub
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n k : ℕ
h : n ∈ k.smoothNumbers
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
⊢ ∃ s ∈ k.primesBelow.powerset, ∃ (m : ℕ), n = HPow.hPow (β := ℕ) m 2 * s.prod id

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

Premises used: Nat.sq_mul_squarefree
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : HPow.hPow (β := ℕ) m 2 * l = n
H₂ : Squarefree l
⊢ l ∈ k.smoothNumbers

Tactic:
have hl : l ∈ smoothNumbers k := mem_smoothNumbers_of_dvd h (Dvd.intro_left (m ^ 2) H₁)
-- Module: Mathlib.NumberTheory.SmoothNumbers
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

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

Premises used: List.toFinset, And.intro, Exists.intro, Nat.primeFactorsList
-- Module: Mathlib.NumberTheory.SmoothNumbers
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
refine_2 : n = HPow.hPow (β := ℕ) m 2 * l.primeFactorsList.toFinset.prod id
⊢ ∃ s ∈ k.primesBelow.powerset, ∃ (m : ℕ), n = HPow.hPow (β := ℕ) m 2 * s.prod id

Tactic:
refine ⟨l.primeFactorsList.toFinset, ?_, m, ?_⟩
-- Module: Mathlib.NumberTheory.SmoothNumbers
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.primeFactors ⊆ k.primesBelow
⊢ l.primeFactorsList.toFinset ∈ k.primesBelow.powerset

Tactic:
simp only [toFinset_factors, Finset.mem_powerset]

Premises used: Finset.mem_powerset, Nat.toFinset_factors
-- Module: Mathlib.NumberTheory.SmoothNumbers
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

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

Premises used: Iff.mpr, And.left, And.intro, Iff.mp, Nat.mem_primesBelow, Nat.mem_primeFactors
-- Module: Mathlib.NumberTheory.SmoothNumbers
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 : ∀ (p : ℕ) (hp : p ∈ l.primeFactors), p < k
⊢ l.primeFactors ⊆ k.primesBelow

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

Premises used: Iff.mpr, And.left, And.intro, Iff.mp, Nat.mem_primesBelow, Nat.mem_primeFactors
-- Module: Mathlib.NumberTheory.SmoothNumbers
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
⊢ Prime p ∧ p ∣ l ∧ l ≠ 0

Tactic:
rw [mem_primeFactors] at hp

Premises used: Nat.mem_primeFactors
-- Module: Mathlib.NumberTheory.SmoothNumbers
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 : Prime p ∧ p ∣ l ∧ l ≠ 0
⊢ p < k

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

Premises used: Nat.mem_smoothNumbers', And.right, And.left, Iff.mp
-- Module: Mathlib.NumberTheory.SmoothNumbers
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 : Prime p ∧ p ∣ l ∧ l ≠ 0
⊢ p < k

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

Premises used: Nat.mem_smoothNumbers', And.right, And.left, Iff.mp
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : HPow.hPow (β := ℕ) m 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
refine_2 : HPow.hPow (β := ℕ) m 2 * l = HPow.hPow (β := ℕ) m 2 * l.primeFactorsList.toFinset.prod id
⊢ n = HPow.hPow (β := ℕ) m 2 * l.primeFactorsList.toFinset.prod id

Tactic:
rw [← H₁]
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : HPow.hPow (β := ℕ) m 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
refine_2 : l = l.primeFactorsList.toFinset.prod id
⊢ HPow.hPow (β := ℕ) m 2 * l = HPow.hPow (β := ℕ) m 2 * l.primeFactorsList.toFinset.prod id

Tactic:
congr
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : HPow.hPow (β := ℕ) m 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ l = l.primeFactors.prod id

Tactic:
(prod_primeFactors_of_squarefree H₂).symm

Premises used: Nat.prod_primeFactors_of_squarefree, Eq.symm
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : HPow.hPow (β := ℕ) m 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ l = l.primeFactors.prod id

Tactic:
exact (prod_primeFactors_of_squarefree H₂).symm

Premises used: Nat.prod_primeFactors_of_squarefree, Eq.symm
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
⊢ n ≤ N

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

Premises used: Iff.mp, Nat.mem_smoothNumbersUpTo
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
⊢ n ∈ k.smoothNumbers

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

Premises used: Iff.mp, Nat.mem_smoothNumbersUpTo
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
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
⊢ 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₂

Premises used: Nat.eq_prod_primes_mul_sq_of_mem_smoothNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
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
simp : ∃ (a : Finset ℕ) (b : ℕ), (a ⊆ k.primesBelow ∧ b ≠ 0 ∧ b < N.sqrt + 1) ∧ HPow.hPow (β := ℕ) b 2 * ∏ x ∈ a, x = 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

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

Premises used: Finset.mem_image, Finset.mem_range, Finset.mem_powerset, Finset.mem_erase, Prod.exists, Finset.mem_product, id_eq
-- Module: Mathlib.NumberTheory.SmoothNumbers
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

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

Premises used: Finset.mem_powerset, And.intro, Exists.intro, Iff.mp, Eq.symm
-- Module: Mathlib.NumberTheory.SmoothNumbers
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
refine_2 : m < N.sqrt + 1
⊢ ∃ (a : Finset ℕ) (b : ℕ), (a ⊆ k.primesBelow ∧ b ≠ 0 ∧ b < N.sqrt + 1) ∧ HPow.hPow (β := ℕ) b 2 * ∏ x ∈ a, x = n

Tactic:
refine ⟨s, m, ⟨Finset.mem_powerset.mp hs, ?_, ?_⟩, hm.symm⟩
-- Module: Mathlib.NumberTheory.SmoothNumbers
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 * s.prod id ≠ 0

Tactic:
have := hm ▸ ne_zero_of_mem_smoothNumbers hn₂
-- Module: Mathlib.NumberTheory.SmoothNumbers
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 ∧ ¬s.prod id = 0

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

Premises used: mul_eq_zero, ne_eq, not_or, sq_eq_zero_iff
-- Module: Mathlib.NumberTheory.SmoothNumbers
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 : ¬m = 0 ∧ ¬s.prod id = 0
⊢ m ≠ 0

Tactic:
this.1

Premises used: And.left
-- Module: Mathlib.NumberTheory.SmoothNumbers
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 : ¬m = 0 ∧ ¬s.prod id = 0
⊢ m ≠ 0

Tactic:
exact this.1

Premises used: And.left
-- Module: Mathlib.NumberTheory.SmoothNumbers
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_2 : HPow.hPow (β := ℕ) m 2 ≤ N
⊢ m < N.sqrt + 1

Tactic:
rw [Nat.lt_succ_iff, le_sqrt']

Premises used: Nat.lt_succ_iff, Nat.le_sqrt'
-- Module: Mathlib.NumberTheory.SmoothNumbers
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

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

Premises used: LE.le.trans
-- Module: Mathlib.NumberTheory.SmoothNumbers
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_2 : HPow.hPow (β := ℕ) m 2 ≤ HPow.hPow (β := ℕ) m 2 * s.prod id
⊢ HPow.hPow (β := ℕ) m 2 ≤ N

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

Premises used: LE.le.trans
-- Module: Mathlib.NumberTheory.SmoothNumbers
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_2 : HPow.hPow (β := ℕ) m 2 * 1 ≤ HPow.hPow (β := ℕ) m 2 * s.prod id
⊢ HPow.hPow (β := ℕ) m 2 ≤ HPow.hPow (β := ℕ) m 2 * s.prod id

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

Premises used: HPow.hPow, mul_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.SmoothNumbers
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_2 : 1 ≤ s.prod id
⊢ HPow.hPow (β := ℕ) m 2 * 1 ≤ HPow.hPow (β := ℕ) m 2 * s.prod id

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.SmoothNumbers
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
⊢ 1 ≤ s.prod id

Tactic:
Finset.one_le_prod' fun p hp ↦
      (prime_of_mem_primesBelow <| Finset.mem_powerset.mp hs hp).one_le

Premises used: Finset.mem_powerset, Nat.Prime.one_le, Iff.mp, Finset.one_le_prod', Nat.prime_of_mem_primesBelow
-- Module: Mathlib.NumberTheory.SmoothNumbers
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
⊢ 1 ≤ s.prod id

Tactic:
exact Finset.one_le_prod' fun p hp ↦
      (prime_of_mem_primesBelow <| Finset.mem_powerset.mp hs hp).one_le

Premises used: Finset.mem_powerset, Nat.Prime.one_le, Iff.mp, Finset.one_le_prod', Nat.prime_of_mem_primesBelow
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k : ℕ
⊢ #(N.smoothNumbersUpTo k) ≤ #(k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0)

Tactic:
(Finset.card_le_card <| smoothNumbersUpTo_subset_image N k).trans <| Finset.card_image_le

Premises used: Nat.smoothNumbersUpTo_subset_image, Finset.card_le_card, Finset.card_image_le, LE.le.trans
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k : ℕ
h : HPow.hPow (α := ℕ) 2 #k.primesBelow * N.sqrt = #(k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0)
⊢ #(N.smoothNumbersUpTo k) ≤ HPow.hPow (α := ℕ) 2 #k.primesBelow * N.sqrt

Tactic:
convert! (Finset.card_le_card <| smoothNumbersUpTo_subset_image N k).trans <| Finset.card_image_le

Premises used: Nat.smoothNumbersUpTo_subset_image, Finset.card_le_card, Finset.card_image_le, LE.le.trans
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k : ℕ
⊢ HPow.hPow (α := ℕ) 2 #k.primesBelow * N.sqrt = #(k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0)

Tactic:
simp only [Finset.card_product, Finset.card_powerset, Finset.mem_range, zero_lt_succ,
    Finset.card_erase_of_mem, Finset.card_range, succ_sub_succ_eq_sub, Nat.sub_zero]

Premises used: Finset.card_product, Nat.zero_lt_succ, Finset.card_range, Finset.card_erase_of_mem, Finset.mem_range, Nat.sub_zero, Nat.succ_sub_succ_eq_sub, Finset.card_powerset
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k : ℕ
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
⊢ N.roughNumbersUpTo k =
    ((N + 1).primesBelow \ k.primesBelow).biUnion fun (p : ℕ) ↦ {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m}

Tactic:
ext m
-- Module: Mathlib.NumberTheory.SmoothNumbers
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)
mpr₃ : ∀ (P Q : Prop), P → Q → P
mpr₄ : ∀ (P Q : Prop), P → Q → P → Q
mp₅ : ∀ (P Q : Prop), P → ¬P → Q
mp₆ mp₇ mp₈ : ∀ (P Q : Prop), P → Q → Q
mpr₅ mpr₆ mpr₇ : ∀ (P Q : Prop), P → Q → P → Q
⊢ ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q

Tactic:
tauto
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k m : ℕ
h :
  (m < N + 1 ∧ m ≠ 0 ∧ ∃ x ≤ m, Prime x ∧ x ∣ m ∧ k ≤ x) ↔
    ∃ (a : ℕ), ((a < N + 1 ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N + 1 ∧ m ≠ 0 ∧ a ∣ 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:
simp only [roughNumbersUpTo, mem_smoothNumbers_iff_forall_le, not_and, not_forall,
    not_lt, exists_prop, Finset.mem_range, Finset.mem_filter,
    Finset.mem_biUnion, Finset.mem_sdiff, mem_primesBelow,
    show ∀ P Q : Prop, P ∧ (P → Q) ↔ P ∧ Q by tauto]

Premises used: Nat.roughNumbersUpTo, Nat.mem_smoothNumbers_iff_forall_le, Finset.mem_range, exists_prop, Finset.mem_sdiff, not_lt, Finset.mem_filter, Nat.mem_primesBelow, not_and, Classical.not_forall, Finset.mem_biUnion
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k m : ℕ
h :
  (∃ (x : ℕ), m < N + 1 ∧ m ≠ 0 ∧ ¬m < x ∧ Prime x ∧ x ∣ m ∧ ¬x < k) ↔
    ∃ (a : ℕ), ((a < N + 1 ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N + 1 ∧ m ≠ 0 ∧ a ∣ m
⊢ (m < N + 1 ∧ m ≠ 0 ∧ ∃ x ≤ m, Prime x ∧ x ∣ m ∧ k ≤ x) ↔
    ∃ (a : ℕ), ((a < N + 1 ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N + 1 ∧ m ≠ 0 ∧ a ∣ m

Tactic:
simp_rw [← exists_and_left, ← not_lt]

Premises used: exists_and_left, not_lt
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k m : ℕ
⊢ (∃ (x : ℕ), m < N + 1 ∧ m ≠ 0 ∧ ¬m < x ∧ Prime x ∧ x ∣ m ∧ ¬x < k) ↔
    ∃ (a : ℕ), ((a < N + 1 ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N + 1 ∧ m ≠ 0 ∧ a ∣ m

Tactic:
exists_congr fun p ↦ ?_

Premises used: exists_congr
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k m : ℕ
h :
  ∀ (p : ℕ),
    m < N + 1 ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k ↔
      ((p < N + 1 ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N + 1 ∧ m ≠ 0 ∧ p ∣ m
⊢ (∃ (x : ℕ), m < N + 1 ∧ m ≠ 0 ∧ ¬m < x ∧ Prime x ∧ x ∣ m ∧ ¬x < k) ↔
    ∃ (a : ℕ), ((a < N + 1 ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N + 1 ∧ m ≠ 0 ∧ a ∣ m

Tactic:
refine exists_congr fun p ↦ ?_

Premises used: exists_congr
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k m p : ℕ
⊢ m ≠ 0 → p ∣ m → ¬m < p

Tactic:
have H : m ≠ 0 → p ∣ m → ¬ m < p :=
    fun h₁ h₂ ↦ not_lt.mpr <| le_of_dvd (Nat.pos_of_ne_zero h₁) h₂
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k m p : ℕ
H : m ≠ 0 → p ∣ m → ¬m < p
⊢ m < N + 1 ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k ↔
    ((p < N + 1 ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N + 1 ∧ m ≠ 0 ∧ p ∣ m

Tactic:
grind
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k : ℕ
rw :
  Finset.card (α := ℕ)
      (((N + 1).primesBelow \ k.primesBelow).biUnion fun (p : ℕ) ↦ {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m}) ≤
    ∑ p ∈ (N + 1).primesBelow \ k.primesBelow, N / p
⊢ #(N.roughNumbersUpTo k) ≤ ∑ p ∈ (N + 1).primesBelow \ k.primesBelow, N / p

Tactic:
rw [roughNumbersUpTo_eq_biUnion]

Premises used: Nat.roughNumbersUpTo_eq_biUnion
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k : ℕ
⊢ Finset.card (α := ℕ)
      (((N + 1).primesBelow \ k.primesBelow).biUnion fun (p : ℕ) ↦ {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m}) ≤
    ∑ p ∈ (N + 1).primesBelow \ k.primesBelow, N / p

Tactic:
Finset.card_biUnion_le.trans <| Finset.sum_le_sum fun p _ ↦ (card_multiples' N p).le

Premises used: Eq.le, Nat.card_multiples', Finset.card_biUnion_le, Finset.sum_le_sum, LE.le.trans
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N k : ℕ
⊢ Finset.card (α := ℕ)
      (((N + 1).primesBelow \ k.primesBelow).biUnion fun (p : ℕ) ↦ {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m}) ≤
    ∑ p ∈ (N + 1).primesBelow \ k.primesBelow, N / p

Tactic:
exact Finset.card_biUnion_le.trans <| Finset.sum_le_sum fun p _ ↦ (card_multiples' N p).le

Premises used: Eq.le, Nat.card_multiples', Finset.card_biUnion_le, Finset.sum_le_sum, LE.le.trans
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
R : Type u_1
inst : CommRing R
a b c d x y z w : R
⊢ HPow.hPow (β := ℕ) (a * x - b * y - c * z - d * w) 2 + HPow.hPow (β := ℕ) (a * y + b * x + c * w - d * z) 2 +
        HPow.hPow (β := ℕ) (a * z - b * w + c * x + d * y) 2 +
      HPow.hPow (β := ℕ) (a * w + b * z - c * y + d * x) 2 =
    (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) *
      (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 + HPow.hPow (β := ℕ) w 2)

Tactic:
ring