awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
rw : ∑ x1 ∈ f.support, single x1 ((f : (a : ℕ) → ℕ) x1) = f
⊢ factorization (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = f

Tactic:
rw [Finsupp.prod, factorization_prod (pow_ne_zero _ <| hf · · |>.ne_zero),
    sum_congr rfl (hf · · |>.factorization_pow)]

Premises used: Nat.Prime.factorization_pow, pow_ne_zero, Nat.Prime.ne_zero, Finset.sum_congr, Nat.factorization_prod, Finsupp.prod, rfl
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
⊢ ∑ x1 ∈ f.support, single x1 ((f : (a : ℕ) → ℕ) x1) = f

Tactic:
sum_single f

Premises used: Finsupp.sum, Finsupp.sum_single
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
⊢ ∑ x1 ∈ f.support, single x1 ((f : (a : ℕ) → ℕ) x1) = f

Tactic:
exact sum_single f

Premises used: Finsupp.sum_single
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
mp : f = n.factorization → (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = n
mpr : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = n → f = n.factorization
⊢ f = n.factorization ↔ (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = n

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
hn : n ≠ 0
hf : ∀ p ∈ n.factorization.support, Prime p
⊢ (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = n

Tactic:
prod_factorization_pow_eq_self hn

Premises used: Nat.prod_factorization_pow_eq_self
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
hn : Ne (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) 0
⊢ f = factorization (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)

Tactic:
prod_pow_factorization_eq_self hf |>.symm

Premises used: Nat.prod_pow_factorization_eq_self, Eq.symm
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
hn : n ≠ 0
hf : ∀ p ∈ n.factorization.support, Prime p
⊢ (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = n

Tactic:
exacts [prod_factorization_pow_eq_self hn, prod_pow_factorization_eq_self hf |>.symm]

Premises used: Nat.prod_pow_factorization_eq_self, Nat.prod_factorization_pow_eq_self, Eq.symm
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
⊢ factorization (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = f

Tactic:
prod_pow_factorization_eq_self fun _ hp ↦ prime_of_mem_primeFactors <| support_mono hf hp

Premises used: Finsupp.support_mono, Nat.prime_of_mem_primeFactors, Nat.prod_pow_factorization_eq_self
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
inl : ∀ (hf : f ≤ factorization 0), Dvd.dvd (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) 0
inr : ∀ (hn : n ≠ 0), (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∣ n
⊢ (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∣ n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
f : ℕ →₀ ℕ
hf : f ≤ factorization 0
⊢ Dvd.dvd (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
rwa : Ne (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) 0
⊢ (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∣ n

Tactic:
rwa [← factorization_le_iff_dvd ?_ hn, factorization_prod_pow_eq_self_of_le_factorization hf]

Premises used: Nat.factorization_prod_pow_eq_self_of_le_factorization, Nat.factorization_le_iff_dvd
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ Ne (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) 0

Tactic:
f.prod_ne_zero_iff.mpr fun _ hp ↦ ?_

Premises used: Iff.mpr, Finsupp.prod_ne_zero_iff
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
refine : ∀ (x : ℕ) (hp : x ∈ f.support), HPow.hPow (β := ℕ) x ((f : (a : ℕ) → ℕ) x : ℕ) ≠ 0
⊢ Ne (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) 0

Tactic:
refine f.prod_ne_zero_iff.mpr fun _ hp ↦ ?_

Premises used: Iff.mpr, Finsupp.prod_ne_zero_iff
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
x : ℕ
hp : x ∈ f.support
⊢ HPow.hPow (β := ℕ) x ((f : (a : ℕ) → ℕ) x : ℕ) ≠ 0

Tactic:
pow_ne_zero _ (prime_of_mem_primeFactors <| support_mono hf hp).ne_zero

Premises used: pow_ne_zero, Finsupp.support_mono, Nat.prime_of_mem_primeFactors, Nat.Prime.ne_zero
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
x : ℕ
hp : x ∈ f.support
⊢ HPow.hPow (β := ℕ) x ((f : (a : ℕ) → ℕ) x : ℕ) ≠ 0

Tactic:
exact pow_ne_zero _ (prime_of_mem_primeFactors <| support_mono hf hp).ne_zero

Premises used: pow_ne_zero, Finsupp.support_mono, Nat.prime_of_mem_primeFactors, Nat.Prime.ne_zero
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ ∀ (a : ℕ), HPow.hPow (β := ℕ) a 0 = 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
rw : n ∣ n * (f - n.factorization).prod HPow.hPow
⊢ n ∣ f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2

Tactic:
rw [← add_tsub_cancel_of_le hf, Finsupp.prod_add_index' (by simp) Nat.pow_add,
    prod_factorization_pow_eq_self hn]

Premises used: Nat.pow_add, Finsupp.prod_add_index', Nat.prod_factorization_pow_eq_self, add_tsub_cancel_of_le
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ n ∣ n * (f - n.factorization).prod HPow.hPow

Tactic:
apply n.dvd_mul_right

Premises used: Nat.dvd_mul_right
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
rw : d.factorization ≤ n.factorization ↔ ∃ f ≤ n.factorization, d = f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
⊢ d ∣ n ↔ ∃ f ≤ n.factorization, d = f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2

Tactic:
rw [← factorization_le_iff_dvd hd hn]

Premises used: Nat.factorization_le_iff_dvd
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d.factorization ≤ n.factorization ↔ ∃ f ≤ n.factorization, d = f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2

Tactic:
⟨fun h ↦ ⟨_, h, prod_factorization_pow_eq_self hd |>.symm⟩, fun ⟨f, hle, hprod⟩ ↦ ?_⟩

Premises used: _private.0.Nat.dvd_iff_exists_le_factorization.match_1, LE.le, Nat.prod_factorization_pow_eq_self, And.intro, Iff.intro, Exists.intro, Eq.symm, Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
refine :
  (∃ f ≤ n.factorization, d = f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) →
    ∀ (f : ℕ →₀ ℕ) (hle : f ≤ n.factorization) (hprod : d = f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2),
      d.factorization ≤ n.factorization
⊢ d.factorization ≤ n.factorization ↔ ∃ f ≤ n.factorization, d = f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2

Tactic:
refine ⟨fun h ↦ ⟨_, h, prod_factorization_pow_eq_self hd |>.symm⟩, fun ⟨f, hle, hprod⟩ ↦ ?_⟩
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
h : ∃ f ≤ n.factorization, d = f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
hprod : d = f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
rwa : factorization (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ≤ n.factorization
rwa₁ rwa₂ rwa₃ rwa₄ : f ≤ n.factorization
⊢ d.factorization ≤ n.factorization

Tactic:
rwa [hprod, factorization_prod_pow_eq_self_of_le_factorization hle]

Premises used: Nat.factorization_prod_pow_eq_self_of_le_factorization
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
p a b : ℕ
hab : a.Coprime b
⊢ ((a * b).factorization : (a : ℕ) → ℕ) p =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp only [← primeFactorsList_count_eq,
    perm_iff_count.mp (perm_primeFactorsList_mul_of_coprime hab), count_append]

Premises used: Nat.perm_primeFactorsList_mul_of_coprime, Nat.primeFactorsList_count_eq, List.perm_iff_count, List.count_append, Iff.mp
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a b : ℕ
hab : a.Coprime b
h :
  ∀ (q : ℕ),
    Eq (α := ℕ) (((a * b).factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization + b.factorization : (a : ℕ) → ℕ) q : ℕ)
⊢ (a * b).factorization = a.factorization + b.factorization

Tactic:
ext q
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a b : ℕ
hab : a.Coprime b
q : ℕ
h :
  ((a * b).factorization : (a : ℕ) → ℕ) q =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ)
h₁ h₂ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ)
⊢ Eq (α := ℕ) (((a * b).factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization + b.factorization : (a : ℕ) → ℕ) q : ℕ)

Tactic:
rw [Finsupp.add_apply, factorization_mul_apply_of_coprime hab]

Premises used: Nat.factorization_mul_apply_of_coprime, Finsupp.add_apply
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hp : ¬Prime p
⊢ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n

Tactic:
simp [hp]
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
⊢ Prime p

Tactic:
if hp : p.Prime then ?_ else simp [hp]

Premises used: Nat.Prime
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hp : Prime p
rw : p ^ count p n.primeFactorsList ∣ n
⊢ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n

Tactic:
rw [← primeFactorsList_count_eq]

Premises used: Nat.primeFactorsList_count_eq
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hp : Prime p
apply : (p ^ count p n.primeFactorsList).primeFactorsList <+~ n.primeFactorsList
⊢ p ^ count p n.primeFactorsList ∣ n

Tactic:
apply dvd_of_primeFactorsList_subperm (pow_ne_zero _ hp.ne_zero)

Premises used: pow_ne_zero, Nat.Prime.ne_zero, Nat.dvd_of_primeFactorsList_subperm
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hp : Prime p
rw :
  ∀ x ∈ replicate (count p n.primeFactorsList) p,
    count x (replicate (count p n.primeFactorsList) p) ≤ count x n.primeFactorsList
⊢ (p ^ count p n.primeFactorsList).primeFactorsList <+~ n.primeFactorsList

Tactic:
rw [hp.primeFactorsList_pow, List.subperm_ext_iff]

Premises used: Nat.Prime.primeFactorsList_pow, List.subperm_ext_iff
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hp : Prime p
q : ℕ
hq : q ∈ replicate (count p n.primeFactorsList) p
⊢ count q (replicate (count p n.primeFactorsList) p) ≤ count q n.primeFactorsList

Tactic:
simp [List.eq_of_mem_replicate hq]

Premises used: List.eq_of_mem_replicate
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
rw :
  (∀ (p : ℕ),
      HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
        HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)) ↔
    ∀ (i : ℕ), LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) i : ℕ) ((b.factorization : (a : ℕ) → ℕ) i : ℕ)
⊢ (∀ (p : ℕ),
      HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
        HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)) ↔
    a ∣ b

Tactic:
rw [← factorization_le_iff_dvd ha hb, Finsupp.le_def]

Premises used: Finsupp.le_def, Nat.factorization_le_iff_dvd
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a₁ :
  ∀ (p : ℕ),
    HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
        HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ↔
      LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ (∀ (p : ℕ),
      HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
        HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)) ↔
    ∀ (i : ℕ), LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) i : ℕ) ((b.factorization : (a : ℕ) → ℕ) i : ℕ)

Tactic:
congr! 1 with p
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
a₁ :
  HPow.hPow (α := ℕ) (β := ℕ) 0 ((a.factorization : (a : ℕ) → ℕ) 0 : ℕ) ∣
      HPow.hPow (α := ℕ) (β := ℕ) 0 ((b.factorization : (a : ℕ) → ℕ) 0 : ℕ) ↔
    LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) 0 : ℕ) ((b.factorization : (a : ℕ) → ℕ) 0 : ℕ)
