awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
rw :
  Eq (α := ℕ →₀ ℕ) ((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) (↑n.primeFactorsList : Multiset ℕ) : ℕ →₀ ℕ)
      (0 : ℕ →₀ ℕ) ↔
    n = 0 ∨ n = 1
⊢ n.factorization = 0 ↔ n = 0 ∨ n = 1

Tactic:
rw [factorization_eq_primeFactorsList_multiset n]

Premises used: Nat.factorization_eq_primeFactorsList_multiset
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
⊢ Eq (α := ℕ →₀ ℕ) ((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) (↑n.primeFactorsList : Multiset ℕ) : ℕ →₀ ℕ)
      (0 : ℕ →₀ ℕ) ↔
    n = 0 ∨ n = 1

Tactic:
simp [Multiset.coe_eq_zero]

Premises used: Multiset.coe_eq_zero
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
α : Type u_1
p : ℕ
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
rw :
  Eq (α := ℕ) ((∑ x ∈ S, (g x).factorization : (a : ℕ) → ℕ) p : ℕ) (∑ x ∈ S, ((g x).factorization : (a : ℕ) → ℕ) p : ℕ)
rw₁ rw₂ : Eq (α := ℕ) (∑ i ∈ S, ((g i).factorization : (a : ℕ) → ℕ) p) (∑ x ∈ S, ((g x).factorization : (a : ℕ) → ℕ) p)
⊢ Eq (α := ℕ) (((S.prod g).factorization : (a : ℕ) → ℕ) p : ℕ) (∑ x ∈ S, ((g x).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [factorization_prod hS, finsetSum_apply]

Premises used: Finsupp.finsetSum_apply, Nat.factorization_prod
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
β : Type u_1
inst : CommMonoid β
f : ℕ → ℕ → β
⊢ n.factorization.prod f = ∏ p ∈ n.primeFactors, f p ((n.factorization : (a : ℕ) → ℕ) p)

Tactic:
rfl

Premises used: Multiset.toFinset, List.toFinset, Nat.primeFactors, Finsupp.prod, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
β : Type u_1
inst : CommMonoid β
f : ℕ → β
⊢ Eq.{u_1 + 1} (α := β) (∏ p ∈ n.primeFactors, f p) (n.factorization.prod fun (p x : ℕ) ↦ f p)

Tactic:
rfl

Premises used: Multiset.toFinset, List.toFinset, Nat.primeFactors, Finsupp.prod, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p : ℕ
hp : Prime p
⊢ Eq (α := ℕ) ((p.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
simp [hp]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p n : ℕ
hp : Prime p
⊢ ((p ^ n).factorization : (a : ℕ) → ℕ) p = n

Tactic:
simp [factorization_pow, Prime.factorization_self hp]

Premises used: Nat.Prime.factorization_self, Nat.factorization_pow
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p k : ℕ
hn : n ≠ 0
h : n.factorization = single p k
rw : (Finsupp.prod (single p k) fun (x1 x2 : ℕ) ↦ x1 ^ x2) = p ^ k
⊢ n = p ^ k

Tactic:
rw [← Nat.prod_factorization_pow_eq_self hn, h]

Premises used: Nat.prod_factorization_pow_eq_self
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p k : ℕ
hn : n ≠ 0
h : n.factorization = single p k
⊢ (Finsupp.prod (single p k) fun (x1 x2 : ℕ) ↦ x1 ^ x2) = p ^ k

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p q : ℕ
hp : Prime p
h : Ne (α := ℕ) ((p.factorization : (a : ℕ) → ℕ) q : ℕ) (0 : ℕ)
⊢ p = q

Tactic:
simpa [hp.factorization, single_apply] using h

Premises used: Nat.Prime.factorization, Finsupp.single_apply
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
⊢ Eq (α := ℕ)
    (↑((factorizationEquiv.symm : (a : { f : ℕ →₀ ℕ // ∀ p ∈ f.support, Prime p }) → ℕ+)
          (Subtype.mk (p := fun (f : ℕ →₀ ℕ) ↦ ∀ p ∈ f.support, Prime p) f hf)) :
      ℕ)
    (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)

Tactic:
factorizationEquiv_symm_apply_coe ⟨f, hf⟩

Premises used: Subtype.mk, Nat.factorizationEquiv_symm_apply_coe
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hp : ¬Prime p
⊢ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1

Tactic:
simp [hp]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hp : ¬Prime p
⊢ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n

Tactic:
simp [hp]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
⊢ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ∣ n

Tactic:
div_dvd_of_dvd (ordProj_dvd n p)

Premises used: Nat.ordProj_dvd, Nat.div_dvd_of_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
pp : Prime p
⊢ 0 < HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp [Nat.pow_pos pp.pos]

Premises used: Nat.Prime.pos, Nat.pow_pos
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
pp : ¬Prime p
⊢ 0 < HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp [pp]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
if : ∀ (pp : Prime p), 0 < HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
if₁ : ∀ (pp : ¬Prime p), 0 < HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
if₂ : ∀ (pp : Prime p), 0 < HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
if₃ if₄ : ∀ (pp : ¬Prime p), 0 < HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ 0 < HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
if pp : p.Prime then simp [Nat.pow_pos pp.pos] else simp [pp]

Premises used: Nat.Prime
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : n ≠ 0
⊢ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ≤ n

Tactic:
le_of_dvd hn.bot_lt (Nat.ordProj_dvd n p)

Premises used: Nat.ordProj_dvd, Nat.le_of_dvd, Ne.bot_lt
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ 0 < n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
Nat.div_pos (ordProj_le p hn) (ordProj_pos n p)

Premises used: Nat.ordProj_le, Nat.ordProj_pos, Nat.div_pos
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ 0 < n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
exact Nat.div_pos (ordProj_le p hn) (ordProj_pos n p)

Premises used: Nat.ordProj_le, Nat.ordProj_pos, Nat.div_pos
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ 0 < n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simpa [Nat.factorization_eq_zero_of_not_prime n pp] using hn.bot_lt

Premises used: Nat.factorization_eq_zero_of_not_prime, Ne.bot_lt
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : n ≠ 0
if : ∀ (pp : Prime p), 0 < n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
if₁ : ∀ (pp : ¬Prime p), 0 < n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
if₂ : ∀ (pp : Prime p), 0 < n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
if₃ if₄ : ∀ (pp : ¬Prime p), 0 < n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ 0 < n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
if pp : p.Prime then
    exact Nat.div_pos (ordProj_le p hn) (ordProj_pos n p)
  else
    simpa [Nat.factorization_eq_zero_of_not_prime n pp] using hn.bot_lt

Premises used: Nat.Prime, Nat.ordProj_le, Nat.ordProj_pos, Nat.div_pos, Ne.bot_lt
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
⊢ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ≤ n

Tactic:
Nat.div_le_self _ _

Premises used: Nat.div_le_self
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
⊢ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) =
    n

Tactic:
Nat.mul_div_cancel' (ordProj_dvd n p)

Premises used: Nat.ordProj_dvd, Nat.mul_div_cancel'
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b p : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
    HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp [factorization_mul ha hb, pow_add]

Premises used: Nat.factorization_mul, pow_add
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b p : ℕ
ha : a = 0
⊢ a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))

Tactic:
simp [ha]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b p : ℕ
ha : ¬a = 0
hb : b = 0
⊢ a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))

Tactic:
simp [hb]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b p : ℕ
ha : ¬a = 0
hb : ¬b = 0
simp :
  a * b /
      (HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
        HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
⊢ a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))

Tactic:
simp only [ordProj_mul p ha hb]

Premises used: Nat.ordProj_mul
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b p : ℕ
ha : ¬a = 0
hb : ¬b = 0
rw rw₁ :
  a * b /
      (HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
        HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)) =
    a * b /
      (HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
        HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
⊢ a * b /
      (HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
        HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))

