awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
⊢ Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ Nat.Prime n

Tactic:
⟨fun h => ?_, fun h => List.length_eq_one_iff.2 ⟨n, primeFactorsList_prime h⟩⟩

Premises used: Iff.mpr, Nat.primeFactorsList_prime, List.length_eq_one_iff, Iff.intro, Exists.intro
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
refine : ∀ (h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)), Nat.Prime n
⊢ Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ Nat.Prime n

Tactic:
refine ⟨fun h => ?_, fun h => List.length_eq_one_iff.2 ⟨n, primeFactorsList_prime h⟩⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)
⊢ Nat.Prime 0

Tactic:
simp at h
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) (n + 1) : ℕ) (1 : ℕ)
succ : ∀ (x : ℕ) (hx : (n + 1).primeFactorsList = [x]), Nat.Prime (n + 1)
⊢ Nat.Prime (n + 1)

Tactic:
rcases List.length_eq_one_iff.1 h with ⟨x, hx⟩

Premises used: List.length_eq_one_iff, Iff.mp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) (n + 1) : ℕ) (1 : ℕ)
x : ℕ
hx : (n + 1).primeFactorsList = [x]
succ : Nat.Prime x
⊢ Nat.Prime (n + 1)

Tactic:
rw [← prod_primeFactorsList n.add_one_ne_zero, hx, List.prod_singleton]

Premises used: Nat.add_one_ne_zero, List.prod_singleton, Nat.prod_primeFactorsList
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) (n + 1) : ℕ) (1 : ℕ)
x : ℕ
hx : (n + 1).primeFactorsList = [x]
succ : x ∈ (n + 1).primeFactorsList
succ₁ : ℕ
⊢ Nat.Prime x

Tactic:
apply prime_of_mem_primeFactorsList

Premises used: Nat.prime_of_mem_primeFactorsList
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)
zero : ∀ (h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)), Nat.Prime 0
succ : ∀ (n : ℕ) (h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) (n + 1) : ℕ) (1 : ℕ)), Nat.Prime (n + 1)
⊢ Nat.Prime n

Tactic:
cases n with | zero => simp at h | succ n =>
  rcases List.length_eq_one_iff.1 h with ⟨x, hx⟩
  rw [← prod_primeFactorsList n.add_one_ne_zero, hx, List.prod_singleton]
  apply prime_of_mem_primeFactorsList
  rw [hx, List.mem_singleton]

Premises used: ArithmeticFunction.zero, Nat.prime_of_mem_primeFactorsList, Nat.add_one_ne_zero, List.mem_singleton, List.length_eq_one_iff, List.prod_singleton, Iff.mp, Nat.succ, Nat.prod_primeFactorsList
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
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
rw₁₀ rw₁₁ :
  m.primeFactorsList.length + n.primeFactorsList.length = m.primeFactorsList.length + n.primeFactorsList.length
⊢ (Ω : (a : ℕ) → ℕ) (m * n) = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)

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]

Premises used: ArithmeticFunction.cardFactors_apply, Multiset.card_add, UniqueFactorizationMonoid.normalizedFactors_mul, Nat.factors_eq, Multiset.coe_card
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
h0 : Ne (α := ℕ) (Multiset.prod 0) 0
⊢ Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) (Multiset.prod 0) : ℕ) (Multiset.sum (Multiset.map (α := ℕ) (⇑Ω : (a : ℕ) → ℕ) 0) : ℕ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
ih : ℕ
s : Multiset ℕ
h :
  ∀ (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:
simp_all [cardFactors_mul, not_or]

Premises used: not_or, ArithmeticFunction.cardFactors_mul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
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) : ℕ)
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)) : ℕ)
⊢ Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) s.prod : ℕ) (Multiset.sum (Multiset.map (⇑Ω : (a : ℕ) → ℕ) s) : ℕ)

Tactic:
induction s using Multiset.induction_on with
  | empty => simp
  | cons ih => simp_all [cardFactors_mul, not_or]

Premises used: Finset.cons, not_or, ArithmeticFunction.cardFactors_mul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
p : ℕ
hp : Nat.Prime p
⊢ Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
cardFactors_eq_one_iff_prime.2 hp

Premises used: Iff.mpr, ArithmeticFunction.cardFactors_eq_one_iff_prime
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
m k : ℕ
pos : ∀ (hm : m = 0), (Ω : (a : ℕ) → ℕ) (m ^ k) = HMul.hMul (β := ℕ) k ((Ω : (a : ℕ) → ℕ) m : ℕ)
neg : ∀ (hm : ¬m = 0), (Ω : (a : ℕ) → ℕ) (m ^ k) = HMul.hMul (β := ℕ) k ((Ω : (a : ℕ) → ℕ) m : ℕ)
⊢ (Ω : (a : ℕ) → ℕ) (m ^ k) = HMul.hMul (β := ℕ) k ((Ω : (a : ℕ) → ℕ) m : ℕ)

