awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
hq : 1 < q
k : ℕ
⊢ Eq (α := R)
    (Function.extend (fun (x : ℕ) ↦ q ^ x)
        (fun (x_1 : ℕ) ↦ (PowerSeries.coeff x_1 : (a : PowerSeries R) → R) (HSMul.hSMul (β := PowerSeries R) x 1)) 0
        (q ^ k) :
      R)
    ((HSMul.hSMul (β := ArithmeticFunction R) x 1 : (a : ℕ) → R) (q ^ k) : R)

Tactic:
simp [(Nat.pow_right_injective hq).extend_apply, one_apply, hq.ne']

Premises used: Function.Injective.extend_apply, LT.lt.ne', Nat.pow_right_injective, ArithmeticFunction.one_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
hn : ¬∃ (k : ℕ), q ^ k = n
neg : n ≠ 1
⊢ Eq (α := R)
    (Function.extend (fun (x : ℕ) ↦ q ^ x)
        (fun (x_1 : ℕ) ↦ (PowerSeries.coeff x_1 : (a : PowerSeries R) → R) (HSMul.hSMul (β := PowerSeries R) x 1)) 0 n :
      R)
    ((HSMul.hSMul (β := ArithmeticFunction R) x 1 : (a : ℕ) → R) n : R)

Tactic:
rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply, smul_map, one_apply_ne, smul_zero]

Premises used: ArithmeticFunction.one_apply_ne, smul_zero, Pi.zero_apply, ArithmeticFunction.smul_map, Function.extend_apply'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
hn : ¬∃ (k : ℕ), q ^ k = n
neg : ∀ (hn : n = 1), ∃ (k : ℕ), q ^ k = n
⊢ n ≠ 1

Tactic:
contrapose hn
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
hn : n = 1
⊢ HPow.hPow (β := ℕ) q 0 = n

Tactic:
simp [hn]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
hn : n = 1
⊢ ∃ (k : ℕ), q ^ k = n

Tactic:
exact ⟨0, by simp [hn]⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : ¬1 < q
⊢ Eq (α := R)
    ((((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
              ((PowerSeries.constantCoeff : (a : PowerSeries R) → R)
                ((algebraMap R (PowerSeries R) : (a : R) → PowerSeries R) x : PowerSeries R)) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        n :
      R)
    ((((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R) x : ArithmeticFunction R) : (a : ℕ) → R)
        n :
      R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
hq : 1 < q
f : PowerSeries R
n : ℕ
⊢ Eq (α := R)
    ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) n : R)
    (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0 n : R)

Tactic:
simp [ofPowerSeries, dif_pos hq]

Premises used: dif_pos, ArithmeticFunction.ofPowerSeries
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
hq : 1 < q
f : PowerSeries R
k : ℕ
rw :
  Eq (α := R)
    (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0 (q ^ k) :
      R)
    ((PowerSeries.coeff k : (a : PowerSeries R) → R) f : R)
rw₁ rw₂ :
  Eq (α := R) ((PowerSeries.coeff k : (a : PowerSeries R) → R) f : R)
    ((PowerSeries.coeff k : (a : PowerSeries R) → R) f : R)
⊢ Eq (α := R)
    ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) (q ^ k) :
      R)
    ((PowerSeries.coeff k : (a : PowerSeries R) → R) f : R)

Tactic:
rw [ofPowerSeries_apply hq, (Nat.pow_right_injective hq).extend_apply]

Premises used: Function.Injective.extend_apply, Nat.pow_right_injective, ArithmeticFunction.ofPowerSeries_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f : PowerSeries R
⊢ Eq (α := R)
    ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) 0 : R)
    (0 : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f : PowerSeries R
pos :
  ∀ (hq : 1 < q),
    Eq (α := R)
      ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) 1 : R)
      ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R)
neg :
  ∀ (hq : ¬1 < q),
    Eq (α := R)
      ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) 1 : R)
      ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R)
⊢ Eq (α := R)
    ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) 1 : R)
    ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R)

