awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
i : ℕ
h1 : p ^ i ∣ n
h2 : 1 ≤ i
h : i < n
⊢ i < b
have h₁ : ∀ (pp : Prime 0) (hb : n < HPow.hPow (α := ℕ) 0 b) (h1 : HPow.hPow (α := ℕ) 0 i ∣ n), i < b
Tactic: rcases p with - | p
Cleared hypotheses: p, pp, hb, h1
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
i : ℕ
h1 : p ^ i ∣ n
h2 : 1 ≤ i
h : i < n
h₁ : ∀ (pp : Prime 0) (hb : n < HPow.hPow (α := ℕ) 0 b) (h1 : HPow.hPow (α := ℕ) 0 i ∣ n), i < b
⊢ i < b
have h₂ : ∀ (p : ℕ) (pp : Prime (p + 1)) (hb : n < (p + 1) ^ b) (h1 : (p + 1) ^ i ∣ n), i < b
Tactic: rcases p with - | p
Cleared hypotheses: p, pp, hb, h1
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
Goal:
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
pp : Prime 0
hb : n < HPow.hPow (α := ℕ) 0 b
h1 : HPow.hPow (α := ℕ) 0 i ∣ n
⊢ i < b
have h1₁ : n = 0
Tactic: rw [zero_pow (by lia), zero_dvd_iff] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
p : ℕ
pp : Prime (p + 1)
hb : n < (p + 1) ^ b
h1 : (p + 1) ^ i ∣ n
⊢ i < b
have h₁ : (p + 1) ^ i < (p + 1) ^ b
Tactic: rw [← Nat.pow_lt_pow_iff_right (Prime.one_lt pp)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
b m n : ℕ
hm : Prime m
hn : 0 < n
hb : n < m ^ b
⊢ (n.factorization : (a : ℕ) → ℕ) m = #({i ∈ Ico 1 b | m ^ i ∣ n})
have rwa : #({i ∈ Ico 1 n | m ^ i ∣ n}) = #({i ∈ Ico 1 b | m ^ i ∣ n})
Tactic: rwa [factorization_eq_card_pow_dvd n hm, Ico_pow_dvd_eq_Ico_of_lt hm (by lia)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
b m n : ℕ
hm : Prime m
hn : 0 < n
hb : n < m ^ b
rwa : #({i ∈ Ico 1 n | m ^ i ∣ n}) = #({i ∈ Ico 1 b | m ^ i ∣ n})
⊢ (n.factorization : (a : ℕ) → ℕ) m = #({i ∈ Ico 1 b | m ^ i ∣ n})
have rwa₁ : #({i ∈ Ico 1 b | m ^ i ∣ n}) = #({i ∈ Ico 1 b | m ^ i ∣ n})
Tactic: rwa [factorization_eq_card_pow_dvd n hm, Ico_pow_dvd_eq_Ico_of_lt hm (by lia)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p a b : ℕ
hab : a.Coprime b
hpa : p ∈ a.primeFactorsList
⊢ Eq (α := ℕ) (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw : HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) =
  (a.factorization : (a : ℕ) → ℕ) p
Tactic: rw [factorization_mul_apply_of_coprime hab, ← primeFactorsList_count_eq,
    ← primeFactorsList_count_eq,
    count_eq_zero_of_not_mem (coprime_primeFactorsList_disjoint hab hpa), add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p a b : ℕ
hab : a.Coprime b
hpa : p ∈ a.primeFactorsList
rw :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) =
    (a.factorization : (a : ℕ) → ℕ) p
⊢ Eq (α := ℕ) (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₁ : HAdd.hAdd (β := ℕ) (count p a.primeFactorsList) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) = count p a.primeFactorsList
Tactic: rw [factorization_mul_apply_of_coprime hab, ← primeFactorsList_count_eq,
    ← primeFactorsList_count_eq,
    count_eq_zero_of_not_mem (coprime_primeFactorsList_disjoint hab hpa), add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p a b : ℕ
hab : a.Coprime b
hpa : p ∈ a.primeFactorsList
rw :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) =
    (a.factorization : (a : ℕ) → ℕ) p
rw₁ :
  HAdd.hAdd (β := ℕ) (count p a.primeFactorsList) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) = count p a.primeFactorsList
⊢ Eq (α := ℕ) (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₂ : count p a.primeFactorsList + count p b.primeFactorsList = count p a.primeFactorsList
Tactic: rw [factorization_mul_apply_of_coprime hab, ← primeFactorsList_count_eq,
    ← primeFactorsList_count_eq,
    count_eq_zero_of_not_mem (coprime_primeFactorsList_disjoint hab hpa), add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p a b : ℕ
hab : a.Coprime b
hpa : p ∈ a.primeFactorsList
rw :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) =
    (a.factorization : (a : ℕ) → ℕ) p
rw₁ :
  HAdd.hAdd (β := ℕ) (count p a.primeFactorsList) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) = count p a.primeFactorsList
rw₂ : count p a.primeFactorsList + count p b.primeFactorsList = count p a.primeFactorsList
⊢ Eq (α := ℕ) (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₃ : count p a.primeFactorsList + 0 = count p a.primeFactorsList
Tactic: rw [factorization_mul_apply_of_coprime hab, ← primeFactorsList_count_eq,
    ← primeFactorsList_count_eq,
    count_eq_zero_of_not_mem (coprime_primeFactorsList_disjoint hab hpa), add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p a b : ℕ
hab : a.Coprime b
hpa : p ∈ a.primeFactorsList
rw :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) =
    (a.factorization : (a : ℕ) → ℕ) p
rw₁ :
  HAdd.hAdd (β := ℕ) (count p a.primeFactorsList) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) = count p a.primeFactorsList
rw₂ : count p a.primeFactorsList + count p b.primeFactorsList = count p a.primeFactorsList
rw₃ : count p a.primeFactorsList + 0 = count p a.primeFactorsList
⊢ Eq (α := ℕ) (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₄ : count p a.primeFactorsList = count p a.primeFactorsList
Tactic: rw [factorization_mul_apply_of_coprime hab, ← primeFactorsList_count_eq,
    ← primeFactorsList_count_eq,
    count_eq_zero_of_not_mem (coprime_primeFactorsList_disjoint hab hpa), add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p a b : ℕ
hab : a.Coprime b
hpb : p ∈ b.primeFactorsList
⊢ Eq (α := ℕ) (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw : Eq (α := ℕ) (((b * a).factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b ↔ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
have mp : a = b → ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
mp : a = b → ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
⊢ a = b ↔ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
have mpr : (∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b) → a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
⊢ a = b
have mpr : ∀ (p : ℕ), Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: refine eq_of_factorization_eq ha hb fun p => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
⊢ Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have pos : ∀ (pp : Prime p), Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: by_cases pp : p.Prime
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pos : ∀ (pp : Prime p), Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have neg : ∀ (pp : ¬Prime p), Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: by_cases pp : p.Prime
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n = n
have nth_rw : Eq (α := ℕ) (∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
Tactic: nth_rw 2 [← prod_factorization_pow_eq_self hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ Eq (α := ℕ) (∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
have rw : Eq (α := ℕ) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n)
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ Eq (α := ℕ) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n)
have h : n.factorization.support ⊆ {p ∈ Finset.range m | Prime p}
Tactic: apply Finset.prod_subset_one_on_sdiff
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
h : n.factorization.support ⊆ {p ∈ Finset.range m | Prime p}
⊢ Eq (α := ℕ) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n)
have hg : ∀ x ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support, x ^ padicValNat x n = 1
Tactic: apply Finset.prod_subset_one_on_sdiff
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
h : n.factorization.support ⊆ {p ∈ Finset.range m | Prime p}
hg : ∀ x ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support, x ^ padicValNat x n = 1
⊢ Eq (α := ℕ) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n)
have hfg : ∀ x ∈ n.factorization.support, (fun (x1 x2 : ℕ) ↦ x1 ^ x2) x ((n.factorization : (a : ℕ) → ℕ) x) = x ^ padicValNat x n
Tactic: apply Finset.prod_subset_one_on_sdiff
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support
⊢ p ^ padicValNat p n = 1
have hp1 : p ∈ {p ∈ Finset.range m | Prime p}
Tactic: obtain ⟨hp1, hp2⟩ := Finset.mem_sdiff.mp hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support
hp1 : p ∈ {p ∈ Finset.range m | Prime p}
⊢ p ^ padicValNat p n = 1
have hp2 : p ∉ n.factorization.support
Tactic: obtain ⟨hp1, hp2⟩ := Finset.mem_sdiff.mp hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support
hp1 : p ∈ {p ∈ Finset.range m | Prime p}
hp2 : p ∉ n.factorization.support
⊢ p ^ padicValNat p n = 1
have hg : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
Tactic: rw [← factorization_def n (Finset.mem_filter.mp hp1).2]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ n = ∏ p : ↥n.primeFactors, HPow.hPow (β := ℕ) (↑p : ℕ) ((n.factorization : (a : ℕ) → ℕ) (↑p : ℕ) : ℕ)
have nth_rw : Eq (α := ℕ) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
  (∏ p : ↥n.primeFactors, HPow.hPow (β := ℕ) (↑p : ℕ) ((n.factorization : (a : ℕ) → ℕ) (↑p : ℕ) : ℕ))
Tactic: nth_rw 1 [← prod_factorization_pow_eq_self hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Function.onFun Coprime
    (fun (p : ↥n.primeFactors) ↦ HPow.hPow (β := ℕ) (↑p : ℕ) ((n.factorization : (a : ℕ) → ℕ) (↑p : ℕ) : ℕ)) p1 p2
have refine : (↑p1 : ℕ).Coprime (↑p2 : ℕ)
Tactic: refine Nat.Coprime.pow (n.factorization p1) (n.factorization p2) ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ (↑p1 : ℕ).Coprime (↑p2 : ℕ)
have refine_1 : Prime (↑p1 : ℕ)
Tactic: refine (Nat.coprime_primes ?_ ?_).mpr <| Subtype.coe_ne_coe.mpr hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
refine_1 : Prime (↑p1 : ℕ)
⊢ (↑p1 : ℕ).Coprime (↑p2 : ℕ)
have refine_2 : Prime (↑p2 : ℕ)
Tactic: refine (Nat.coprime_primes ?_ ?_).mpr <| Subtype.coe_ne_coe.mpr hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
⊢ #({e ∈ Finset.range n | p ∣ e + 1}) = n / p
have zero : #({e ∈ Finset.range 0 | p ∣ e + 1}) = 0 / p
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    simp [Nat.succ_div, add_ite, add_zero, Finset.range_add_one, filter_insert, apply_ite card,
      card_insert_of_notMem, hn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
zero : #({e ∈ Finset.range 0 | p ∣ e + 1}) = 0 / p
⊢ #({e ∈ Finset.range n | p ∣ e + 1}) = n / p
have succ : ∀ (n : ℕ) (hn : #({e ∈ Finset.range n | p ∣ e + 1}) = n / p), #({e ∈ Finset.range (n + 1) | p ∣ e + 1}) = (n + 1) / p
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    simp [Nat.succ_div, add_ite, add_zero, Finset.range_add_one, filter_insert, apply_ite card,
      card_insert_of_notMem, hn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
⊢ #({x ∈ Ioc 0 n | p ∣ x}) = n / p
have zero : card (α := ℕ) ({x ∈ Ioc 0 0 | p ∣ x}) = 0 / p
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
zero : card (α := ℕ) ({x ∈ Ioc 0 0 | p ∣ x}) = 0 / p
⊢ #({x ∈ Ioc 0 n | p ∣ x}) = n / p
have succ : ∀ (n : ℕ), #({x ∈ Ioc 0 n | p ∣ x}) = n / p → #({x ∈ Ioc 0 (n + 1) | p ∣ x}) = (n + 1) / p
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
⊢ #({k ∈ Finset.range (N + 1).succ | k ≠ 0 ∧ n ∣ k}) = (N + 1) / n
have succ : #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
    else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
  (N + 1) / n
Tactic: rw [Finset.range_add_one, Finset.filter_insert]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n
have pos : ∀ (h : n ∣ N.succ),
  #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n
Tactic: by_cases h : n ∣ N.succ
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
pos :
  ∀ (h : n ∣ N.succ),
    #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
        else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
      (N + 1) / n
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n
have neg : ∀ (h : ¬n ∣ N.succ),
  #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n
Tactic: by_cases h : n ∣ N.succ
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
N n : ℕ
⊢ #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
have zero : #({k ∈ Finset.range (succ 0) | k ≠ 0 ∧ n ∣ k}) = 0 / n
Tactic: induction N with
  | zero => simp [Finset.filter_false_of_mem]
  | succ N ih =>
    rw [Finset.range_add_one, Finset.filter_insert]
    by_cases h : n ∣ N.succ
    · simp [h, succ_div_of_dvd, ih]
    · simp [h, succ_div_of_not_dvd, ih]
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
N n : ℕ
zero : #({k ∈ Finset.range (succ 0) | k ≠ 0 ∧ n ∣ k}) = 0 / n
⊢ #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
have succ : ∀ (N : ℕ) (ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n),
  #({k ∈ Finset.range (N + 1).succ | k ≠ 0 ∧ n ∣ k}) = (N + 1) / n
Tactic: induction N with
  | zero => simp [Finset.filter_false_of_mem]
  | succ N ih =>
    rw [Finset.range_add_one, Finset.filter_insert]
    by_cases h : n ∣ N.succ
    · simp [h, succ_div_of_dvd, ih]
    · simp [h, succ_div_of_not_dvd, ih]
Cleared hypotheses: N
-- 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
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
have pos : ∀ (ha0 : a = 0), ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
Tactic: by_cases ha0 : a = 0
-- 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
pos : ∀ (ha0 : a = 0), ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
have neg : ∀ (ha0 : ¬a = 0), ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
Tactic: by_cases ha0 : a = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : a = 0
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
have h₁ : b ^ n = a ^ m
Tactic: symm at h
Cleared hypotheses: h, ha0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
have pos : ∀ (hm0 : m = 0), ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
Tactic: by_cases hm0 : m = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
pos : ∀ (hm0 : m = 0), ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
have neg : ∀ (hm0 : ¬m = 0), ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
Tactic: by_cases hm0 : m = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
hm0 : ¬m = 0
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
have h₁ : a = HPow.hPow (α := ℕ) 0 n ∧ b = HPow.hPow (α := ℕ) 0 m
Tactic: use 0
-- 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
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
have pos : ∀ (hn0 : n = 0), ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
Tactic: by_cases hn0 : n = 0
-- 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
pos : ∀ (hn0 : n = 0), ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
have neg : ∀ (hn0 : ¬n = 0), ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
Tactic: by_cases hn0 : n = 0
-- 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
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
have h₁ : a = b ^ n ∧ b = b ^ m
Tactic: use b
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
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 : ℕ), a = c ^ n ∧ b = c ^ m
have hc : let c : ℕ := factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2;
c = factors.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
Tactic: set c := factors.prod (· ^ ·) with hc
-- 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
⊢ ∃ (c : ℕ), a = c ^ n ∧ b = c ^ m
have h₁ : a = c ^ n ∧ b = c ^ m
Tactic: use c
-- 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
ha : a = c ^ n
⊢ a = c ^ n ∧ b = c ^ m
have refine : b = c ^ m
Tactic: refine ⟨ha, ?_⟩
-- 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
ha : a = c ^ n
⊢ b = c ^ m
have a₁ : Eq (α := ℕ) ((fun (a : ℕ) ↦ a ^ n) b) ((fun (a : ℕ) ↦ a ^ n) (c ^ m))
Tactic: apply Nat.pow_left_injective hn0
-- 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
⊢ a = c ^ n ∧ b = c ^ m
have h₁ : a = c ^ n
Tactic: suffices ha : a = c ^ n by
    refine ⟨ha, ?_⟩
    apply Nat.pow_left_injective hn0
    simp [← h, ha, Nat.pow_right_comm]
-- 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
⊢ a = c ^ n
have h₁ : ∀ (p : ℕ), Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (((c ^ n).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: apply eq_of_factorization_eq ha0 (by simp [c, factors])
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
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 : ℕ
⊢ Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (((c ^ n).factorization : (a : ℕ) → ℕ) p : ℕ)
have foo : ∀ (p : ℕ) (hp : p ∈ factors.support), Prime p
Tactic: have foo (p) (hp : p ∈ factors.support) : Prime p :=
    prime_of_mem_primeFactors (Finsupp.support_mapRange hp)
-- 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
⊢ Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (((c ^ n).factorization : (a : ℕ) → ℕ) p : ℕ)
have h₁ : Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((n • factors : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [factorization_pow, hc, prod_pow_factorization_eq_self foo]
-- 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
⊢ Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((n • factors : (a : ℕ) → ℕ) p : ℕ)
have h₁ : n ∣ (a.factorization : (a : ℕ) → ℕ) p
Tactic: suffices n ∣ a.factorization p by
    simp [factors, Nat.mul_div_cancel' this]