awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun (x : ℕ) ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
hc : c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
p : ℕ
foo : ∀ (p : ℕ) (hp : p ∈ factors.support), Prime p
⊢ n ∣ (a.factorization : (a : ℕ) → ℕ) p
have h₁ : HMul.hMul (β := ℕ) m ((a.factorization : (a : ℕ) → ℕ) p : ℕ) =
  HMul.hMul (β := ℕ) n ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: refine hmn.symm.dvd_of_dvd_mul_left ⟨b.factorization p, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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
⊢ m'.Coprime n'
have inl : ∀ (hm : m ≠ 0), m'.Coprime n'
Tactic: rcases hmn with hm | hn
Cleared hypotheses: hmn
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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
inl : ∀ (hm : m ≠ 0), m'.Coprime n'
⊢ m'.Coprime n'
have inr : ∀ (hn : n ≠ 0), m'.Coprime n'
Tactic: rcases hmn with hm | hn
Cleared hypotheses: hmn
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
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
⊢ ∃ (c : ℕ), a = c ^ (n / g) ∧ b = c ^ (m / g)
have coprime : m'.Coprime n'
Tactic: have coprime : m'.Coprime n' := by
    rcases hmn with hm | hn
    · exact gcd_div_gcd_div_gcd_of_pos_left (zero_lt_of_ne_zero hm)
    · exact gcd_div_gcd_div_gcd_of_pos_right (zero_lt_of_ne_zero hn)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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
