Theorem: LSeries.mul_convolution_distrib (EulerProducts/DirichletLSeries.lean)

State before:
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
⊢ φ * (f ⍟ g) = φ * f ⍟ (φ * g)
Tactic:
ext n
State after:
case h
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
n : ℕ
⊢ (φ * (f ⍟ g)) n = (φ * f ⍟ (φ * g)) n

State before:
case h
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
n : ℕ
⊢ (φ * (f ⍟ g)) n = (φ * f ⍟ (φ * g)) n
Tactic:
simp only [Pi.mul_apply, LSeries.convolution_def, Finset.mul_sum]
State after:
case h
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
n : ℕ
⊢ ∑ i ∈ n.divisorsAntidiagonal, φ n * (f i.1 * g i.2) = ∑ x ∈ n.divisorsAntidiagonal, φ x.1 * f x.1 * (φ x.2 * g x.2)

State before:
case h
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
n : ℕ
⊢ ∑ i ∈ n.divisorsAntidiagonal, φ n * (f i.1 * g i.2) = ∑ x ∈ n.divisorsAntidiagonal, φ x.1 * f x.1 * (φ x.2 * g x.2)
Tactic:
refine Finset.sum_congr rfl fun p hp ↦ ?_
State after:
case h
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ φ n * (f p.1 * g p.2) = φ p.1 * f p.1 * (φ p.2 * g p.2)

State before:
case h
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ φ n * (f p.1 * g p.2) = φ p.1 * f p.1 * (φ p.2 * g p.2)
Tactic:
rw [(Nat.mem_divisorsAntidiagonal.mp hp).1.symm, hφ]
State after:
case h
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ φ p.1 * φ p.2 * (f p.1 * g p.2) = φ p.1 * f p.1 * (φ p.2 * g p.2)

State before:
case h
R : Type u_1
inst✝ : CommSemiring R
φ : ℕ → R
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ φ p.1 * φ p.2 * (f p.1 * g p.2) = φ p.1 * f p.1 * (φ p.2 * g p.2)
Tactic:
exact mul_mul_mul_comm ..
State after:
no goals