awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
rw : (m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s) ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
⊢ m ∈ factoredNumbers s ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s

Tactic:
rw [mem_factoredNumbers_iff_forall_le]

Premises used: Nat.mem_factoredNumbers_iff_forall_le
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
⊢ (m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s) ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s

Tactic:
⟨fun ⟨H₀, H₁⟩ ↦ fun p hp₁ hp₂ ↦ H₁ p (le_of_dvd (Nat.pos_of_ne_zero H₀) hp₂) hp₁ hp₂,
         fun H ↦ ⟨fun h ↦ lt_irrefl p ?_, fun p _ ↦ H p⟩⟩

Premises used: lt_irrefl, _private.0.Nat.mem_factoredNumbers_iff_forall_le.match_4, Nat.pos_of_ne_zero, And.intro, Iff.intro, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
refine : ∀ (H : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s) (h : m = 0), p < p
⊢ (m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s) ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s

Tactic:
refine ⟨fun ⟨H₀, H₁⟩ ↦ fun p hp₁ hp₂ ↦ H₁ p (le_of_dvd (Nat.pos_of_ne_zero H₀) hp₂) hp₁ hp₂,
         fun H ↦ ⟨fun h ↦ lt_irrefl p ?_, fun p _ ↦ H p⟩⟩
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
H : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
h : m = 0
⊢ p ≤ s.sup id

Tactic:
Finset.le_sup (f := @id ℕ) <| H p hp₂ <| h.symm ▸ dvd_zero p

Premises used: dvd_zero, Eq.rec, Eq.symm, Finset.le_sup
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
H : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
h : m = 0
⊢ s.sup id < 1 + s.sup id

Tactic:
lt_one_add _

Premises used: lt_one_add
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
H : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
h : m = 0
⊢ 1 + s.sup id ≤ p

Tactic:
hp₁
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
H : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
h : m = 0
⊢ p < p

Tactic:
calc
    p ≤ s.sup id := Finset.le_sup (f := @id ℕ) <| H p hp₂ <| h.symm ▸ dvd_zero p
    _ < 1 + s.sup id := lt_one_add _
    _ ≤ p := hp₁

Premises used: id, Finset.sup, lt_one_add, Finset.le_sup
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m : ℕ
h : m ∈ factoredNumbers s
⊢ m ≠ 0

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m : ℕ
hm : m ∈ factoredNumbers s
⊢ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s

Tactic:
rw [mem_factoredNumbers] at hm

Premises used: Nat.mem_factoredNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m : ℕ
hm : m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ m.primeFactors ⊆ s

Tactic:
fun n hn ↦ hm.2 n (mem_primeFactors_iff_mem_primeFactorsList.mp hn)

Premises used: And.right, Nat.mem_primeFactors_iff_mem_primeFactorsList, Iff.mp
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m : ℕ
hm : m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ m.primeFactors ⊆ s

Tactic:
exact fun n hn ↦ hm.2 n (mem_primeFactors_iff_mem_primeFactorsList.mp hn)

Premises used: And.right, Nat.mem_primeFactors_iff_mem_primeFactorsList, Iff.mp
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m : ℕ
hm : m ≠ 0
hp : m.primeFactors ⊆ s
⊢ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s

Tactic:
⟨hm, fun p hp' ↦ hp <| mem_primeFactors_iff_mem_primeFactorsList.mpr hp'⟩

Premises used: Iff.mpr, And.intro, Nat.mem_primeFactors_iff_mem_primeFactorsList
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m : ℕ
hm : m ≠ 0
hp : m.primeFactors ⊆ s
⊢ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s

Tactic:
exact ⟨hm, fun p hp' ↦ hp <| mem_primeFactors_iff_mem_primeFactorsList.mpr hp'⟩
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m : ℕ
⊢ m ∈ factoredNumbers s ↔ m ≠ 0 ∧ m.primeFactors ⊆ s

Tactic:
⟨fun h ↦ ⟨ne_zero_of_mem_factoredNumbers h, primeFactors_subset_of_mem_factoredNumbers h⟩,
   fun ⟨h₁, h₂⟩ ↦ mem_factoredNumbers_of_primeFactors_subset h₁ h₂⟩

Premises used: Nat.ne_zero_of_mem_factoredNumbers, Membership.mem, Nat.mem_factoredNumbers_of_primeFactors_subset, Nat.factoredNumbers, Nat.primeFactors_subset_of_mem_factoredNumbers, And.intro, Iff.intro, _private.0.Nat.mem_factoredNumbers_iff_primeFactors_subset.match_1
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
h : ∀ (m : ℕ), m ∈ factoredNumbers ∅ ↔ Membership.mem (γ := Set ℕ) {1} m
⊢ factoredNumbers ∅ = {1}

