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
hn : ¬∃ (a : ℕ), q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ∃ (i : ℕ), q ^ i = a
hb : ¬∃ (j : ℕ), q ^ j = b
neg :
  HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
        (a, b).2)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0
        (a, b).1) =
    0
neg₁ :
  HMul.hMul (α := R) (0 (a, b).2)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0
        (a, b).1) =
    0
neg₂ : ¬∃ (a_1 : ℕ), q ^ a_1 = (a, b).2
neg₃ :
  HMul.hMul (α := R) 0
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0
        (a, b).1) =
    0
neg₄ : ¬∃ (a_1 : ℕ), q ^ a_1 = (a, b).2
⊢ HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0
        (a, b).1)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
        (a, b).2) =
    0
have neg₅ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rwa [mul_comm, Function.extend_apply', Pi.zero_apply, zero_mul]
-- 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
hn : ¬∃ (a : ℕ), q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ¬∃ (i : ℕ), q ^ i = a
⊢ HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0
        (a, b).1)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
        (a, b).2) =
    0
have neg : HMul.hMul (α := R) (0 (a, b).1)
    (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
      (a, b).2) =
  0
Tactic: rwa [Function.extend_apply', Pi.zero_apply, zero_mul]
-- 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
hn : ¬∃ (a : ℕ), q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ¬∃ (i : ℕ), q ^ i = a
neg :
  HMul.hMul (α := R) (0 (a, b).1)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
        (a, b).2) =
    0
⊢ HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0
        (a, b).1)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
        (a, b).2) =
    0
have neg₁ : ¬∃ (a_1 : ℕ), q ^ a_1 = (a, b).1
Tactic: rwa [Function.extend_apply', Pi.zero_apply, zero_mul]
-- 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
hn : ¬∃ (a : ℕ), q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ¬∃ (i : ℕ), q ^ i = a
neg :
  HMul.hMul (α := R) (0 (a, b).1)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
        (a, b).2) =
    0
neg₁ : ¬∃ (a_1 : ℕ), q ^ a_1 = (a, b).1
⊢ HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0
        (a, b).1)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
        (a, b).2) =
    0
have neg₂ : HMul.hMul (α := R) 0
    (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
      (a, b).2) =
  0
Tactic: rwa [Function.extend_apply', Pi.zero_apply, zero_mul]
-- 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
hn : ¬∃ (a : ℕ), q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ¬∃ (i : ℕ), q ^ i = a
neg :
  HMul.hMul (α := R) (0 (a, b).1)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
        (a, b).2) =
    0
neg₁ : ¬∃ (a_1 : ℕ), q ^ a_1 = (a, b).1
neg₂ :
  HMul.hMul (α := R) 0
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
        (a, b).2) =
    0
neg₃ : ¬∃ (a_1 : ℕ), q ^ a_1 = (a, b).1
⊢ HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0
        (a, b).1)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
        (a, b).2) =
    0
have neg₄ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rwa [Function.extend_apply', Pi.zero_apply, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
⊢ Eq.{u_1 + 1} (α := ArithmeticFunction R)
    (if hq : 1 < q then
      {
        toFun :=
          Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) 0) 0,
        map_zero' := ⋯ }
    else
      (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
        ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) 0))
    0
have h : ∀ (x : ℕ),
  Eq.{u_1 + 1} (α := R)
    ((if hq : 1 < q then
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) 0)
                  0,
              map_zero' := sorry }
          else
            (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
              ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) 0) :
          (a : ℕ) → R)
        x :
      R)
    ((0 : (a : ℕ) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommSemiring R
q x : ℕ
⊢ Eq.{u_1 + 1} (α := R)
    ((if hq : 1 < q then
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) 0)
                  0,
              map_zero' := ⋯ }
          else
            (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
              ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) 0) :
          (a : ℕ) → R)
        x :
      R)
    ((0 : (a : ℕ) → R) x : R)
