awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), IsMultiplicative.{u_2} (R := R) (f i)
hf' : Multipliable f
h_1 : ∀ (s : Finset ι), IsMultiplicative.{u_2} (R := R) (∏ b ∈ s, f b)
h : ∀ (x : Finset ι), Eq.{u_2 + 1} (α := R) ((∏ b ∈ x, f b : (a : ℕ) → R) 1 : R) (1 : R)
key :
  ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter,
    Eq.{u_2 + 1} (α := R) (1 : R) ((∏' (b : ι), f b : (a : ℕ) → R) 1 : R)
pos :
  ∀ (key : Eq.{u_2 + 1} (α := R) (1 : R) ((∏' (b : ι), f b : (a : ℕ) → R) 1 : R)),
    Eq (α := R) ((eulerProduct f : (a : ℕ) → R) 1 : R) (1 : R)
pos₁ pos₂ pos₃ pos₄ :
  ∀ (key : Eq.{u_2 + 1} (α := R) ((∏' (b : ι), f b : (a : ℕ) → R) 1 : R) (1 : R)),
    Eq (α := R) ((eulerProduct f : (a : ℕ) → R) 1 : R) (1 : R)
⊢ Eq (α := R) ((eulerProduct f : (a : ℕ) → R) 1 : R) (1 : R)

Tactic:
rwa [eventually_const, eq_comm] at key

Premises used: eq_comm, Filter.eventually_const
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), IsMultiplicative.{u_2} (R := R) (f i)
hf' : Multipliable f
h_1 : ∀ (s : Finset ι), IsMultiplicative.{u_2} (R := R) (∏ b ∈ s, f b)
key :
  ∀ (n : ℕ),
    ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter,
      Eq.{u_2 + 1} (α := R) ((∏ b ∈ i, f b : (a : ℕ) → R) n : R) ((∏' (b : ι), f b : (a : ℕ) → R) n : R)
h :
  ∀ (x : Finset ι) {m n : ℕ},
    m.Coprime n →
      (∏ b ∈ x, f b : (a : ℕ) → R) (m * n) =
        HMul.hMul (α := R) (β := R) ((∏ b ∈ x, f b : (a : ℕ) → R) m : R) ((∏ b ∈ x, f b : (a : ℕ) → R) n : R)
m n : ℕ
hmn : m.Coprime n
⊢ ∀ (s : Finset ι),
    (∏ b ∈ s, f b : (a : ℕ) → R) (m * n) =
      HMul.hMul (α := R) (β := R) ((∏ b ∈ s, f b : (a : ℕ) → R) m : R) ((∏ b ∈ s, f b : (a : ℕ) → R) n : R)

Tactic:
replace h s : (∏ b ∈ s, f b) (m * n) = (∏ b ∈ s, f b) m * (∏ b ∈ s, f b) n := h s hmn
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), IsMultiplicative.{u_2} (R := R) (f i)
hf' : Multipliable f
h_1 : ∀ (s : Finset ι), IsMultiplicative.{u_2} (R := R) (∏ b ∈ s, f b)
key :
  ∀ (n : ℕ),
    ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter,
      Eq.{u_2 + 1} (α := R) ((∏ b ∈ i, f b : (a : ℕ) → R) n : R) ((∏' (b : ι), f b : (a : ℕ) → R) n : R)
m n : ℕ
hmn : m.Coprime n
h :
  ∀ (s : Finset ι),
    (∏ b ∈ s, f b : (a : ℕ) → R) (m * n) =
      HMul.hMul (α := R) (β := R) ((∏ b ∈ s, f b : (a : ℕ) → R) m : R) ((∏ b ∈ s, f b : (a : ℕ) → R) n : R)
⊢ ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter,
    Eq.{u_2 + 1} (α := R) ((∏ b ∈ i, f b : (a : ℕ) → R) (m * n) : R) ((∏' (b : ι), f b : (a : ℕ) → R) (m * n) : R)

Tactic:
have h2 := key (m * n)
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), IsMultiplicative.{u_2} (R := R) (f i)
hf' : Multipliable f
h_1 : ∀ (s : Finset ι), IsMultiplicative.{u_2} (R := R) (∏ b ∈ s, f b)
key :
  ∀ (n : ℕ),
    ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter,
      Eq.{u_2 + 1} (α := R) ((∏ b ∈ i, f b : (a : ℕ) → R) n : R) ((∏' (b : ι), f b : (a : ℕ) → R) n : R)
m n : ℕ
hmn : m.Coprime n
h :
  ∀ (s : Finset ι),
    (∏ b ∈ s, f b : (a : ℕ) → R) (m * n) =
      HMul.hMul (α := R) (β := R) ((∏ b ∈ s, f b : (a : ℕ) → R) m : R) ((∏ b ∈ s, f b : (a : ℕ) → R) n : R)
h2 :
  ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter,
    Eq.{u_2 + 1} (α := R) ((∏ b ∈ i, f b : (a : ℕ) → R) (m * n) : R) ((∏' (b : ι), f b : (a : ℕ) → R) (m * n) : R)
⊢ ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter,
    HMul.hMul (α := R) (β := R) ((∏ b ∈ i, f b : (a : ℕ) → R) m : R) ((∏ b ∈ i, f b : (a : ℕ) → R) n : R) =
      (∏' (b : ι), f b : (a : ℕ) → R) (m * n)

Tactic:
simp_rw [h] at h2
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), IsMultiplicative.{u_2} (R := R) (f i)
hf' : Multipliable f
h_1 : ∀ (s : Finset ι), IsMultiplicative.{u_2} (R := R) (∏ b ∈ s, f b)
key :
  ∀ (n : ℕ),
    ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter,
      Eq.{u_2 + 1} (α := R) ((∏ b ∈ i, f b : (a : ℕ) → R) n : R) ((∏' (b : ι), f b : (a : ℕ) → R) n : R)
m n : ℕ
hmn : m.Coprime n
h :
  ∀ (s : Finset ι),
    (∏ b ∈ s, f b : (a : ℕ) → R) (m * n) =
      HMul.hMul (α := R) (β := R) ((∏ b ∈ s, f b : (a : ℕ) → R) m : R) ((∏ b ∈ s, f b : (a : ℕ) → R) n : R)
h2 :
  ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter,
    HMul.hMul (α := R) (β := R) ((∏ b ∈ i, f b : (a : ℕ) → R) m : R) ((∏ b ∈ i, f b : (a : ℕ) → R) n : R) =
      (∏' (b : ι), f b : (a : ℕ) → R) (m * n)
⊢ (eulerProduct f : (a : ℕ) → R) (m * n) =
    HMul.hMul (α := R) (β := R) ((eulerProduct f : (a : ℕ) → R) m : R) ((eulerProduct f : (a : ℕ) → R) n : R)

Tactic:
eventually_const.mp (EventuallyEq.trans (.symm h2) (.mul (key m) (key n)))

Premises used: Filter.EventuallyEq.trans, Filter.EventuallyEq.mul, Filter.eventually_const, Iff.mp, Filter.EventuallyEq.symm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), IsMultiplicative.{u_2} (R := R) (f i)
hf' : Multipliable f
h_1 : ∀ (s : Finset ι), IsMultiplicative.{u_2} (R := R) (∏ b ∈ s, f b)
key :
  ∀ (n : ℕ),
    ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter,
      Eq.{u_2 + 1} (α := R) ((∏ b ∈ i, f b : (a : ℕ) → R) n : R) ((∏' (b : ι), f b : (a : ℕ) → R) n : R)
m n : ℕ
hmn : m.Coprime n
h :
  ∀ (s : Finset ι),
    (∏ b ∈ s, f b : (a : ℕ) → R) (m * n) =
      HMul.hMul (α := R) (β := R) ((∏ b ∈ s, f b : (a : ℕ) → R) m : R) ((∏ b ∈ s, f b : (a : ℕ) → R) n : R)
h2 :
  ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter,
    HMul.hMul (α := R) (β := R) ((∏ b ∈ i, f b : (a : ℕ) → R) m : R) ((∏ b ∈ i, f b : (a : ℕ) → R) n : R) =
      (∏' (b : ι), f b : (a : ℕ) → R) (m * n)
⊢ (eulerProduct f : (a : ℕ) → R) (m * n) =
    HMul.hMul (α := R) (β := R) ((eulerProduct f : (a : ℕ) → R) m : R) ((eulerProduct f : (a : ℕ) → R) n : R)

Tactic:
exact eventually_const.mp (EventuallyEq.trans (.symm h2) (.mul (key m) (key n)))

Premises used: Filter.EventuallyEq.trans, Filter.EventuallyEq.mul, Filter.eventually_const, Iff.mp, Filter.EventuallyEq.symm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), IsMultiplicative.{u_2} (R := R) (f i)
hf' : ¬Multipliable f
neg : IsMultiplicative.{u_2} (R := R) 1
⊢ IsMultiplicative.{u_2} (R := R) (eulerProduct f)

Tactic:
rw [eulerProduct, tprod_eq_one_of_not_multipliable hf']

Premises used: tprod_eq_one_of_not_multipliable, ArithmeticFunction.eulerProduct
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), IsMultiplicative.{u_2} (R := R) (f i)
hf' : ¬Multipliable f
⊢ IsMultiplicative.{u_2} (R := R) 1

Tactic:
isMultiplicative_one

Premises used: ArithmeticFunction.isMultiplicative_one
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), IsMultiplicative.{u_2} (R := R) (f i)
hf' : ¬Multipliable f
⊢ IsMultiplicative.{u_2} (R := R) 1

Tactic:
exact isMultiplicative_one

Premises used: ArithmeticFunction.isMultiplicative_one
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f i) : R) (1 : R)
n : ℕ
hf₁ :
  ∀ (n : ℕ),
    ∀ᶠ (i : ι) in cofinite,
      Eq (α := R)
        ((((ofPowerSeries (q i) : (a : PowerSeries R) → ArithmeticFunction R) (f i) : ArithmeticFunction R) :
              (a : ℕ) → R)
            n :
          R)
        ((1 : (a : ℕ) → R) n : R)
⊢ ∀ᶠ (s : Finset ι) in atTop,
    Eq.{u_2 + 1} (α := R)
      ((∏ i ∈ s, (ofPowerSeries (q i) : (a : PowerSeries R) → ArithmeticFunction R) (f i) : (a : ℕ) → R) n : R)
      ((eulerProduct fun (i : ι) ↦ (ofPowerSeries (q i) : (a : PowerSeries R) → ArithmeticFunction R) (f i) :
            (a : ℕ) → R)
          n :
        R)

Tactic:
apply tendsTo_eulerProduct_of_tendsTo

Premises used: ArithmeticFunction.tendsTo_eulerProduct_of_tendsTo
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f i) : R) (1 : R)
n : ℕ
⊢ ∀ (n : ℕ),
    ∀ᶠ (i : ι) in cofinite,
      Eq (α := R)
        ((((ofPowerSeries (q i) : (a : PowerSeries R) → ArithmeticFunction R) (f i) : ArithmeticFunction R) :
              (a : ℕ) → R)
            n :
          R)
        ((1 : (a : ℕ) → R) n : R)

Tactic:
fun n ↦ (tendsto_atTop.mp ((northcott_iff_tendsto q).mp hq) (n + 1)).mono fun i hi ↦ ?_

Premises used: northcott_iff_tendsto, Filter.tendsto_atTop, Filter.Eventually.mono, HAdd.hAdd, Iff.mp, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f i) : R) (1 : R)
n : ℕ
hf₁ :
  ∀ (n : ℕ) (i : ι) (hi : n + 1 ≤ q i),
    Eq (α := R)
      ((((ofPowerSeries (q i) : (a : PowerSeries R) → ArithmeticFunction R) (f i) : ArithmeticFunction R) : (a : ℕ) → R)
          n :
        R)
      ((1 : (a : ℕ) → R) n : R)
⊢ ∀ (n : ℕ),
    ∀ᶠ (i : ι) in cofinite,
      Eq (α := R)
        ((((ofPowerSeries (q i) : (a : PowerSeries R) → ArithmeticFunction R) (f i) : ArithmeticFunction R) :
              (a : ℕ) → R)
            n :
          R)
        ((1 : (a : ℕ) → R) n : R)

Tactic:
refine fun n ↦ (tendsto_atTop.mp ((northcott_iff_tendsto q).mp hq) (n + 1)).mono fun i hi ↦ ?_

Premises used: northcott_iff_tendsto, Filter.tendsto_atTop, Filter.Eventually.mono, HAdd.hAdd, Iff.mp, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f i) : R) (1 : R)
n_1 n : ℕ
i : ι
hi : n + 1 ≤ q i
hf₁ :
  ∀ (hi : HAdd.hAdd (α := ℕ) 0 1 ≤ q i),
    Eq (α := R)
      ((((ofPowerSeries (q i) : (a : PowerSeries R) → ArithmeticFunction R) (f i) : ArithmeticFunction R) : (a : ℕ) → R)
          0 :
        R)
      ((1 : (a : ℕ) → R) 0 : R)
hf₂ :
  ∀ (hi : HAdd.hAdd (α := ℕ) 0 1 + 1 ≤ q i),
    Eq (α := R)
      ((((ofPowerSeries (q i) : (a : PowerSeries R) → ArithmeticFunction R) (f i) : ArithmeticFunction R) : (a : ℕ) → R)
          (HAdd.hAdd (α := ℕ) 0 1) :
        R)
      ((1 : (a : ℕ) → R) (HAdd.hAdd (α := ℕ) 0 1) : R)
hf₃ :
  ∀ (n : ℕ) (hi : n + 1 + 1 + 1 ≤ q i),
    Eq (α := R)
      ((((ofPowerSeries (q i) : (a : PowerSeries R) → ArithmeticFunction R) (f i) : ArithmeticFunction R) : (a : ℕ) → R)
          (n + 1 + 1) :
        R)
      ((1 : (a : ℕ) → R) (n + 1 + 1) : R)
⊢ Eq (α := R)
    ((((ofPowerSeries (q i) : (a : PowerSeries R) → ArithmeticFunction R) (f i) : ArithmeticFunction R) : (a : ℕ) → R)
        n :
      R)
    ((1 : (a : ℕ) → R) n : R)

Tactic:
rcases n with rfl | rfl | n

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f i) : R) (1 : R)
n : ℕ
i : ι
hi : HAdd.hAdd (α := ℕ) 0 1 ≤ q i
⊢ Eq (α := R)
    ((((ofPowerSeries (q i) : (a : PowerSeries R) → ArithmeticFunction R) (f i) : ArithmeticFunction R) : (a : ℕ) → R)
        0 :
      R)
    ((1 : (a : ℕ) → R) 0 : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f i) : R) (1 : R)
n : ℕ
i : ι
hi : HAdd.hAdd (α := ℕ) 0 1 + 1 ≤ q i
⊢ Eq (α := R)
    ((((ofPowerSeries (q i) : (a : PowerSeries R) → ArithmeticFunction R) (f i) : ArithmeticFunction R) : (a : ℕ) → R)
        (HAdd.hAdd (α := ℕ) 0 1) :
      R)
    ((1 : (a : ℕ) → R) (HAdd.hAdd (α := ℕ) 0 1) : R)

Tactic:
simp [hf]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f i) : R) (1 : R)
n_1 : ℕ
i : ι
n : ℕ
hi : n + 1 + 1 + 1 ≤ q i
⊢ 1 < q i

Tactic:
lia
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f i) : R) (1 : R)
n_1 : ℕ
i : ι
n : ℕ
hi : n + 1 + 1 + 1 ≤ q i
⊢ 1 < q i

Tactic:
have hqi : 1 < q i := by lia
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f i) : R) (1 : R)
n_1 : ℕ
i : ι
n : ℕ
hi : n + 1 + 1 + 1 ≤ q i
hqi : 1 < q i
⊢ n + 1 + 1 ≠ 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f i) : R) (1 : R)
n_1 : ℕ
i : ι
n : ℕ
hi : n + 1 + 1 + 1 ≤ q i
hqi : 1 < q i
hf₁ : ¬∃ (a : ℕ), q i ^ a = n + 1 + 1
⊢ Eq (α := R)
    ((((ofPowerSeries (q i) : (a : PowerSeries R) → ArithmeticFunction R) (f i) : ArithmeticFunction R) : (a : ℕ) → R)
        (n + 1 + 1) :
      R)
    ((1 : (a : ℕ) → R) (n + 1 + 1) : R)

