awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
rw : (m * n).primeFactorsList.length = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₁ : (m * n).primeFactorsList.length = HAdd.hAdd (β := ℕ) m.primeFactorsList.length ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₂ : (m * n).primeFactorsList.length = m.primeFactorsList.length + n.primeFactorsList.length
rw₃ : (↑(m * n).primeFactorsList : Multiset ℕ).card = m.primeFactorsList.length + n.primeFactorsList.length
rw₄ : (UniqueFactorizationMonoid.normalizedFactors (m * n)).card = m.primeFactorsList.length + n.primeFactorsList.length
rw₅ :
  (UniqueFactorizationMonoid.normalizedFactors m + UniqueFactorizationMonoid.normalizedFactors n).card =
    m.primeFactorsList.length + n.primeFactorsList.length
⊢ (Ω : (a : ℕ) → ℕ) (m * n) = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
have rw₆ : ((↑m.primeFactorsList : Multiset ℕ) + UniqueFactorizationMonoid.normalizedFactors n).card =
  m.primeFactorsList.length + n.primeFactorsList.length
Tactic: rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
    UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq,
    Multiset.card_add, Multiset.coe_card, Multiset.coe_card]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
rw : (m * n).primeFactorsList.length = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₁ : (m * n).primeFactorsList.length = HAdd.hAdd (β := ℕ) m.primeFactorsList.length ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₂ : (m * n).primeFactorsList.length = m.primeFactorsList.length + n.primeFactorsList.length
rw₃ : (↑(m * n).primeFactorsList : Multiset ℕ).card = m.primeFactorsList.length + n.primeFactorsList.length
rw₄ : (UniqueFactorizationMonoid.normalizedFactors (m * n)).card = m.primeFactorsList.length + n.primeFactorsList.length
rw₅ :
  (UniqueFactorizationMonoid.normalizedFactors m + UniqueFactorizationMonoid.normalizedFactors n).card =
    m.primeFactorsList.length + n.primeFactorsList.length
rw₆ :
  ((↑m.primeFactorsList : Multiset ℕ) + UniqueFactorizationMonoid.normalizedFactors n).card =
    m.primeFactorsList.length + n.primeFactorsList.length
⊢ (Ω : (a : ℕ) → ℕ) (m * n) = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
have rw₇ : ((↑m.primeFactorsList : Multiset ℕ) + (↑n.primeFactorsList : Multiset ℕ)).card =
  m.primeFactorsList.length + n.primeFactorsList.length
Tactic: rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
    UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq,
    Multiset.card_add, Multiset.coe_card, Multiset.coe_card]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
rw : (m * n).primeFactorsList.length = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₁ : (m * n).primeFactorsList.length = HAdd.hAdd (β := ℕ) m.primeFactorsList.length ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₂ : (m * n).primeFactorsList.length = m.primeFactorsList.length + n.primeFactorsList.length
rw₃ : (↑(m * n).primeFactorsList : Multiset ℕ).card = m.primeFactorsList.length + n.primeFactorsList.length
rw₄ : (UniqueFactorizationMonoid.normalizedFactors (m * n)).card = m.primeFactorsList.length + n.primeFactorsList.length
rw₅ :
  (UniqueFactorizationMonoid.normalizedFactors m + UniqueFactorizationMonoid.normalizedFactors n).card =
    m.primeFactorsList.length + n.primeFactorsList.length
rw₆ :
  ((↑m.primeFactorsList : Multiset ℕ) + UniqueFactorizationMonoid.normalizedFactors n).card =
    m.primeFactorsList.length + n.primeFactorsList.length
rw₇ :
  ((↑m.primeFactorsList : Multiset ℕ) + (↑n.primeFactorsList : Multiset ℕ)).card =
    m.primeFactorsList.length + n.primeFactorsList.length
⊢ (Ω : (a : ℕ) → ℕ) (m * n) = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
have rw₈ : (↑m.primeFactorsList : Multiset ℕ).card + (↑n.primeFactorsList : Multiset ℕ).card =
  m.primeFactorsList.length + n.primeFactorsList.length
Tactic: rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
    UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq,
    Multiset.card_add, Multiset.coe_card, Multiset.coe_card]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