Tactic:
by_cases hq : 1 < q
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f : PowerSeries R
hq : 1 < q
pos :
  Eq (α := R)
    ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
        (HPow.hPow (β := ℕ) q 0) :
      R)
    ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R)
pos₁ :
  Eq (α := R) ((PowerSeries.coeff 0 : (a : PowerSeries R) → R) f : R)
    ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R)
pos₂ pos₃ :
  Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R)
    ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R)
⊢ Eq (α := R)
    ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) 1 : R)
    ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R)

Tactic:
rw [← pow_zero q, ofPowerSeries_apply_pow hq, PowerSeries.coeff_zero_eq_constantCoeff]

Premises used: pow_zero, ArithmeticFunction.ofPowerSeries_apply_pow, PowerSeries.coeff_zero_eq_constantCoeff
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f : PowerSeries R
hq : ¬1 < q
⊢ Eq (α := R)
    ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) 1 : R)
    ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R)

Tactic:
simp [ofPowerSeries, dif_neg hq]

Premises used: ArithmeticFunction.ofPowerSeries, dif_neg
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
pos :
  ∀ (hq : 1 < q),
    Eq (α := ArithmeticFunction R)
      ((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R)
      ((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R)
          (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
        ArithmeticFunction R)
neg :
  ∀ (hq : ¬1 < q),
    Eq (α := ArithmeticFunction R)
      ((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R)
      ((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R)
          (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
        ArithmeticFunction R)
⊢ Eq (α := ArithmeticFunction R)
    ((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R)
    ((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R)
        (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
      ArithmeticFunction R)

Tactic:
by_cases hq : 1 < q
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
pos :
  ∀ (n : ℕ),
    Eq (α := R)
      ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
          n :
        R)
      ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          n :
        R)
⊢ Eq (α := ArithmeticFunction R)
    ((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R)
    ((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R)
        (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
      ArithmeticFunction R)

Tactic:
ext n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
pos :
  ∀ (hn : ∃ (i : ℕ), q ^ i = n),
    Eq (α := R)
      ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
          n :
        R)
      ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          n :
        R)
neg :
  ∀ (hn : ¬∃ (i : ℕ), q ^ i = n),
    Eq (α := R)
      ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
          n :
        R)
      ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          n :
        R)
⊢ Eq (α := R)
    ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) n :
      R)
    ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        n :
      R)

Tactic:
by_cases hn : ∃ i, q ^ i = n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
hn : ∃ (i : ℕ), q ^ i = n
pos :
  ∀ (i : ℕ),
    Eq (α := R)
      ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
          (q ^ i) :
        R)
      ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (q ^ i) :
        R)
⊢ Eq (α := R)
    ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) n :
      R)
    ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        n :
      R)

Tactic:
obtain ⟨i, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
pos :
  Eq (α := R)
    ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
        (q ^ i) :
      R)
    (if k ∣ i then (algebraMap R R : (a : R) → R) ((PowerSeries.coeff (i / k) : (a : PowerSeries R) → R) f : R) else 0 :
      R)
⊢ Eq (α := R)
    ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
        (q ^ i) :
      R)
    ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        (q ^ i) :
      R)

Tactic:
rw [ofPowerSeries_apply_pow hq, PowerSeries.coeff_subst_X_pow hk]

Premises used: ArithmeticFunction.ofPowerSeries_apply_pow, PowerSeries.coeff_subst_X_pow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
pos :
  ∀ (hn : k ∣ i),
    Eq (α := R)
      ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
          (q ^ i) :
        R)
      ((algebraMap R R : (a : R) → R) ((PowerSeries.coeff (i / k) : (a : PowerSeries R) → R) f : R) : R)
neg :
  ∀ (hn : ¬k ∣ i),
    Eq (α := R)
      ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
          (q ^ i) :
        R)
      (0 : R)
⊢ Eq (α := R)
    ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
        (q ^ i) :
      R)
    (if k ∣ i then (algebraMap R R : (a : R) → R) ((PowerSeries.coeff (i / k) : (a : PowerSeries R) → R) f : R) else 0 :
      R)

