awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
right :
  List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e).primeFactorsList ++
      List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~
    m.primeFactorsList
right₁ :
  List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (replicate e p) ++
      List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~
    m.primeFactorsList
right₂ : [] ++ List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~ m.primeFactorsList
right₃ : List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~ m.primeFactorsList
right₄ right₅ : m.primeFactorsList ~ m.primeFactorsList
⊢ List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) ((p ^ e).primeFactorsList ++ m.primeFactorsList) ~ m.primeFactorsList

Tactic:
rw [filter_append, hp.primeFactorsList_pow,
          filter_eq_nil_iff.mpr fun q hq ↦ by rw [mem_replicate] at hq; simp [hq.2, hs],
          nil_append, filter_eq_self.mpr fun q hq ↦ by simp only [hm q hq, decide_true]]

Premises used: Iff.mpr, Nat.Prime.primeFactorsList_pow, List.filter_eq_nil_iff, List.filter_eq_self, List.filter_append, List.nil_append
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
simp :
  HPow.hPow (β := ℕ) p ((m.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList).prod =
    m
⊢ Eq (α := (↑(factoredNumbers (insert p s)) : Type))
    ((fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦
        (match (motive := ℕ × (↑(factoredNumbers s) : Type) → (↑(factoredNumbers (insert p s)) : Type)) x with
          | (e, n) => Subtype.mk (p := fun (x : ℕ) ↦ x ∈ factoredNumbers (insert p s)) (p ^ e * (↑n : ℕ)) ⋯ :
          (↑(factoredNumbers (insert p s)) : Type)))
      ((fun (x : (↑(factoredNumbers (insert p s)) : Type)) ↦
          (match (motive := (↑(factoredNumbers (insert p s)) : Type) → ℕ × (↑(factoredNumbers s) : Type)) x with
            | ⟨m, property⟩ =>
              ((m.factorization : (a : ℕ) → ℕ) p,
                Subtype.mk (p := fun (x : ℕ) ↦ x ∈ factoredNumbers s)
                  (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList).prod ⋯) :
            ℕ × (↑(factoredNumbers s) : Type)))
        (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ factoredNumbers (insert p s)) m ⋯)))
    (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ factoredNumbers (insert p s)) m ⋯)

Tactic:
simp only [Subtype.mk.injEq]

Premises used: Subtype.mk.injEq
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
rw :
  (replicate (List.count p m.primeFactorsList) p ++
        List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList).prod =
    m
⊢ HPow.hPow (β := ℕ) p ((m.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList).prod =
    m

Tactic:
rw [← primeFactorsList_count_eq, ← prod_replicate, ← prod_append]

Premises used: List.prod_append, Nat.primeFactorsList_count_eq, List.prod_replicate
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
nth_rewrite :
  (replicate (List.count p m.primeFactorsList) p ++
        List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList).prod =
    m.primeFactorsList.prod
⊢ (replicate (List.count p m.primeFactorsList) p ++
        List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList).prod =
    m

Tactic:
nth_rewrite 3 [← prod_primeFactorsList hm₀]

Premises used: Nat.prod_primeFactorsList
-- Module: Mathlib.NumberTheory.SmoothNumbers
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

Tactic:
(filter_congr fun q hq ↦ ?_).symm

Premises used: Eq.symm, List.filter_congr
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
refine : ∀ (q : ℕ) (hq : q ∈ m.primeFactorsList), decide (q ∉ s) = decide (q = p)
⊢ List.filter (fun (x : ℕ) ↦ decide (x = p)) m.primeFactorsList =
    List.filter (fun (x : ℕ) ↦ decide (x ∉ s)) m.primeFactorsList

Tactic:
refine (filter_congr fun q hq ↦ ?_).symm

Premises used: Eq.symm, List.filter_congr
-- Module: Mathlib.NumberTheory.SmoothNumbers
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
simp : (!decide (q ∈ s)) = decide (q = p)
⊢ decide (q ∉ s) = decide (q = p)

Tactic:
simp only [decide_not]

Premises used: decide_not
-- Module: Mathlib.NumberTheory.SmoothNumbers
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)
inr : ∀ (h : q ∈ s), (!decide (q ∈ s)) = decide (q = p)
⊢ (!decide (q ∈ s)) = decide (q = p)

Tactic:
rcases Finset.mem_insert.mp <| hm _ hq with h | h

Premises used: Finset.mem_insert, Iff.mp
-- Module: Mathlib.NumberTheory.SmoothNumbers
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 = p
⊢ (!decide (q ∈ s)) = decide (q = p)