Tactic:
rw [ofPowerSeries_apply hqi, Function.extend_apply', Pi.zero_apply, one_apply_ne (by lia)]

Premises used: ArithmeticFunction.one_apply_ne, Pi.zero_apply, Function.extend_apply', ArithmeticFunction.ofPowerSeries_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f i) : R) (1 : R)
n_1 : ℕ
i : ι
n : ℕ
hi : n + 1 + 1 + 1 ≤ q i
hqi : 1 < q i
k : ℕ
hk : q i ^ k = n + 1 + 1
h : k = 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f i) : R) (1 : R)
n_1 : ℕ
i : ι
n : ℕ
hi : n + 1 + 1 + 1 ≤ q i
hqi : 1 < q i
k : ℕ
hk : q i ^ k = n + 1 + 1
⊢ k ≠ 0

Tactic:
have h : k ≠ 0 := fun h ↦ by simp_all
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f i) : R) (1 : R)
n_1 : ℕ
i : ι
n : ℕ
hi : n + 1 + 1 + 1 ≤ q i
hqi : 1 < q i
k : ℕ
hk : q i ^ k = n + 1 + 1
h : k ≠ 0
⊢ False

Tactic:
grind [Nat.le_pow h.pos (a := q i)]

Premises used: Ne.pos, Nat.le_pow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Liouville
Goal:
⊢ (if Eq (α := ℕ) 0 0 then 0 else HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) 0 : ℕ)) = 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Liouville
Goal:
n : ℕ
h : n ≠ 0
⊢ (liouville : (a : ℕ) → ℤ) n = HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ)