have rw : a ^ (m' * g)
Tactic: rw [show m = m' * g from (Nat.div_mul_cancel (gcd_dvd_left m n)).symm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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'
have conv_lhs : ∀ (h : a ^ (m' * g) = b ^ n),
  let n' := n / m.gcd n;
  ∀ (coprime : m'.Coprime n'), a ^ m' = b ^ n'
Tactic: conv_lhs at h => rw [show m = m' * g from (Nat.div_mul_cancel (gcd_dvd_left m n)).symm]
Cleared hypotheses: h, n', coprime
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
h : a ^ (m' * g) = b ^ n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
| b ^ n
have rw : b ^ (n' * g)
Tactic: rw [show n = n' * g from (Nat.div_mul_cancel (gcd_dvd_right m n)).symm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
Goal:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
h : a ^ (m' * g) = b ^ n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
⊢ a ^ m' = b ^ n'
have h₁ : a ^ (m' * g) = b ^ (n' * g)
Tactic: conv_rhs at h => rw [show n = n' * g from (Nat.div_mul_cancel (gcd_dvd_right m n)).symm]
Cleared hypotheses: h, coprime
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
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'
⊢ a ^ m' = b ^ n'
have h₁ : (a ^ m') ^ g = (b ^ n') ^ g
Tactic: rw [pow_mul, pow_mul] at h
Cleared hypotheses: h, coprime
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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'
⊢ g ≠ 0
have inl : ∀ (hm : m ≠ 0), g ≠ 0
Tactic: rcases hmn with hm | hn
Cleared hypotheses: hmn
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
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'
inl : ∀ (hm : m ≠ 0), g ≠ 0
⊢ g ≠ 0
have inr : ∀ (hn : n ≠ 0), g ≠ 0
Tactic: rcases hmn with hm | hn
Cleared hypotheses: hmn
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
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'
⊢ a ^ m' = b ^ n'
have this : g ≠ 0
Tactic: have : g ≠ 0 := by
      rcases hmn with hm | hn
      · exact gcd_ne_zero_left hm
      · exact gcd_ne_zero_right hn
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
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'
⊢ ∃ (c : ℕ), a = c ^ (n / g) ∧ b = c ^ (m / g)
have pow_eq : 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
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
a b m n_1 p n : ℕ
⊢ ∀ (a : ℕ), a ∈ n.primeFactors ↔ (if Prime a then padicValNat a n else 0) ≠ 0
have simp : ∀ (a : ℕ), Prime a → (a ∣ n ∧ ¬n = 0 ↔ ¬a = 1 ∧ ¬n = 0 ∧ a ∣ n)
Tactic: simp [not_or]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n p : ℕ
⊢ count p n.primeFactorsList = (n.factorization : (a : ℕ) → ℕ) p
have inl : count p (primeFactorsList 0) = (factorization 0 : (a : ℕ) → ℕ) p
Tactic: rcases n.eq_zero_or_pos with (rfl | hn0)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n p : ℕ
inl : count p (primeFactorsList 0) = (factorization 0 : (a : ℕ) → ℕ) p
⊢ count p n.primeFactorsList = (n.factorization : (a : ℕ) → ℕ) p
have inr : ∀ (hn0 : n > 0), count p n.primeFactorsList = (n.factorization : (a : ℕ) → ℕ) p
Tactic: rcases n.eq_zero_or_pos with (rfl | hn0)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ count p n.primeFactorsList = (n.factorization : (a : ℕ) → ℕ) p
have rw : Eq (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [count_eq_zero_of_not_mem (mt prime_of_mem_primeFactorsList pp)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (hypothesis)
Goal:
n p : ℕ
hn0 : n > 0
⊢ count p n.primeFactorsList = (n.factorization : (a : ℕ) → ℕ) p
have pp : 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList = (n.factorization : (a : ℕ) → ℕ) p
have inr : count p n.primeFactorsList = padicValNat p n
Tactic: simp only [factorization_def _ pp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList = padicValNat p n
have inr : count p n.primeFactorsList ≤ padicValNat p n
Tactic: apply _root_.le_antisymm
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n p : ℕ
hn0 : n > 0
pp : Prime p
inr : count p n.primeFactorsList ≤ padicValNat p n
⊢ count p n.primeFactorsList = padicValNat p n
have inr₁ : padicValNat p n ≤ count p n.primeFactorsList
Tactic: apply _root_.le_antisymm
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList ≤ padicValNat p n
have inr : replicate (count p n.primeFactorsList) p <+~ n.primeFactorsList
Tactic: rw [le_padicValNat_iff_replicate_subperm_primeFactorsList pp hn0.ne']
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ padicValNat p n ≤ count p n.primeFactorsList
have inr : ¬replicate (count p n.primeFactorsList + 1) p <+~ n.primeFactorsList
Tactic: rw [← Nat.lt_add_one_iff, lt_iff_not_ge,
      le_padicValNat_iff_replicate_subperm_primeFactorsList pp hn0.ne']
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (hypothesis)
Goal:
n p : ℕ
hn0 : n > 0
pp : Prime p
h : replicate (count p n.primeFactorsList + 1) p <+~ n.primeFactorsList
⊢ False
have this : count p (replicate (count p n.primeFactorsList + 1) p) ≤ count p n.primeFactorsList
Tactic: have := h.count_le p
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n : ℕ
⊢ n.factorization = (Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) (↑n.primeFactorsList : Multiset ℕ)
have h : ∀ (p : ℕ),
  Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
    ((((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) (↑n.primeFactorsList : Multiset ℕ) : ℕ →₀ ℕ) : (a : ℕ) → ℕ) p :
      ℕ)
Tactic: ext p
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n p : ℕ
hp : Prime p
hn : n ≠ 0
h : p ∣ n
⊢ LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have rwa : 0 < count p n.primeFactorsList
Tactic: rwa [← primeFactorsList_count_eq, count_pos_iff, mem_primeFactorsList_iff_dvd hn hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n p : ℕ
hp : Prime p
hn : n ≠ 0
h : p ∣ n
rwa : 0 < count p n.primeFactorsList
⊢ LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have rwa₁ : p ∈ n.primeFactorsList
Tactic: rwa [← primeFactorsList_count_eq, count_pos_iff, mem_primeFactorsList_iff_dvd hn hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = n
have rw : (Finsupp.prod ((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) (↑n.primeFactorsList : Multiset ℕ)) fun (x1 x2 : ℕ) ↦
    x1 ^ x2) =
  n
Tactic: rw [factorization_eq_primeFactorsList_multiset n]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ (Finsupp.prod ((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) (↑n.primeFactorsList : Multiset ℕ)) fun (x1 x2 : ℕ) ↦
      x1 ^ x2) =
    n
have simp : n.primeFactorsList.prod = n
Tactic: simp only [← prod_toMultiset, Multiset.prod_coe, Multiset.toFinsupp_toMultiset]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
⊢ factorization 0 = 0
have h : ∀ (a : ℕ), Eq (α := ℕ) ((factorization 0 : (a : ℕ) → ℕ) a : ℕ) ((0 : (a : ℕ) → ℕ) a : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
⊢ factorization 1 = 0
have h : ∀ (a : ℕ), Eq (α := ℕ) ((factorization 1 : (a : ℕ) → ℕ) a : ℕ) ((0 : (a : ℕ) → ℕ) a : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n p : ℕ
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
have simp_rw : p ∉ n.factorization.support ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
Tactic: simp_rw [← notMem_support_iff, support_factorization, mem_primeFactors, not_and_or, not_ne_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n p : ℕ
simp_rw : p ∉ n.factorization.support ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
have simp_rw₁ : p ∉ n.primeFactors ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
Tactic: simp_rw [← notMem_support_iff, support_factorization, mem_primeFactors, not_and_or, not_ne_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
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
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
have simp_rw₂ : ¬(Prime p ∧ p ∣ n ∧ n ≠ 0) ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
Tactic: simp_rw [← notMem_support_iff, support_factorization, mem_primeFactors, not_and_or, not_ne_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
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
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
have simp_rw₃ : ¬Prime p ∨ ¬p ∣ n ∨ ¬n ≠ 0 ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
Tactic: simp_rw [← notMem_support_iff, support_factorization, mem_primeFactors, not_and_or, not_ne_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
p r i : ℕ
hr : ¬p ∣ r
⊢ Eq (α := ℕ) (((p * i + r).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have h : ¬p ∣ p * i + r
Tactic: apply factorization_eq_zero_of_not_dvd
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b).factorization = a.factorization + b.factorization
have h : ∀ (p : ℕ),
  Eq (α := ℕ) (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization + b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: ext p
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d.factorization ≤ n.factorization ↔ d ∣ n
have refine_1 : ∀ (hdn : d.factorization ≤ n.factorization), d ∣ n
Tactic: refine ⟨fun hdn ↦ ?_, fun ⟨c, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
refine_1 : ∀ (hdn : d.factorization ≤ n.factorization), d ∣ n
⊢ d.factorization ≤ n.factorization ↔ d ∣ n
have refine_2 : d ∣ n → ∀ (c : ℕ) (h : n = d * c), d.factorization ≤ n.factorization
Tactic: refine ⟨fun hdn ↦ ?_, fun ⟨c, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : d.factorization ≤ n.factorization
⊢ d ∣ n
have refine_1 : Dvd.dvd (α := ℕ) (d.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
Tactic: rw [← prod_factorization_pow_eq_self hn, ← prod_factorization_pow_eq_self hd]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
h_1 : d ∣ n
c : ℕ
h : n = d * c
⊢ d.factorization ≤ n.factorization
have refine_2 : ∀ (hn : d * c ≠ 0), d ∣ d * c → d.factorization ≤ (d * c).factorization
Tactic: subst h
Cleared hypotheses: n, hn, h_1, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
d : ℕ
hd : d ≠ 0
c : ℕ
hn : d * c ≠ 0
h : d ∣ d * c
⊢ d.factorization ≤ (d * c).factorization
have refine_2 : d.factorization ≤ d.factorization + c.factorization
Tactic: rw [factorization_mul hd <| right_ne_zero_of_mul hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ (S.prod g).factorization = ∑ x ∈ S, (g x).factorization
have refine_1 : (Finset.prod ∅ g).factorization = ∑ x ∈ ∅, (g x).factorization
Tactic: refine Finset.induction_on' S ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
refine_1 : (Finset.prod ∅ g).factorization = ∑ x ∈ ∅, (g x).factorization
⊢ (S.prod g).factorization = ∑ x ∈ S, (g x).factorization
have 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
Tactic: refine Finset.induction_on' S ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (hypothesis)
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
⊢ ((insert x T).prod g).factorization = ∑ x ∈ insert x T, (g x).factorization
have hT : T.prod g ≠ 0
Tactic: have hT : T.prod g ≠ 0 := prod_ne_zero_iff.mpr fun x hx => hS x (hTS hx)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ (S.prod g).factorization = ∑ x ∈ S, (g x).factorization
have refine_1 : (Finset.prod ∅ g).factorization = ∑ x ∈ ∅, (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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
refine_1 : (Finset.prod ∅ g).factorization = ∑ x ∈ ∅, (g x).factorization
⊢ (S.prod g).factorization = ∑ x ∈ S, (g x).factorization
have 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
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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization
have succ : ∀ (ih : (HPow.hPow (α := ℕ) 0 k).factorization = k • factorization 0),
  (HPow.hPow (α := ℕ) 0 (k + 1)).factorization = (k + 1) • factorization 0
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n, ih
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
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
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization
have succ₁ : ∀ (hn : n ≠ 0), (n ^ (k + 1)).factorization = (k + 1) • n.factorization
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization
have succ : (n ^ k * n).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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
succ : (n ^ k * n).factorization = (k + 1) • n.factorization
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization
have succ₁ : (n * n ^ k).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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
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
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization
have succ₂ : n.factorization + (n ^ k).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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
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
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization
have succ₃ : n.factorization + k • n.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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
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
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization
have succ₄ : n.factorization + k • n.factorization = k • n.factorization + HSMul.hSMul (α := ℕ) 1 n.factorization
Tactic: rw [Nat.pow_succ, mul_comm, factorization_mul hn (pow_ne_zero _ hn), ih,
      add_smul, one_smul, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
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
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization
have succ₅ : n.factorization + k • n.factorization = k • n.factorization + n.factorization
Tactic: rw [Nat.pow_succ, mul_comm, factorization_mul hn (pow_ne_zero _ hn), ih,
      add_smul, one_smul, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
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
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization
have succ₆ : k • n.factorization + n.factorization = k • n.factorization + n.factorization
Tactic: rw [Nat.pow_succ, mul_comm, factorization_mul hn (pow_ne_zero _ hn), ih,
      add_smul, one_smul, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n k : ℕ
⊢ (n ^ k).factorization = k • n.factorization
have zero : (HPow.hPow (β := ℕ) n 0).factorization = HSMul.hSMul (α := ℕ) 0 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]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
n k : ℕ
zero : (HPow.hPow (β := ℕ) n 0).factorization = HSMul.hSMul (α := ℕ) 0 n.factorization
⊢ (n ^ k).factorization = k • n.factorization
have succ : ∀ (k : ℕ) (ih : (n ^ k).factorization = k • n.factorization), (n ^ (k + 1)).factorization = (k + 1) • 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]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
p : ℕ
hp : Prime p
⊢ p.factorization = single p 1
have h : ∀ (q : ℕ), Eq (α := ℕ) ((p.factorization : (a : ℕ) → ℕ) q : ℕ) ((single p 1 : (a : ℕ) → ℕ) q : ℕ)
Tactic: ext q
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Defs (goal)
Goal:
p : ℕ
hp : Prime p
q : ℕ
⊢ Eq (α := ℕ) ((p.factorization : (a : ℕ) → ℕ) q : ℕ) ((single p 1 : (a : ℕ) → ℕ) q : ℕ)
have h : Eq (α := ℕ) 1 1
Tactic: rw [← primeFactorsList_count_eq, primeFactorsList_prime hp, single_apply, count_singleton',
    if_congr eq_comm]