rw : (m * n).primeFactorsList.length = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₁ : (m * n).primeFactorsList.length = HAdd.hAdd (β := ℕ) m.primeFactorsList.length ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₂ : (m * n).primeFactorsList.length = m.primeFactorsList.length + n.primeFactorsList.length
rw₃ : (↑(m * n).primeFactorsList : Multiset ℕ).card = m.primeFactorsList.length + n.primeFactorsList.length
rw₄ : (UniqueFactorizationMonoid.normalizedFactors (m * n)).card = m.primeFactorsList.length + n.primeFactorsList.length
rw₅ :
  (UniqueFactorizationMonoid.normalizedFactors m + UniqueFactorizationMonoid.normalizedFactors n).card =
    m.primeFactorsList.length + n.primeFactorsList.length
rw₆ :
  ((↑m.primeFactorsList : Multiset ℕ) + UniqueFactorizationMonoid.normalizedFactors n).card =
    m.primeFactorsList.length + n.primeFactorsList.length
rw₇ :
  ((↑m.primeFactorsList : Multiset ℕ) + (↑n.primeFactorsList : Multiset ℕ)).card =
    m.primeFactorsList.length + n.primeFactorsList.length
rw₈ :
  (↑m.primeFactorsList : Multiset ℕ).card + (↑n.primeFactorsList : Multiset ℕ).card =
    m.primeFactorsList.length + n.primeFactorsList.length
⊢ (Ω : (a : ℕ) → ℕ) (m * n) = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
have rw₉ : m.primeFactorsList.length + (↑n.primeFactorsList : Multiset ℕ).card =
  m.primeFactorsList.length + n.primeFactorsList.length
Tactic: rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
    UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq,
    Multiset.card_add, Multiset.coe_card, Multiset.coe_card]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
rw : (m * n).primeFactorsList.length = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₁ : (m * n).primeFactorsList.length = HAdd.hAdd (β := ℕ) m.primeFactorsList.length ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₂ : (m * n).primeFactorsList.length = m.primeFactorsList.length + n.primeFactorsList.length
rw₃ : (↑(m * n).primeFactorsList : Multiset ℕ).card = m.primeFactorsList.length + n.primeFactorsList.length
rw₄ : (UniqueFactorizationMonoid.normalizedFactors (m * n)).card = m.primeFactorsList.length + n.primeFactorsList.length
rw₅ :
  (UniqueFactorizationMonoid.normalizedFactors m + UniqueFactorizationMonoid.normalizedFactors n).card =
    m.primeFactorsList.length + n.primeFactorsList.length
rw₆ :
  ((↑m.primeFactorsList : Multiset ℕ) + UniqueFactorizationMonoid.normalizedFactors n).card =
    m.primeFactorsList.length + n.primeFactorsList.length
rw₇ :
  ((↑m.primeFactorsList : Multiset ℕ) + (↑n.primeFactorsList : Multiset ℕ)).card =
    m.primeFactorsList.length + n.primeFactorsList.length
rw₈ :
  (↑m.primeFactorsList : Multiset ℕ).card + (↑n.primeFactorsList : Multiset ℕ).card =
    m.primeFactorsList.length + n.primeFactorsList.length
rw₉ :
  m.primeFactorsList.length + (↑n.primeFactorsList : Multiset ℕ).card =
    m.primeFactorsList.length + n.primeFactorsList.length
⊢ (Ω : (a : ℕ) → ℕ) (m * n) = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
have rw₁₀ : m.primeFactorsList.length + n.primeFactorsList.length = m.primeFactorsList.length + n.primeFactorsList.length
Tactic: rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
    UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq,
    Multiset.card_add, Multiset.coe_card, Multiset.coe_card]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
s : Multiset ℕ
h0 : s.prod ≠ 0
⊢ Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) s.prod : ℕ) (Multiset.sum (Multiset.map (⇑Ω : (a : ℕ) → ℕ) s) : ℕ)
have empty : ∀ (h0 : Ne (α := ℕ) (Multiset.prod 0) 0),
  Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) (Multiset.prod 0) : ℕ) (Multiset.sum (Multiset.map (α := ℕ) (⇑Ω : (a : ℕ) → ℕ) 0) : ℕ)
