awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Nat.Prime p
hk : 0 < k
rw :
  (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (m * n) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          m :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          n :
        R)
⊢ (((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)

Tactic:
rw [ofPowerSeries_pow p hk.ne']

Premises used: ArithmeticFunction.ofPowerSeries_pow, LT.lt.ne'
-- 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 : Nat.Prime p
hk : 0 < k
pos :
  ∀ (hm : ∃ (i : ℕ), p ^ i = m),
    (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        (m * n) =
      HMul.hMul (α := R) (β := R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            m :
          R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            n :
          R)
neg :
  ∀ (hm : ¬∃ (i : ℕ), p ^ i = m),
    (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        (m * n) =
      HMul.hMul (α := R) (β := R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            m :
          R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            n :
          R)
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (m * n) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          m :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          n :
        R)

Tactic:
by_cases hm : ∃ i, p ^ i = m
-- 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 : Nat.Prime p
hk : 0 < k
hm : ∃ (i : ℕ), p ^ i = m
pos :
  ∀ (i : ℕ) (hmn : (p ^ i).Coprime n),
    (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        (p ^ i * n) =
      HMul.hMul (α := R) (β := R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (p ^ i) :
          R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            n :
          R)
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (m * n) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          m :
        R)
      ((((ofPowerSeries p : (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⟩ := hm

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)
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hmn : (p ^ i).Coprime n
pos :
  ∀ (hn : ∃ (j : ℕ), p ^ j = n),
    (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        (p ^ i * n) =
      HMul.hMul (α := R) (β := R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (p ^ i) :
          R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            n :
          R)
neg :
  ∀ (hn : ¬∃ (j : ℕ), p ^ j = n),
    (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        (p ^ i * n) =
      HMul.hMul (α := R) (β := R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (p ^ i) :
          R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            n :
          R)
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ i * n) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ i) :
        R)
      ((((ofPowerSeries p : (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 : ∃ j, p ^ j = n
-- 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)
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hmn : (p ^ i).Coprime n
hn : ∃ (j : ℕ), p ^ j = n
pos :
  ∀ (j : ℕ) (hmn : (p ^ i).Coprime (p ^ j)),
    (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        (p ^ i * p ^ j) =
      HMul.hMul (α := R) (β := R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (p ^ i) :
          R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (p ^ j) :
          R)
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ i * n) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ i) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          n :
        R)

Tactic:
obtain ⟨j, rfl⟩ := hn

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)
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i j : ℕ
hmn : (p ^ i).Coprime (p ^ j)
pos :
  ∀ (hmn : (HPow.hPow (β := ℕ) p 0).Coprime (p ^ j)),
    (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        (HPow.hPow (β := ℕ) p 0 * p ^ j) =
      HMul.hMul (α := R) (β := R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (HPow.hPow (β := ℕ) p 0) :
          R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (p ^ j) :
          R)
pos₁ :
  ∀ (n : ℕ) (hmn : (p ^ (n + 1)).Coprime (p ^ j)),
    (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        (p ^ (n + 1) * p ^ j) =
      HMul.hMul (α := R) (β := R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (p ^ (n + 1)) :
          R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (p ^ j) :
          R)
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ i * p ^ j) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ i) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ j) :
        R)

Tactic:
cases i
-- 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)
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
j : ℕ
hmn : (HPow.hPow (β := ℕ) p 0).Coprime (p ^ j)
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (HPow.hPow (β := ℕ) p 0 * p ^ j) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (HPow.hPow (β := ℕ) p 0) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ j) :
        R)

Tactic:
simp [hk.ne', hf]

Premises used: LT.lt.ne'
-- 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)
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
j n : ℕ
hmn : (p ^ (n + 1)).Coprime (p ^ j)
pos :
  ∀ (hmn : (p ^ (n + 1)).Coprime (HPow.hPow (β := ℕ) p 0)),
    (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        (p ^ (n + 1) * HPow.hPow (β := ℕ) p 0) =
      HMul.hMul (α := R) (β := R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (p ^ (n + 1)) :
          R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (HPow.hPow (β := ℕ) p 0) :
          R)
pos₁ :
  ∀ (n_1 : ℕ) (hmn : (p ^ (n + 1)).Coprime (p ^ (n_1 + 1))),
    (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        (p ^ (n + 1) * p ^ (n_1 + 1)) =
      HMul.hMul (α := R) (β := R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (p ^ (n + 1)) :
          R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (p ^ (n_1 + 1)) :
          R)
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ (n + 1) * p ^ j) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ (n + 1)) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ j) :
        R)

Tactic:
cases j
-- 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)
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
n : ℕ
hmn : (p ^ (n + 1)).Coprime (HPow.hPow (β := ℕ) p 0)
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ (n + 1) * HPow.hPow (β := ℕ) p 0) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ (n + 1)) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (HPow.hPow (β := ℕ) p 0) :
        R)

