awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
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)
have 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)
Tactic: rw [ofPowerSeries_apply_pow hq, PowerSeries.coeff_subst_X_pow hk]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
⊢ 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)
have 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)
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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)
⊢ 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)
have neg : ∀ (hn : ¬k ∣ i),
  Eq (α := R)
    ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
        (q ^ i) :
      R)
    (0 : R)
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
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)
have 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)
Tactic: obtain ⟨j, rfl⟩ := hn
Cleared hypotheses: i, hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
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)
have 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)
Tactic: rw [pow_mul, ofPowerSeries_apply_pow (one_lt_pow' hq hk)]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : ¬k ∣ i
⊢ Eq (α := R)
    ((((ofPowerSeries (q ^ k) : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R)
        (q ^ i) :
      R)
    (0 : R)
have neg : ¬∃ (a : ℕ), (q ^ k) ^ a = q ^ i
Tactic: rw [ofPowerSeries_apply (one_lt_pow' hq hk), Function.extend_apply', Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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
⊢ 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)
have neg : ¬∃ (a : ℕ), (q ^ k) ^ a = n
Tactic: rwa [ofPowerSeries_apply hq, ofPowerSeries_apply (one_lt_pow' hq hk),
        Function.extend_apply', Function.extend_apply']
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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
⊢ ¬∃ (a : ℕ), (q ^ k) ^ a = n
have neg : ∀ (hn : ∃ (a : ℕ), (q ^ k) ^ a = n), ∃ (i : ℕ), q ^ i = n
Tactic: contrapose! hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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
⊢ ∃ (i : ℕ), q ^ i = n
have neg : ∀ (i : ℕ), ∃ (i_1 : ℕ), q ^ i_1 = (q ^ k) ^ i
Tactic: obtain ⟨i, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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)
have 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)
Tactic: refine ⟨(ofPowerSeries_apply_one q f).trans hf, fun {m n} hmn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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
⊢ (((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)
have 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)
Tactic: obtain ⟨p, k, hp, hk, rfl⟩ := hq
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (hypothesis)
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
⊢ (((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)
have hp₁ : Nat.Prime p
Tactic: rw [← Nat.prime_iff] at hp
Cleared hypotheses: hp, hk
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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
⊢ (((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)
have 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)
Tactic: rw [ofPowerSeries_pow p hk.ne']
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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
⊢ (((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)
have 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)
Tactic: by_cases hm : ∃ i, p ^ i = m
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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)
⊢ (((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)
have 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)
Tactic: by_cases hm : ∃ i, p ^ i = m
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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
⊢ (((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)
have 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)
Tactic: obtain ⟨i, rfl⟩ := hm
Cleared hypotheses: m, hmn, hm
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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
⊢ (((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)
have 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)
Tactic: by_cases hn : ∃ j, p ^ j = n