have pos : ∀ (h : 1 < q),
  Eq.{u_1 + 1} (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) 0) 0,
            map_zero' := sorry } :
          (a : ℕ) → R)
        x :
      R)
    ((0 : (a : ℕ) → R) x : R)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommSemiring R
q x : ℕ
pos :
  ∀ (h : 1 < q),
    Eq.{u_1 + 1} (α := R)
      (({
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) 0)
                  0,
              map_zero' := ⋯ } :
            (a : ℕ) → R)
          x :
        R)
      ((0 : (a : ℕ) → R) x : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((if hq : 1 < q then
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) 0)
                  0,
              map_zero' := ⋯ }
          else
            (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
              ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) 0) :
          (a : ℕ) → R)
        x :
      R)
    ((0 : (a : ℕ) → R) x : R)
have neg : ¬1 < q →
  Eq (α := R)
    ((((algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
              ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) 0) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        x :
      R)
    ((0 : (a : ℕ) → R) x : R)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f g : PowerSeries R
⊢ (if hq : 1 < q then
      {
        toFun :=
          Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) (f + g))
            0,
        map_zero' := ⋯ }
    else
      (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
        ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f + g))) =
    HAdd.hAdd (α := ArithmeticFunction R)
      (if hq : 1 < q then
        {
          toFun :=
            Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0,
          map_zero' := ⋯ : ZeroHom ℕ R }
      else
        (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
          ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f))
      (if hq : 1 < q then
        {
          toFun :=
            Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0,
          map_zero' := ⋯ : ZeroHom ℕ R }
      else
        (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
          ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) g))
have h : ∀ (n : ℕ),
  Eq (α := R)
    ((if hq : 1 < q then
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x)
                  (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) (f + g)) 0,
              map_zero' := sorry }
          else
            (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
              ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f + g)) :
          (a : ℕ) → R)
        n :
      R)
    ((HAdd.hAdd (α := ArithmeticFunction R)
            (if hq : 1 < q then
              {
                toFun :=
                  Function.extend (fun (x : ℕ) ↦ q ^ x)
                    (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0,
                map_zero' := sorry : ZeroHom ℕ R }
            else
              (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
                ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f))
            (if hq : 1 < q then
              {
                toFun :=
                  Function.extend (fun (x : ℕ) ↦ q ^ x)
                    (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0,
                map_zero' := sorry : ZeroHom ℕ R }
            else
              (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
                ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) g)) :
          (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 : ℕ
f g : PowerSeries R
n : ℕ
⊢ Eq (α := R)
    ((if hq : 1 < q then
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x)
                  (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) (f + g)) 0,
              map_zero' := ⋯ }
          else
            (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
              ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) (f + g)) :
          (a : ℕ) → R)
        n :
      R)
    ((HAdd.hAdd (α := ArithmeticFunction R)
            (if hq : 1 < q then
              {
                toFun :=
                  Function.extend (fun (x : ℕ) ↦ q ^ x)
                    (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0,
                map_zero' := ⋯ : ZeroHom ℕ R }
            else
              (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
                ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f))
            (if hq : 1 < q then
              {
                toFun :=
                  Function.extend (fun (x : ℕ) ↦ q ^ x)
                    (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0,
                map_zero' := ⋯ : ZeroHom ℕ R }
            else
              (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
                ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) g)) :
          (a : ℕ) → R)
        n :
      R)
have pos : ∀ (hq : 1 < q),
  Eq (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x)
                (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) (f + g)) 0,
            map_zero' := sorry } :
          (a : ℕ) → R)
        n :
      R)
    ((HAdd.hAdd (α := ArithmeticFunction R)
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f)
                  0,
              map_zero' := sorry : ZeroHom ℕ R }
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g)
                  0,
              map_zero' := sorry : ZeroHom ℕ 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 : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
⊢ Eq (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x)
                (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) (f + g)) 0,
            map_zero' := ⋯ } :
          (a : ℕ) → R)
        n :
      R)
    ((HAdd.hAdd (α := ArithmeticFunction R)
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f)
                  0,
              map_zero' := ⋯ : ZeroHom ℕ R }
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g)
                  0,
              map_zero' := ⋯ : ZeroHom ℕ R } :
          (a : ℕ) → R)
        n :
      R)