Tactic:
rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]

Premises used: Nat.ordProj_dvd, Nat.div_mul_div_comm
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b p : ℕ
ha : ¬a = 0
if :
  ∀ (hb : b = 0),
    a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
      a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
        (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
if₁ :
  ∀ (hb : ¬b = 0),
    a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
      a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
        (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
if₂ :
  ∀ (hb : b = 0),
    a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
      a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
        (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
if₃ if₄ :
  ∀ (hb : ¬b = 0),
    a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
      a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
        (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
⊢ a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))

Tactic:
if hb : b = 0 then simp [hb] else
  simp only [ordProj_mul p ha hb]
  rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]

Premises used: Nat.ordProj_dvd, Nat.div_mul_div_comm
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b p : ℕ
if :
  ∀ (ha : a = 0),
    a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
      a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
        (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
if₁ :
  ∀ (ha : ¬a = 0),
    a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
      a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
        (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
if₂ :
  ∀ (ha : a = 0),
    a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
      a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
        (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
if₃ if₄ :
  ∀ (ha : ¬a = 0),
    a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
      a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
        (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
⊢ a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))

Tactic:
if ha : a = 0 then simp [ha] else
  if hb : b = 0 then simp [hb] else
  simp only [ordProj_mul p ha hb]
  rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]

Premises used: Nat.ordProj_dvd, Nat.div_mul_div_comm
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : n ≠ 0
pos : ∀ (pp : Prime p), (n.factorization : (a : ℕ) → ℕ) p < n
neg : ∀ (pp : ¬Prime p), (n.factorization : (a : ℕ) → ℕ) p < n
⊢ (n.factorization : (a : ℕ) → ℕ) p < n

Tactic:
by_cases pp : p.Prime

Premises used: Nat.Prime
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ (n.factorization : (a : ℕ) → ℕ) p < n

Tactic:
(Nat.pow_lt_pow_iff_right pp.one_lt).1 <| (ordProj_le p hn).trans_lt <|
      Nat.lt_pow_self pp.one_lt

Premises used: Nat.lt_pow_self, Nat.Prime.one_lt, Nat.ordProj_le, Nat.pow_lt_pow_iff_right, Iff.mp, LE.le.trans_lt
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ (n.factorization : (a : ℕ) → ℕ) p < n

Tactic:
exact (Nat.pow_lt_pow_iff_right pp.one_lt).1 <| (ordProj_le p hn).trans_lt <|
      Nat.lt_pow_self pp.one_lt

Premises used: Nat.lt_pow_self, Nat.Prime.one_lt, Nat.ordProj_le, Nat.pow_lt_pow_iff_right, Iff.mp, LE.le.trans_lt
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ (n.factorization : (a : ℕ) → ℕ) p < n

Tactic:
simpa only [factorization_eq_zero_of_not_prime n pp] using hn.bot_lt

Premises used: Nat.factorization_eq_zero_of_not_prime, Ne.bot_lt
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p b : ℕ
hb : n ≤ p ^ b
hn : n = 0
⊢ (n.factorization : (a : ℕ) → ℕ) p ≤ b

Tactic:
simp [hn]
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
pp : Prime p
⊢ (n.factorization : (a : ℕ) → ℕ) p ≤ b

Tactic:
(Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)

Premises used: Nat.Prime.one_lt, Nat.ordProj_le, Iff.mp, Nat.pow_le_pow_iff_right, LE.le.trans
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
pp : Prime p
⊢ (n.factorization : (a : ℕ) → ℕ) p ≤ b

Tactic:
exact (Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)

Premises used: Nat.Prime.one_lt, Nat.ordProj_le, Iff.mp, Nat.pow_le_pow_iff_right, LE.le.trans
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
pp : ¬Prime p
⊢ (n.factorization : (a : ℕ) → ℕ) p ≤ b

Tactic:
simp [factorization_eq_zero_of_not_prime n pp]

Premises used: Nat.factorization_eq_zero_of_not_prime
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
if : ∀ (pp : Prime p), (n.factorization : (a : ℕ) → ℕ) p ≤ b
if₁ : ∀ (pp : ¬Prime p), (n.factorization : (a : ℕ) → ℕ) p ≤ b
if₂ : ∀ (pp : Prime p), (n.factorization : (a : ℕ) → ℕ) p ≤ b
if₃ if₄ : ∀ (pp : ¬Prime p), (n.factorization : (a : ℕ) → ℕ) p ≤ b
⊢ (n.factorization : (a : ℕ) → ℕ) p ≤ b

Tactic:
if pp : p.Prime then
    exact (Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)
  else
    simp [factorization_eq_zero_of_not_prime n pp]

Premises used: Nat.Prime
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p b : ℕ
hb : n ≤ p ^ b
if : ∀ (hn : n = 0), (n.factorization : (a : ℕ) → ℕ) p ≤ b
if₁ : ∀ (hn : ¬n = 0), (n.factorization : (a : ℕ) → ℕ) p ≤ b
if₂ : ∀ (hn : n = 0), (n.factorization : (a : ℕ) → ℕ) p ≤ b
if₃ if₄ : ∀ (hn : ¬n = 0), (n.factorization : (a : ℕ) → ℕ) p ≤ b
⊢ (n.factorization : (a : ℕ) → ℕ) p ≤ b

Tactic:
if hn : n = 0 then simp [hn] else
  if pp : p.Prime then
    exact (Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)
  else
    simp [factorization_eq_zero_of_not_prime n pp]

Premises used: Nat.Prime
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
rw :
  (∀ (p : ℕ),
      Prime p → LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) ↔
    d.factorization ≤ n.factorization
⊢ (∀ (p : ℕ),
      Prime p → LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) ↔
    d ∣ n

Tactic:
rw [← factorization_le_iff_dvd hd hn]

Premises used: Nat.factorization_le_iff_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ (∀ (p : ℕ),
      Prime p → LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) ↔
    d.factorization ≤ n.factorization

Tactic:
⟨fun h p => (em p.Prime).elim (h p) fun hp => ?_, fun h p _ => h p⟩

Premises used: Nat.Prime, em, Iff.intro, Or.elim
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
refine :
  ∀
    (h :
      ∀ (p : ℕ),
        Prime p → LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ))
    (p : ℕ) (hp : ¬Prime p),
    LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ (∀ (p : ℕ),
      Prime p → LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) ↔
    d.factorization ≤ n.factorization

Tactic:
refine ⟨fun h p => (em p.Prime).elim (h p) fun hp => ?_, fun h p _ => h p⟩
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
h : ∀ (p : ℕ), Prime p → LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
p : ℕ
hp : ¬Prime p
simp_rw : LE.le (α := ℕ) 0 0
⊢ LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp_rw [factorization_eq_zero_of_not_prime _ hp]

Premises used: Nat.factorization_eq_zero_of_not_prime
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
h : ∀ (p : ℕ), Prime p → LE.le (α := ℕ) ((d.factorization : (a : ℕ) → ℕ) p : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
p : ℕ
hp : ¬Prime p
⊢ LE.le (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
hb : b ≠ 0
inl : factorization 0 ≤ (0 * b).factorization
inr : ∀ (ha : a ≠ 0), a.factorization ≤ (a * b).factorization
⊢ a.factorization ≤ (a * b).factorization

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
b : ℕ
hb : b ≠ 0
⊢ factorization 0 ≤ (0 * b).factorization

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
inr : a ∣ a * b
⊢ a.factorization ≤ (a * b).factorization

Tactic:
rw [factorization_le_iff_dvd ha <| mul_ne_zero ha hb]

Premises used: Nat.factorization_le_iff_dvd, mul_ne_zero
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a ∣ a * b

Tactic:
Dvd.intro b rfl

Premises used: Dvd.intro, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a ∣ a * b

Tactic:
exact Dvd.intro b rfl

Premises used: Dvd.intro, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
rw : b.factorization ≤ (b * a).factorization
⊢ b.factorization ≤ (a * b).factorization

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
⊢ b.factorization ≤ (b * a).factorization

Tactic:
apply factorization_le_factorization_mul_left ha

Premises used: Nat.factorization_le_factorization_mul_left
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p k n : ℕ
pp : Prime p
hn : n ≠ 0
rw : (p ^ k).factorization ≤ n.factorization ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
rw₁ : single p k ≤ n.factorization ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
rw₂ rw₃ : k ≤ (n.factorization : (a : ℕ) → ℕ) p ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
⊢ p ^ k ∣ n ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p

Tactic:
rw [← factorization_le_iff_dvd (Nat.pow_pos pp.pos).ne' hn, pp.factorization_pow, single_le_iff]

Premises used: Nat.Prime.factorization_pow, Nat.Prime.pos, LT.lt.ne', Nat.factorization_le_iff_dvd, Finsupp.single_le_iff, Nat.pow_pos
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p k n : ℕ
pp : Prime p
hn : n ≠ 0
rw : p ^ k ∣ n ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
rw₁ rw₂ : k ≤ (n.factorization : (a : ℕ) → ℕ) p ↔ k ≤ (n.factorization : (a : ℕ) → ℕ) p
⊢ p ^ k ∣ n ↔ p ^ k ∣ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [pow_dvd_pow_iff_le_right pp.one_lt, pp.pow_dvd_iff_le_factorization hn]

Premises used: Nat.Prime.one_lt, Nat.pow_dvd_pow_iff_le_right, Nat.Prime.pow_dvd_iff_le_factorization
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ∣ n ↔ HPow.hPow (β := ℕ) p 1 ∣ n

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
hab : a < b
⊢ b ≠ 0

Tactic:
have hb : b ≠ 0 := (ha.bot_lt.trans hab).ne'
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
hab : a < b
hb : b ≠ 0
contrapose! :
  ∀ (hab : ∀ (p : ℕ), LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)),
    b ≤ a
⊢ ∃ (p : ℕ), LT.lt (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
contrapose! hab
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (p : ℕ), LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ b ∣ a

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

Premises used: Finsupp.le_def, Nat.factorization_le_iff_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : b ∣ a
⊢ b ≤ a

Tactic:
le_of_dvd ha.bot_lt hab

Premises used: Nat.le_of_dvd, Ne.bot_lt
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : b ∣ a
⊢ b ≤ a

Tactic:
exact le_of_dvd ha.bot_lt hab

Premises used: Nat.le_of_dvd, Ne.bot_lt
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
h : d ∣ n
inl : ∀ (h : 0 ∣ n), (n / 0).factorization = n.factorization - factorization 0
inr : ∀ (hd : d ≠ 0), (n / d).factorization = n.factorization - d.factorization
⊢ (n / d).factorization = n.factorization - d.factorization

Tactic:
rcases eq_or_ne d 0 with (rfl | hd)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
h : 0 ∣ n
⊢ (n / 0).factorization = n.factorization - factorization 0

Tactic:
simp [zero_dvd_iff.mp h]

Premises used: zero_dvd_iff, Iff.mp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
h : d ∣ n
hd : d ≠ 0
inr : ∀ (h : d ∣ 0), (0 / d).factorization = factorization 0 - d.factorization
inr₁ : ∀ (hn : n ≠ 0), (n / d).factorization = n.factorization - d.factorization
⊢ (n / d).factorization = n.factorization - d.factorization

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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d : ℕ
hd : d ≠ 0
h : d ∣ 0
⊢ (0 / d).factorization = factorization 0 - d.factorization

Tactic:
simp [tsub_eq_zero_of_le]

Premises used: tsub_eq_zero_of_le
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
inr :
  Eq (α := ℕ →₀ ℕ) ((fun (x : ℕ →₀ ℕ) ↦ x + d.factorization) (n / d).factorization)
    ((fun (x : ℕ →₀ ℕ) ↦ x + d.factorization) (n.factorization - d.factorization))
⊢ (n / d).factorization = n.factorization - d.factorization

Tactic:
apply add_left_injective d.factorization

Premises used: add_left_injective, Nat.factorization