A way to do it would be to reify first-order formulas as an inductive type. Then you would define two interpretations of these formulas: one over the real numbers and the other one over the hyperreal numbers. And finally, you would prove that, for any first-order formula, the former interpretation implies the latter, by induction on the reified formula. This is not so different from manually using the properties of ultrapowers, except that you do it once and for all. Later, you can just reify whatever formula you want to prove, which can be done automatically if needed (e.g., in Ltac), and then apply this transfer theorem.
2 Likes