mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
⊢ (f.ppow k).IsMultiplicative

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
⊢ f * g = g * f

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid S
inst✝ : Module R S
x : R
f : ArithmeticFunction S
⊢ (x • ⇑f) 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid S
inst✝ : Module R S
x : R
f : ArithmeticFunction S
n : ℕ
⊢ (x • f) n = x • f n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : R
f g : ArithmeticFunction S
n : ℕ
⊢ (x • f * g) n = (x • (f * g)) n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : R
f g : ArithmeticFunction S
n : ℕ
⊢ (f * x • g) n = (x • (f * g)) n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : R
⊢ ((algebraMap R (ArithmeticFunction S)) x) 1 = (algebraMap R S) x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : ArithmeticFunction R
⊢ r • 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
hn : IsPrimePow n
⊢ n.minFac ^ n.factorization n.minFac = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
h : n.minFac ^ n.factorization n.minFac = n
hn : n ≠ 1
⊢ IsPrimePow n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : p ^ k = n
⊢ n.factorization = Finsupp.single p k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case mpr
n p k : ℕ
⊢ 0 < k ∧ n.factorization = Finsupp.single p k → Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rintro ⟨hk, hn⟩

Goal state after:
case mpr
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
⊢ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : ArithmeticFunction R
x y : ArithmeticFunction M
⊢ r • (x + y) = r • x + r • y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
hn0 : n ≠ 0
⊢ n.factorization p ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : ArithmeticFunction R
x : ArithmeticFunction M
⊢ (r + s) • x = r • x + s • x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ p k, 0 < k ∧ n.factorization = Finsupp.single p k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : ArithmeticFunction M
⊢ 0 • r = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ n.primeFactors.card = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
⊢ dirichletInverseFun f hf 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
⊢ ¬IsPrimePow n ↔ n.primeFactors.Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
⊢ dirichletInverseFun f hf 1 = ⅟(f 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
⊢ 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ coeff (m.degree f ⊔ m.degree g) (m.sPolynomial f g) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
h : IsPrimePow n
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ dirichletInverseFun f hf n = -⅟(f 1) * ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h₁ : m.degree f = 0
h₂ : m.degree g = 0
this : C (m.leadingCoeff g) * f - C (m.leadingCoeff f) * g = 0
⊢ m.sPolynomial f g = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n p : ℕ
hn : p ^ n.factorization p ≠ 1
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ p ^ n.factorization p = p ^ n.factorization p

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
hn : n ≠ 1
⊢ IsPrimePow n ↔ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h : 0 < n
⊢ ∃ a b, (b + 1) ^ 2 * (a + 1) = n ∧ Squarefree (a + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: ⊢ 0 ^ 2 * 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
⊢ ∃ a b, b ^ 2 * a = n ∧ Squarefree a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ Squarefree (m * n) ↔ Squarefree m ∧ Squarefree n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: m n : ℕ
⊢ Squarefree (m * n) ↔ m.Coprime n ∧ Squarefree m ∧ Squarefree n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: m n : ℕ
hm : Squarefree m
hn : n ≠ 0
⊢ Squarefree (m / m.gcd n * m.gcd n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: m n : ℕ
hm : Squarefree m
hn : n ≠ 0
⊢ (m / m.gcd n).Coprime n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
⊢ f * dirichletInverse (⇑f) hf = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, p = n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : Invertible (f 1)
⊢ dirichletInverse (⇑f) hf * f = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: s : Finset ℕ
hs : ∀ p ∈ s, Prime p
⊢ (∏ p ∈ s, p).primeFactors = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃! p, Nat.Prime p ∧ p ∣ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n k : ℕ
hk : k ≠ 0
⊢ IsPrimePow (n ^ k) ↔ IsPrimePow n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
this : Invertible (f 1) → Invertible f
⊢ IsUnit (f 1) → IsUnit f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n k : ℕ
hk : k ≠ 0
⊢ ∏ p ∈ n.primeFactors, p ∣ k ↔ n.primeFactors ⊆ k.primeFactors

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
⊢ m / m.gcd n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
⊢ IsUnit f ↔ IsUnit (f 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: m n : ℕ
hm : Squarefree m
hn : n ≠ 0
⊢ (m / m.gcd n).primeFactors = m.primeFactors \ n.primeFactors

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
⊢ ∏ a ∈ n.primeFactors \ t, a = n / ∏ a ∈ t, a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f ⊔ m.degree g) ∨ m.sPolynomial f g = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.degree f = m.degree g
hs : m.sPolynomial f g ≠ 0
⊢ m.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
⊢ (ArithmeticFunction.prodPrimeFactors f).IsMultiplicative

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ a.factorization p = 0 ∨ b.factorization p = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)
  · simp
  rcases eq_or_ne b 0 with (rfl | hb)
  · simp
  refine
    ⟨?_, fun h =>
      Or.elim h (fun i => i.trans ((@dvd_mul_right a b a hab).mpr (dvd_refl a)))
          fun i => i.trans ((@dvd_mul_left a b b hab.symm).mpr (dvd_refl b))⟩
  obtain ⟨p, k, hp, _, rfl⟩ := (isPrimePow_nat_iff _).1 hn
  simp only [hp.pow_dvd_iff_le_factorization (mul_ne_zero ha hb), Nat.factorization_mul ha hb,
    hp.pow_dvd_iff_le_factorization ha, hp.pow_dvd_iff_le_factorization hb, Pi.add_apply,
    Finsupp.coe_add]
  have : a.factorization p = 0 ∨ b.factorization p = 0 := by
    rw [← Finsupp.notMem_support_iff, ← Finsupp.notMem_support_iff, ← not_and_or, ←
      Finset.mem_inter]
    intro t
    simpa using hab.disjoint_primeFactors.le_bot t
  rcases this with h | h <;> simp [h, imp_or]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
s : Finset ι
hs : (↑s).Pairwise (Coprime on g)
⊢ f (∏ i ∈ s, g i) = ∏ i ∈ s, f (g i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
⊢ {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
l : ℕ
hl : Squarefree l
⊢ ∏ a ∈ l.primeFactors, f a = f l

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ (ArithmeticFunction.prodPrimeFactors fun p ↦ (f + g) p) n = (f * g) n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: x✝ : Primes × ℕ
p : Primes
k : ℕ
⊢ (fun n ↦ (⟨(↑n).minFac, ⋯⟩, (↑n).factorization (↑n).minFac - 1)) ((fun pk ↦ ⟨↑pk.1 ^ (pk.2 + 1), ⋯⟩) (p, k)) = (p, k)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k n : ℕ
⊢ (pow k) n = if k = 0 ∧ n = 0 then 0 else n ^ k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: ⊢ pow 0 = ζ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: ⊢ pow 1 = ArithmeticFunction.id

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : GroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : (l / d).Coprime d
hd : f d ≠ 0
⊢ f (l / d) = f l / f d

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_1
k : ℕ
⊢ ∑ d ∈ divisors 0, d ^ k = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
f : ArithmeticFunction ℕ
inst✝ : Semiring R
h : f.IsMultiplicative
⊢ ↑f 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : { n // IsPrimePow n }
⊢ (fun pk ↦ ⟨↑pk.1 ^ (pk.2 + 1), ⋯⟩) ((fun n ↦ (⟨(↑n).minFac, ⋯⟩, (↑n).factorization (↑n).minFac - 1)) n) = n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k n : ℕ
⊢ (σ k) n = 0 ↔ n = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
f : ArithmeticFunction ℕ
inst✝ : Semiring R
h : f.IsMultiplicative
m✝ n✝ : ℕ
cop : m✝.Coprime n✝
⊢ ↑f (m✝ * n✝) = ↑f m✝ * ↑f n✝

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k n : ℕ
⊢ 0 < (σ k) n ↔ 0 < n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: p : Primes
k : ℕ
⊢ prodNatEquiv (p, k) = ⟨↑p ^ (k + 1), ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k p i : ℕ
hp : Nat.Prime p
⊢ (σ k) (p ^ i) = ∑ j ∈ range (i + 1), p ^ (j * k)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ (σ 1) n = ∑ d ∈ n.divisors, d

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
f : ArithmeticFunction ℤ
inst✝ : Ring R
h : f.IsMultiplicative
⊢ ↑f 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: p i : ℕ
hp : Nat.Prime p
⊢ (σ 1) (p ^ i) = ∑ k ∈ range (i + 1), p ^ k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
f : ArithmeticFunction ℤ
inst✝ : Ring R
h : f.IsMultiplicative
m✝ n✝ : ℕ
cop : m✝.Coprime n✝
⊢ ↑f (m✝ * n✝) = ↑f m✝ * ↑f n✝

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k n : ℕ
⊢ (σ k) n = ∑ d ∈ n.divisors, (n / d) ^ k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ (σ 0) n = #n.divisors

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
⊢ (f * g) 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: p i : ℕ
hp : Nat.Prime p
⊢ (σ 0) (p ^ i) = i + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k : ℕ
⊢ (σ k) 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: p a m n : ℕ
hp : Prime p
h : p ^ m = a ^ n
⊢ m = n * a.factorization p

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k n : ℕ
hn0 : n ≠ 0
⊢ 0 < (σ k) n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k k' n : ℕ
hk : k ≤ k'
⊢ (σ k) n ≤ (σ k') n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k : ℕ
⊢ ζ * pow k = σ k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k : ℕ
⊢ (σ k).IsMultiplicative

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: p a m n : ℕ
hp : Prime p
hn : n ≠ 0
h : p ^ m = a ^ n
⊢ ∃ k, a = p ^ k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k n : ℕ
hn : n ≠ 0
⊢ (σ k) n = ∏ p ∈ n.primeFactors, ∑ i ∈ range (n.factorization p + 1), p ^ (i * k)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k n : ℕ
⊢ (σ k) n ≤ n ^ (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: divisorsAntidiagonal : ℕ+ → Finset (ℕ+ × ℕ+) :=
  fun n ↦ map { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩), inj' := ⋯ } (↑n).divisorsAntidiagonal.attach
n : ℕ+
x : ℕ+ × ℕ+
⊢ x ∈ divisorsAntidiagonal n ↔ x.1 * x.2 = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: divisorsAntidiagonal : ℕ+ → Finset (ℕ+ × ℕ+) :=
  fun n ↦ map { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩), inj' := ⋯ } (↑n).divisorsAntidiagonal.attach
mem_divisorsAntidiagonal : ∀ {n : ℕ+} (x : ℕ+ × ℕ+), x ∈ divisorsAntidiagonal n ↔ x.1 * x.2 = n
⊢ ∀ {n : Additive ℕ+} {a : Additive ℕ+ × Additive ℕ+},
    a ∈ map (Additive.ofMul.toEmbedding.prodMap Additive.ofMul.toEmbedding) (divisorsAntidiagonal (Additive.toMul n)) ↔
      a.1 + a.2 = n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ #n.divisors = ∏ x ∈ n.primeFactors, (n.factorization x + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
hn : n ≠ 0
h : n = 1
⊢ #n.divisors = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ #n.divisors = 1 ↔ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ (σ 0) n = 1 ↔ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k n : ℕ
⊢ (σ k) n = 1 ↔ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ∑ d ∈ n.divisors, d = ∏ p ∈ n.primeFactors, ∑ k ∈ range (n.factorization p + 1), p ^ k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_1
⊢ (primeFactorsList 0).length = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: ⊢ Ω 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: ⊢ Ω 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ Ω n = 0 ↔ n = 0 ∨ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ 0 < Ω n ↔ 1 < n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ Ω n = 1 ↔ Nat.Prime n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ f ∈
      map (Additive.toMul.toEmbedding.trans { toFun := PNat.val, inj' := PNat.coe_injective }).arrowCongrRight
        (finAntidiagonal d (Additive.ofMul ⟨n, h⟩)) ↔
    ∏ i, f i = n ∧ n ≠ 0

Tactic:
simp_rw [mem_map, mem_finAntidiagonal, Function.Embedding.arrowCongrRight_apply,
      Function.comp_def, Function.Embedding.trans_apply, Equiv.coe_toEmbedding,
      Function.Embedding.coeFn_mk, ← Additive.ofMul.symm_apply_eq, Additive.ofMul_symm_eq,
      toMul_sum, (Equiv.piCongrRight fun _ => Additive.ofMul).surjective.exists,
      Equiv.piCongrRight_apply, Pi.map_apply, toMul_ofMul, ← PNat.coe_inj, PNat.mk_coe,
      PNat.coe_prod]
    constructor
    · rintro ⟨a, ha_mem, rfl⟩
      exact ⟨ha_mem, h.ne.symm⟩
    · rintro ⟨rfl, _⟩
      refine ⟨fun i ↦ ⟨f i, ?_⟩, rfl, funext fun _ => rfl⟩
      apply Nat.pos_of_ne_zero
      exact Finset.prod_ne_zero_iff.mp h.ne.symm _ (mem_univ _)

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ Ω (m * n) = Ω m + Ω n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: s : Multiset ℕ
h0 : s.prod ≠ 0
⊢ Ω s.prod = (Multiset.map (⇑Ω) s).sum

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n : ℕ
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag n ↔ ∏ i, f i = n ∧ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d : ℕ
⊢ d.finMulAntidiag 1 = {fun x ↦ 1}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: m k : ℕ
⊢ Ω (m ^ k) = k * Ω m

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: p k : ℕ
hp : Nat.Prime p
⊢ Ω (p ^ k) = k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ Ω n = n.factorization.sum fun x k ↦ k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
hn : n ≠ 1
⊢ finMulAntidiag 0 n = ∅

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_1
⊢ (primeFactorsList 0).dedup.length = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: ⊢ ω 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: ⊢ ω 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ ω n = 0 ↔ n ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ 0 < ω n ↔ 1 < n

Tactic:
by

Goal state after: