awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
p : ℕ
h : p ∈ x.primeFactors ∪ y.primeFactors
neg :
  ∀ (h : LE.le (α := ℕ) ((x.factorization : (a : ℕ) → ℕ) p : ℕ) ((y.factorization : (a : ℕ) → ℕ) p : ℕ)),
    HMul.hMul (α := R) (β := R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.lcm y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.gcd y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R) =
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((x.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((y.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
⊢ HMul.hMul (α := R) (β := R)
      ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.lcm y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
      ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.gcd y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((x.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
      ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((y.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
have neg₁ : ∀ (h : LE.le (α := ℕ) ((y.factorization : (a : ℕ) → ℕ) p : ℕ) ((x.factorization : (a : ℕ) → ℕ) p : ℕ)),
  HMul.hMul (α := R) (β := R)
      ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.lcm y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
      ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.gcd y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((x.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
      ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((y.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
Tactic: rcases Nat.le_or_le (x.factorization p) (y.factorization p) with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
⊢ (x.gcd y).factorization.support ⊆ x.primeFactors ∪ y.primeFactors
have rw : x.factorization.support ∩ y.factorization.support ⊆ x.primeFactors ∪ y.primeFactors
Tactic: rw [factorization_gcd hx hy, Finsupp.support_inf]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
Goal:
R : Type u_1
inst : CommGroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hf_lcm : Ne (α := R) ((f : (a : ℕ) → R) (x.lcm y) : R) (0 : R)
⊢ (f : (a : ℕ) → R) (x.gcd y) =
    HDiv.hDiv (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R))
      ((f : (a : ℕ) → R) (x.lcm y) : R)
have rw : (f : (a : ℕ) → R) (x.gcd y) =
  HDiv.hDiv (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R))
    ((f : (a : ℕ) → R) (x.lcm y) : R)
Tactic: rw [← hf.lcm_apply_mul_gcd_apply, mul_div_cancel_left₀ _ hf_lcm]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
Goal:
R : Type u_1
inst : CommGroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hf_lcm : Ne (α := R) ((f : (a : ℕ) → R) (x.lcm y) : R) (0 : R)
rw :
  (f : (a : ℕ) → R) (x.gcd y) =
    HDiv.hDiv (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R))
      ((f : (a : ℕ) → R) (x.lcm y) : R)
⊢ (f : (a : ℕ) → R) (x.gcd y) =
    HDiv.hDiv (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R))
      ((f : (a : ℕ) → R) (x.lcm y) : R)
have rw₁ : Eq (α := R) ((f : (a : ℕ) → R) (x.gcd y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R)
Tactic: rw [← hf.lcm_apply_mul_gcd_apply, mul_div_cancel_left₀ _ hf_lcm]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
Goal:
R : Type u_1
inst : CommGroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hf_gcd : Ne (α := R) ((f : (a : ℕ) → R) (x.gcd y) : R) (0 : R)
⊢ (f : (a : ℕ) → R) (x.lcm y) =
    HDiv.hDiv (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R))
      ((f : (a : ℕ) → R) (x.gcd y) : R)
have rw : (f : (a : ℕ) → R) (x.lcm y) =
  HDiv.hDiv (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R))
    ((f : (a : ℕ) → R) (x.gcd y) : R)
Tactic: rw [← hf.lcm_apply_mul_gcd_apply, mul_div_cancel_right₀ _ hf_gcd]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
Goal:
R : Type u_1
inst : CommGroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hf_gcd : Ne (α := R) ((f : (a : ℕ) → R) (x.gcd y) : R) (0 : R)
rw :
  (f : (a : ℕ) → R) (x.lcm y) =
    HDiv.hDiv (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R))
      ((f : (a : ℕ) → R) (x.gcd y) : R)
⊢ (f : (a : ℕ) → R) (x.lcm y) =
    HDiv.hDiv (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R))
      ((f : (a : ℕ) → R) (x.gcd y) : R)
have rw₁ : Eq (α := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.lcm y) : R)
Tactic: rw [← hf.lcm_apply_mul_gcd_apply, mul_div_cancel_right₀ _ hf_gcd]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
m n : ℕ
hn : Squarefree n
hmn : m ∣ n
h_zero : Eq (α := R) ((f : (a : ℕ) → R) m : R) (0 : R)
⊢ Eq (α := R) ((f : (a : ℕ) → R) n : R) (0 : R)
have rcases : ∀ (k : ℕ) (hn : Squarefree (m * k)), Eq (α := R) ((f : (a : ℕ) → R) (m * k) : R) (0 : R)
Tactic: rcases hmn with ⟨k, rfl⟩
Cleared hypotheses: n, hn, hmn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
hmn : m.Coprime n
⊢ (1 : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((1 : (a : ℕ) → R) m : R) ((1 : (a : ℕ) → R) n : R)
have pos : ∀ (h : m = 1),
  (1 : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((1 : (a : ℕ) → R) m : R) ((1 : (a : ℕ) → R) n : R)
Tactic: by_cases h : m = 1
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
hmn : m.Coprime n
pos :
  ∀ (h : m = 1),
    (1 : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((1 : (a : ℕ) → R) m : R) ((1 : (a : ℕ) → R) n : R)
⊢ (1 : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((1 : (a : ℕ) → R) m : R) ((1 : (a : ℕ) → R) n : R)
have neg : ∀ (h : ¬m = 1),
  (1 : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((1 : (a : ℕ) → R) m : R) ((1 : (a : ℕ) → R) n : R)
Tactic: by_cases h : m = 1
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
f : ι → ArithmeticFunction R
s : Finset ι
hf : ∀ i ∈ s, IsMultiplicative.{u_1} (R := R) (f i)
⊢ IsMultiplicative.{u_1} (R := R) (∏ i ∈ s, f i)
have induction : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsMultiplicative.{u_1} (R := R) (f i)),
  IsMultiplicative.{u_1} (R := R) (∏ i ∈ ∅, f i)
Tactic: induction s using Finset.cons_induction
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
f : ι → ArithmeticFunction R
s : Finset ι
hf : ∀ i ∈ s, IsMultiplicative.{u_1} (R := R) (f i)
induction :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsMultiplicative.{u_1} (R := R) (f i)),
    IsMultiplicative.{u_1} (R := R) (∏ i ∈ ∅, f i)
⊢ IsMultiplicative.{u_1} (R := R) (∏ i ∈ s, f i)
have cons : ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
  (∀ (hf : ∀ i ∈ s, IsMultiplicative.{u_1} (R := R) (f i)), IsMultiplicative.{u_1} (R := R) (∏ i ∈ s, f i)) →
    ∀ (hf : ∀ i ∈ cons a s h, IsMultiplicative.{u_1} (R := R) (f i)),
      IsMultiplicative.{u_1} (R := R) (∏ i ∈ cons a s h, f i)
Tactic: induction s using Finset.cons_induction
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
f : ι → ArithmeticFunction R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (hf : ∀ i ∈ s, IsMultiplicative.{u_1} (R := R) (f i)), IsMultiplicative.{u_1} (R := R) (∏ i ∈ s, f i)
hf : ∀ i ∈ cons a s ha, IsMultiplicative.{u_1} (R := R) (f i)
⊢ IsMultiplicative.{u_1} (R := R) (∏ i ∈ cons a s ha, f i)
have rw : (f a * ∏ x ∈ s, f x).IsMultiplicative
Tactic: rw [Finset.prod_cons]
-- 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) 1) 0,
        map_zero' := ⋯ }
    else
      (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
        ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) 1))
    1
have h : ∀ (n : ℕ),
  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) 1)
                  0,
              map_zero' := sorry }
          else
            (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
              ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) 1) :
          (a : ℕ) → R)
        n :
      R)
    ((1 : (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 n : ℕ
⊢ 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) 1)
                  0,
              map_zero' := ⋯ }
          else
            (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
              ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) 1) :
          (a : ℕ) → R)
        n :
      R)
    ((1 : (a : ℕ) → R) n : R)
