  Computational reflection allows us to turn verified decision procedures into
efficient automated reasoning tools in proof assistants. The typical
applications of such methodology include mathematical structures that have
decidable theory fragments, e.g., equational theories of commutative rings and
lattices. However, such existing tools are known not to cooperate with packed
classes, a methodology to define mathematical structures in dependent type
theory, that allows for the sharing of vocabulary across the inheritance
hierarchy. Additionally, such tools do not support homomorphisms whose domain
and codomain types may differ. This paper demonstrates how to implement
reflexive tactics that support packed classes and homomorphisms. As
applications of our methodology, we adapt the ring and field tactics of Coq to
the commutative ring and field structures of the Mathematical Components
library, and apply the resulting tactics to the formal proof of the
irrationality of $\zeta(3)$ by Chyzak, Mahboubi, and Sibut-Pinote, to bring
more proof automation.