a₂ :
  HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℕ) 0 1) ((a.factorization : (a : ℕ) → ℕ) (HAdd.hAdd (α := ℕ) 0 1) : ℕ) ∣
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℕ) 0 1) ((b.factorization : (a : ℕ) → ℕ) (HAdd.hAdd (α := ℕ) 0 1) : ℕ) ↔
    LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) (HAdd.hAdd (α := ℕ) 0 1) : ℕ)
      ((b.factorization : (a : ℕ) → ℕ) (HAdd.hAdd (α := ℕ) 0 1) : ℕ)
a₃ :
  ∀ (p : ℕ),
    HPow.hPow (β := ℕ) (p + 1 + 1) ((a.factorization : (a : ℕ) → ℕ) (p + 1 + 1) : ℕ) ∣
        HPow.hPow (β := ℕ) (p + 1 + 1) ((b.factorization : (a : ℕ) → ℕ) (p + 1 + 1) : ℕ) ↔
      LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) (p + 1 + 1) : ℕ) ((b.factorization : (a : ℕ) → ℕ) (p + 1 + 1) : ℕ)
⊢ HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ↔
    LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
obtain _ | _ | p := p
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ HPow.hPow (α := ℕ) (β := ℕ) 0 ((a.factorization : (a : ℕ) → ℕ) 0 : ℕ) ∣
      HPow.hPow (α := ℕ) (β := ℕ) 0 ((b.factorization : (a : ℕ) → ℕ) 0 : ℕ) ↔
    LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) 0 : ℕ) ((b.factorization : (a : ℕ) → ℕ) 0 : ℕ)