Tactic:
if_neg h

Premises used: if_neg, ite
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Liouville
Goal:
n : ℕ
h : n ≠ 0
⊢ Ne (α := ℤ) ((liouville : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ)

Tactic:
simp [liouville_apply h]

Premises used: ArithmeticFunction.liouville_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Liouville
Goal:
⊢ Eq (α := ℤ) ((liouville : (a : ℕ) → ℤ) 1 : ℤ) (1 : ℤ)

Tactic:
simp [liouville_apply]

Premises used: ArithmeticFunction.liouville_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Liouville
Goal:
m n : ℕ
pos :
  ∀ (hm : m = 0),
    (liouville : (a : ℕ) → ℤ) (m * n) =
      HMul.hMul (α := ℤ) (β := ℤ) ((liouville : (a : ℕ) → ℤ) m : ℤ) ((liouville : (a : ℕ) → ℤ) n : ℤ)
neg :
  ∀ (hm : ¬m = 0),
    (liouville : (a : ℕ) → ℤ) (m * n) =
      HMul.hMul (α := ℤ) (β := ℤ) ((liouville : (a : ℕ) → ℤ) m : ℤ) ((liouville : (a : ℕ) → ℤ) n : ℤ)
⊢ (liouville : (a : ℕ) → ℤ) (m * n) =
    HMul.hMul (α := ℤ) (β := ℤ) ((liouville : (a : ℕ) → ℤ) m : ℤ) ((liouville : (a : ℕ) → ℤ) n : ℤ)

Tactic:
by_cases hm : m = 0
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Liouville
Goal:
m n : ℕ
hm : m = 0
⊢ (liouville : (a : ℕ) → ℤ) (m * n) =
    HMul.hMul (α := ℤ) (β := ℤ) ((liouville : (a : ℕ) → ℤ) m : ℤ) ((liouville : (a : ℕ) → ℤ) n : ℤ)

Tactic:
simp [hm]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Liouville
Goal:
m n : ℕ
hm : ¬m = 0
pos :
  ∀ (hn : n = 0),
    (liouville : (a : ℕ) → ℤ) (m * n) =
      HMul.hMul (α := ℤ) (β := ℤ) ((liouville : (a : ℕ) → ℤ) m : ℤ) ((liouville : (a : ℕ) → ℤ) n : ℤ)
neg :
  ∀ (hn : ¬n = 0),
    (liouville : (a : ℕ) → ℤ) (m * n) =
      HMul.hMul (α := ℤ) (β := ℤ) ((liouville : (a : ℕ) → ℤ) m : ℤ) ((liouville : (a : ℕ) → ℤ) n : ℤ)
⊢ (liouville : (a : ℕ) → ℤ) (m * n) =
    HMul.hMul (α := ℤ) (β := ℤ) ((liouville : (a : ℕ) → ℤ) m : ℤ) ((liouville : (a : ℕ) → ℤ) n : ℤ)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Liouville
Goal:
m n : ℕ
hm : ¬m = 0
hn : n = 0
⊢ (liouville : (a : ℕ) → ℤ) (m * n) =
    HMul.hMul (α := ℤ) (β := ℤ) ((liouville : (a : ℕ) → ℤ) m : ℤ) ((liouville : (a : ℕ) → ℤ) n : ℤ)

Tactic:
simp [hn]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Liouville
Goal:
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ (liouville : (a : ℕ) → ℤ) (m * n) =
    HMul.hMul (α := ℤ) (β := ℤ) ((liouville : (a : ℕ) → ℤ) m : ℤ) ((liouville : (a : ℕ) → ℤ) n : ℤ)

Tactic:
simp [liouville_apply, cardFactors_mul, hm, hn, pow_add]

Premises used: pow_add, ArithmeticFunction.liouville_apply, ArithmeticFunction.cardFactors_mul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Liouville
Goal:
⊢ liouville.IsMultiplicative

Tactic:
⟨liouville_apply_one, fun {m n} _ ↦ liouville_apply_mul m n⟩

Premises used: ArithmeticFunction.liouville_apply_mul, ArithmeticFunction.liouville_apply_one, ArithmeticFunction.IsMultiplicative, And.intro
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ℕ → R
n : ℕ
hn : n ≠ 0
⊢ Eq.{u_1 + 1} (α := R) ((prodPrimeFactors fun (p : ℕ) ↦ f p : (a : ℕ) → R) n : R) (∏ p ∈ n.primeFactors, f p : R)

Tactic:
if_neg hn

Premises used: if_neg, ite
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ℕ → R
rw :
  Eq (α := R) ((ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) 1 : R) (1 : R) ∧
    ∀ {m n : ℕ},
      m ≠ 0 →
        n ≠ 0 →
          m.Coprime n →
            (ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) (m * n) =
              HMul.hMul (α := R) (β := R) ((ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) m : R)
                ((ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) n : R)
⊢ IsMultiplicative (ArithmeticFunction.prodPrimeFactors f)

Tactic:
rw [iff_ne_zero]

Premises used: ArithmeticFunction.IsMultiplicative.iff_ne_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ℕ → R
simp :
  ∀ {m n : ℕ},
    ¬m = 0 →
      ¬n = 0 →
        m.Coprime n →
          (ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) (m * n) =
            HMul.hMul (α := R) (β := R) ((ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) m : R)
              ((ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) n : R)
⊢ Eq (α := R) ((ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) 1 : R) (1 : R) ∧
    ∀ {m n : ℕ},
      m ≠ 0 →
        n ≠ 0 →
          m.Coprime n →
            (ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) (m * n) =
              HMul.hMul (α := R) (β := R) ((ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) m : R)
                ((ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) n : R)

Tactic:
simp only [ne_eq, one_ne_zero, not_false_eq_true, prodPrimeFactors_apply, primeFactors_one,
    prod_empty, true_and]

Premises used: Finset.prod_empty, ne_eq, ArithmeticFunction.prodPrimeFactors_apply, Nat.primeFactors_one, one_ne_zero, not_false_eq_true, true_and
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ℕ → R
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hxy : x.Coprime y
⊢ x * y ≠ 0

Tactic:
have hxy₀ : x * y ≠ 0 := mul_ne_zero hx hy
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ℕ → R
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hxy : x.Coprime y
hxy₀ : x * y ≠ 0
rw :
  ∏ p ∈ (x * y).primeFactors, f p =
    HMul.hMul (α := R) (β := R) ((ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) x : R)
      ((ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) y : R)
rw₁ :
  ∏ p ∈ (x * y).primeFactors, f p =
    HMul.hMul (α := R) (β := R) (∏ p ∈ x.primeFactors, f p : R)
      ((ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) y : R)
rw₂ : ∏ p ∈ (x * y).primeFactors, f p = HMul.hMul (α := R) (∏ p ∈ x.primeFactors, f p) (∏ p ∈ y.primeFactors, f p)
rw₃ :
  ∏ p ∈ x.primeFactors ∪ y.primeFactors, f p =
    HMul.hMul (α := R) (∏ p ∈ x.primeFactors, f p) (∏ p ∈ y.primeFactors, f p)
rw₄ rw₅ :
  Eq.{u_1 + 1} (α := R) (∏ p ∈ x.primeFactors ∪ y.primeFactors, f p) (∏ x ∈ x.primeFactors ∪ y.primeFactors, f x)
⊢ (ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) (x * y) =
    HMul.hMul (α := R) (β := R) ((ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) x : R)
      ((ArithmeticFunction.prodPrimeFactors f : (a : ℕ) → R) y : R)

Tactic:
rw [prodPrimeFactors_apply hxy₀, prodPrimeFactors_apply hx, prodPrimeFactors_apply hy,
    primeFactors_mul hx hy, ← prod_union hxy.disjoint_primeFactors]

Premises used: Finset.prod_union, ArithmeticFunction.prodPrimeFactors_apply, Nat.primeFactors_mul, Nat.Coprime.disjoint_primeFactors
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
n : ℕ
hn : Squarefree n
rw : Eq (α := R) (∏ p ∈ n.primeFactors, (f + g : (a : ℕ) → R) p : R) ((f * g : (a : ℕ) → R) n : R)
⊢ Eq (α := R) ((ArithmeticFunction.prodPrimeFactors fun (p : ℕ) ↦ (f + g : (a : ℕ) → R) p : (a : ℕ) → R) n : R)
    ((f * g : (a : ℕ) → R) n : R)

Tactic:
rw [prodPrimeFactors_apply hn.ne_zero]

Premises used: ArithmeticFunction.prodPrimeFactors_apply, Squarefree.ne_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
n : ℕ
hn : Squarefree n
simp_rw :
  Eq (α := R)
    (∏ x ∈ n.primeFactors, HAdd.hAdd (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((g : (a : ℕ) → R) x : R) : R)
    ((f * g : (a : ℕ) → R) n : R)
⊢ Eq (α := R) (∏ p ∈ n.primeFactors, (f + g : (a : ℕ) → R) p : R) ((f * g : (a : ℕ) → R) n : R)

Tactic:
simp_rw [add_apply (f := f) (g := g)]

Premises used: ArithmeticFunction.add_apply