Tactic:
simp only [h, hs, decide_false, Bool.not_false, decide_true]

Premises used: Bool.not_false, decide_false, decide_true
-- Module: Mathlib.NumberTheory.SmoothNumbers
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
inr : ¬q = p
⊢ (!decide (q ∈ s)) = decide (q = p)

Tactic:
simp only [h, decide_true, Bool.not_true, false_eq_decide_iff]

Premises used: false_eq_decide_iff, decide_true, Bool.not_true
-- Module: Mathlib.NumberTheory.SmoothNumbers
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
⊢ ¬q = p

Tactic:
fun H ↦ hs <| H ▸ h

Premises used: Eq.rec, Not
-- Module: Mathlib.NumberTheory.SmoothNumbers
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
⊢ ¬q = p

Tactic:
exact fun H ↦ hs <| H ▸ h
-- Module: Mathlib.NumberTheory.SmoothNumbers
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

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
-- Module: Mathlib.NumberTheory.SmoothNumbers
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

Tactic:
prod_eq <| (filter_eq p).symm ▸ this ▸ perm_append_comm.trans ?_

Premises used: List.Perm.prod_eq, Eq.rec, List.Perm.trans, List.perm_append_comm, List.filter_eq, Eq.symm
-- Module: Mathlib.NumberTheory.SmoothNumbers
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
refine :
  List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ++
      List.filter (fun (x : ℕ) ↦ decide (x ∉ s)) m.primeFactorsList ~
    m.primeFactorsList
⊢ (replicate (List.count p m.primeFactorsList) p ++
        List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList).prod =
    m.primeFactorsList.prod

Tactic:
refine prod_eq <| (filter_eq p).symm ▸ this ▸ perm_append_comm.trans ?_

Premises used: List.Perm.prod_eq
-- Module: Mathlib.NumberTheory.SmoothNumbers
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
simp :
  List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ++
      List.filter (fun (x : ℕ) ↦ !decide (x ∈ s)) m.primeFactorsList ~
    m.primeFactorsList
⊢ 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]

Premises used: decide_not
-- Module: Mathlib.NumberTheory.SmoothNumbers
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

Tactic:
filter_append_perm (· ∈ s) (primeFactorsList m)

Premises used: Membership.mem, List.filter_append_perm, Decidable.decide, Nat.primeFactorsList
-- Module: Mathlib.NumberTheory.SmoothNumbers
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

Tactic:
exact filter_append_perm (· ∈ s) (primeFactorsList m)

Premises used: Membership.mem, List.filter_append_perm, Decidable.decide, Nat.primeFactorsList
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p e m : ℕ
hp : Prime p
hs : p ∉ s
hm : m ∈ factoredNumbers s
⊢ (↑((equivProdNatFactoredNumbers hp hs :
            (a : ℕ × (↑(factoredNumbers s) : Type)) → (↑(factoredNumbers (insert p s)) : Type))
          (e, Subtype.mk (p := fun (x : ℕ) ↦ x ∈ factoredNumbers s) m hm)) :
      ℕ) =
    p ^ e * m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
