awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
hmn : m.Coprime n
h : ¬m = 1
⊢ (1 : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((1 : (a : ℕ) → R) m : R) ((1 : (a : ℕ) → R) n : R)

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
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)
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 ∈ Finset.cons a s h, IsMultiplicative.{u_1} (R := R) (f i)),
        IsMultiplicative.{u_1} (R := R) (∏ i ∈ Finset.cons a s h, f i)
⊢ IsMultiplicative.{u_1} (R := R) (∏ i ∈ s, f i)

Tactic:
induction s using Finset.cons_induction
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsMultiplicative.{u_1} (R := R) (f i)
⊢ IsMultiplicative.{u_1} (R := R) (∏ i ∈ ∅, f i)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsMultiplicative.{u_1} (R := R) (f i)
⊢ IsMultiplicative.{u_1} (R := R) (∏ i ∈ ∅, f i)

Tactic:
case empty => simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
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)
rw : (f a * ∏ x ∈ s, f x).IsMultiplicative
⊢ IsMultiplicative.{u_1} (R := R) (∏ i ∈ cons a s ha, f i)

Tactic:
rw [Finset.prod_cons]

Premises used: Finset.prod_cons
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
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)
⊢ a ∈ cons a s ha

Tactic:
grind
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
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) (∏ x ∈ s, f x)

Tactic:
grind
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
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)
⊢ (f a * ∏ x ∈ s, f x).IsMultiplicative

Tactic:
exact (hf a (by grind)).mul (by grind)

Premises used: ArithmeticFunction.IsMultiplicative.mul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f : PowerSeries R
hq : 1 < q
⊢ Eq.{u_1 + 1} (α := R)
    (Function.extend (β := ℕ) (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0
      0)
    0

Tactic:
simp [Nat.ne_zero_of_lt hq]

Premises used: Nat.ne_zero_of_lt
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
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' := ⋯ }
            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)
⊢ 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

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

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

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

Tactic:
obtain ⟨a, rfl⟩ := hn

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

Tactic:
simp [(Nat.pow_right_injective hq).extend_apply, one_apply, hq.ne']

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

Tactic:
simp [hn, one_apply_ne (fun H ↦ hn ⟨0, H.symm⟩)]

Premises used: ArithmeticFunction.one_apply_ne, Exists.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q n : ℕ
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:
simp
-- 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)
      ((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)
⊢ (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))

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 :
  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))
⊢ 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)

Tactic:
simp_rw [mul_apply, coe_mk]

Premises used: ArithmeticFunction.coe_mk, ArithmeticFunction.mul_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
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))
neg :
  ∀ (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))
⊢ 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
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ∃ (a : ℕ), q ^ a = n
pos :
  ∀ (k : ℕ),
    Eq.{u_1 + 1} (α := R)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) (f * g)) 0
        (q ^ k))
      (∑ x ∈ (q ^ k).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))
⊢ 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:
obtain ⟨k, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
pos :
  Eq (α := R) ((PowerSeries.coeff k : (a : PowerSeries R) → R) (f * g) : R)
    (∑ x ∈ (q ^ k).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) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) (f * g)) 0
      (q ^ k))
    (∑ x ∈ (q ^ k).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:
rw [(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
hq : 1 < q
k : ℕ
⊢ Finset.map
      ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
      (@Finset.antidiagonal _ Nat.instAddMonoid _ k) ⊆
    (q ^ k).divisorsAntidiagonal

Tactic:
have hs : (Finset.antidiagonal k).map (.prodMap ⟨fun k ↦ q ^ k, Nat.pow_right_injective hq⟩
            ⟨fun k ↦ q ^ k, Nat.pow_right_injective hq⟩) ⊆ (q ^ k).divisorsAntidiagonal :=
          Nat.antidiagonal_map_subset_divisorsAntidiagonal_pow hq k
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map
      ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
      (@Finset.antidiagonal _ Nat.instAddMonoid _ k) ⊆
    (q ^ k).divisorsAntidiagonal
pos :
  Eq.{u_1 + 1} (α := R)
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
      HMul.hMul (α := R) (β := R) ((PowerSeries.coeff p.1 : (a : PowerSeries R) → R) f : R)
        ((PowerSeries.coeff p.2 : (a : PowerSeries R) → R) g : R))
    (∑
      x ∈
        Finset.map
          ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap
            { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
          (@Finset.antidiagonal _ Nat.instAddMonoid _ k),
      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))
pos₁ :
  ∀ x ∈ (q ^ k).divisorsAntidiagonal,
    x ∉
        Finset.map
          ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap
            { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
          (@Finset.antidiagonal _ Nat.instAddMonoid _ k) →
      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) =
        0
⊢ Eq (α := R) ((PowerSeries.coeff k : (a : PowerSeries R) → R) (f * g) : R)
    (∑ x ∈ (q ^ k).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) :
      R)

Tactic:
rw [PowerSeries.coeff_mul k f g, ← Finset.sum_subset hs]

Premises used: PowerSeries.coeff_mul, Finset.sum_subset
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map
      ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
      (@Finset.antidiagonal _ Nat.instAddMonoid _ k) ⊆
    (q ^ k).divisorsAntidiagonal
⊢ Eq.{u_1 + 1} (α := R)
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
      HMul.hMul (α := R) (β := R) ((PowerSeries.coeff p.1 : (a : PowerSeries R) → R) f : R)
        ((PowerSeries.coeff p.2 : (a : PowerSeries R) → R) g : R))
    (∑
      x ∈
        Finset.map
          ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap
            { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
          (@Finset.antidiagonal _ Nat.instAddMonoid _ k),
      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 [(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
hq : 1 < q
k : ℕ
hs :
  Finset.map
      ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
      (@Finset.antidiagonal _ Nat.instAddMonoid _ k) ⊆
    (q ^ k).divisorsAntidiagonal
a b : ℕ
hab : (a, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (a, b) ∉
    Finset.map
      ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
      (@Finset.antidiagonal _ Nat.instAddMonoid _ k)
pos :
  ∀ (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
neg :
  ∀ (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
⊢ 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

Tactic:
by_cases ha : ∃ i, q ^ i = a