Tactic:
split_ifs with hn
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : k ∣ i
pos :
  ∀ (j : ℕ),
    Eq (α := R)
      ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
          (q ^ (k * j)) :
        R)
      ((algebraMap R R : (a : R) → R) ((PowerSeries.coeff (k * j / k) : (a : PowerSeries R) → R) f : R) : R)
⊢ Eq (α := R)
    ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
        (q ^ i) :
      R)
    ((algebraMap R R : (a : R) → R) ((PowerSeries.coeff (i / k) : (a : PowerSeries R) → R) f : R) : R)

Tactic:
obtain ⟨j, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
j : ℕ
pos :
  Eq (α := R) ((PowerSeries.coeff j : (a : PowerSeries R) → R) f : R)
    ((algebraMap R R : (a : R) → R) ((PowerSeries.coeff (k * j / k) : (a : PowerSeries R) → R) f : R) : R)
⊢ Eq (α := R)
    ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
        (q ^ (k * j)) :
      R)
    ((algebraMap R R : (a : R) → R) ((PowerSeries.coeff (k * j / k) : (a : PowerSeries R) → R) f : R) : R)

Tactic:
rw [pow_mul, ofPowerSeries_apply_pow (one_lt_pow' hq hk)]

Premises used: one_lt_pow', pow_mul, ArithmeticFunction.ofPowerSeries_apply_pow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
j : ℕ
⊢ Eq (α := R) ((PowerSeries.coeff j : (a : PowerSeries R) → R) f : R)
    ((algebraMap R R : (a : R) → R) ((PowerSeries.coeff (k * j / k) : (a : PowerSeries R) → R) f : R) : R)

Tactic:
simp [hk]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : ¬k ∣ i
neg : ¬∃ (a : ℕ), (q ^ k) ^ a = q ^ i
⊢ Eq (α := R)
    ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
        (q ^ i) :
      R)
    (0 : R)

Tactic:
rw [ofPowerSeries_apply (one_lt_pow' hq hk), Function.extend_apply', Pi.zero_apply]

Premises used: one_lt_pow', Pi.zero_apply, Function.extend_apply', ArithmeticFunction.ofPowerSeries_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : ¬k ∣ i
neg : ¬k ∣ i
⊢ ¬∃ (a : ℕ), (q ^ k) ^ a = q ^ i

Tactic:
simp_rw [← pow_mul, Nat.pow_right_inj hq, eq_comm, ← dvd_def]

Premises used: dvd_def, eq_comm, pow_mul, Nat.pow_right_inj
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : ¬k ∣ i
⊢ ¬k ∣ i

Tactic:
hn
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : ¬k ∣ i
⊢ ¬k ∣ i

Tactic:
exact hn
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
hn : ¬∃ (i : ℕ), q ^ i = n
neg : ¬∃ (a : ℕ), (q ^ k) ^ a = n
⊢ Eq (α := R)
    ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) n :
      R)
    ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        n :
      R)

