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

Goal state before:
pp: case empty
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
α : Type u_3
f : α → MvPolynomial σ R
⊢ m.toSyn (m.degree (∑ x ∈ ∅, f x)) ≤ ∅.sup fun x ↦ m.toSyn (m.degree (f x))

Tactic:
simp

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

Goal state before:
pp: case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : ¬m.toSyn (m.degree f) ≤ m.toSyn (m.degree g)
hf : f = 0
⊢ False

Tactic:
hf

Goal state after:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : ¬m.toSyn (m.degree 0) ≤ m.toSyn (m.degree g)
hf : f = 0
⊢ False
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: α : Type u_1
n✝ n k : ℕ
s : { s // 0 ∈ s }
⊢ (fun s ↦ ⟨0 ::ₛ s, ⋯⟩) ((fun s ↦ (↑s).erase 0 ⋯) s) = s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: α : Type u_1
n✝ n k : ℕ
s : Sym (Fin n.succ) k
⊢ (fun s ↦ (↑s).erase 0 ⋯) ((fun s ↦ ⟨0 ::ₛ s, ⋯⟩) s) = s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: n : ℕ
⊢ Fintype.card (Sym (Fin n) 0) = n.multichoose 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = multichoose 0 (k + 1)

Tactic:
by rw [multichoose_zero_succ]; exact card_eq_zero

Goal state after:
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: k : ℕ
⊢ Fintype.card (Sym (Fin 1) (k + 1)) = multichoose 1 (k + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring L
this : ∀ (a b c : L), associator a b c = 0
⊢ ∀ (x y z : L),
    associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring L
⊢ ∀ (a b c : L), associator a b c = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring L
inst✝ : Algebra R L
⊢ ∀ (m : R) (n a : L), m • n • a = n • m • a

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : { P // (P.sum fun x ↦ id) = n }
⊢ (fun f ↦ ⟨subtypeDomain (fun x ↦ x ∈ s) ↑f, ⋯⟩) ((fun f ↦ ⟨(↑f).extendDomain, ⋯⟩) f) = f

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: case succ.zero
a : ℕ
h : DvdNotUnit (a + 1) 0
⊢ (if a + 1 = 0 then ⊤ else ↑(a + 1)) < if 0 = 0 then ⊤ else ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: case succ.succ
a n✝ : ℕ
h : DvdNotUnit (a + 1) (n✝ + 1)
h1 : a + 1 ∣ n✝ + 1
h2 : ¬n✝ + 1 ∣ a + 1
con : a + 1 = n✝ + 1
⊢ n✝ + 1 ∣ a + 1

Tactic:
con

Goal state after:
case succ.succ
a n✝ : ℕ
h : DvdNotUnit (a + 1) (n✝ + 1)
h1 : a + 1 ∣ n✝ + 1
h2 : ¬n✝ + 1 ∣ a + 1
con : a + 1 = n✝ + 1
⊢ n✝ + 1 ∣ n✝ + 1
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: ⊢ normalizedFactors 0 = ↑(primeFactorsList 0)

Tactic:
simp

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

Goal state before:
pp: case h₁
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
⊢ (a, b) ∉ Finset.antidiagonal (a + b) → coeff (a, b).1 f * coeff (a, b).2 g = 0

Tactic:
simp

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

Goal state before:
pp: case zero
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ coeff (0 • m.degree f) (f ^ 0) = m.leadingCoeff f ^ 0

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (C r) + m.degree f) = m.toSyn (m.degree f)

Tactic:
simp

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

Goal state before:
pp: case empty
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
⊢ coeff (∑ i ∈ ∅, m.degree (P i)) (∏ i ∈ ∅, P i) = ∏ i ∈ ∅, m.leadingCoeff (P i)

Tactic:
simp

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

Goal state before:
pp: case inr.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
    (p q : MvPolynomial σ R), p ≠ 0 ∧ q ≠ 0 → m.degree (m.leadingTerm p * q) = m.degree (p * q)
⊢ m.degree (m.leadingTerm 0 * q) = m.degree (0 * q)

Tactic:
simp

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

Goal state before:
pp: case inr.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
    (p q : MvPolynomial σ R), p ≠ 0 ∧ q ≠ 0 → m.degree (m.leadingTerm p * q) = m.degree (p * q)
⊢ m.degree (m.leadingTerm p * 0) = m.degree (p * 0)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
⊢ (↑n.primeFactorsList).Nodup ↔ n.primeFactorsList.Nodup

Tactic:
simp

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

Goal state before:
pp: case inl
p : ℕ
hn : Squarefree 0
⊢ (factorization 0) p ≤ 1

Tactic:
simp

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

Goal state before:
pp: n : ℕ
hn hm : Squarefree n
⊢ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ n)

Tactic:
simp

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

Goal state before:
pp: case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
⊢ n.MinSqFacProp none

pp: case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
⊢ n.MinSqFacProp (if k ∣ n then if k ∣ n / k then some k else (n / k).minSqFacAux (k + 2) else n.minSqFacAux (k + 2))

Tactic:
· refine squarefree_iff_prime_squarefree.2 fun p pp d => ?_
    have := ih p pp (dvd_trans ⟨_, rfl⟩ d)
    have := Nat.mul_le_mul this this
    exact not_le_of_gt h (le_trans this (le_of_dvd n0 d))

Goal state after:
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
⊢ n.MinSqFacProp (if k ∣ n then if k ∣ n / k then some k else (n / k).minSqFacAux (k + 2) else n.minSqFacAux (k + 2))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
pk : k ∣ n → Prime k
⊢ n.MinSqFacProp (if k ∣ n then if k ∣ n / k then some k else (n / k).minSqFacAux (k + 2) else n.minSqFacAux (k + 2))

Tactic:
split_ifs with dk dkk

Goal state after:
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : k ∣ n / k
⊢ n.MinSqFacProp (some k)

case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : ¬k ∣ n / k
⊢ n.MinSqFacProp ((n / k).minSqFacAux (k + 2))

case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
pk : k ∣ n → Prime k
dk : ¬k ∣ n
⊢ n.MinSqFacProp (n.minSqFacAux (k + 2))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: ⊢ (primeFactorsList 2).Nodup

Tactic:
simp

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

Goal state before:
pp: ⊢ 2 ≠ 0

Tactic:
simp

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

Goal state before:
pp: case mpr
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ (∃ a_1 ∈ (normalizedFactors n).toFinset.powerset, a_1.val.prod = a) → (a ∣ n ∧ n ≠ 0) ∧ Squarefree a

Tactic:
· rintro ⟨s, hs, rfl⟩
      rw [Finset.mem_powerset, ← Finset.val_le_iff, Multiset.toFinset_val] at hs
      have hs0 : s.val.prod ≠ 0 := by
        rw [Ne, Multiset.prod_eq_zero_iff]
        intro con
        apply
          not_irreducible_zero
            (irreducible_of_normalized_factor 0 (Multiset.mem_dedup.1 (Multiset.mem_of_le hs con)))
      rw [(prod_normalizedFactors h0).symm.dvd_iff_dvd_right]
      refine ⟨⟨Multiset.prod_dvd_prod_of_le (le_trans hs (Multiset.dedup_le _)), h0⟩, ?_⟩
      have h :=
        UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor
          (fun x hx =>
            irreducible_of_normalized_factor x
              (Multiset.mem_of_le (le_trans hs (Multiset.dedup_le _)) hx))
          (prod_normalizedFactors hs0)
      rw [associated_eq_eq, Multiset.rel_eq] at h
      rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors hs0, h]
      apply s.nodup

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

