awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
p : ℕ
hp : Prime p
q : ℕ
h : Eq (α := ℕ) 1 1
⊢ Eq (α := ℕ) ((p.factorization : (a : ℕ) → ℕ) q : ℕ) ((single p 1 : (a : ℕ) → ℕ) q : ℕ)
have h₁ : Eq (α := ℕ) 0 0
Tactic: rw [← primeFactorsList_count_eq, primeFactorsList_prime hp, single_apply, count_singleton',
    if_congr eq_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (hypothesis)
Goal:
n p : ℕ
hn : n ≠ 0
hp : Prime p
h : p ^ HAdd.hAdd (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) ∣ n
⊢ False
have h₁ : (p ^ HAdd.hAdd (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)).factorization ≤ n.factorization
Tactic: rw [← factorization_le_iff_dvd (pow_ne_zero _ hp.ne_zero) hn] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n : ℕ
hn : 1 < n
⊢ Ne (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ) (0 : ℕ)
have refine : ¬(¬Prime n.minFac ∨ ¬n.minFac ∣ n ∨ n = 0)
Tactic: refine mt (factorization_eq_zero_iff _ _).mp ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n : ℕ
hn : 1 < n
⊢ ¬(¬Prime n.minFac ∨ ¬n.minFac ∣ n ∨ n = 0)
have push : Prime n.minFac ∧ n.minFac ∣ n ∧ n ≠ 0
Tactic: push Not
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
⊢ factorization (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = f
have rw : ∑ x1 ∈ f.support, single x1 ((f : (a : ℕ) → ℕ) x1) = f
Tactic: rw [Finsupp.prod, factorization_prod (pow_ne_zero _ <| hf · · |>.ne_zero),
    sum_congr rfl (hf · · |>.factorization_pow)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
⊢ f = n.factorization ↔ (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = n
have mp : f = n.factorization → (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
mp : f = n.factorization → (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = n
⊢ f = n.factorization ↔ (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = n
have mpr : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = n → f = n.factorization
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
⊢ (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∣ n
have inl : ∀ (hf : f ≤ factorization 0), Dvd.dvd (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) 0
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n, hf
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
inl : ∀ (hf : f ≤ factorization 0), Dvd.dvd (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) 0
⊢ (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∣ n
have inr : ∀ (hn : n ≠ 0), (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∣ n
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∣ n
have rwa : Ne (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) 0
Tactic: rwa [← factorization_le_iff_dvd ?_ hn, factorization_prod_pow_eq_self_of_le_factorization hf]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ Ne (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) 0
have refine : ∀ (x : ℕ) (hp : x ∈ f.support), HPow.hPow (β := ℕ) x ((f : (a : ℕ) → ℕ) x : ℕ) ≠ 0
Tactic: refine f.prod_ne_zero_iff.mpr fun _ hp ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ n ∣ f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
have rw : n ∣ n * (f - n.factorization).prod HPow.hPow
Tactic: rw [← add_tsub_cancel_of_le hf, Finsupp.prod_add_index' (by simp) Nat.pow_add,
    prod_factorization_pow_eq_self hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d ∣ n ↔ ∃ f ≤ n.factorization, d = f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
have rw : d.factorization ≤ n.factorization ↔ ∃ f ≤ n.factorization, d = f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
Tactic: rw [← factorization_le_iff_dvd hd hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d.factorization ≤ n.factorization ↔ ∃ f ≤ n.factorization, d = f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
have 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
Tactic: refine ⟨fun h ↦ ⟨_, h, prod_factorization_pow_eq_self hd |>.symm⟩, fun ⟨f, hle, hprod⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
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
⊢ d.factorization ≤ n.factorization
have rwa : factorization (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ≤ n.factorization
Tactic: rwa [hprod, factorization_prod_pow_eq_self_of_le_factorization hle]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
a b : ℕ
hab : a.Coprime b
⊢ (a * b).factorization = a.factorization + b.factorization
have h : ∀ (q : ℕ),
  Eq (α := ℕ) (((a * b).factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization + b.factorization : (a : ℕ) → ℕ) q : ℕ)
Tactic: ext q
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
a b : ℕ
hab : a.Coprime b
q : ℕ
⊢ Eq (α := ℕ) (((a * b).factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization + b.factorization : (a : ℕ) → ℕ) q : ℕ)
have h : ((a * b).factorization : (a : ℕ) → ℕ) q =
  HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ)
Tactic: rw [Finsupp.add_apply, factorization_mul_apply_of_coprime hab]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
a b : ℕ
hab : a.Coprime b
q : ℕ
h :
  ((a * 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 : ℕ)
have h₁ : HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) =
  HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ)
Tactic: rw [Finsupp.add_apply, factorization_mul_apply_of_coprime hab]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (hypothesis)
Goal:
n p : ℕ
⊢ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n
have hp : Prime p
Tactic: if hp : p.Prime then ?_ else simp [hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n p : ℕ
hp : Prime p
⊢ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n
have rw : p ^ count p n.primeFactorsList ∣ n
Tactic: rw [← primeFactorsList_count_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n p : ℕ
hp : Prime p
⊢ p ^ count p n.primeFactorsList ∣ n
have apply : (p ^ count p n.primeFactorsList).primeFactorsList <+~ n.primeFactorsList
Tactic: apply dvd_of_primeFactorsList_subperm (pow_ne_zero _ hp.ne_zero)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n p : ℕ
hp : Prime p
⊢ (p ^ count p n.primeFactorsList).primeFactorsList <+~ n.primeFactorsList
have rw : ∀ x ∈ replicate (count p n.primeFactorsList) p,
  count x (replicate (count p n.primeFactorsList) p) ≤ count x n.primeFactorsList
Tactic: rw [hp.primeFactorsList_pow, List.subperm_ext_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ),
      HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
        HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)) ↔
    a ∣ b
have 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 : ℕ)
Tactic: rw [← factorization_le_iff_dvd ha hb, Finsupp.le_def]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (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 : ℕ)
have 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 : ℕ)
Tactic: congr! 1 with p
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
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 : ℕ)
have 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 : ℕ)
Tactic: obtain _ | _ | p := p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
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 : ℕ)
⊢ HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ↔
    LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have 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) : ℕ)
Tactic: obtain _ | _ | p := p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
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) : ℕ)
⊢ HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ↔
    LE.le (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have 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) : ℕ)
Tactic: obtain _ | _ | p := p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ (↑n.divisors : Set ℕ) = {x : ℕ | ∃ f ≤ n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x}
have refine_1 : ∀ (k : ℕ) (h : k ∈ (↑n.divisors : Set ℕ)),
  Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f ≤ n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
Tactic: refine Set.ext fun k ↦ ⟨fun h ↦ ?_, fun ⟨f, hle, h⟩ ↦ mem_divisors.mpr ⟨?_, hn⟩⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
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
⊢ (↑n.divisors : Set ℕ) = {x : ℕ | ∃ f ≤ n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x}
have 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
Tactic: refine Set.ext fun k ↦ ⟨fun h ↦ ?_, fun ⟨f, hle, h⟩ ↦ mem_divisors.mpr ⟨?_, hn⟩⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
h : k ∈ (↑n.divisors : Set ℕ)
⊢ Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f ≤ n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
have hdvd : k ∣ n
Tactic: have hdvd := dvd_of_mem_divisors h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
h : k ∈ (↑n.divisors : Set ℕ)
hdvd : k ∣ n
⊢ Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f ≤ n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
have hk : k ≠ 0
Tactic: have hk := ne_zero_of_dvd_ne_zero hn hdvd
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
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
⊢ k ∣ n
have refine_2 : Dvd.dvd (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
Tactic: rw [← h, ← prod_factorization_pow_eq_self hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ n.divisors = Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iic n.factorization)
have apply : (↑n.divisors : Set ℕ) =
  (↑(Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iic n.factorization)) : Set ℕ)
Tactic: apply Finset.coe_inj.mp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ 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
have rw : n.divisors =
  Finset.image
    (⇑{ toFun := fun (x : ↥(Finset.Iic n.factorization)) ↦ (↑x : ℕ →₀ ℕ).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2, inj' := sorry :
          ↥(Finset.Iic n.factorization) ↪ ℕ } :
      (a : ↥(Finset.Iic n.factorization)) → ℕ)
    (Finset.Iic n.factorization).attach
Tactic: rw [Finset.map_eq_image]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ 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
have rw : n.divisors = Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iic n.factorization)
Tactic: rw [← Finset.image_image, Finset.attach_image_val]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
Goal:
n : ℕ
⊢ (↑n.properDivisors : Set ℕ) = {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x}
have pos : ∀ (hn : n = 0), (↑n.properDivisors : Set ℕ) = {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x}
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
Goal:
n : ℕ
pos :
  ∀ (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}
have neg : ∀ (hn : ¬n = 0), (↑n.properDivisors : Set ℕ) = {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x}
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
Goal:
n : ℕ
hn : ¬n = 0
⊢ (↑n.properDivisors : Set ℕ) = {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x}
have neg : ∀ (k : ℕ) (h : k ∈ (↑n.properDivisors : Set ℕ)),
  Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
Tactic: refine Set.ext fun k ↦ ⟨fun h ↦ ?_, fun ⟨f, hlt, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
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
⊢ (↑n.properDivisors : Set ℕ) = {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x}
have 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 ℕ)
Tactic: refine Set.ext fun k ↦ ⟨fun h ↦ ?_, fun ⟨f, hlt, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (hypothesis)
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ (↑n.properDivisors : Set ℕ)
⊢ Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
have hdvd : k ∣ n
Tactic: have ⟨hdvd, hlt⟩ := mem_properDivisors.mp h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (hypothesis)
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ (↑n.properDivisors : Set ℕ)
hdvd : k ∣ n
⊢ Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
have hlt : k < n
Tactic: have ⟨hdvd, hlt⟩ := mem_properDivisors.mp h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (hypothesis)
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ (↑n.properDivisors : Set ℕ)
hdvd : k ∣ n
hlt : k < n
⊢ Membership.mem (γ := Set ℕ) {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = x} k
have hk : k ≠ 0
Tactic: have hk := ne_zero_of_dvd_ne_zero hn hdvd
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
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
have neg : k.factorization < n.factorization
Tactic: refine ⟨_, ?_, prod_factorization_pow_eq_self hk⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
Goal:
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ (↑n.properDivisors : Set ℕ)
hdvd : k ∣ n
hlt : k < n
hk : k ≠ 0
⊢ k.factorization < n.factorization
have neg : k.factorization ≠ n.factorization
Tactic: apply lt_of_le_of_ne <| factorization_le_iff_dvd hk hn |>.mpr hdvd
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
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 : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
⊢ k ∣ n
have rw : Dvd.dvd (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
Tactic: rw [← h, ← prod_factorization_pow_eq_self hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
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 : ℕ →₀ ℕ
hlt : 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)
have apply : ∀ a ∈ f.support,
  HPow.hPow (β := ℕ) a ((f : (a : ℕ) → ℕ) a : ℕ) ∣ HPow.hPow (β := ℕ) a ((n.factorization : (a : ℕ) → ℕ) a : ℕ)
Tactic: apply prod_dvd_prod_of_subset_of_dvd <| support_mono hlt.le
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (hypothesis)
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 : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
⊢ k ∈ (↑n.properDivisors : Set ℕ)
have this : k ∣ n
Tactic: have : k ∣ n := by
      rw [← h, ← prod_factorization_pow_eq_self hn]
      apply prod_dvd_prod_of_subset_of_dvd <| support_mono hlt.le
      exact fun p _ ↦ Nat.pow_dvd_pow p <| hlt.le p
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
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 : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
this : k ∣ n
⊢ k ∈ (↑n.properDivisors : Set ℕ)
have neg : k ≠ n
Tactic: refine mem_properDivisors.mpr ⟨this, lt_of_le_of_ne (le_of_dvd (Nat.pos_of_ne_zero hn) this) ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
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 : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = k
this : k ∣ n
⊢ k ≠ n
have neg : k.factorization = f
Tactic: suffices k.factorization = f from (this ▸ hlt.ne <| congrArg _ ·)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
Goal:
n : ℕ
⊢ n.properDivisors = Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iio n.factorization)
have apply : (↑n.properDivisors : Set ℕ) =
  (↑(Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iio n.factorization)) : Set ℕ)