x : ℕ × (↑(factoredNumbers s) : Type)
⊢ (↑((equivProdNatFactoredNumbers hp hs :
            (a : ℕ × (↑(factoredNumbers s) : Type)) → (↑(factoredNumbers (insert p s)) : Type))
          x) :
      ℕ) =
    p ^ x.1 * (↑x.2 : ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n m : ℕ
⊢ m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p < n

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Nat.smoothNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n : ℕ
⊢ n.smoothNumbers = factoredNumbers (Finset.range n)

Tactic:
simp only [smoothNumbers, ne_eq, mem_primeFactorsList', and_imp, factoredNumbers,
    Finset.mem_range]

Premises used: and_imp, Finset.mem_range, ne_eq, Nat.factoredNumbers, Nat.mem_primeFactorsList', Nat.smoothNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n : ℕ
rw : factoredNumbers (Finset.range n) = factoredNumbers n.primesBelow
⊢ n.smoothNumbers = factoredNumbers n.primesBelow

Tactic:
rw [smoothNumbers_eq_factoredNumbers]

Premises used: Nat.smoothNumbers_eq_factoredNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n : ℕ
⊢ factoredNumbers (Finset.range n) = factoredNumbers n.primesBelow

Tactic:
Set.Subset.antisymm (fun m hm ↦ ?_) <| factoredNumbers_mono Finset.mem_of_mem_filter

Premises used: Set.Subset.antisymm, Nat.factoredNumbers_mono, Finset.mem_of_mem_filter
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n : ℕ
refine : ∀ (m : ℕ) (hm : m ∈ factoredNumbers (Finset.range n)), m ∈ factoredNumbers n.primesBelow
⊢ factoredNumbers (Finset.range n) = factoredNumbers n.primesBelow

Tactic:
refine Set.Subset.antisymm (fun m hm ↦ ?_) <| factoredNumbers_mono Finset.mem_of_mem_filter

Premises used: Set.Subset.antisymm, Nat.factoredNumbers_mono, Finset.mem_of_mem_filter
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n m : ℕ
hm : m ∈ factoredNumbers (Finset.range n)
simp_rw : ∀ (hm : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ Finset.range n) (p : ℕ), Prime p → p ∣ m → p ∈ n.primesBelow
⊢ m ∈ factoredNumbers n.primesBelow

Tactic:
simp_rw [mem_factoredNumbers'] at hm ⊢

Premises used: Nat.mem_factoredNumbers'
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n m : ℕ
hm : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ Finset.range n
⊢ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ n.primesBelow

Tactic:
fun p hp hp' ↦ mem_primesBelow.mpr ⟨Finset.mem_range.mp <| hm p hp hp', hp⟩

Premises used: Iff.mpr, Finset.mem_range, And.intro, Iff.mp, Nat.mem_primesBelow
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n m : ℕ
hm : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ Finset.range n
⊢ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ n.primesBelow

Tactic:
exact fun p hp hp' ↦ mem_primesBelow.mpr ⟨Finset.mem_range.mp <| hm p hp hp', hp⟩

Premises used: Iff.mpr, Finset.mem_range, And.intro, Iff.mp, Nat.mem_primesBelow
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n m k : ℕ
h : m ∈ n.smoothNumbers
h' : k ∣ m
simp : ∀ (h : m ∈ factoredNumbers (Finset.range n)), k ∈ factoredNumbers (Finset.range n)
⊢ k ∈ n.smoothNumbers

Tactic:
simp only [smoothNumbers_eq_factoredNumbers] at h ⊢

Premises used: Nat.smoothNumbers_eq_factoredNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n m k : ℕ
h' : k ∣ m
h : m ∈ factoredNumbers (Finset.range n)
⊢ k ∈ factoredNumbers (Finset.range n)

Tactic:
mem_factoredNumbers_of_dvd h h'

Premises used: Nat.mem_factoredNumbers_of_dvd
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n m k : ℕ
h' : k ∣ m
h : m ∈ factoredNumbers (Finset.range n)
⊢ k ∈ factoredNumbers (Finset.range n)

Tactic:
exact mem_factoredNumbers_of_dvd h h'

Premises used: Nat.mem_factoredNumbers_of_dvd
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n m : ℕ
⊢ m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p < n

Tactic:
simp only [smoothNumbers_eq_factoredNumbers, mem_factoredNumbers_iff_forall_le, Finset.mem_range]

Premises used: Nat.mem_factoredNumbers_iff_forall_le, Finset.mem_range, Nat.smoothNumbers_eq_factoredNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n m : ℕ
⊢ m ∈ n.smoothNumbers ↔ ∀ (p : ℕ), Prime p → p ∣ m → p < n

Tactic:
simp only [smoothNumbers_eq_factoredNumbers, mem_factoredNumbers', Finset.mem_range]

Premises used: Nat.mem_factoredNumbers', Finset.mem_range, Nat.smoothNumbers_eq_factoredNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
m n : ℕ
hms : m ∈ n.smoothNumbers
⊢ m.primeFactors ⊆ n.primesBelow

Tactic:
primeFactors_subset_of_mem_factoredNumbers <|
    smoothNumbers_eq_factoredNumbers_primesBelow n ▸ hms

Premises used: Nat.smoothNumbers_eq_factoredNumbers_primesBelow, Eq.rec, Nat.primeFactors_subset_of_mem_factoredNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
m n : ℕ
hm : m ≠ 0
hp : m.primeFactors ⊆ Finset.range n
⊢ m ∈ n.smoothNumbers

Tactic:
smoothNumbers_eq_factoredNumbers n ▸ mem_factoredNumbers_of_primeFactors_subset hm hp

Premises used: Eq.rec, Nat.mem_factoredNumbers_of_primeFactors_subset, Nat.smoothNumbers_eq_factoredNumbers, Eq.symm
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
m n : ℕ
⊢ m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ m.primeFactors ⊆ n.primesBelow

Tactic:
⟨fun h ↦ ⟨h.1, primeFactors_subset_of_mem_smoothNumbers h⟩,
   fun h ↦ mem_smoothNumbers_of_primeFactors_subset h.1 <| h.2.trans <| Finset.filter_subset ..⟩

Premises used: Nat.Prime, Nat.primeFactors_subset_of_mem_smoothNumbers, Finset.filter_subset, HasSubset.Subset.trans, Finset.range, And.right, And.left, Nat.mem_smoothNumbers_of_primeFactors_subset, And.intro, Iff.intro
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n m : ℕ
h : m ∈ n.smoothNumbers
⊢ m ≠ 0

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
⊢ smoothNumbers 0 = {1}

Tactic:
simp only [smoothNumbers_eq_factoredNumbers, Finset.range_zero, factoredNumbers_empty]

Premises used: Nat.smoothNumbers_eq_factoredNumbers, Nat.factoredNumbers_empty, Finset.range_zero
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
m₁ m₂ n : ℕ
hm1 : m₁ ∈ n.smoothNumbers
hm2 : m₂ ∈ n.smoothNumbers
rw :
  ∀ (hm1 : m₁ ∈ factoredNumbers (Finset.range n)) (hm2 : m₂ ∈ factoredNumbers (Finset.range n)),
    m₁ * m₂ ∈ factoredNumbers (Finset.range n)
⊢ m₁ * m₂ ∈ n.smoothNumbers

Tactic:
rw [smoothNumbers_eq_factoredNumbers] at hm1 hm2 ⊢

Premises used: Nat.smoothNumbers_eq_factoredNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
m₁ m₂ n : ℕ
hm1 : m₁ ∈ factoredNumbers (Finset.range n)
hm2 : m₂ ∈ factoredNumbers (Finset.range n)
⊢ m₁ * m₂ ∈ factoredNumbers (Finset.range n)

Tactic:
mul_mem_factoredNumbers hm1 hm2

Premises used: Nat.mul_mem_factoredNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
m₁ m₂ n : ℕ
hm1 : m₁ ∈ factoredNumbers (Finset.range n)
hm2 : m₂ ∈ factoredNumbers (Finset.range n)
⊢ m₁ * m₂ ∈ factoredNumbers (Finset.range n)

Tactic:
exact mul_mem_factoredNumbers hm1 hm2

Premises used: Nat.mul_mem_factoredNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
n N : ℕ
⊢ (List.filter (fun (x : ℕ) ↦ decide (x < N)) n.primeFactorsList).prod ∈ N.smoothNumbers

Tactic:
simp only [smoothNumbers_eq_factoredNumbers, ← Finset.mem_range, prod_mem_factoredNumbers]

Premises used: Nat.prod_mem_factoredNumbers, Finset.mem_range, Nat.smoothNumbers_eq_factoredNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N : ℕ
hN : ¬Prime N
⊢ (N + 1).smoothNumbers = N.smoothNumbers

Tactic:
simp only [smoothNumbers_eq_factoredNumbers, Finset.range_add_one, factoredNumbers_insert _ hN]

Premises used: Nat.factoredNumbers_insert, Finset.range_add_one, Nat.smoothNumbers_eq_factoredNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
⊢ smoothNumbers 1 = {1}

Tactic:
simp +decide only [not_false_eq_true, smoothNumbers_succ, smoothNumbers_zero]

Premises used: Nat.smoothNumbers_succ, Nat.smoothNumbers_zero, not_false_eq_true, Decidable.decide
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N M : ℕ
hNM : N ≤ M
⊢ N.smoothNumbers ⊆ M.smoothNumbers

Tactic:
fun _ hx ↦ ⟨hx.1, fun p hp => (hx.2 p hp).trans_le hNM⟩

Premises used: Set.Mem, setOf, Set.Subset, And.right, And.left, LT.lt.trans_le, And.intro, Nat.smoothNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
m n : ℕ
hm : 0 < m
hmn : m < n
⊢ m ∈ n.smoothNumbers

Tactic:
smoothNumbers_eq_factoredNumbers _ ▸ ⟨ne_zero_of_lt hm,
  fun _ h => Finset.mem_range.mpr <| lt_of_le_of_lt (le_of_mem_primeFactorsList h) hmn⟩

Premises used: Iff.mpr, lt_of_le_of_lt, ne_zero_of_lt, Eq.rec, Finset.mem_range, Nat.smoothNumbers_eq_factoredNumbers, And.intro, Nat.le_of_mem_primeFactorsList, Eq.symm
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N : ℕ
⊢ N.smoothNumbersᶜ \ {0} ⊆ {n : ℕ | N ≤ n}

Tactic:
simpa only [smoothNumbers_eq_factoredNumbers]
    using factoredNumbers_compl <| Finset.filter_subset _ (Finset.range N)

Premises used: Finset.filter_subset, Finset.range, Nat.smoothNumbers_eq_factoredNumbers, Nat.factoredNumbers_compl
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
⊢ NoZeroDivisors ℕ

Tactic:
have : NoZeroDivisors ℕ := inferInstance
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
⊢ p ^ e ≠ 0

Tactic:
have hp' := pow_ne_zero e hp
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
⊢ p ^ e * n ∈ p.succ.smoothNumbers

Tactic:
⟨mul_ne_zero hp' hn.1, fun q hq ↦ ?_⟩

Premises used: Set.Mem, setOf, And.left, And.intro, Nat.smoothNumbers, mul_ne_zero
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
refine : ∀ (q : ℕ) (hq : q ∈ (p ^ e * n).primeFactorsList), q < p.succ
⊢ p ^ e * n ∈ p.succ.smoothNumbers

Tactic:
refine ⟨mul_ne_zero hp' hn.1, fun q hq ↦ ?_⟩
-- Module: Mathlib.NumberTheory.SmoothNumbers
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
inr : ∀ (H : q ∈ n.primeFactorsList), q < p.succ
⊢ q < p.succ

Tactic:
rcases (mem_primeFactorsList_mul hp' hn.1).mp hq with H | H

Premises used: And.left, Iff.mp, Nat.mem_primeFactorsList_mul
-- Module: Mathlib.NumberTheory.SmoothNumbers
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
⊢ Prime q ∧ q ∣ p ^ e

Tactic:
rw [mem_primeFactorsList hp'] at H

Premises used: Nat.mem_primeFactorsList
-- Module: Mathlib.NumberTheory.SmoothNumbers
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 : Prime q ∧ q ∣ p ^ e
⊢ q < p.succ

Tactic:
Nat.lt_succ_of_le <| le_of_dvd hp.bot_lt <| H.1.dvd_of_dvd_pow H.2

Premises used: Nat.Prime.dvd_of_dvd_pow, Nat.lt_succ_of_le, And.right, And.left, Nat.le_of_dvd, Ne.bot_lt
-- Module: Mathlib.NumberTheory.SmoothNumbers
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 : Prime q ∧ q ∣ p ^ e
⊢ q < p.succ

Tactic:
exact Nat.lt_succ_of_le <| le_of_dvd hp.bot_lt <| H.1.dvd_of_dvd_pow H.2

Premises used: Nat.Prime.dvd_of_dvd_pow, Nat.lt_succ_of_le, And.right, And.left, Nat.le_of_dvd, Ne.bot_lt
-- Module: Mathlib.NumberTheory.SmoothNumbers
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 ∈ n.primeFactorsList
⊢ q < p.succ

Tactic:
(hn.2 q H).trans <| lt_succ_self p

Premises used: Nat.lt_succ_self, And.right, LT.lt.trans
-- Module: Mathlib.NumberTheory.SmoothNumbers
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 ∈ n.primeFactorsList
⊢ q < p.succ

Tactic:
exact (hn.2 q H).trans <| lt_succ_self p

Premises used: Nat.lt_succ_self, And.right, LT.lt.trans
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
p n : ℕ
hp : Prime p
hn : n ∈ p.smoothNumbers
⊢ n ∈ factoredNumbers (Finset.range p)

Tactic:
simp only [smoothNumbers_eq_factoredNumbers] at hn

Premises used: Nat.smoothNumbers_eq_factoredNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
p n : ℕ
hp : Prime p
hn : n ∈ factoredNumbers (Finset.range p)
⊢ p.Coprime n

Tactic:
hp.factoredNumbers_coprime Finset.notMem_range_self hn

Premises used: Nat.Prime.factoredNumbers_coprime, Finset.notMem_range_self
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
p n : ℕ
hp : Prime p
hn : n ∈ factoredNumbers (Finset.range p)
⊢ p.Coprime n

Tactic:
exact hp.factoredNumbers_coprime Finset.notMem_range_self hn

Premises used: Nat.Prime.factoredNumbers_coprime, Finset.notMem_range_self
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
F : Type u_1
inst : Mul F
f : ℕ → F
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
p : ℕ
hp : Prime p
e : ℕ
m : (↑p.smoothNumbers : Type)
⊢ f (p ^ e * (↑m : ℕ)) = f (p ^ e) * f (↑m : ℕ)

Tactic:
hmul <| Coprime.pow_left _ <| hp.smoothNumbers_coprime <| Subtype.mem m

Premises used: Nat.Coprime.pow_left, Subtype.mem, Nat.Prime.smoothNumbers_coprime