Goal state before:
pp: case empty
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
α : Type u_3
f : α → MvPolynomial σ R
⊢ m.toWithBotSyn (m.withBotDegree (∑ x ∈ ∅, f x)) ≤ ∅.sup fun x ↦ m.toWithBotSyn (m.withBotDegree (f x))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
⊢ ↑(#({f ∈ piFinset fun x ↦ S | (eval f) p = 0})) / ↑(#S) ^ n =
    ↑(#({f ∈ piFinset fun x ↦ S | (eval f) p = 0})) / ∏ i, ↑(#S)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
⊢ (p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#∅)) = ↑p.totalDegree / ↑(#∅)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Zero R
f : ArithmeticFunction R
⊢ ⇑f ∈ {f | f 0 = 0}

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
f : ArithmeticFunction ℕ
⊢ ↑(f 0) = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : AddGroupWithOne R
f : ArithmeticFunction ℤ
⊢ ↑(f 0) = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : AddGroupWithOne R
f : ArithmeticFunction ℕ
x✝ : ℕ
⊢ ↑↑f x✝ = ↑f x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoid R
f g : ArithmeticFunction R
⊢ (⇑f + ⇑g) 0 = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ (if 0 = 1 then ↑n else 0) = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
x✝ : ℕ
⊢ { toFun := fun x ↦ if x = 1 then ↑0 else 0, map_zero' := ⋯ } x✝ = 0 x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : NegZeroClass R
f : ArithmeticFunction R
⊢ (-⇑f) 0 = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Zero R
inst✝¹ : AddCommMonoid M
inst✝ : SMul R M
f : ArithmeticFunction R
g : ArithmeticFunction M
⊢ ∑ x ∈ divisorsAntidiagonal 0, f x.1 • g x.2 = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : ArithmeticFunction R
⊢ (f * g) 1 = f 1 * g 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : ArithmeticFunction ℕ
n : ℕ
⊢ ↑(f * g) n = (↑f * ↑g) n

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f g : ArithmeticFunction ℤ
n : ℕ
⊢ ↑(f * g) n = (↑f * ↑g) n

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
⊢ (f.pmul ↑ζ) 0 = f 0

Tactic:
simp

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
n✝ : ℕ
⊢ (f.pmul ↑ζ) (n✝ + 1) = f (n✝ + 1)

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
⊢ ((↑ζ).pmul f) 0 = f 0

Tactic:
simp

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
n✝ : ℕ
⊢ ((↑ζ).pmul f) (n✝ + 1) = f (n✝ + 1)

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ f x * f x ^ 0 = (f.pmul (f.ppow 0)) x

Tactic:
simp

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x n✝ : ℕ
a✝ : f x * f x ^ n✝ = (f.pmul (f.ppow n✝)) x
⊢ f x * f x ^ (n✝ + 1) = (f.pmul (f.ppow (n✝ + 1))) x

Tactic:
simp

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

Goal state before:
pp: case inr.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
g : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
    f ≠ 0 ∧ g ≠ 0 → m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)
⊢ m.toSyn (m.degree (m.sPolynomial 0 g)) ≤ m.toSyn (m.degree 0 ⊔ m.degree g)

Tactic:
simp

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

Goal state before:
pp: case inr.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
    f ≠ 0 ∧ g ≠ 0 → m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)
⊢ m.toSyn (m.degree (m.sPolynomial f 0)) ≤ m.toSyn (m.degree f ⊔ m.degree 0)

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
kpos : 0 < 0
⊢ f x ^ 0 * f x = ((f.ppow 0).pmul f) x

Tactic:
simp

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x n✝ : ℕ
a✝ : ∀ {kpos : 0 < n✝}, f x ^ n✝ * f x = ((f.ppow n✝).pmul f) x
kpos : 0 < n✝ + 1
⊢ f x ^ (n✝ + 1) * f x = ((f.ppow (n✝ + 1)).pmul f) x

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : DivisionSemiring R
f : ArithmeticFunction R
⊢ (f.pdiv ↑ζ) 0 = f 0

Tactic:
simp

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : DivisionSemiring R
f : ArithmeticFunction R
n✝ : ℕ
⊢ (f.pdiv ↑ζ) (n✝ + 1) = f (n✝ + 1)

Tactic:
simp

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

Goal state before:
pp: ⊢ ζ 1 = 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m✝ n✝ : ℕ
cop : m✝.Coprime n✝
⊢ (f.pmul g) (m✝ * n✝) = (f.pmul g) m✝ * (f.pmul g) n✝

Tactic:
simp only [pmul_apply, hf.map_mul_of_coprime cop, hg.map_mul_of_coprime cop]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m✝ n✝ : ℕ
cop : m✝.Coprime n✝
⊢ f m✝ * f n✝ * (g m✝ * g n✝) = f m✝ * g m✝ * (f n✝ * g n✝)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
⊢ f * 1 = f

Tactic:
ext x
    simp_all [← map_div_left_divisors, sum_eq_single 1]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x✝ : ℕ
⊢ (0 * f) x✝ = 0 x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x✝ : ℕ
⊢ (f * 0) x✝ = 0 x✝

Tactic:
simp

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:
simp

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:
simp

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

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

Tactic:
simp

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:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case mpr.inr.refl
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
hq' : Nat.Prime p ∧ p ∣ n
⊢ List.count p n.primeFactorsList ≤ List.count p (List.replicate (n.factorization p) p)

Tactic:
simp

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

Goal state before:
pp: case inl
n b : ℕ
hn : IsPrimePow n
hab : Coprime 0 b
⊢ n ∣ 0 * b ↔ n ∣ 0 ∨ n ∣ b

Tactic:
simp

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

Goal state before:
pp: case inr.inl
n a : ℕ
hn : IsPrimePow n
ha : a ≠ 0
hab : a.Coprime 0
⊢ n ∣ a * 0 ↔ n ∣ a ∨ n ∣ 0

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ (pow 0) n = ζ n

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ (pow 1) n = ArithmeticFunction.id n

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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:
isMultiplicative_sigma.multiplicative_factorization _ hn

Goal state after:
k n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun p k_1 ↦ (σ k) (p ^ k_1)) =
    ∏ p ∈ n.primeFactors, ∑ i ∈ range (n.factorization p + 1), p ^ (i * k)
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 : ℕ+ × ℕ+
⊢ (∃ a, ↑⟨(↑a).1, ⋯⟩ = ↑x.1 ∧ ↑⟨(↑a).2, ⋯⟩ = ↑x.2) ↔ ↑(x.1 * x.2) = ↑n

Tactic:
Subtype.exists

Goal state after:
divisorsAntidiagonal : ℕ+ → Finset (ℕ+ × ℕ+) :=
  fun n ↦ map { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩), inj' := ⋯ } (↑n).divisorsAntidiagonal.attach
n : ℕ+
x : ℕ+ × ℕ+
⊢ (∃ a, ∃ (h : a ∈ (↑n).divisorsAntidiagonal), ↑⟨a.1, ⋯⟩ = ↑x.1 ∧ ↑⟨a.2, ⋯⟩ = ↑x.2) ↔ ↑(x.1 * x.2) = ↑n
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 : ℕ+ × ℕ+
⊢ (∃ a, ∃ (h : a ∈ (↑n).divisorsAntidiagonal), ↑⟨a.1, ⋯⟩ = ↑x.1 ∧ ↑⟨a.2, ⋯⟩ = ↑x.2) ↔ ↑(x.1 * x.2) = ↑n

Tactic:
simp

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

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

Tactic:
isMultiplicative_sigma.multiplicative_factorization _ hn

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun p k ↦ (σ 0) (p ^ k)) = ∏ x ∈ n.primeFactors, (n.factorization x + 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case inl
⊢ #(divisors 0) = 1 ↔ 0 = 1

Tactic:
simp

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

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

Tactic:
· refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
    exact (card_le_one.mp h.le 1 (one_mem_divisors.mpr hn) n (n.mem_divisors_self hn)).symm

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

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

Tactic:
isMultiplicative_sigma.multiplicative_factorization _ hn

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun p k ↦ (σ 1) (p ^ k)) = ∏ p ∈ n.primeFactors, ∑ k ∈ range (n.factorization p + 1), p ^ k
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

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

Tactic:
simp

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

Goal state before:
pp: ⊢ Ω 0 = 0

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case neg.zero
m : ℕ
hm : ¬m = 0
⊢ Ω (m ^ 0) = 0 * Ω m

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: ⊢ ω 0 = 0

Tactic:
simp

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

Goal state before:
pp: case empty
ι : Type u_2
f : ι → ℕ
h : (↑∅).Pairwise (Coprime on f)
⊢ ω (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, ω (f i)

Tactic:
simp

Goal state after: