Induction over products is too strong?

Stream: new members

[Riley Riles]

Hi! I'd like to prove a theorem of the following form.

import  Mathlib
have n : ℕ
set numDivisors := (fun n => n.divisors.card)
set P := (fun n => ∃ j, numDivisors n = 2^j)
have pVal : ℕ → ℕ := sorry -- the details of this function are irrelevant, it just spits out a natural number
have thingIWantToProve : P (∏ x ∈ n.primeFactors, x ^ (2 ^ (pVal x + 1) - 1))

Attempting to use Finset.prod_induction seems to be the most natural choice. However, the description of FInset.prod_induction is

theorem Finset.prod_induction{α : Type u_3} {s : Finset α} {M : Type u_6} [CommMonoid M] (f : α → M) (p : M → Prop) (hom : ∀ (a b : M), p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ s, p (f x)) :
p (∏ x ∈ s, f x)

This has the serious issue that it requires hom to be true of all M, and I cannot seem to limit the scope of this. Unfortunately, P is only true multiplicatively over coprimes, which is not a problem for the purpose of proving this theorem but stops me from using Finset.prod_induction. How should I proceed?

[Riley Riles]

SOLVED: By searching Loogle for "Finset.prod, 'induction'" I found this theorem which appears to be suitable: UniqueFactorizationMonoid.induction_on_prime_power

[Eric Wieser]

Please post a #mwe next time, your code above does not compile

[Eric Wieser]

As a more general strategy, induction h : n.primeFactors using Finset.cons_induction generalizing n works here