mathlib3

16fb8e26 - chore(model_theory/terms_and_formulas): `realize_to_prenex` (#12884)

chore(model_theory/terms_and_formulas): `realize_to_prenex` (#12884) Proves that `phi.to_prenex` has the same realization in a nonempty structure as the original formula `phi` directly, rather than using `semantically_equivalent`.