Tactic:
simp [hk.ne', hf]

Premises used: LT.lt.ne'
-- 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)
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
n n_1 : ℕ
hmn : (p ^ (n + 1)).Coprime (p ^ (n_1 + 1))
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ (n + 1) * p ^ (n_1 + 1)) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ (n + 1)) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ (n_1 + 1)) :
        R)

Tactic:
simp [hp.ne_one] at hmn

Premises used: Nat.Prime.ne_one
-- 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)
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hmn : (p ^ i).Coprime n
hn : ¬∃ (j : ℕ), p ^ j = n
neg :
  Function.extend (fun (x : ℕ) ↦ p ^ x)
      (fun (x : ℕ) ↦
        (PowerSeries.coeff x : (a : PowerSeries R) → R)
          (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
      0 (p ^ i * n) =
    HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ p ^ x)
        (fun (x : ℕ) ↦
          (PowerSeries.coeff x : (a : PowerSeries R) → R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
        0 (p ^ i))
      (Function.extend (fun (x : ℕ) ↦ p ^ x)
        (fun (x : ℕ) ↦
          (PowerSeries.coeff x : (a : PowerSeries R) → R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
        0 n)
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ i * n) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ i) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          n :
        R)

Tactic:
simp_rw [ofPowerSeries_apply hp.one_lt]

Premises used: Nat.Prime.one_lt, ArithmeticFunction.ofPowerSeries_apply
-- 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)
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hmn : (p ^ i).Coprime n
hn : ¬∃ (j : ℕ), p ^ j = n
neg : ¬∃ (a : ℕ), p ^ a = p ^ i * n
⊢ Function.extend (fun (x : ℕ) ↦ p ^ x)
      (fun (x : ℕ) ↦
        (PowerSeries.coeff x : (a : PowerSeries R) → R)
          (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
      0 (p ^ i * n) =
    HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ p ^ x)
        (fun (x : ℕ) ↦
          (PowerSeries.coeff x : (a : PowerSeries R) → R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
        0 (p ^ i))
      (Function.extend (fun (x : ℕ) ↦ p ^ x)
        (fun (x : ℕ) ↦
          (PowerSeries.coeff x : (a : PowerSeries R) → R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
        0 n)

Tactic:
rw [Function.extend_apply', Function.extend_apply' _ _ _ hn,
        Pi.zero_apply, Pi.zero_apply, mul_zero]

Premises used: Pi.zero_apply, MulZeroClass.mul_zero, Function.extend_apply'
-- 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)
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hmn : (p ^ i).Coprime n
hn : ¬∃ (j : ℕ), p ^ j = n
neg : ∀ (hn : ∃ (a : ℕ), p ^ a = p ^ i * n), ∃ (j : ℕ), p ^ j = n
⊢ ¬∃ (a : ℕ), p ^ a = p ^ i * n

Tactic:
contrapose! hn
-- 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)
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hmn : (p ^ i).Coprime n
hn : ∃ (a : ℕ), p ^ a = p ^ i * n
neg : ∀ (j : ℕ) (hj : p ^ j = p ^ i * n), ∃ (j : ℕ), p ^ j = n
⊢ ∃ (j : ℕ), p ^ j = n

Tactic:
obtain ⟨j, hj⟩ := hn