Tactic: apply Finset.coe_inj.mp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
Goal:
n : ℕ
⊢ n.properDivisors =
    Finset.map
      { toFun := fun (x : ↥(Finset.Iio n.factorization)) ↦ (↑x : ℕ →₀ ℕ).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2, inj' := ⋯ :
        ↥(Finset.Iio n.factorization) ↪ ℕ }
      (Finset.Iio n.factorization).attach
have rw : n.properDivisors =
  Finset.image
    (⇑{ toFun := fun (x : ↥(Finset.Iio n.factorization)) ↦ (↑x : ℕ →₀ ℕ).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2, inj' := sorry :
          ↥(Finset.Iio n.factorization) ↪ ℕ } :
      (a : ↥(Finset.Iio n.factorization)) → ℕ)
    (Finset.Iio n.factorization).attach
Tactic: rw [Finset.map_eq_image]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Divisors (goal)
Goal:
n : ℕ
⊢ n.properDivisors =
    Finset.image
      ((fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) ∘
        Subtype.val (p := fun (x : ℕ →₀ ℕ) ↦ x ∈ Finset.Iio n.factorization))
      (Finset.Iio n.factorization).attach
have rw : n.properDivisors = Finset.image (fun (x : ℕ →₀ ℕ) ↦ x.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (Finset.Iio n.factorization)
Tactic: rw [← Finset.image_image, Finset.attach_image_val]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (hypothesis)
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
⊢ motive (k + 2)
have hp : Prime p
Tactic: haveI hp : Prime p := minFac_prime (succ_succ_ne_one k)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (hypothesis)
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := ((k + 2).factorization : (a : ℕ) → ℕ) p
⊢ motive (k + 2)
have hpt : p ^ t ∣ k + 2
Tactic: haveI hpt : p ^ t ∣ k + 2 := ordProj_dvd _ _