Tactic: induction s using Multiset.induction_on with
  | empty => simp
  | cons ih => simp_all [cardFactors_mul, not_or]
Cleared hypotheses: s, h0
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
s : Multiset ℕ
h0 : s.prod ≠ 0
empty :
  ∀ (h0 : Ne (α := ℕ) (Multiset.prod 0) 0),
    Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) (Multiset.prod 0) : ℕ)
      (Multiset.sum (Multiset.map (α := ℕ) (⇑Ω : (a : ℕ) → ℕ) 0) : ℕ)
⊢ Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) s.prod : ℕ) (Multiset.sum (Multiset.map (⇑Ω : (a : ℕ) → ℕ) s) : ℕ)
have cons : ∀ (ih : ℕ) (s : Multiset ℕ),
  (∀ (h0 : s.prod ≠ 0),
      Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) s.prod : ℕ) (Multiset.sum (Multiset.map (⇑Ω : (a : ℕ) → ℕ) s) : ℕ)) →
    ∀ (h0 : (ih ::ₘ s).prod ≠ 0),
      Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) (ih ::ₘ s).prod : ℕ)
        (Multiset.sum (Multiset.map (⇑Ω : (a : ℕ) → ℕ) (ih ::ₘ s)) : ℕ)
Tactic: induction s using Multiset.induction_on with
  | empty => simp
  | cons ih => simp_all [cardFactors_mul, not_or]
Cleared hypotheses: s, h0
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m k : ℕ
⊢ (Ω : (a : ℕ) → ℕ) (m ^ k) = HMul.hMul (β := ℕ) k ((Ω : (a : ℕ) → ℕ) m : ℕ)
have pos : ∀ (hm : m = 0), (Ω : (a : ℕ) → ℕ) (m ^ k) = HMul.hMul (β := ℕ) k ((Ω : (a : ℕ) → ℕ) m : ℕ)
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m k : ℕ
pos : ∀ (hm : m = 0), (Ω : (a : ℕ) → ℕ) (m ^ k) = HMul.hMul (β := ℕ) k ((Ω : (a : ℕ) → ℕ) m : ℕ)
⊢ (Ω : (a : ℕ) → ℕ) (m ^ k) = HMul.hMul (β := ℕ) k ((Ω : (a : ℕ) → ℕ) m : ℕ)
have neg : ∀ (hm : ¬m = 0), (Ω : (a : ℕ) → ℕ) (m ^ k) = HMul.hMul (β := ℕ) k ((Ω : (a : ℕ) → ℕ) m : ℕ)
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m k : ℕ
hm : m = 0
⊢ (Ω : (a : ℕ) → ℕ) (m ^ k) = HMul.hMul (β := ℕ) k ((Ω : (a : ℕ) → ℕ) m : ℕ)
have pos : (Ω : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) m 0) = HMul.hMul (α := ℕ) (β := ℕ) (0 : ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ)
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m k : ℕ
hm : m = 0
pos : (Ω : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) m 0) = HMul.hMul (α := ℕ) (β := ℕ) (0 : ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ)
⊢ (Ω : (a : ℕ) → ℕ) (m ^ k) = HMul.hMul (β := ℕ) k ((Ω : (a : ℕ) → ℕ) m : ℕ)
have pos₁ : ∀ (n : ℕ), (Ω : (a : ℕ) → ℕ) (m ^ (n + 1)) = HMul.hMul (β := ℕ) (n + 1) ((Ω : (a : ℕ) → ℕ) m : ℕ)
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m : ℕ
hm : ¬m = 0
n : ℕ
ih : (Ω : (a : ℕ) → ℕ) (m ^ n) = HMul.hMul (β := ℕ) n ((Ω : (a : ℕ) → ℕ) m : ℕ)
⊢ (Ω : (a : ℕ) → ℕ) (m ^ (n + 1)) = HMul.hMul (β := ℕ) (n + 1) ((Ω : (a : ℕ) → ℕ) m : ℕ)
have neg : HAdd.hAdd (β := ℕ) (HMul.hMul (β := ℕ) n ((Ω : (a : ℕ) → ℕ) m : ℕ)) ((Ω : (a : ℕ) → ℕ) m : ℕ) =
  HMul.hMul (β := ℕ) (n + 1) ((Ω : (a : ℕ) → ℕ) m : ℕ)
