awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
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' := ⋯ }
            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)
⊢ 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

Tactic:
ext
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
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)
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)
⊢ 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)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q x : ℕ
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)

Tactic:
simp [Function.extend]

Premises used: Function.extend
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q x : ℕ
h : ¬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:
simp [Function.extend]

Premises used: Function.extend
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f g : PowerSeries R
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' := ⋯ }
            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)
⊢ (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))

Tactic:
ext n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
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)
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' := ⋯ } :
            (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)

Tactic:
by_cases h : ∃ a, q ^ a = n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
h : ∃ (a : ℕ), q ^ a = n
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' := ⋯ } :
            (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' := ⋯ : 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)
          (q ^ a) :
        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)

Tactic:
obtain ⟨a, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
a : ℕ
⊢ 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)
        (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' := ⋯ : 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)
        (q ^ a) :
      R)

Tactic:
simp [(Nat.pow_right_injective hq).extend_apply]

Premises used: Function.Injective.extend_apply, Nat.pow_right_injective
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
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)

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
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)
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)
⊢ 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
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : ¬1 < q
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:
simp [hn]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : ¬1 < q
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:
simp [hn]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
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' := ⋯ }
            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)
⊢ 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)

Tactic:
ext n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
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)
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)
⊢ 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)

Tactic:
split_ifs with hq
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
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)
⊢ 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)

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, coe_mk]

Premises used: ArithmeticFunction.coe_mk, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
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)
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)
⊢ 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
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
hn : ∃ (k : ℕ), q ^ k = n
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)
⊢ 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:
obtain ⟨k, rfl⟩ := hn

Premises used: rfl