-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
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' := ⋯ } :
            (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)
    ((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 neg : ∀ (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)
Tactic: split_ifs with hq