Tactic:
simp [Nat.pow_dvd_pow_iff_le_right]

Premises used: Nat.pow_dvd_pow_iff_le_right
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℕ) 0 1) ((a.factorization : (a : ℕ) → ℕ) (HAdd.hAdd (α := ℕ) 0 1) : ℕ) ∣
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℕ) 0 1) ((b.factorization : (a : ℕ) → ℕ) (HAdd.hAdd (α := ℕ) 0 1) : ℕ) ↔
    LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) (HAdd.hAdd (α := ℕ) 0 1) : ℕ)
      ((b.factorization : (a : ℕ) → ℕ) (HAdd.hAdd (α := ℕ) 0 1) : ℕ)

Tactic:
simp [Nat.pow_dvd_pow_iff_le_right]

Premises used: Nat.pow_dvd_pow_iff_le_right
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ HPow.hPow (β := ℕ) (p + 1 + 1) ((a.factorization : (a : ℕ) → ℕ) (p + 1 + 1) : ℕ) ∣
      HPow.hPow (β := ℕ) (p + 1 + 1) ((b.factorization : (a : ℕ) → ℕ) (p + 1 + 1) : ℕ) ↔
    LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) (p + 1 + 1) : ℕ) ((b.factorization : (a : ℕ) → ℕ) (p + 1 + 1) : ℕ)

