awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : ¬1 < q
pos :
  ∀ (hn : n = 1),
    Eq (α := R)
      ((((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
                ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f + g)) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          n :
        R)
      ((HAdd.hAdd (α := ArithmeticFunction R) (β := ArithmeticFunction R)
              ((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
                  ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f) :
                ArithmeticFunction R)
              ((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
                  ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) g) :
                ArithmeticFunction R) :
            (a : ℕ) → R)
          n :
        R)
⊢ Eq (α := R)
    ((((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
              ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f + g)) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        n :
      R)
    ((HAdd.hAdd (α := ArithmeticFunction R) (β := ArithmeticFunction R)
            ((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
                ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f) :
              ArithmeticFunction R)
            ((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
                ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) g) :
              ArithmeticFunction R) :
          (a : ℕ) → R)
        n :
      R)
have neg : ∀ (hn : ¬n = 1),
  Eq (α := R)
    ((((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
              ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f + g)) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        n :
      R)
    ((HAdd.hAdd (α := ArithmeticFunction R) (β := ArithmeticFunction R)
            ((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
                ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f) :
              ArithmeticFunction R)
            ((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
                ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) g) :
              ArithmeticFunction R) :
          (a : ℕ) → R)
        n :
      R)
Tactic: by_cases hn : n = 1
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
⊢ Eq (α := ArithmeticFunction R)
    (if hq : 1 < q then
        {
          toFun :=
            Function.extend (fun (x : ℕ) ↦ q ^ x)
              (fun (x_1 : ℕ) ↦
                (PowerSeries.coeff x_1 : (a : PowerSeries R) → R)
                  ((algebraMap R (PowerSeries R) : (a : R) → PowerSeries R) x : PowerSeries R))
              0,
          map_zero' := ⋯ }
      else
        (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)
    ((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R) x : ArithmeticFunction R)
have h : ∀ (n : ℕ),
  Eq (α := R)
    ((if hq : 1 < q then
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x)
                  (fun (x_1 : ℕ) ↦
                    (PowerSeries.coeff x_1 : (a : PowerSeries R) → R)
                      ((algebraMap R (PowerSeries R) : (a : R) → PowerSeries R) x : PowerSeries R))
                  0,
              map_zero' := sorry }
          else
            (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)) :
          (a : ℕ) → R)
        n :
      R)
    ((((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R) x : ArithmeticFunction R) : (a : ℕ) → R)
        n :
      R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
n : ℕ
⊢ Eq (α := R)
    ((if hq : 1 < q then
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x)
                  (fun (x_1 : ℕ) ↦
                    (PowerSeries.coeff x_1 : (a : PowerSeries R) → R)
                      ((algebraMap R (PowerSeries R) : (a : R) → PowerSeries R) x : PowerSeries R))
                  0,
              map_zero' := ⋯ }
          else
            (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)) :
          (a : ℕ) → R)
        n :
      R)
    ((((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R) x : ArithmeticFunction R) : (a : ℕ) → R)
        n :
      R)
have pos : ∀ (hq : 1 < q),
  Eq (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x)
                (fun (x_1 : ℕ) ↦
                  (PowerSeries.coeff x_1 : (a : PowerSeries R) → R)
                    ((algebraMap R (PowerSeries R) : (a : R) → PowerSeries R) x : PowerSeries R))
                0,
            map_zero' := sorry } :
          (a : ℕ) → R)
        n :
      R)
    ((((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R) x : ArithmeticFunction R) : (a : ℕ) → R)
        n :
      R)
Tactic: split_ifs with hq
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
n : ℕ
pos :
  ∀ (hq : 1 < q),
    Eq (α := R)
      (({
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x)
                  (fun (x_1 : ℕ) ↦
                    (PowerSeries.coeff x_1 : (a : PowerSeries R) → R)
                      ((algebraMap R (PowerSeries R) : (a : R) → PowerSeries R) x : PowerSeries R))
                  0,
              map_zero' := ⋯ } :
            (a : ℕ) → R)
          n :
        R)
      ((((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R) x : ArithmeticFunction R) : (a : ℕ) → R)
          n :
        R)
