awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
ha : ∃ (i : ℕ), q ^ i = a
pos :
  ∀ (hb : ∃ (j : ℕ), q ^ j = b),
    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 :
  ∀ (hb : ¬∃ (j : ℕ), q ^ j = b),
    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 hb : ∃ j, q ^ j = b
-- 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)
ha : ∃ (i : ℕ), q ^ i = a
hb : ∃ (j : ℕ), q ^ j = b
pos :
  ∀ (i : ℕ) (hab : (q ^ i, b) ∈ (q ^ k).divisorsAntidiagonal)
    (h :
      (q ^ i, b) ∉
        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
          (q ^ i, b).1)
        (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
          (q ^ i, 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:
obtain ⟨i, rfl⟩ := ha

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 : ℕ
hs :
  Finset.map
      ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
      (@Finset.antidiagonal _ Nat.instAddMonoid _ k) ⊆
    (q ^ k).divisorsAntidiagonal
b : ℕ
hb : ∃ (j : ℕ), q ^ j = b
i : ℕ
hab : (q ^ i, b) ∈ (q ^ k).divisorsAntidiagonal
h :
  (q ^ i, b) ∉
    Finset.map
      ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
      (@Finset.antidiagonal _ Nat.instAddMonoid _ k)
pos :
  ∀ (j : ℕ) (hab : (q ^ i, q ^ j) ∈ (q ^ k).divisorsAntidiagonal)
    (h :
      (q ^ i, q ^ j) ∉
        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
          (q ^ i, q ^ j).1)
        (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
          (q ^ i, q ^ j).2) =
      0
⊢ HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0
        (q ^ i, b).1)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
        (q ^ i, b).2) =
    0

Tactic:
obtain ⟨j, rfl⟩ := hb

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 : ℕ
hs :
  Finset.map
      ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
      (@Finset.antidiagonal _ Nat.instAddMonoid _ k) ⊆
    (q ^ k).divisorsAntidiagonal
i j : ℕ
hab : (q ^ i, q ^ j) ∈ (q ^ k).divisorsAntidiagonal
h :
  (q ^ i, q ^ j) ∉
    Finset.map
      ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
      (@Finset.antidiagonal _ Nat.instAddMonoid _ k)
⊢ i + j = k ∧ q ^ k ≠ 0

Tactic:
rw [Nat.mem_divisorsAntidiagonal, ← pow_add, Nat.pow_right_inj hq] at hab

Premises used: Nat.mem_divisorsAntidiagonal, pow_add, Nat.pow_right_inj
-- 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
i j : ℕ
hab : (q ^ i, q ^ j) ∈ (q ^ k).divisorsAntidiagonal
h :
  (q ^ i, q ^ j) ∉
    Finset.map
      ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
      (@Finset.antidiagonal _ Nat.instAddMonoid _ k)
hab₁ : i + j = k ∧ q ^ k ≠ 0
⊢ (q ^ i, q ^ j) ∉
    Finset.map
      ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
      (@Finset.antidiagonal _ Nat.instAddMonoid _ k)

Tactic:
rw [Nat.mem_divisorsAntidiagonal, ← pow_add, Nat.pow_right_inj hq] at hab

Premises used: Nat.mem_divisorsAntidiagonal, pow_add, Nat.pow_right_inj
-- 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
i j : ℕ
hab : i + j = k ∧ q ^ k ≠ 0
h :
  (q ^ i, q ^ j) ∉
    Finset.map
      ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
      (@Finset.antidiagonal _ Nat.instAddMonoid _ k)
⊢ ∀ (x : ℕ × ℕ),
    x.1 + x.2 = k →
      ¬({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap
                { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ } :
              (a : ℕ × ℕ) → ℕ × ℕ)
            x =
          (q ^ i, q ^ j)

Tactic:
simp_rw [Finset.mem_map, not_exists, not_and, Finset.mem_antidiagonal] at h

Premises used: not_exists, Finset.HasAntidiagonal.mem_antidiagonal, Finset.mem_map, not_and
-- 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
i j : ℕ
hab : i + j = k ∧ q ^ k ≠ 0
h :
  ∀ (x : ℕ × ℕ),
    x.1 + x.2 = k →
      ¬({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap
                { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ } :
              (a : ℕ × ℕ) → ℕ × ℕ)
            x =
          (q ^ i, q ^ j)
⊢ HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0
        (q ^ i, q ^ j).1)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
        (q ^ i, q ^ j).2) =
    0

Tactic:
simpa using h (i, j) hab.1

Premises used: Prod.mk, And.left
-- 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)
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
neg₅ : Eq.{u_1 + 1} (α := R) 0 0
neg₆ : ¬∃ (a_1 : ℕ), q ^ a_1 = (a, b).2
neg₇ : Eq.{u_1 + 1} (α := R) 0 0
neg₈ neg₉ 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