Tactic: rw [pow_succ, cardFactors_mul (pow_ne_zero n hm) hm, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m k : ℕ
hm : ¬m = 0
⊢ (Ω : (a : ℕ) → ℕ) (m ^ k) = HMul.hMul (β := ℕ) k ((Ω : (a : ℕ) → ℕ) m : ℕ)
have neg : (Ω : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) m 0) = HMul.hMul (α := ℕ) (β := ℕ) (0 : ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ)
Tactic: induction k with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, cardFactors_mul (pow_ne_zero n hm) hm, ih]
    ring
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m k : ℕ
hm : ¬m = 0
neg : (Ω : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) m 0) = HMul.hMul (α := ℕ) (β := ℕ) (0 : ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ)
⊢ (Ω : (a : ℕ) → ℕ) (m ^ k) = HMul.hMul (β := ℕ) k ((Ω : (a : ℕ) → ℕ) m : ℕ)
have neg₁ : ∀ (n : ℕ) (ih : (Ω : (a : ℕ) → ℕ) (m ^ n) = HMul.hMul (β := ℕ) n ((Ω : (a : ℕ) → ℕ) m : ℕ)),
  (Ω : (a : ℕ) → ℕ) (m ^ (n + 1)) = HMul.hMul (β := ℕ) (n + 1) ((Ω : (a : ℕ) → ℕ) m : ℕ)
Tactic: induction k with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, cardFactors_mul (pow_ne_zero n hm) hm, ih]
    ring
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
h0 : n ≠ 0
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) n : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) ↔ Squarefree n
have rw : n.primeFactorsList.dedup.length = (Ω : (a : ℕ) → ℕ) n ↔ n.primeFactorsList.Nodup
Tactic: rw [squarefree_iff_nodup_primeFactorsList h0, cardDistinctFactors_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
h0 : n ≠ 0
⊢ n.primeFactorsList.dedup.length = (Ω : (a : ℕ) → ℕ) n ↔ n.primeFactorsList.Nodup
have mp : n.primeFactorsList.dedup.length = (Ω : (a : ℕ) → ℕ) n → n.primeFactorsList.Nodup
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
h0 : n ≠ 0
mp : n.primeFactorsList.dedup.length = (Ω : (a : ℕ) → ℕ) n → n.primeFactorsList.Nodup
⊢ n.primeFactorsList.dedup.length = (Ω : (a : ℕ) → ℕ) n ↔ n.primeFactorsList.Nodup
have mpr : n.primeFactorsList.Nodup → n.primeFactorsList.dedup.length = (Ω : (a : ℕ) → ℕ) n
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.dedup.length = (Ω : (a : ℕ) → ℕ) n
⊢ n.primeFactorsList.Nodup
have mp : n.primeFactorsList.dedup.Nodup
Tactic: rw [← n.primeFactorsList.dedup_sublist.eq_of_length h]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ IsPrimePow n
have rw : n.primeFactorsList.dedup.length = 1 ↔ IsPrimePow n
Tactic: rw [ArithmeticFunction.cardDistinctFactors_apply, isPrimePow_iff_card_primeFactors_eq_one,
    ← toFinset_factors, List.card_toFinset]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
rw : n.primeFactorsList.dedup.length = 1 ↔ IsPrimePow n
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ IsPrimePow n
have rw₁ : n.primeFactorsList.dedup.length = 1 ↔ #n.primeFactors = 1
Tactic: rw [ArithmeticFunction.cardDistinctFactors_apply, isPrimePow_iff_card_primeFactors_eq_one,
    ← toFinset_factors, List.card_toFinset]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
rw : n.primeFactorsList.dedup.length = 1 ↔ IsPrimePow n
rw₁ : n.primeFactorsList.dedup.length = 1 ↔ #n.primeFactors = 1
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ IsPrimePow n
have rw₂ : n.primeFactorsList.dedup.length = 1 ↔ #n.primeFactorsList.toFinset = 1
Tactic: rw [ArithmeticFunction.cardDistinctFactors_apply, isPrimePow_iff_card_primeFactors_eq_one,
    ← toFinset_factors, List.card_toFinset]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
rw : n.primeFactorsList.dedup.length = 1 ↔ IsPrimePow n
rw₁ : n.primeFactorsList.dedup.length = 1 ↔ #n.primeFactors = 1
rw₂ : n.primeFactorsList.dedup.length = 1 ↔ #n.primeFactorsList.toFinset = 1
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ IsPrimePow n
have rw₃ : n.primeFactorsList.dedup.length = 1 ↔ n.primeFactorsList.dedup.length = 1
Tactic: rw [ArithmeticFunction.cardDistinctFactors_apply, isPrimePow_iff_card_primeFactors_eq_one,
    ← toFinset_factors, List.card_toFinset]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
p : ℕ
hp : Nat.Prime p
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
have rw : Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) p 1) : ℕ) (1 : ℕ)
Tactic: rw [← pow_one p, cardDistinctFactors_apply_prime_pow hp one_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
p : ℕ
hp : Nat.Prime p
rw : Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) p 1) : ℕ) (1 : ℕ)
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [← pow_one p, cardDistinctFactors_apply_prime_pow hp one_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
ι : Type u_2
f : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (h : (↑s : Set ι).Pairwise (Coprime on f)),
    Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (∏ i ∈ s, f i) : ℕ) (∑ i ∈ s, (ω : (a : ℕ) → ℕ) (f i) : ℕ)