have pos : ∀ (h : ∃ (a : ℕ), q ^ a = n),
  Eq (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x)
                (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) (f + g)) 0,
            map_zero' := sorry } :
          (a : ℕ) → R)
        n :
      R)
    ((HAdd.hAdd (α := ArithmeticFunction R)
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f)
                  0,
              map_zero' := sorry : ZeroHom ℕ R }
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g)
                  0,
              map_zero' := sorry : ZeroHom ℕ R } :
          (a : ℕ) → R)
        n :
      R)
Tactic: by_cases h : ∃ a, q ^ a = n
-- 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 :
  ∀ (h : ∃ (a : ℕ), q ^ a = n),
    Eq (α := R)
      (({
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x)
                  (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) (f + g)) 0,
              map_zero' := ⋯ } :
            (a : ℕ) → R)
          n :
        R)
      ((HAdd.hAdd (α := ArithmeticFunction R)
              {
                toFun :=
                  Function.extend (fun (x : ℕ) ↦ q ^ x)
                    (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0,
                map_zero' := ⋯ : ZeroHom ℕ R }
              {
                toFun :=
                  Function.extend (fun (x : ℕ) ↦ q ^ x)
                    (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0,
                map_zero' := ⋯ : ZeroHom ℕ R } :
            (a : ℕ) → R)
          n :
        R)
⊢ Eq (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x)
                (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) (f + g)) 0,
            map_zero' := ⋯ } :
          (a : ℕ) → R)
        n :
      R)
    ((HAdd.hAdd (α := ArithmeticFunction R)
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f)
                  0,
              map_zero' := ⋯ : ZeroHom ℕ R }
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g)
                  0,
              map_zero' := ⋯ : ZeroHom ℕ R } :
          (a : ℕ) → R)
        n :
      R)
have neg : ∀ (h : ¬∃ (a : ℕ), q ^ a = n),
  Eq (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x)
                (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) (f + g)) 0,
            map_zero' := sorry } :
          (a : ℕ) → R)
        n :
      R)
    ((HAdd.hAdd (α := ArithmeticFunction R)
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f)
                  0,
              map_zero' := sorry : ZeroHom ℕ R }
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g)
                  0,
              map_zero' := sorry : ZeroHom ℕ R } :
          (a : ℕ) → R)
        n :
      R)
Tactic: by_cases h : ∃ a, q ^ a = n
-- 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
h : ∃ (a : ℕ), q ^ a = n
⊢ Eq (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x)
                (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) (f + g)) 0,
            map_zero' := ⋯ } :
          (a : ℕ) → R)
        n :
      R)
    ((HAdd.hAdd (α := ArithmeticFunction R)
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f)
                  0,
              map_zero' := ⋯ : ZeroHom ℕ R }
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g)
                  0,
              map_zero' := ⋯ : ZeroHom ℕ R } :
          (a : ℕ) → R)
        n :
      R)
have pos : ∀ (a : ℕ),
  Eq (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x)
                (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) (f + g)) 0,
            map_zero' := sorry } :
          (a : ℕ) → R)
        (q ^ a) :
      R)
    ((HAdd.hAdd (α := ArithmeticFunction R)
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f)
                  0,
              map_zero' := sorry : ZeroHom ℕ R }
            {
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g)
                  0,
              map_zero' := sorry : ZeroHom ℕ R } :
          (a : ℕ) → R)
        (q ^ a) :
      R)
Tactic: obtain ⟨a, rfl⟩ := h
Cleared hypotheses: n, h
-- 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
⊢ 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 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)
Tactic: by_cases hn : n = 1