Tactic:
ext m
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
m : ℕ
⊢ m ∈ factoredNumbers ∅ ↔ Membership.mem (γ := Set ℕ) {1} m

Tactic:
simp only [mem_factoredNumbers, Finset.notMem_empty, ← List.eq_nil_iff_forall_not_mem,
    primeFactorsList_eq_nil, and_or_left, not_and_self_iff, ne_and_eq_iff_right zero_ne_one,
    false_or, Set.mem_singleton_iff]

Premises used: and_or_left, zero_ne_one, false_or, Finset.notMem_empty, Set.mem_singleton_iff, ne_and_eq_iff_right, Nat.mem_factoredNumbers, Nat.primeFactorsList_eq_nil, not_and_self_iff, List.eq_nil_iff_forall_not_mem
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m n : ℕ
hm : m ∈ factoredNumbers s
hn : n ∈ factoredNumbers s
⊢ m.primeFactors ⊆ s

Tactic:
have hm' := primeFactors_subset_of_mem_factoredNumbers hm
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m n : ℕ
hm : m ∈ factoredNumbers s
hn : n ∈ factoredNumbers s
hm' : m.primeFactors ⊆ s
⊢ n.primeFactors ⊆ s

Tactic:
have hn' := primeFactors_subset_of_mem_factoredNumbers hn
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m n : ℕ
hm : m ∈ factoredNumbers s
hn : n ∈ factoredNumbers s
hm' : m.primeFactors ⊆ s
hn' : n.primeFactors ⊆ s
⊢ m * n ∈ factoredNumbers s

Tactic:
mem_factoredNumbers_of_primeFactors_subset (mul_ne_zero hm.1 hn.1)
    <| primeFactors_mul hm.1 hn.1 ▸ Finset.union_subset hm' hn'

Premises used: Finset.union_subset, Eq.rec, Nat.mem_factoredNumbers_of_primeFactors_subset, And.left, Nat.primeFactors_mul, mul_ne_zero, Eq.symm
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m n : ℕ
hm : m ∈ factoredNumbers s
hn : n ∈ factoredNumbers s
hm' : m.primeFactors ⊆ s
hn' : n.primeFactors ⊆ s
⊢ m * n ∈ factoredNumbers s

Tactic:
exact mem_factoredNumbers_of_primeFactors_subset (mul_ne_zero hm.1 hn.1)
    <| primeFactors_mul hm.1 hn.1 ▸ Finset.union_subset hm' hn'

Premises used: Nat.mem_factoredNumbers_of_primeFactors_subset, And.left, mul_ne_zero
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
n : ℕ
⊢ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod ≠ 0