have pos : ∀ (hq : 1 < q),
  Eq.{u_1 + 1} (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) 1) 0,
            map_zero' := sorry } :
          (a : ℕ) → R)
        n :
      R)
    ((1 : (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 n : ℕ
pos :
  ∀ (hq : 1 < q),
    Eq.{u_1 + 1} (α := R)
      (({
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) 1)
                  0,
              map_zero' := ⋯ } :
            (a : ℕ) → R)
          n :
        R)
      ((1 : (a : ℕ) → R) n : 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) 1)
                  0,
              map_zero' := ⋯ }
          else
            (algebraMap R (ArithmeticFunction R) : (a : R) → ArithmeticFunction R)
              ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) 1) :
          (a : ℕ) → R)
        n :
      R)
    ((1 : (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) 1) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        n :
      R)
    ((1 : (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 n : ℕ
hq : 1 < q
⊢ Eq.{u_1 + 1} (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) 1) 0,
            map_zero' := ⋯ } :
          (a : ℕ) → R)
        n :
      R)
    ((1 : (a : ℕ) → R) n : R)
have pos : ∀ (hn : ∃ (k : ℕ), q ^ k = n),
  Eq.{u_1 + 1} (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) 1) 0,
            map_zero' := sorry } :
          (a : ℕ) → R)
        n :
      R)
    ((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 n : ℕ
hq : 1 < q
pos :
  ∀ (hn : ∃ (k : ℕ), q ^ k = n),
    Eq.{u_1 + 1} (α := R)
      (({
              toFun :=
                Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) 1)
                  0,
              map_zero' := ⋯ } :
            (a : ℕ) → R)
          n :
        R)
      ((1 : (a : ℕ) → R) n : R)
⊢ Eq.{u_1 + 1} (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) 1) 0,
            map_zero' := ⋯ } :
          (a : ℕ) → R)
        n :
      R)
    ((1 : (a : ℕ) → R) n : R)
