-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
@[to_additive tsum_eq_tsum_primes_add_tsum_primes_of_support_subset_prime_powers]
lemma tprod_eq_tprod_primes_mul_tprod_primes_of_mulSupport_subset_prime_powers {f : ℕ → α}
    (hfm : Multipliable f) (hf : Function.mulSupport f ⊆ {n | IsPrimePow n}) :
    ∏' n : ℕ, f n = (∏' p : Nat.Primes, f p) *  ∏' (p : Nat.Primes) (k : ℕ), f (p ^ (k + 2))

Proof state:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable fun k => f (↑p ^ (k + 1))
⊢ ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 1)) =
    (∏' (p : Nat.Primes), f ↑p) * ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 2))

Tactic:
conv_lhs =>
  enter [1, p]; rw [tprod_eq_zero_mul (hfs' p), zero_add, pow_one]
  enter [2, 1, k]; rw [add_assoc, one_add_one_eq_two]

Result:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable fun k => f (↑p ^ (k + 1))
⊢ ∏' (p : Nat.Primes), f ↑p * ∏' (k : ℕ), f (↑p ^ (k + 2)) =
    (∏' (p : Nat.Primes), f ↑p) * ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 2))

Proof state:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
⊢ ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 1)) =
    (∏' (p : Nat.Primes), f ↑p) * ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 2))

Tactic:
have hfs' (p : Nat.Primes) : Multipliable fun k : ℕ ↦ f (p ^ (k + 1)) :=
  hfm.comp_injective <| (strictMono_nat_of_lt_succ
    fun k ↦ pow_lt_pow_right₀ p.prop.one_lt <| lt_add_one (k + 1)).injective

Result:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable fun k => f (↑p ^ (k + 1))
⊢ ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 1)) =
    (∏' (p : Nat.Primes), f ↑p) * ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 2))

Proof state:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
⊢ ∏' (n : ℕ), f n = (∏' (p : Nat.Primes), f ↑p) * ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 2))

Tactic:
rw [tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers hfm hf]

Result:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
⊢ ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 1)) =
    (∏' (p : Nat.Primes), f ↑p) * ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 2))

Proof state:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable fun k => f (↑p ^ (k + 1))
⊢ ∏' (p : Nat.Primes), f ↑p * ∏' (k : ℕ), f (↑p ^ (k + 2)) =
    (∏' (p : Nat.Primes), f ↑p) * ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 2))

Tactic:
exact tprod_mul (Multipliable.subtype hfm _) <|
  Multipliable.prod (f := fun (pk : Nat.Primes × ℕ) ↦ f (pk.1 ^ (pk.2 + 2))) <|
  hfm.comp_injective <| Subtype.val_injective |>.comp
  Nat.Primes.prodNatEquiv.injective |>.comp <|
  Function.Injective.prodMap (fun ⦃_ _⦄ a ↦ a) <| add_left_injective 1

Result:
no goals