Tactic:
have h₀ : (n.primeFactorsList.filter (· ∈ s)).prod ≠ 0 :=
    List.prod_ne_zero fun h ↦ (pos_of_mem_primeFactorsList (List.mem_of_mem_filter h)).false
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
n : ℕ
h₀ : (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod ≠ 0
⊢ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod ∈ factoredNumbers s

Tactic:
⟨h₀, fun p hp ↦ ?_⟩

Premises used: Set.Mem, setOf, Nat.factoredNumbers, And.intro
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
n : ℕ
h₀ : (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod ≠ 0
refine :
  ∀ (p : ℕ) (hp : p ∈ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod.primeFactorsList), p ∈ s
⊢ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod ∈ factoredNumbers s

Tactic:
refine ⟨h₀, fun p hp ↦ ?_⟩
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
n : ℕ
h₀ : (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod ≠ 0
p : ℕ
hp : p ∈ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod.primeFactorsList
⊢ Prime p

Tactic:
obtain ⟨H₁, H₂⟩ := (mem_primeFactorsList h₀).mp hp

Premises used: Nat.mem_primeFactorsList, Iff.mp
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
n : ℕ
h₀ : (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod ≠ 0
p : ℕ
hp : p ∈ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod.primeFactorsList
H₁ : Prime p
⊢ p ∣ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod

Tactic:
obtain ⟨H₁, H₂⟩ := (mem_primeFactorsList h₀).mp hp

Premises used: Nat.mem_primeFactorsList, Iff.mp
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
n : ℕ
h₀ : (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod ≠ 0
p : ℕ
hp : p ∈ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod.primeFactorsList
H₁ : Prime p
H₂ : p ∣ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod
⊢ p ∈ s

Tactic:
simpa only [decide_eq_true_eq] using List.of_mem_filter <| mem_list_primes_of_dvd_prod H₁.prime
    (fun _ hq ↦ (prime_of_mem_primeFactorsList (List.mem_of_mem_filter hq)).prime) H₂

Premises used: Nat.prime_of_mem_primeFactorsList, Nat.Prime.prime, mem_list_primes_of_dvd_prod, decide_eq_true_eq, List.mem_of_mem_filter, List.of_mem_filter
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
N : ℕ
hN : ¬Prime N
h : ∀ (m : ℕ), m ∈ factoredNumbers (insert N s) ↔ m ∈ factoredNumbers s
⊢ factoredNumbers (insert N s) = factoredNumbers s

Tactic:
ext m
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
N : ℕ
hN : ¬Prime N
m : ℕ
⊢ m ∈ factoredNumbers (insert N s) ↔ m ∈ factoredNumbers s

Tactic:
⟨fun hm ↦ ⟨hm.1, fun p hp ↦ ?_⟩,
          fun hm ↦ ⟨hm.1, fun p hp ↦ Finset.mem_insert_of_mem <| hm.2 p hp⟩⟩

Premises used: Finset.mem_insert_of_mem, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
N : ℕ
hN : ¬Prime N
m : ℕ
h : ∀ (hm : m ∈ factoredNumbers (insert N s)) (p : ℕ) (hp : p ∈ m.primeFactorsList), p ∈ s
⊢ m ∈ factoredNumbers (insert N s) ↔ m ∈ factoredNumbers s

Tactic:
refine ⟨fun hm ↦ ⟨hm.1, fun p hp ↦ ?_⟩,
          fun hm ↦ ⟨hm.1, fun p hp ↦ Finset.mem_insert_of_mem <| hm.2 p hp⟩⟩
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
N : ℕ
hN : ¬Prime N
m : ℕ
hm : m ∈ factoredNumbers (insert N s)
p : ℕ
hp : p ∈ m.primeFactorsList
⊢ p ∈ s

Tactic:
Finset.mem_of_mem_insert_of_ne (hm.2 p hp)
    fun h ↦ hN <| h ▸ prime_of_mem_primeFactorsList hp

Premises used: Nat.prime_of_mem_primeFactorsList, Eq.rec, And.right, Finset.mem_of_mem_insert_of_ne
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
N : ℕ
hN : ¬Prime N
m : ℕ
hm : m ∈ factoredNumbers (insert N s)
p : ℕ
hp : p ∈ m.primeFactorsList
⊢ p ∈ s

Tactic:
exact Finset.mem_of_mem_insert_of_ne (hm.2 p hp)
    fun h ↦ hN <| h ▸ prime_of_mem_primeFactorsList hp

Premises used: Nat.prime_of_mem_primeFactorsList, Eq.rec, And.right, Finset.mem_of_mem_insert_of_ne
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s t : Finset ℕ
hst : s ≤ t
⊢ factoredNumbers s ⊆ factoredNumbers t

Tactic:
fun _ hx ↦ ⟨hx.1, fun p hp ↦ hst <| hx.2 p hp⟩

Premises used: Set.Mem, setOf, Set.Subset, Nat.factoredNumbers, And.right, And.left, And.intro
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : n ∈ (factoredNumbers s)ᶜ \ {0}
⊢ (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0

Tactic:
simp only [Set.mem_compl_iff, mem_factoredNumbers, Set.mem_diff, ne_eq, not_and, not_forall,
    exists_prop, Set.mem_singleton_iff] at hn

Premises used: exists_prop, ne_eq, Set.mem_singleton_iff, Set.mem_diff, Nat.mem_factoredNumbers, not_and, Classical.not_forall, Set.mem_compl_iff
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
obtain : ∀ (p : ℕ) (hp₁ : p ∈ n.primeFactorsList) (hp₂ : p ∉ s), N ≤ n
⊢ N ≤ n

Tactic:
obtain ⟨p, hp₁, hp₂⟩ := hn.1 hn.2

Premises used: And.right, And.left
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
p : ℕ
hp₁ : p ∈ n.primeFactorsList
hp₂ : p ∉ s
contrapose! : ∀ (hp₂ : p < N), p ∈ s
⊢ N ≤ p

Tactic:
contrapose! hp₂
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
p : ℕ
hp₁ : p ∈ n.primeFactorsList
hp₂ : p < N
⊢ p ∈ s

Tactic:
h <| mem_primesBelow.mpr ⟨hp₂, prime_of_mem_primeFactorsList hp₁⟩

Premises used: Iff.mpr, Nat.prime_of_mem_primeFactorsList, And.intro, Nat.mem_primesBelow
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
p : ℕ
hp₁ : p ∈ n.primeFactorsList
hp₂ : p < N
⊢ p ∈ s

Tactic:
exact h <| mem_primesBelow.mpr ⟨hp₂, prime_of_mem_primeFactorsList hp₁⟩

Premises used: Iff.mpr, Nat.prime_of_mem_primeFactorsList, And.intro, Nat.mem_primesBelow
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
p : ℕ
hp₁ : p ∈ n.primeFactorsList
hp₂ : p ∉ s
⊢ N ≤ p

Tactic:
have : N ≤ p := by
    contrapose! hp₂
    exact h <| mem_primesBelow.mpr ⟨hp₂, prime_of_mem_primeFactorsList hp₁⟩
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
p : ℕ
hp₁ : p ∈ n.primeFactorsList
hp₂ : p ∉ s
this : N ≤ p
⊢ N ≤ n

Tactic:
this.trans <| le_of_mem_primeFactorsList hp₁

Premises used: Nat.le_of_mem_primeFactorsList, LE.le.trans
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
p : ℕ
hp₁ : p ∈ n.primeFactorsList
hp₂ : p ∉ s
this : N ≤ p
⊢ N ≤ n

Tactic:
exact this.trans <| le_of_mem_primeFactorsList hp₁

Premises used: Nat.le_of_mem_primeFactorsList, LE.le.trans
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
⊢ p ^ e ≠ 0

Tactic:
have hp' := pow_ne_zero e hp.ne_zero
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
⊢ p ^ e * n ∈ factoredNumbers (insert p s)

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

Premises used: Set.Mem, setOf, Nat.factoredNumbers, And.left, And.intro, mul_ne_zero
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
refine : ∀ (q : ℕ) (hq : q ∈ (p ^ e * n).primeFactorsList), q ∈ insert p s
⊢ p ^ e * n ∈ factoredNumbers (insert p s)

Tactic:
refine ⟨mul_ne_zero hp' hn.1, fun q hq ↦ ?_⟩
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
inl : ∀ (H : q ∈ (p ^ e).primeFactorsList), q ∈ insert p s
inr : ∀ (H : q ∈ n.primeFactorsList), q ∈ insert p s
⊢ q ∈ insert p s

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:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
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:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : Prime q ∧ q ∣ p ^ e
inl : p ∈ insert p s
⊢ q ∈ insert p s

Tactic:
rw [(prime_dvd_prime_iff_eq H.1 hp).mp <| H.1.dvd_of_dvd_pow H.2]

Premises used: Nat.Prime.dvd_of_dvd_pow, Nat.prime_dvd_prime_iff_eq, And.right, And.left, Iff.mp
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : Prime q ∧ q ∣ p ^ e
⊢ p ∈ insert p s

Tactic:
Finset.mem_insert_self p s

Premises used: Finset.mem_insert_self
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : Prime q ∧ q ∣ p ^ e
⊢ p ∈ insert p s

Tactic:
exact Finset.mem_insert_self p s

Premises used: Finset.mem_insert_self
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : q ∈ n.primeFactorsList
⊢ q ∈ insert p s

Tactic:
Finset.mem_insert_of_mem <| hn.2 _ H

Premises used: Finset.mem_insert_of_mem, And.right
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : q ∈ n.primeFactorsList
⊢ q ∈ insert p s

Tactic:
exact Finset.mem_insert_of_mem <| hn.2 _ H

Premises used: Finset.mem_insert_of_mem, And.right
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
hs : p ∉ s
hn : n ∈ factoredNumbers s
rw : p ∉ n.primeFactorsList
⊢ p.Coprime n

Tactic:
rw [hp.coprime_iff_not_dvd, ← mem_primeFactorsList_iff_dvd hn.1 hp]

Premises used: Nat.mem_primeFactorsList_iff_dvd, And.left, Nat.Prime.coprime_iff_not_dvd
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
hs : p ∉ s
hn : n ∈ factoredNumbers s
⊢ p ∉ n.primeFactorsList

Tactic:
fun H ↦ hs <| hn.2 p H

Premises used: And.right, Not
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
hs : p ∉ s
hn : n ∈ factoredNumbers s
⊢ p ∉ n.primeFactorsList

Tactic:
exact fun H ↦ hs <| hn.2 p H

Premises used: And.right
-- 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
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e : ℕ
m : (↑(factoredNumbers s) : Type)
⊢ f (p ^ e * (↑m : ℕ)) = f (p ^ e) * f (↑m : ℕ)

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

Premises used: Nat.Prime.factoredNumbers_coprime, Nat.Coprime.pow_left, Subtype.mem
-- 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
simp :
  ((p ^ e * m).factorization : (a : ℕ) → ℕ) p = e ∧
    (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m
⊢ Eq (α := ℕ × (↑(factoredNumbers 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)))
      ((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)))
        (e, Subtype.mk (p := fun (x : ℕ) ↦ x ∈ factoredNumbers s) m ⋯)))
    (e, Subtype.mk (p := fun (x : ℕ) ↦ x ∈ factoredNumbers s) m ⋯)

Tactic:
simp (etaStruct := .all) only [Prod.mk.injEq, Subtype.mk.injEq]

Premises used: Prod.mk.injEq, Subtype.mk.injEq
-- 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
left : ((p ^ e * m).factorization : (a : ℕ) → ℕ) p = e
right : (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m
⊢ ((p ^ e * m).factorization : (a : ℕ) → ℕ) p = e ∧
    (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m

Tactic:
constructor
-- 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
left : ((p ^ e).factorization + m.factorization : (a : ℕ) → ℕ) p = e
⊢ ((p ^ e * m).factorization : (a : ℕ) → ℕ) p = e

Tactic:
rw [factorization_mul (pos_iff_ne_zero.mp <| Nat.pow_pos hp.pos) hm₀]

Premises used: Nat.factorization_mul, Nat.Prime.pos, Iff.mp, Nat.pow_pos, pos_iff_ne_zero
-- 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
left : Eq (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ ((p ^ e).factorization + m.factorization : (a : ℕ) → ℕ) p = e

Tactic:
simp only [factorization_pow, Finsupp.coe_add, Finsupp.coe_smul, nsmul_eq_mul,
        Pi.natCast_def, cast_id, Pi.add_apply, Pi.mul_apply, hp.factorization_self,
        mul_one, add_eq_left]

Premises used: Pi.mul_apply, Nat.cast_id, Pi.add_apply, Finsupp.coe_add, Nat.Prime.factorization_self, Finsupp.coe_smul, add_eq_left, nsmul_eq_mul, Nat.factorization_pow, mul_one, Pi.natCast_def
-- 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
⊢ p ∉ m.primeFactorsList

Tactic:
fun H ↦ hs (hm p H)

Premises used: Not
-- 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
⊢ p ∉ m.primeFactorsList

Tactic:
exact fun H ↦ hs (hm p H)
-- 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 * m).primeFactorsList).prod = m.primeFactorsList.prod
⊢ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m

Tactic:
nth_rewrite 2 [← prod_primeFactorsList hm₀]

Premises used: Nat.prod_primeFactorsList
-- 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
⊢ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m.primeFactorsList.prod

Tactic:
prod_eq <|
        (filter _ <| perm_primeFactorsList_mul (pow_ne_zero e hp.ne_zero) hm₀).trans ?_

Premises used: List.Perm.prod_eq, pow_ne_zero, List.Perm.trans, Nat.Prime.ne_zero, Nat.perm_primeFactorsList_mul, List.Perm.filter
-- 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 ++ m.primeFactorsList) ~ m.primeFactorsList
⊢ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m.primeFactorsList.prod

Tactic:
refine prod_eq <|
        (filter _ <| perm_primeFactorsList_mul (pow_ne_zero e hp.ne_zero) hm₀).trans ?_

Premises used: List.Perm.prod_eq, pow_ne_zero, List.Perm.trans, Nat.Prime.ne_zero, Nat.perm_primeFactorsList_mul, List.Perm.filter
-- 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
q : ℕ
hq : q ∈ replicate e p
⊢ e ≠ 0 ∧ q = p

Tactic:
rw [mem_replicate] at hq

Premises used: List.mem_replicate
-- 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
q : ℕ
hq : e ≠ 0 ∧ q = p
⊢ ¬decide (q ∈ s) = true

Tactic:
simp [hq.2, hs]

Premises used: And.right
-- 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
q : ℕ
hq : q ∈ m.primeFactorsList
⊢ decide (q ∈ s) = true

Tactic:
simp only [hm q hq, decide_true]

Premises used: decide_true