h : (↑(cons a s ha) : Set ι).Pairwise (Coprime on f)
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (∏ i ∈ cons a s ha, f i) : ℕ) (∑ i ∈ cons a s ha, (ω : (a : ℕ) → ℕ) (f i) : ℕ)
have cons : (↑s : Set ι).Pairwise (Coprime on f)
Tactic: rw [prod_cons, sum_cons, cardDistinctFactors_mul, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
ι : Type u_2
f : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (h : (↑s : Set ι).Pairwise (Coprime on f)),
    Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (∏ i ∈ s, f i) : ℕ) (∑ i ∈ s, (ω : (a : ℕ) → ℕ) (f i) : ℕ)
h : (↑(Finset.cons a s ha) : Set ι).Pairwise (Coprime on f)
cons : (↑s : Set ι).Pairwise (Coprime on f)
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (∏ i ∈ Finset.cons a s ha, f i) : ℕ)
    (∑ i ∈ Finset.cons a s ha, (ω : (a : ℕ) → ℕ) (f i) : ℕ)
have cons₁ : (f a).Coprime (∏ x ∈ s, f x)
Tactic: rw [prod_cons, sum_cons, cardDistinctFactors_mul, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
ι : Type u_2
s : Finset ι
f : ι → ℕ
h : (↑s : Set ι).Pairwise (Coprime on f)
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (∏ i ∈ s, f i) : ℕ) (∑ i ∈ s, (ω : (a : ℕ) → ℕ) (f i) : ℕ)
have empty : ∀ (h : (↑∅ : Set ι).Pairwise (Coprime on f)),
  Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (∏ i ∈ ∅, f i) : ℕ) (∑ i ∈ ∅, (ω : (a : ℕ) → ℕ) (f i) : ℕ)
Tactic: induction s using cons_induction_on with
  | empty => simp
  | cons a s ha ih =>
    rw [prod_cons, sum_cons, cardDistinctFactors_mul, ih]
    · exact fun x hx y hy hxy => h (by simp [hx]) (by simp [hy]) hxy
    · exact Coprime.prod_right fun i hi =>
        h (by simp) (by simp [hi]) (ne_of_mem_of_not_mem hi ha).symm
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
ι : Type u_2
s : Finset ι
f : ι → ℕ
h : (↑s : Set ι).Pairwise (Coprime on f)
empty :
  ∀ (h : (↑∅ : Set ι).Pairwise (Coprime on f)),
    Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (∏ i ∈ ∅, f i) : ℕ) (∑ i ∈ ∅, (ω : (a : ℕ) → ℕ) (f i) : ℕ)
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (∏ i ∈ s, f i) : ℕ) (∑ i ∈ s, (ω : (a : ℕ) → ℕ) (f i) : ℕ)
have cons : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (ih :
    ∀ (h : (↑s : Set ι).Pairwise (Coprime on f)),
      Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (∏ i ∈ s, f i) : ℕ) (∑ i ∈ s, (ω : (a : ℕ) → ℕ) (f i) : ℕ))
  (h : (↑(cons a s ha) : Set ι).Pairwise (Coprime on f)),
  Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (∏ i ∈ cons a s ha, f i) : ℕ) (∑ i ∈ cons a s ha, (ω : (a : ℕ) → ℕ) (f i) : ℕ)