⊢ Eq (α := R)
    ((if hq : 1 < q then
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x)
                  (fun (x_1 : ℕ) ↦
                    (PowerSeries.coeff x_1 : (a : PowerSeries R) → R)
                      ((algebraMap R (PowerSeries R) : (a : R) → PowerSeries R) x : PowerSeries R))
                  0,
              map_zero' := ⋯ }
          else
            (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)) :
          (a : ℕ) → R)
        n :
      R)
    ((((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R) x : ArithmeticFunction R) : (a : ℕ) → R)
        n :
      R)
have neg : ∀ (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: split_ifs with hq
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
⊢ Eq (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x)
                (fun (x_1 : ℕ) ↦
                  (PowerSeries.coeff x_1 : (a : PowerSeries R) → R)
                    ((algebraMap R (PowerSeries R) : (a : R) → PowerSeries R) x : PowerSeries R))
                0,
            map_zero' := ⋯ } :
          (a : ℕ) → R)
        n :
      R)
    ((((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R) x : ArithmeticFunction R) : (a : ℕ) → R)
        n :
      R)
have pos : 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: simp only [Algebra.algebraMap_eq_smul_one, coe_mk]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
⊢ 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)
have pos : ∀ (hn : ∃ (k : ℕ), q ^ k = n),
  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: by_cases hn : ∃ k, q ^ k = n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
pos :
  ∀ (hn : ∃ (k : ℕ), q ^ k = n),
    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)
⊢ 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)
have neg : ∀ (hn : ¬∃ (k : ℕ), q ^ k = n),
  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: by_cases hn : ∃ k, q ^ k = n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
hn : ∃ (k : ℕ), q ^ k = n
⊢ 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)
have pos : ∀ (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: obtain ⟨k, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
hn : ¬∃ (k : ℕ), q ^ k = n
⊢ 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)
have neg : n ≠ 1
Tactic: rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply, smul_map, one_apply_ne, smul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
hn : ¬∃ (k : ℕ), q ^ k = n
⊢ n ≠ 1
have neg : ∀ (hn : n = 1), ∃ (k : ℕ), q ^ k = n
Tactic: contrapose hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
hq : 1 < q
f : PowerSeries R
k : ℕ
⊢ 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)
have 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)
Tactic: rw [ofPowerSeries_apply hq, (Nat.pow_right_injective hq).extend_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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)
⊢ 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)
have rw₁ : Eq (α := R) ((PowerSeries.coeff k : (a : PowerSeries R) → R) f : R)
  ((PowerSeries.coeff k : (a : PowerSeries R) → R) f : R)
Tactic: rw [ofPowerSeries_apply hq, (Nat.pow_right_injective hq).extend_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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) 1 : R)
    ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R)
have 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)
Tactic: by_cases hq : 1 < q
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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)
⊢ Eq (α := R)
    ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) 1 : R)
    ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R)
have 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)
Tactic: by_cases hq : 1 < q
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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)
have 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)
Tactic: rw [← pow_zero q, ofPowerSeries_apply_pow hq, PowerSeries.coeff_zero_eq_constantCoeff]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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)
⊢ Eq (α := R)
    ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) 1 : R)
    ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R)
have pos₁ : Eq (α := R) ((PowerSeries.coeff 0 : (a : PowerSeries R) → R) f : R)
  ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R)
Tactic: rw [← pow_zero q, ofPowerSeries_apply_pow hq, PowerSeries.coeff_zero_eq_constantCoeff]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
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)
⊢ Eq (α := R)
    ((((ofPowerSeries q : (a : PowerSeries R) → ArithmeticFunction R) f : ArithmeticFunction R) : (a : ℕ) → R) 1 : R)
    ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R)
have pos₂ : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R)
  ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R)
Tactic: rw [← pow_zero q, ofPowerSeries_apply_pow hq, PowerSeries.coeff_zero_eq_constantCoeff]
-- 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: by_cases hq : 1 < q
-- 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: by_cases hq : 1 < q
-- 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
⊢ 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 : ∀ (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: ext n
-- 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 : ℕ
⊢ 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 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)
Tactic: by_cases hn : ∃ i, q ^ i = n
-- 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 : ℕ
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)
⊢ 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 : ∀ (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)
Tactic: by_cases hn : ∃ i, q ^ i = n
-- 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 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)
Tactic: obtain ⟨i, rfl⟩ := hn
Cleared hypotheses: n, hn