Satisfiability modulo theories (SMT) solvers are widely used to ensure the correctness of safety- and security- critical applications. Therefore, being able to trust a solver's results is crucial. One way to increase trust is to generate proof certificates, which record the reasoning steps the solver has done. These proof certificates can be given to a proof checker which determines whether the steps in the proof are correct. One key challenge with this approach is that it is dificult to eficiently and accurately produce proofs for reasoning steps involving term rewriting rules (of which there are many in modern SMT solvers). Previous work showed how a domain-specific language, RARE, can be used to capture rewriting rules for the purposes of proof production. However, the RARE rules were trusted-i.e., the correctness of the rules themselves was not checked by the proof checker. In this paper, we present IsaRARE, a tool that can automatically generate lemmas in the interactive theorem prover Isabelle/HOL corresponding to RARE rewrite rules. The correctness of the rules can then be verified by proving the lemmas. We evaluate our approach by verifying an extensive set of rewrite rules used by the cvc5 SMT solver.