Tactic:
simp [Nat.pow_dvd_pow_iff_le_right]

Premises used: Nat.pow_dvd_pow_iff_le_right
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : n ≠ 0
⊢ (↑n.divisors : Set ℕ) = {x : ℕ | ∃ f ≤ n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x}

Tactic:
Set.ext fun k ↦ ⟨fun h ↦ ?_, fun ⟨f, hle, h⟩ ↦ mem_divisors.mpr ⟨?_, hn⟩⟩

Premises used: Iff.mpr, Set.ext, Nat.mem_divisors, Membership.mem, Nat.divisors, SetLike.coe, And.intro, Iff.intro, _private.0.Nat.coe_divisors_eq_prod_pow_le_factorization.match_1
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : n ≠ 0
refine_1 :
  ∀ (k : ℕ) (h : k ∈ (↑n.divisors : Set ℕ)),
    Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f ≤ n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
refine_2 :
  ∀ (k : ℕ),
    Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f ≤ n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k →
      ∀ (f : ℕ →₀ ℕ) (hle : f ≤ n.factorization) (h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k), k ∣ n
⊢ (↑n.divisors : Set ℕ) = {x : ℕ | ∃ f ≤ n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x}

Tactic:
refine Set.ext fun k ↦ ⟨fun h ↦ ?_, fun ⟨f, hle, h⟩ ↦ mem_divisors.mpr ⟨?_, hn⟩⟩
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
h : k ∈ (↑n.divisors : Set ℕ)
⊢ k ∣ n

Tactic:
have hdvd := dvd_of_mem_divisors h
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
h : k ∈ (↑n.divisors : Set ℕ)
hdvd : k ∣ n
⊢ k ≠ 0

Tactic:
have hk := ne_zero_of_dvd_ne_zero hn hdvd
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
h : k ∈ (↑n.divisors : Set ℕ)
hdvd : k ∣ n
hk : k ≠ 0
⊢ Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f ≤ n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k

Tactic:
⟨_, factorization_le_iff_dvd hk hn |>.mpr hdvd, prod_factorization_pow_eq_self hk⟩

Premises used: Iff.mpr, Set.Mem, setOf, Nat.factorization_le_iff_dvd, Nat.prod_factorization_pow_eq_self, And.intro, Exists.intro
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
h : k ∈ (↑n.divisors : Set ℕ)
hdvd : k ∣ n
hk : k ≠ 0
⊢ Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f ≤ n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k

Tactic:
exact ⟨_, factorization_le_iff_dvd hk hn |>.mpr hdvd, prod_factorization_pow_eq_self hk⟩
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
h_1 : Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f ≤ n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
refine_2 : Dvd.dvd (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
⊢ k ∣ n

Tactic:
rw [← h, ← prod_factorization_pow_eq_self hn]

Premises used: Nat.prod_factorization_pow_eq_self
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
h_1 : Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f ≤ n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
⊢ Dvd.dvd (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)

Tactic:
prod_dvd_prod_of_subset_of_dvd (support_mono hle) fun p _ ↦ Nat.pow_dvd_pow p <| hle p

Premises used: Finsupp.support_mono, Finsupp.prod_dvd_prod_of_subset_of_dvd, Nat.pow_dvd_pow
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
h_1 : Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f ≤ n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
⊢ Dvd.dvd (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)

Tactic:
exact prod_dvd_prod_of_subset_of_dvd (support_mono hle) fun p _ ↦ Nat.pow_dvd_pow p <| hle p

Premises used: Finsupp.support_mono, Finsupp.prod_dvd_prod_of_subset_of_dvd, Nat.pow_dvd_pow
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : n ≠ 0
apply :
  (↑n.divisors : Set ℕ) =
    (↑(Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iic n.factorization)) : Set ℕ)
⊢ n.divisors = Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iic n.factorization)

Tactic:
apply Finset.coe_inj.mp

Premises used: Finset.coe_inj, Iff.mp
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : n ≠ 0
⊢ (↑n.divisors : Set ℕ) =
    (↑(Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iic n.factorization)) : Set ℕ)

Tactic:
grind [coe_divisors_eq_prod_pow_le_factorization]

Premises used: Nat.coe_divisors_eq_prod_pow_le_factorization
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
⊢ Function.Injective (β := ℕ) fun (x : ↥(Finset.Iic n.factorization)) ↦ (↑x : ℕ →₀ ℕ).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2

Tactic:
grind [Function.Injective, factorization_prod_pow_eq_self_of_le_factorization]