Tactic:
rwa [ofPowerSeries_apply hq, ofPowerSeries_apply (one_lt_pow' hq hk),
        Function.extend_apply', Function.extend_apply']

Premises used: one_lt_pow', Function.extend_apply', ArithmeticFunction.ofPowerSeries_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
hn : ¬∃ (i : ℕ), q ^ i = n
neg : ∀ (hn : ∃ (a : ℕ), (q ^ k) ^ a = n), ∃ (i : ℕ), q ^ i = n
⊢ ¬∃ (a : ℕ), (q ^ k) ^ a = n

Tactic:
contrapose! hn
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
hn : ∃ (a : ℕ), (q ^ k) ^ a = n
neg : ∀ (i : ℕ), ∃ (i_1 : ℕ), q ^ i_1 = (q ^ k) ^ i
⊢ ∃ (i : ℕ), q ^ i = n

Tactic:
obtain ⟨i, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
⊢ ∃ (i_1 : ℕ), q ^ i_1 = (q ^ k) ^ i

Tactic:
⟨k * i, pow_mul q k i⟩

Premises used: HMul.hMul, pow_mul, Exists.intro
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
⊢ ∃ (i_1 : ℕ), q ^ i_1 = (q ^ k) ^ i

Tactic:
exact ⟨k * i, pow_mul q k i⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : ¬1 < q
⊢ Eq (α := ArithmeticFunction R)
    ((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R)
    ((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R)
        (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
      ArithmeticFunction R)

Tactic:
simp [ofPowerSeries, hq, hk]

Premises used: ArithmeticFunction.ofPowerSeries
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
pos :
  ∀ (hq : 1 < q),
    Eq (α := ArithmeticFunction R)
      ((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R)
      ((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R)
          (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
        ArithmeticFunction R)
neg neg₁ :
  ∀ (hq : ¬1 < q),
    Eq (α := ArithmeticFunction R)
      ((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R)
      ((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R)
          (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
        ArithmeticFunction R)
⊢ Eq (α := ArithmeticFunction R)
    ((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R)
    ((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R)
        (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
      ArithmeticFunction R)

Tactic:
classical
  by_cases hq : 1 < q
  · ext n
    by_cases hn : ∃ i, q ^ i = n
    · obtain ⟨i, rfl⟩ := hn
      rw [ofPowerSeries_apply_pow hq, PowerSeries.coeff_subst_X_pow hk]
      split_ifs with hn
      · obtain ⟨j, rfl⟩ := hn
        rw [pow_mul, ofPowerSeries_apply_pow (one_lt_pow' hq hk)]
        simp [hk]
      · rw [ofPowerSeries_apply (one_lt_pow' hq hk), Function.extend_apply', Pi.zero_apply]
        simp_rw [← pow_mul, Nat.pow_right_inj hq, eq_comm, ← dvd_def]
        exact hn
    · rwa [ofPowerSeries_apply hq, ofPowerSeries_apply (one_lt_pow' hq hk),
        Function.extend_apply', Function.extend_apply']
      contrapose! hn
      obtain ⟨i, rfl⟩ := hn
      exact ⟨k * i, pow_mul q k i⟩
  · simp [ofPowerSeries, hq, hk]

Premises used: dvd_def, Pi.zero_apply, ArithmeticFunction.ofPowerSeries, eq_comm, pow_mul, PowerSeries.coeff_subst_X_pow, Function.extend_apply', rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q : ℕ
hq : IsPrimePow q
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
⊢ IsMultiplicative.{u_1} (R := R) ((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f)

Tactic:
⟨(ofPowerSeries_apply_one q f).trans hf, fun {m n} hmn ↦ ?_⟩

Premises used: ArithmeticFunction.IsMultiplicative, ArithmeticFunction.ofPowerSeries_apply_one, And.intro, Eq.trans
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q : ℕ
hq : IsPrimePow q
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
refine :
  ∀ {m n : ℕ} (hmn : m.Coprime n),
    (((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) (m * n) =
      HMul.hMul (α := R) (β := R)
        ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) m :
          R)
        ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) n :
          R)
⊢ IsMultiplicative.{u_1} (R := R) ((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f)

Tactic:
refine ⟨(ofPowerSeries_apply_one q f).trans hf, fun {m n} hmn ↦ ?_⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
q : ℕ
hq : IsPrimePow q
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
m n : ℕ
hmn : m.Coprime n
obtain :
  ∀ (p k : ℕ) (hp : Prime p) (hk : 0 < k),
    (((ofPowerSeries (p ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
        (m * n) =
      HMul.hMul (α := R) (β := R)
        ((((ofPowerSeries (p ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
            m :
          R)
        ((((ofPowerSeries (p ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
            n :
          R)
⊢ (((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) (m * n) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) m : R)
      ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) n : R)

Tactic:
obtain ⟨p, k, hp, hk, rfl⟩ := hq

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Prime p
hk : 0 < k
⊢ Nat.Prime p

Tactic:
rw [← Nat.prime_iff] at hp

Premises used: Nat.prime_iff
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Prime p
hk : 0 < k
hp₁ : Nat.Prime p
⊢ 0 < k

Tactic:
rw [← Nat.prime_iff] at hp

Premises used: Nat.prime_iff