have neg : ∀ (hn : ¬∃ (k : ℕ), q ^ k = n),
  Eq.{u_1 + 1} (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) 1) 0,
            map_zero' := sorry } :
          (a : ℕ) → R)
        n :
      R)
    ((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 n : ℕ
hq : 1 < q
hn : ∃ (k : ℕ), q ^ k = n
⊢ Eq.{u_1 + 1} (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) 1) 0,
            map_zero' := ⋯ } :
          (a : ℕ) → R)
        n :
      R)
    ((1 : (a : ℕ) → R) n : R)
have pos : ∀ (a : ℕ),
  Eq.{u_1 + 1} (α := R)
    (({
            toFun :=
              Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) 1) 0,
            map_zero' := sorry } :
          (a : ℕ) → R)
        (q ^ a) :
      R)
    ((1 : (a : ℕ) → R) (q ^ a) : R)
Tactic: obtain ⟨a, 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 : ℕ
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))) =
    HMul.hMul (α := 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)
    ((HMul.hMul (α := 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)
    ((HMul.hMul (α := 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)
    ((HMul.hMul (α := 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)
    ((HMul.hMul (α := 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 : Eq.{u_1 + 1} (α := R)
  (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) (f * g)) 0 n)
  (∑ x ∈ n.divisorsAntidiagonal,
    HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0 x.1)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0 x.2))
Tactic: simp_rw [mul_apply, coe_mk]
-- 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.{u_1 + 1} (α := R)
    (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) (f * g)) 0 n)
    (∑ x ∈ n.divisorsAntidiagonal,
      HMul.hMul (α := R)
        (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0 x.1)
        (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0 x.2))
have pos : ∀ (hn : ∃ (a : ℕ), q ^ a = n),
  Eq.{u_1 + 1} (α := R)
    (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) (f * g)) 0 n)
    (∑ x ∈ n.divisorsAntidiagonal,
      HMul.hMul (α := R)
        (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0 x.1)
        (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0 x.2))
Tactic: by_cases hn : ∃ a, q ^ a = n