Premises used: Nat.factorization_prod_pow_eq_self_of_le_factorization, Function.Injective
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : n ≠ 0
rw :
  n.divisors =
    Finset.image
      (⇑{ toFun := fun (x : ↥(Finset.Iic n.factorization)) ↦ (↑x : ℕ →₀ ℕ).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2, inj' := ⋯ :
            ↥(Finset.Iic n.factorization) ↪ ℕ } :
        (a : ↥(Finset.Iic n.factorization)) → ℕ)
      (Finset.Iic n.factorization).attach
⊢ n.divisors =
    Finset.map
      { toFun := fun (x : ↥(Finset.Iic n.factorization)) ↦ (↑x : ℕ →₀ ℕ).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2, inj' := ⋯ :
        ↥(Finset.Iic n.factorization) ↪ ℕ }
      (Finset.Iic n.factorization).attach

Tactic:
rw [Finset.map_eq_image]

Premises used: Finset.map_eq_image
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : n ≠ 0
rw : n.divisors = Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iic n.factorization)
⊢ n.divisors =
    Finset.image
      ((fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∘
        Subtype.val (p := fun (x : ℕ →₀ ℕ) ↦ x ∈ Finset.Iic n.factorization))
      (Finset.Iic n.factorization).attach

Tactic:
rw [← Finset.image_image, Finset.attach_image_val]

Premises used: Finset.image_image, Finset.attach_image_val
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : n ≠ 0
⊢ n.divisors = Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iic n.factorization)

Tactic:
divisors_eq_image_Iic_factorization_prod_pow hn

Premises used: Nat.divisors_eq_image_Iic_factorization_prod_pow
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : n ≠ 0
⊢ n.divisors = Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iic n.factorization)

Tactic:
exact divisors_eq_image_Iic_factorization_prod_pow hn

Premises used: Nat.divisors_eq_image_Iic_factorization_prod_pow
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
pos :
  ∀ (hn : n = 0), (↑n.properDivisors : Set ℕ) = {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x}
neg :
  ∀ (hn : ¬n = 0), (↑n.properDivisors : Set ℕ) = {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x}
⊢ (↑n.properDivisors : Set ℕ) = {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x}

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : n = 0
⊢ (↑n.properDivisors : Set ℕ) = {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x}

Tactic:
simp [hn]
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
⊢ (↑n.properDivisors : Set ℕ) = {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x}

Tactic:
Set.ext fun k ↦ ⟨fun h ↦ ?_, fun ⟨f, hlt, h⟩ ↦ ?_⟩

Premises used: Set.ext, Membership.mem, Nat.properDivisors, SetLike.coe, Iff.intro, _private.0.Nat.coe_properDivisors_eq_prod_pow_lt_factorization.match_1
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
neg :
  ∀ (k : ℕ) (h : k ∈ (↑n.properDivisors : Set ℕ)),
    Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
neg₁ :
  ∀ (k : ℕ),
    Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k →
      ∀ (f : ℕ →₀ ℕ) (hlt : f < n.factorization) (h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k),
        k ∈ (↑n.properDivisors : Set ℕ)
⊢ (↑n.properDivisors : Set ℕ) = {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x}

Tactic:
refine Set.ext fun k ↦ ⟨fun h ↦ ?_, fun ⟨f, hlt, h⟩ ↦ ?_⟩
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ (↑n.properDivisors : Set ℕ)
⊢ k ∣ n

Tactic:
have ⟨hdvd, hlt⟩ := mem_properDivisors.mp h
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ (↑n.properDivisors : Set ℕ)
hdvd : k ∣ n
⊢ k < n

Tactic:
have ⟨hdvd, hlt⟩ := mem_properDivisors.mp h
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ (↑n.properDivisors : Set ℕ)
hdvd : k ∣ n
hlt : k < n
⊢ k ≠ 0

Tactic:
have hk := ne_zero_of_dvd_ne_zero hn hdvd
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ (↑n.properDivisors : Set ℕ)
hdvd : k ∣ n
hlt : k < n
hk : k ≠ 0
⊢ Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k

Tactic:
⟨_, ?_, prod_factorization_pow_eq_self hk⟩

Premises used: Set.Mem, setOf, Nat.prod_factorization_pow_eq_self, And.intro, Exists.intro
-- Module: Mathlib.Data.Nat.Factorization.Divisors
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ (↑n.properDivisors : Set ℕ)
hdvd : k ∣ n
hlt : k < n
hk : k ≠ 0
neg : k.factorization < n.factorization
⊢ Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k

Tactic:
refine ⟨_, ?_, prod_factorization_pow_eq_self hk⟩