Tactic:
by_cases hm : m = 0
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
m k : ℕ
hm : m = 0
pos : (Ω : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) m 0) = HMul.hMul (α := ℕ) (β := ℕ) (0 : ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ)
pos₁ : ∀ (n : ℕ), (Ω : (a : ℕ) → ℕ) (m ^ (n + 1)) = HMul.hMul (β := ℕ) (n + 1) ((Ω : (a : ℕ) → ℕ) m : ℕ)
⊢ (Ω : (a : ℕ) → ℕ) (m ^ k) = HMul.hMul (β := ℕ) k ((Ω : (a : ℕ) → ℕ) m : ℕ)

Tactic:
cases k
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
m : ℕ
hm : m = 0
⊢ (Ω : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) m 0) = HMul.hMul (α := ℕ) (β := ℕ) (0 : ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ)

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
m : ℕ
hm : m = 0
n : ℕ
⊢ (Ω : (a : ℕ) → ℕ) (m ^ (n + 1)) = HMul.hMul (β := ℕ) (n + 1) ((Ω : (a : ℕ) → ℕ) m : ℕ)

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
m : ℕ
hm : ¬m = 0
⊢ (Ω : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) m 0) = HMul.hMul (α := ℕ) (β := ℕ) (0 : ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
m : ℕ
hm : ¬m = 0
n : ℕ
ih : (Ω : (a : ℕ) → ℕ) (m ^ n) = HMul.hMul (β := ℕ) n ((Ω : (a : ℕ) → ℕ) m : ℕ)
neg :
  HAdd.hAdd (β := ℕ) (HMul.hMul (β := ℕ) n ((Ω : (a : ℕ) → ℕ) m : ℕ)) ((Ω : (a : ℕ) → ℕ) m : ℕ) =
    HMul.hMul (β := ℕ) (n + 1) ((Ω : (a : ℕ) → ℕ) m : ℕ)
⊢ (Ω : (a : ℕ) → ℕ) (m ^ (n + 1)) = HMul.hMul (β := ℕ) (n + 1) ((Ω : (a : ℕ) → ℕ) m : ℕ)

Tactic:
rw [pow_succ, cardFactors_mul (pow_ne_zero n hm) hm, ih]

Premises used: pow_succ, pow_ne_zero, ArithmeticFunction.cardFactors_mul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
m : ℕ
hm : ¬m = 0
n : ℕ
ih : (Ω : (a : ℕ) → ℕ) (m ^ n) = HMul.hMul (β := ℕ) n ((Ω : (a : ℕ) → ℕ) m : ℕ)
⊢ HAdd.hAdd (β := ℕ) (HMul.hMul (β := ℕ) n ((Ω : (a : ℕ) → ℕ) m : ℕ)) ((Ω : (a : ℕ) → ℕ) m : ℕ) =
    HMul.hMul (β := ℕ) (n + 1) ((Ω : (a : ℕ) → ℕ) m : ℕ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
m k : ℕ
hm : ¬m = 0
neg : (Ω : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) m 0) = HMul.hMul (α := ℕ) (β := ℕ) (0 : ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ)
neg₁ :
  ∀ (n : ℕ) (ih : (Ω : (a : ℕ) → ℕ) (m ^ n) = HMul.hMul (β := ℕ) n ((Ω : (a : ℕ) → ℕ) m : ℕ)),
    (Ω : (a : ℕ) → ℕ) (m ^ (n + 1)) = HMul.hMul (β := ℕ) (n + 1) ((Ω : (a : ℕ) → ℕ) m : ℕ)
⊢ (Ω : (a : ℕ) → ℕ) (m ^ k) = HMul.hMul (β := ℕ) k ((Ω : (a : ℕ) → ℕ) m : ℕ)

Tactic:
induction k with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, cardFactors_mul (pow_ne_zero n hm) hm, ih]
    ring

Premises used: ArithmeticFunction.zero, pow_succ, Nat.succ
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
p k : ℕ
hp : Nat.Prime p
⊢ (Ω : (a : ℕ) → ℕ) (p ^ k) = k

Tactic:
simp [cardFactors_pow, hp]

Premises used: ArithmeticFunction.cardFactors_pow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
⊢ Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) (n.factorization.sum fun (x k : ℕ) ↦ k : ℕ)

Tactic:
simp [cardFactors_apply, ← List.sum_toFinset_count_eq_length, Finsupp.sum]