Tactic: induction s using cons_induction_on with
  | empty => simp
  | cons a s ha ih =>
    rw [prod_cons, sum_cons, cardDistinctFactors_mul, ih]
    · exact fun x hx y hy hxy => h (by simp [hx]) (by simp [hy]) hxy
    · exact Coprime.prod_right fun i hi =>
        h (by simp) (by simp [hi]) (ne_of_mem_of_not_mem hi ha).symm
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
N : ℕ
⊢ ∑ n ∈ Ioc 0 N, (zeta : (a : ℕ) → ℕ) n = N
have simp : #({x ∈ Ioc 0 N | ¬x = 0}) = N
Tactic: simp only [zeta_apply, sum_ite, sum_const_zero, sum_const, smul_eq_mul, mul_one, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
N : ℕ
⊢ {x ∈ Ioc 0 N | ¬x = 0} = Ioc 0 N
have h : ∀ (a : ℕ), a ∈ {x ∈ Ioc 0 N | ¬x = 0} ↔ a ∈ Ioc 0 N
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
N a : ℕ
⊢ a ∈ {x ∈ Ioc 0 N | ¬x = 0} ↔ a ∈ Ioc 0 N
have h : 0 < a → a ≤ N → ¬a = 0
Tactic: simp
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
N : ℕ
⊢ #({x ∈ Ioc 0 N | ¬x = 0}) = N
have rw : #(Ioc 0 N) = N
Tactic: rw [show {x ∈ Ioc 0 N | ¬x = 0} = Ioc 0 N by ext; simp; lia]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ Eq.{u_2 + 1} (α := R) (∑ n ∈ Ioc 0 N, (f * g : (a : ℕ) → R) n)
    (∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 ≤ N,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
have simp : Eq.{u_2 + 1} (α := R)
  (∑ x ∈ Ioc 0 N,
    ∑ x ∈ x.divisorsAntidiagonal, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
  (∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 ≤ N,
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
Tactic: simp only [mul_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ Ioc 0 N,
      ∑ x ∈ x.divisorsAntidiagonal, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
    (∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 ≤ N,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
have trans : Eq.{u_2 + 1} (α := R)
  (∑ x ∈ Ioc 0 N,
    ∑ x ∈ x.divisorsAntidiagonal, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
  (∑ n ∈ Ioc 0 N,
    ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
Tactic: trans ∑ n ∈ Ioc 0 N, ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n, f x.1 * g x.2
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N : ℕ
trans :
  Eq.{u_2 + 1} (α := R)
    (∑ x ∈ Ioc 0 N,
      ∑ x ∈ x.divisorsAntidiagonal, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
    (∑ n ∈ Ioc 0 N,
      ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n,
        HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ Ioc 0 N,
      ∑ x ∈ x.divisorsAntidiagonal, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
    (∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 ≤ N,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
have trans₁ : Eq.{u_2 + 1} (α := R)
  (∑ n ∈ Ioc 0 N,
    ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
  (∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 ≤ N,
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
Tactic: trans ∑ n ∈ Ioc 0 N, ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n, f x.1 * g x.2
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ Ioc 0 N,
      ∑ x ∈ x.divisorsAntidiagonal, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
    (∑ n ∈ Ioc 0 N,
      ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n,
        HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
have refine : ∀ (n : ℕ) (hn : n ∈ Ioc 0 N),
  Eq.{u_2 + 1} (α := R)
    (∑ x ∈ n.divisorsAntidiagonal, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
    (∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
Tactic: refine sum_congr rfl fun n hn ↦ ?_