awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
h : (a ^ m') ^ g = (b ^ n') ^ g
coprime : m'.Coprime n'
this : g ≠ 0
⊢ a ^ m' = b ^ n'

Tactic:
exact Nat.pow_left_injective this h

Premises used: Nat.pow_left_injective
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
⊢ a ^ m' = b ^ n'

Tactic:
have pow_eq : a ^ m' = b ^ n' := by
    conv_lhs at h => rw [show m = m' * g from (Nat.div_mul_cancel (gcd_dvd_left m n)).symm]
    conv_rhs at h => rw [show n = n' * g from (Nat.div_mul_cancel (gcd_dvd_right m n)).symm]
    rw [pow_mul, pow_mul] at h
    have : g ≠ 0 := by
      rcases hmn with hm | hn
      · exact gcd_ne_zero_left hm
      · exact gcd_ne_zero_right hn
    exact Nat.pow_left_injective this h
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
pow_eq : a ^ m' = b ^ n'
⊢ ∃ (c : ℕ), a = c ^ (n / g) ∧ b = c ^ (m / g)

Tactic:
exists_eq_pow_of_exponent_coprime_of_pow_eq_pow coprime pow_eq

Premises used: Nat.exists_eq_pow_of_exponent_coprime_of_pow_eq_pow
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
pow_eq : a ^ m' = b ^ n'
⊢ ∃ (c : ℕ), a = c ^ (n / g) ∧ b = c ^ (m / g)

Tactic:
exact exists_eq_pow_of_exponent_coprime_of_pow_eq_pow coprime pow_eq

Premises used: Nat.exists_eq_pow_of_exponent_coprime_of_pow_eq_pow
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a b m n_1 p n : ℕ
simp : ∀ (a : ℕ), Prime a → (a ∣ n ∧ ¬n = 0 ↔ ¬a = 1 ∧ ¬n = 0 ∧ a ∣ n)
⊢ ∀ (a : ℕ), a ∈ n.primeFactors ↔ (if Prime a then padicValNat a n else 0) ≠ 0

Tactic:
simp [not_or]

Premises used: not_or
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a b m n_1 p n : ℕ
⊢ ∀ (a : ℕ), Prime a → (a ∣ n ∧ ¬n = 0 ↔ ¬a = 1 ∧ ¬n = 0 ∧ a ∣ n)

Tactic:
aesop
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
⊢ n.factorization.support = n.primeFactors

Tactic:
rfl

Premises used: Multiset.toFinset, List.toFinset, Nat.primeFactors, rfl
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
pp : Prime p
⊢ (n.factorization : (a : ℕ) → ℕ) p = padicValNat p n

Tactic:
simpa [factorization] using absurd pp

Premises used: absurd, Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
inl : count p (primeFactorsList 0) = (factorization 0 : (a : ℕ) → ℕ) p
inr : ∀ (hn0 : n > 0), count p n.primeFactorsList = (n.factorization : (a : ℕ) → ℕ) p
⊢ count p n.primeFactorsList = (n.factorization : (a : ℕ) → ℕ) p

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn0)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
p : ℕ
⊢ count p (primeFactorsList 0) = (factorization 0 : (a : ℕ) → ℕ) p

Tactic:
simp [factorization, count]

Premises used: List.count, Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hn0 : n > 0
pp : ¬Prime p
rw : Eq (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ count p n.primeFactorsList = (n.factorization : (a : ℕ) → ℕ) p

Tactic:
rw [count_eq_zero_of_not_mem (mt prime_of_mem_primeFactorsList pp)]

Premises used: Nat.prime_of_mem_primeFactorsList, mt, List.count_eq_zero_of_not_mem
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ Eq (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp [factorization, pp]

Premises used: Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hn0 : n > 0
⊢ Prime p

Tactic:
if pp : p.Prime then ?_ else
    rw [count_eq_zero_of_not_mem (mt prime_of_mem_primeFactorsList pp)]
    simp [factorization, pp]

Premises used: Nat.Prime, Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hn0 : n > 0
pp : Prime p
inr : count p n.primeFactorsList = padicValNat p n
⊢ count p n.primeFactorsList = (n.factorization : (a : ℕ) → ℕ) p

Tactic:
simp only [factorization_def _ pp]

Premises used: Nat.factorization_def
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hn0 : n > 0
pp : Prime p
inr : count p n.primeFactorsList ≤ padicValNat p n
inr₁ : padicValNat p n ≤ count p n.primeFactorsList
⊢ count p n.primeFactorsList = padicValNat p n

Tactic:
apply _root_.le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hn0 : n > 0
pp : Prime p
inr : replicate (count p n.primeFactorsList) p <+~ n.primeFactorsList
⊢ count p n.primeFactorsList ≤ padicValNat p n

Tactic:
rw [le_padicValNat_iff_replicate_subperm_primeFactorsList pp hn0.ne']

Premises used: LT.lt.ne', le_padicValNat_iff_replicate_subperm_primeFactorsList
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ replicate (count p n.primeFactorsList) p <+~ n.primeFactorsList

Tactic:
List.replicate_sublist_iff.mpr le_rfl |>.subperm

Premises used: Iff.mpr, le_rfl, List.replicate_sublist_iff, List.Sublist.subperm
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ replicate (count p n.primeFactorsList) p <+~ n.primeFactorsList

Tactic:
exact List.replicate_sublist_iff.mpr le_rfl |>.subperm

Premises used: Iff.mpr, le_rfl, List.replicate_sublist_iff, List.Sublist.subperm
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hn0 : n > 0
pp : Prime p
inr : ¬replicate (count p n.primeFactorsList + 1) p <+~ n.primeFactorsList
⊢ padicValNat p n ≤ count p n.primeFactorsList

Tactic:
rw [← Nat.lt_add_one_iff, lt_iff_not_ge,
      le_padicValNat_iff_replicate_subperm_primeFactorsList pp hn0.ne']

Premises used: lt_iff_not_ge, Nat.lt_add_one_iff, LT.lt.ne', le_padicValNat_iff_replicate_subperm_primeFactorsList
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hn0 : n > 0
pp : Prime p
h : replicate (count p n.primeFactorsList + 1) p <+~ n.primeFactorsList
⊢ count p (replicate (count p n.primeFactorsList + 1) p) ≤ count p n.primeFactorsList

Tactic:
have := h.count_le p
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hn0 : n > 0
pp : Prime p
h : replicate (count p n.primeFactorsList + 1) p <+~ n.primeFactorsList
this : count p (replicate (count p n.primeFactorsList + 1) p) ≤ count p n.primeFactorsList
⊢ False

Tactic:
simp at this
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
h :
  ∀ (p : ℕ),
    Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
      ((((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) (↑n.primeFactorsList : Multiset ℕ) : ℕ →₀ ℕ) : (a : ℕ) → ℕ)
          p :
        ℕ)
⊢ n.factorization = (Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) (↑n.primeFactorsList : Multiset ℕ)

Tactic:
ext p
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
    ((((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) (↑n.primeFactorsList : Multiset ℕ) : ℕ →₀ ℕ) : (a : ℕ) → ℕ) p :
      ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hp : Prime p
hn : n ≠ 0
h : p ∣ n
rwa : 0 < count p n.primeFactorsList
rwa₁ : p ∈ n.primeFactorsList
rwa₂ rwa₃ rwa₄ rwa₅ : p ∣ n
⊢ LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rwa [← primeFactorsList_count_eq, count_pos_iff, mem_primeFactorsList_iff_dvd hn hp]

Premises used: Nat.mem_primeFactorsList_iff_dvd, List.count_pos_iff, Nat.primeFactorsList_count_eq
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ multiplicity p n = (n.factorization : (a : ℕ) → ℕ) p

Tactic:
simp [factorization, pp, padicValNat_def' pp.ne_one hn]

Premises used: Nat.Prime.ne_one, padicValNat_def', Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
hn : n ≠ 0
rw :
  (Finsupp.prod ((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) (↑n.primeFactorsList : Multiset ℕ)) fun (x1 x2 : ℕ) ↦
      x1 ^ x2) =
    n
⊢ (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = n

Tactic:
rw [factorization_eq_primeFactorsList_multiset n]

Premises used: Nat.factorization_eq_primeFactorsList_multiset
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
hn : n ≠ 0
simp : n.primeFactorsList.prod = n
⊢ (Finsupp.prod ((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) (↑n.primeFactorsList : Multiset ℕ)) fun (x1 x2 : ℕ) ↦
      x1 ^ x2) =
    n

Tactic:
simp only [← prod_toMultiset, Multiset.prod_coe, Multiset.toFinsupp_toMultiset]

Premises used: Finsupp.prod_toMultiset, Multiset.toFinsupp_toMultiset, Multiset.prod_coe
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
hn : n ≠ 0
⊢ n.primeFactorsList.prod = n

Tactic:
prod_primeFactorsList hn

Premises used: Nat.prod_primeFactorsList
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
hn : n ≠ 0
⊢ n.primeFactorsList.prod = n

Tactic:
exact prod_primeFactorsList hn

Premises used: Nat.prod_primeFactorsList
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ a.primeFactorsList ~ b.primeFactorsList

Tactic:
simpa only [List.perm_iff_count, primeFactorsList_count_eq] using h

Premises used: Nat.primeFactorsList_count_eq, List.perm_iff_count
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : a.factorization = b.factorization
⊢ a = b

Tactic:
eq_of_factorization_eq ha hb (congrFun (congrArg DFunLike.coe h))

Premises used: congrArg, congrFun, DFunLike.coe, Nat.eq_of_factorization_eq
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a : ℕ
ha : Membership.mem (γ := Set ℕ) {x : ℕ | x ≠ 0} a
b : ℕ
hb : Membership.mem (γ := Set ℕ) {x : ℕ | x ≠ 0} b
h : a.factorization = b.factorization
p : ℕ
⊢ Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp [h]
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
h : ∀ (a : ℕ), Eq (α := ℕ) ((factorization 0 : (a : ℕ) → ℕ) a : ℕ) ((0 : (a : ℕ) → ℕ) a : ℕ)
⊢ factorization 0 = 0

Tactic:
ext
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a : ℕ
⊢ Eq (α := ℕ) ((factorization 0 : (a : ℕ) → ℕ) a : ℕ) ((0 : (a : ℕ) → ℕ) a : ℕ)

Tactic:
simp [factorization]

Premises used: Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
h : ∀ (a : ℕ), Eq (α := ℕ) ((factorization 1 : (a : ℕ) → ℕ) a : ℕ) ((0 : (a : ℕ) → ℕ) a : ℕ)
⊢ factorization 1 = 0

Tactic:
ext
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a : ℕ
⊢ Eq (α := ℕ) ((factorization 1 : (a : ℕ) → ℕ) a : ℕ) ((0 : (a : ℕ) → ℕ) a : ℕ)

Tactic:
simp [factorization]

Premises used: Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
simp_rw : p ∉ n.factorization.support ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
simp_rw₁ : p ∉ n.primeFactors ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
simp_rw₂ : ¬(Prime p ∧ p ∣ n ∧ n ≠ 0) ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
simp_rw₃ : ¬Prime p ∨ ¬p ∣ n ∨ ¬n ≠ 0 ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0

Tactic:
simp_rw [← notMem_support_iff, support_factorization, mem_primeFactors, not_and_or, not_ne_iff]

Premises used: Finsupp.notMem_support_iff, Nat.support_factorization, not_ne_iff, not_and_or, Nat.mem_primeFactors
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hp : ¬Prime p
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
simp [factorization_eq_zero_iff, hp]

Premises used: Nat.factorization_eq_zero_iff
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ)

Tactic:
factorization_eq_zero_of_not_prime _ not_prime_zero

Premises used: Nat.factorization_eq_zero_of_not_prime, Nat.not_prime_zero
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) 1 : ℕ) (0 : ℕ)

Tactic:
factorization_eq_zero_of_not_prime _ not_prime_one

Premises used: Nat.not_prime_one, Nat.factorization_eq_zero_of_not_prime
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
h : ¬p ∣ n
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
simp [factorization_eq_zero_iff, h]

Premises used: Nat.factorization_eq_zero_iff
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
p r i : ℕ
hr : ¬p ∣ r
h : ¬p ∣ p * i + r
⊢ Eq (α := ℕ) (((p * i + r).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
apply factorization_eq_zero_of_not_dvd

Premises used: Nat.factorization_eq_zero_of_not_dvd
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
p r i : ℕ
hr h h₁ h₂ h₃ : ¬p ∣ r
⊢ ¬p ∣ p * i + r

Tactic:
rwa [← Nat.dvd_add_iff_right (Dvd.intro i rfl)]

Premises used: Dvd.intro, Nat.dvd_add_iff_right, rfl
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h :
  ∀ (p : ℕ),
    Eq (α := ℕ) (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization + b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ (a * b).factorization = a.factorization + b.factorization

Tactic:
ext p
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ Eq (α := ℕ) (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization + b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp only [add_apply, ← primeFactorsList_count_eq,
    perm_iff_count.mp (perm_primeFactorsList_mul ha hb) p, count_append]

Premises used: Finsupp.add_apply, Nat.primeFactorsList_count_eq, List.perm_iff_count, List.count_append, Nat.perm_primeFactorsList_mul, Iff.mp
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d.factorization ≤ n.factorization ↔ d ∣ n

Tactic:
⟨fun hdn ↦ ?_, fun ⟨c, h⟩ ↦ ?_⟩

Premises used: LE.le, Iff.intro, _private.0.Nat.factorization_le_iff_dvd.match_1, Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
refine_1 : ∀ (hdn : d.factorization ≤ n.factorization), d ∣ n
refine_2 : d ∣ n → ∀ (c : ℕ) (h : n = d * c), d.factorization ≤ n.factorization
⊢ d.factorization ≤ n.factorization ↔ d ∣ n

Tactic:
refine ⟨fun hdn ↦ ?_, fun ⟨c, h⟩ ↦ ?_⟩
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : d.factorization ≤ n.factorization
refine_1 :
  Dvd.dvd (α := ℕ) (d.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
⊢ d ∣ n

Tactic:
rw [← prod_factorization_pow_eq_self hn, ← prod_factorization_pow_eq_self hd]

Premises used: Nat.prod_factorization_pow_eq_self
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : d.factorization ≤ n.factorization
⊢ Dvd.dvd (α := ℕ) (d.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)

Tactic:
prod_dvd_prod_of_subset_of_dvd (support_mono hdn) fun a _ ↦ pow_dvd_pow a (hdn a)

Premises used: pow_dvd_pow, Finsupp.support_mono, Finsupp.prod_dvd_prod_of_subset_of_dvd
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : d.factorization ≤ n.factorization
⊢ Dvd.dvd (α := ℕ) (d.factorization.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 hdn) fun a _ ↦ pow_dvd_pow a (hdn a)

Premises used: pow_dvd_pow, Finsupp.support_mono, Finsupp.prod_dvd_prod_of_subset_of_dvd
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
h_1 : d ∣ n
c : ℕ
h : n = d * c
refine_2 : ∀ (hn : d * c ≠ 0), d ∣ d * c → d.factorization ≤ (d * c).factorization
⊢ d.factorization ≤ n.factorization

Tactic:
subst h
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
d : ℕ
hd : d ≠ 0
c : ℕ
hn : d * c ≠ 0
h : d ∣ d * c
refine_2 : d.factorization ≤ d.factorization + c.factorization
⊢ d.factorization ≤ (d * c).factorization

Tactic:
rw [factorization_mul hd <| right_ne_zero_of_mul hn]

Premises used: Nat.factorization_mul, right_ne_zero_of_mul
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
d : ℕ
hd : d ≠ 0
c : ℕ
hn : d * c ≠ 0
h : d ∣ d * c
⊢ d.factorization ≤ d.factorization + c.factorization

Tactic:
apply self_le_add_right

Premises used: self_le_add_right
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ (S.prod g).factorization = ∑ x ∈ S, (g x).factorization

Tactic:
Finset.induction_on' S ?_ ?_

Premises used: Finset.induction_on'
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
refine_1 : (Finset.prod ∅ g).factorization = ∑ x ∈ ∅, (g x).factorization
refine_2 :
  ∀ (a : α) (s : Finset α),
    a ∈ S →
      s ⊆ S →
        a ∉ s →
          (s.prod g).factorization = ∑ x ∈ s, (g x).factorization →
            ((insert a s).prod g).factorization = ∑ x ∈ insert a s, (g x).factorization
⊢ (S.prod g).factorization = ∑ x ∈ S, (g x).factorization

Tactic:
refine Finset.induction_on' S ?_ ?_
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ (Finset.prod ∅ g).factorization = ∑ x ∈ ∅, (g x).factorization

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
hxT : x ∉ T
IH : (T.prod g).factorization = ∑ x ∈ T, (g x).factorization
⊢ T.prod g ≠ 0

Tactic:
have hT : T.prod g ≠ 0 := prod_ne_zero_iff.mpr fun x hx => hS x (hTS hx)
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
hxT : x ∉ T
IH : (T.prod g).factorization = ∑ x ∈ T, (g x).factorization
hT : T.prod g ≠ 0
⊢ ((insert x T).prod g).factorization = ∑ x ∈ insert x T, (g x).factorization

Tactic:
simp [prod_insert hxT, sum_insert hxT, IH, factorization_mul (hS x hxS) hT]

Premises used: Finset.prod_insert, Nat.factorization_mul, Finset.sum_insert
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
refine_1 : (Finset.prod ∅ g).factorization = ∑ x ∈ ∅, (g x).factorization
refine_2 refine_2₁ :
  ∀ (a : α) (s : Finset α),
    a ∈ S →
      s ⊆ S →
        a ∉ s →
          (s.prod g).factorization = ∑ x ∈ s, (g x).factorization →
            ((insert a s).prod g).factorization = ∑ x ∈ insert a s, (g x).factorization
⊢ (S.prod g).factorization = ∑ x ∈ S, (g x).factorization

Tactic:
classical
    refine Finset.induction_on' S ?_ ?_
    · simp
    · intro x T hxS hTS hxT IH
      have hT : T.prod g ≠ 0 := prod_ne_zero_iff.mpr fun x hx => hS x (hTS hx)
      simp [prod_insert hxT, sum_insert hxT, IH, factorization_mul (hS x hxS) hT]
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
⊢ (HPow.hPow (β := ℕ) n 0).factorization = HSMul.hSMul (α := ℕ) 0 n.factorization

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
succ :
  ∀ (ih : (HPow.hPow (α := ℕ) 0 k).factorization = k • factorization 0),
    (HPow.hPow (α := ℕ) 0 (k + 1)).factorization = (k + 1) • factorization 0
succ₁ : ∀ (hn : n ≠ 0), (n ^ (k + 1)).factorization = (k + 1) • n.factorization
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization

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:
k : ℕ
ih : (HPow.hPow (α := ℕ) 0 k).factorization = k • factorization 0
⊢ (HPow.hPow (α := ℕ) 0 (k + 1)).factorization = (k + 1) • factorization 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
succ : (n ^ k * n).factorization = (k + 1) • n.factorization
succ₁ : (n * n ^ k).factorization = (k + 1) • n.factorization
succ₂ : n.factorization + (n ^ k).factorization = (k + 1) • n.factorization
succ₃ : n.factorization + k • n.factorization = (k + 1) • n.factorization
succ₄ : n.factorization + k • n.factorization = k • n.factorization + HSMul.hSMul (α := ℕ) 1 n.factorization
succ₅ : n.factorization + k • n.factorization = k • n.factorization + n.factorization
succ₆ succ₇ : k • n.factorization + n.factorization = k • n.factorization + n.factorization
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization

Tactic:
rw [Nat.pow_succ, mul_comm, factorization_mul hn (pow_ne_zero _ hn), ih,
      add_smul, one_smul, add_comm]

Premises used: Nat.factorization_mul, pow_ne_zero, Nat.pow_succ, add_comm, one_smul, add_smul, mul_comm
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n k : ℕ
zero : (HPow.hPow (β := ℕ) n 0).factorization = HSMul.hSMul (α := ℕ) 0 n.factorization
succ :
  ∀ (k : ℕ) (ih : (n ^ k).factorization = k • n.factorization), (n ^ (k + 1)).factorization = (k + 1) • n.factorization
⊢ (n ^ k).factorization = k • n.factorization

Tactic:
induction k with
  | zero => simp
  | succ k ih =>
    rcases eq_or_ne n 0 with (rfl | hn)
    · simp
    rw [Nat.pow_succ, mul_comm, factorization_mul hn (pow_ne_zero _ hn), ih,
      add_smul, one_smul, add_comm]

Premises used: Nat.pow_succ, add_comm, one_smul, add_smul, mul_comm, eq_or_ne, Nat.zero, OfNat.ofNat, Nat.succ, rfl
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
p : ℕ
hp : Prime p
h : ∀ (q : ℕ), Eq (α := ℕ) ((p.factorization : (a : ℕ) → ℕ) q : ℕ) ((single p 1 : (a : ℕ) → ℕ) q : ℕ)
⊢ p.factorization = single p 1

Tactic:
ext q
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
p : ℕ
hp : Prime p
q : ℕ
h : Eq (α := ℕ) 1 1
h₁ : Eq (α := ℕ) 0 0
rw rw₁ : ℕ
⊢ Eq (α := ℕ) ((p.factorization : (a : ℕ) → ℕ) q : ℕ) ((single p 1 : (a : ℕ) → ℕ) q : ℕ)

Tactic:
rw [← primeFactorsList_count_eq, primeFactorsList_prime hp, single_apply, count_singleton',
    if_congr eq_comm]

Premises used: Nat.primeFactorsList_prime, if_congr, eq_comm, Nat.primeFactorsList_count_eq, List.count_singleton', Finsupp.single_apply
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
p : ℕ
hp : Prime p
q : ℕ
⊢ Eq (α := ℕ) 1 1

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
p : ℕ
hp : Prime p
q : ℕ
⊢ Eq (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
p k : ℕ
hp : Prime p
⊢ (p ^ k).factorization = single p k

Tactic:
simp [hp]
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hn : n ≠ 0
hp : Prime p
h : p ^ HAdd.hAdd (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) ∣ n
⊢ (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

Premises used: pow_ne_zero, Nat.factorization_le_iff_dvd, Nat.Prime.ne_zero
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n p : ℕ
hn : n ≠ 0
hp : Prime p
h : (p ^ HAdd.hAdd (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)).factorization ≤ n.factorization
⊢ False

Tactic:
simpa [hp.factorization] using h p

Premises used: Nat.Prime.factorization
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
hn : 1 < n
⊢ Ne (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ) (0 : ℕ)

Tactic:
mt (factorization_eq_zero_iff _ _).mp ?_

Premises used: mt, Iff.mp, Nat.factorization_eq_zero_iff
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
hn : 1 < n
refine : ¬(¬Prime n.minFac ∨ ¬n.minFac ∣ n ∨ n = 0)
⊢ Ne (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ) (0 : ℕ)

Tactic:
refine mt (factorization_eq_zero_iff _ _).mp ?_

Premises used: mt, Iff.mp, Nat.factorization_eq_zero_iff
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
hn : 1 < n
push : Prime n.minFac ∧ n.minFac ∣ n ∧ n ≠ 0
⊢ ¬(¬Prime n.minFac ∨ ¬n.minFac ∣ n ∨ n = 0)

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
hn : 1 < n
⊢ n ≠ 1

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorization.Defs
Goal:
n : ℕ
hn : 1 < n
⊢ Prime n.minFac ∧ n.minFac ∣ n ∧ n ≠ 0

Tactic:
exact ⟨minFac_prime (by lia), minFac_dvd n, Nat.ne_zero_of_lt hn⟩