Premises used: List.sum_toFinset_count_eq_length, ArithmeticFunction.cardFactors_apply, Finsupp.sum
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_1
⊢ Eq (α := ℕ) ((fun (n : ℕ) ↦ n.primeFactorsList.dedup.length) 0) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) 1 : ℕ) (0 : ℕ)

Tactic:
simp [cardDistinctFactors]

Premises used: ArithmeticFunction.cardDistinctFactors
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
⊢ (ω : (a : ℕ) → ℕ) n = n.primeFactorsList.dedup.length

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) n : ℕ) (0 : ℕ) ↔ n ≤ 1

Tactic:
simp [cardDistinctFactors_apply, le_one_iff_eq_zero_or_eq_one]

Premises used: Nat.le_one_iff_eq_zero_or_eq_one, ArithmeticFunction.cardDistinctFactors_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
⊢ LT.lt (α := ℕ) (0 : ℕ) ((ω : (a : ℕ) → ℕ) n : ℕ) ↔ 1 < n

Tactic:
simp [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
h0 : n ≠ 0
rw : n.primeFactorsList.dedup.length = (Ω : (a : ℕ) → ℕ) n ↔ n.primeFactorsList.Nodup
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) n : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) ↔ Squarefree n

Tactic:
rw [squarefree_iff_nodup_primeFactorsList h0, cardDistinctFactors_apply]

Premises used: ArithmeticFunction.cardDistinctFactors_apply, Nat.squarefree_iff_nodup_primeFactorsList
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
h0 : n ≠ 0
mp : n.primeFactorsList.dedup.length = (Ω : (a : ℕ) → ℕ) n → n.primeFactorsList.Nodup
mpr : n.primeFactorsList.Nodup → n.primeFactorsList.dedup.length = (Ω : (a : ℕ) → ℕ) n
⊢ n.primeFactorsList.dedup.length = (Ω : (a : ℕ) → ℕ) n ↔ n.primeFactorsList.Nodup

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.dedup.length = (Ω : (a : ℕ) → ℕ) n
mp : n.primeFactorsList.dedup.Nodup
⊢ n.primeFactorsList.Nodup

Tactic:
rw [← n.primeFactorsList.dedup_sublist.eq_of_length h]

Premises used: List.Sublist.eq_of_length, List.dedup_sublist, Nat.primeFactorsList
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.dedup.length = (Ω : (a : ℕ) → ℕ) n
⊢ n.primeFactorsList.dedup.Nodup

Tactic:
apply List.nodup_dedup

Premises used: List.nodup_dedup
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.Nodup
⊢ n.primeFactorsList.dedup.length = (Ω : (a : ℕ) → ℕ) n

Tactic:
simp [h.dedup, cardFactors]

Premises used: ArithmeticFunction.cardFactors, List.Nodup.dedup
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
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
rw₃ rw₄ : n.primeFactorsList.dedup.length = 1 ↔ n.primeFactorsList.dedup.length = 1
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ IsPrimePow n

Tactic:
rw [ArithmeticFunction.cardDistinctFactors_apply, isPrimePow_iff_card_primeFactors_eq_one,
    ← toFinset_factors, List.card_toFinset]

Premises used: ArithmeticFunction.cardDistinctFactors_apply, isPrimePow_iff_card_primeFactors_eq_one, List.card_toFinset, Nat.toFinset_factors
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (p ^ k) : ℕ) (1 : ℕ)

Tactic:
cardDistinctFactors_eq_one_iff.mpr <| hp.isPrimePow.pow hk

Premises used: Iff.mpr, ArithmeticFunction.cardDistinctFactors_eq_one_iff, Nat.Prime.isPrimePow, IsPrimePow.pow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
p : ℕ
hp : Nat.Prime p
rw : Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) p 1) : ℕ) (1 : ℕ)
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
rw [← pow_one p, cardDistinctFactors_apply_prime_pow hp one_ne_zero]

Premises used: ArithmeticFunction.cardDistinctFactors_apply_prime_pow, pow_one, one_ne_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
m n : ℕ
h : m.Coprime n
⊢ (ω : (a : ℕ) → ℕ) (m * n) = HAdd.hAdd (α := ℕ) (β := ℕ) ((ω : (a : ℕ) → ℕ) m : ℕ) ((ω : (a : ℕ) → ℕ) n : ℕ)

Tactic:
simp [cardDistinctFactors_apply, perm_primeFactorsList_mul_of_coprime h |>.dedup |>.length_eq,
    coprime_primeFactorsList_disjoint h |>.dedup_append]

Premises used: Nat.perm_primeFactorsList_mul_of_coprime, List.Disjoint.dedup_append, ArithmeticFunction.cardDistinctFactors_apply, List.Perm.dedup, List.Perm.length_eq, Nat.coprime_primeFactorsList_disjoint
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
ι : Type u_2
f : ι → ℕ
h : (↑∅ : Set ι).Pairwise (Coprime on f)
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (∏ i ∈ ∅, f i) : ℕ) (∑ i ∈ ∅, (ω : (a : ℕ) → ℕ) (f i) : ℕ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
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)
cons₁ : (f a).Coprime (∏ x ∈ s, f x)
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (∏ i ∈ Finset.cons a s ha, f i) : ℕ)
    (∑ i ∈ Finset.cons a s ha, (ω : (a : ℕ) → ℕ) (f i) : ℕ)

Tactic:
rw [prod_cons, sum_cons, cardDistinctFactors_mul, ih]

Premises used: Finset.sum_cons, ArithmeticFunction.cardDistinctFactors_mul, Finset.prod_cons
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
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)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hxy : x ≠ y
⊢ x ∈ (↑(cons a s ha) : Set ι)

Tactic:
simp [hx]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
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)
x : ι
hx : x ∈ (↑s : Set ι)
y : ι
hy : y ∈ (↑s : Set ι)
hxy : x ≠ y
⊢ y ∈ (↑(cons a s ha) : Set ι)

Tactic:
simp [hy]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
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)
⊢ (↑s : Set ι).Pairwise (Coprime on f)

Tactic:
exact fun x hx y hy hxy => h (by simp [hx]) (by simp [hy]) hxy
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
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)
i : ι
hi : i ∈ s
⊢ a ∈ (↑(cons a s ha) : Set ι)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
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)
i : ι
hi : i ∈ s
⊢ i ∈ (↑(cons a s ha) : Set ι)

Tactic:
simp [hi]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
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)
⊢ (f a).Coprime (∏ x ∈ s, f x)

Tactic:
exact Coprime.prod_right fun i hi =>
        h (by simp) (by simp [hi]) (ne_of_mem_of_not_mem hi ha).symm

Premises used: Ne.symm, ne_of_mem_of_not_mem, Nat.Coprime.prod_right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
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) : ℕ)
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 : (↑(Finset.cons a s ha) : Set ι).Pairwise (Coprime on f)),
    Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (∏ i ∈ Finset.cons a s ha, f i) : ℕ)
      (∑ i ∈ Finset.cons a s ha, (ω : (a : ℕ) → ℕ) (f i) : ℕ)
⊢ Eq (α := ℕ) ((ω : (a : ℕ) → ℕ) (∏ i ∈ s, f i) : ℕ) (∑ i ∈ s, (ω : (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

Premises used: Finset.sum_cons, Finset.cons, ArithmeticFunction.cardDistinctFactors_mul, Finset.prod_cons
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
N : ℕ
simp : #({x ∈ Ioc 0 N | ¬x = 0}) = N
⊢ ∑ n ∈ Ioc 0 N, (zeta : (a : ℕ) → ℕ) n = N

Tactic:
simp only [zeta_apply, sum_ite, sum_const_zero, sum_const, smul_eq_mul, mul_one, zero_add]

Premises used: ArithmeticFunction.zeta_apply, zero_add, Finset.sum_const_zero, smul_eq_mul, mul_one, Finset.sum_ite, Finset.sum_const
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
N : ℕ
h : ∀ (a : ℕ), a ∈ {x ∈ Ioc 0 N | ¬x = 0} ↔ a ∈ Ioc 0 N
⊢ {x ∈ Ioc 0 N | ¬x = 0} = Ioc 0 N

Tactic:
ext
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
N a : ℕ
h : 0 < a → a ≤ N → ¬a = 0
⊢ a ∈ {x ∈ Ioc 0 N | ¬x = 0} ↔ a ∈ Ioc 0 N

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
N a : ℕ
⊢ 0 < a → a ≤ N → ¬a = 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
N : ℕ
rw : #(Ioc 0 N) = N
⊢ #({x ∈ Ioc 0 N | ¬x = 0}) = N

Tactic:
rw [show {x ∈ Ioc 0 N | ¬x = 0} = Ioc 0 N by ext; simp; lia]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
N : ℕ
⊢ #(Ioc 0 N) = N

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N : ℕ
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))
⊢ 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))

Tactic:
simp only [mul_apply]

Premises used: ArithmeticFunction.mul_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
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))
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))
⊢ 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:
trans ∑ n ∈ Ioc 0 N, ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n, f x.1 * g x.2

Premises used: OfNat.ofNat, Finset.Ioc
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
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))

Tactic:
sum_congr rfl fun n hn ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N : ℕ
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))
⊢ 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:
refine sum_congr rfl fun n hn ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
⊢ 0 < n ∧ n ≤ N

Tactic:
simp only [mem_Ioc] at hn

Premises used: Finset.mem_Ioc