Tactic:
rwa [mul_comm, Function.extend_apply', Pi.zero_apply, zero_mul]

Premises used: MulZeroClass.zero_mul, Pi.zero_apply, mul_comm, Function.extend_apply'
-- 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)
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
neg₄ : Eq.{u_1 + 1} (α := R) 0 0
neg₅ : ¬∃ (a_1 : ℕ), q ^ a_1 = (a, b).1
neg₆ : Eq.{u_1 + 1} (α := R) 0 0
neg₇ neg₈ 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

Tactic:
rwa [Function.extend_apply', Pi.zero_apply, zero_mul]

Premises used: MulZeroClass.zero_mul, Pi.zero_apply, Function.extend_apply'
-- 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
neg :
  ∀ 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) =
      0
⊢ 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:
rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply, Finset.sum_eq_zero]

Premises used: Finset.sum_eq_zero, Pi.zero_apply, Function.extend_apply'
-- 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
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
⊢ (a, b).1 * (a, b).2 = n

Tactic:
obtain ⟨hab, -⟩ := Nat.mem_divisorsAntidiagonal.mp hk

Premises used: Nat.mem_divisorsAntidiagonal, Iff.mp
-- 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
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
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
-- 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
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ∃ (i : ℕ), q ^ i = a
pos :
  ∀ (hb : ∃ (j : ℕ), q ^ j = b),
    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 :
  ∀ (hb : ¬∃ (j : ℕ), q ^ j = b),
    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 hb : ∃ j, q ^ j = b
-- 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
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
pos :
  ∀ (i : ℕ) (hk : (q ^ i, b) ∈ n.divisorsAntidiagonal) (hab : (q ^ i, b).1 * (q ^ i, b).2 = n),
    HMul.hMul (α := R)
        (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0
          (q ^ i, b).1)
        (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
          (q ^ i, 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:
obtain ⟨i, rfl⟩ := ha

Premises used: rfl
-- 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
b : ℕ
hb : ∃ (j : ℕ), q ^ j = b
i : ℕ
hk : (q ^ i, b) ∈ n.divisorsAntidiagonal
hab : (q ^ i, b).1 * (q ^ i, b).2 = n
pos :
  ∀ (j : ℕ) (hk : (q ^ i, q ^ j) ∈ n.divisorsAntidiagonal) (hab : (q ^ i, q ^ j).1 * (q ^ i, q ^ j).2 = n),
    HMul.hMul (α := R)
        (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0
          (q ^ i, q ^ j).1)
        (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
          (q ^ i, q ^ j).2) =
      0
⊢ HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0
        (q ^ i, b).1)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
        (q ^ i, b).2) =
    0

Tactic:
obtain ⟨j, rfl⟩ := hb

Premises used: rfl
-- 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
i j : ℕ
hk : (q ^ i, q ^ j) ∈ n.divisorsAntidiagonal
hab : (q ^ i, q ^ j).1 * (q ^ i, q ^ j).2 = n
⊢ q ^ (i + j) = n

Tactic:
rw [← pow_add] at hab

Premises used: pow_add
-- 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
i j : ℕ
hk : (q ^ i, q ^ j) ∈ n.divisorsAntidiagonal
hab : q ^ (i + j) = n
⊢ HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0
        (q ^ i, q ^ j).1)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
        (q ^ i, q ^ j).2) =
    0

Tactic:
(hn ⟨i + j, hab⟩).elim

Premises used: False.elim, HAdd.hAdd, Exists.intro
-- 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
i j : ℕ
hk : (q ^ i, q ^ j) ∈ n.divisorsAntidiagonal
hab : q ^ (i + j) = n
⊢ HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) f) 0
        (q ^ i, q ^ j).1)
      (Function.extend (fun (x : ℕ) ↦ q ^ x) (fun (x : ℕ) ↦ (PowerSeries.coeff x : (a : PowerSeries R) → R) g) 0
        (q ^ i, q ^ j).2) =
    0

Tactic:
exact (hn ⟨i + j, hab⟩).elim

Premises used: False.elim, HAdd.hAdd, Exists.intro
-- 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
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
neg₅ : Eq.{u_1 + 1} (α := R) 0 0
neg₆ : ¬∃ (a_1 : ℕ), q ^ a_1 = (a, b).2
neg₇ : Eq.{u_1 + 1} (α := R) 0 0
neg₈ neg₉ 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

Tactic:
rwa [mul_comm, Function.extend_apply', Pi.zero_apply, zero_mul]

Premises used: MulZeroClass.zero_mul, Pi.zero_apply, mul_comm, Function.extend_apply'
-- 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
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
neg₄ : Eq.{u_1 + 1} (α := R) 0 0
neg₅ : ¬∃ (a_1 : ℕ), q ^ a_1 = (a, b).1
neg₆ : Eq.{u_1 + 1} (α := R) 0 0
neg₇ neg₈ 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

Tactic:
rwa [Function.extend_apply', Pi.zero_apply, zero_mul]

Premises used: MulZeroClass.zero_mul, Pi.zero_apply, Function.extend_apply'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
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)
    ((HMul.hMul (α := 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