Assume that the statement we want to prove has a proof.

Can we find it with only the “standard” Coq tactics?

i.e. is programming a custom tactic ever necessary? (not sufficient is not what I care, if it has a proof this in theory could be a silly tactic that encodes the proof of the statement which is not interested)

Motivation: I recently learned that one can implement their own tactics…!