eq_iff_toReal_eq
plain-language theorem explainer
The biconditional equates equality of recovered reals with equality of their images under the transport to Mathlib reals. Workers on the Recognition Science foundation cite it to justify pulling back every real-number identity along the embedding. The term proof applies congrArg in one direction and the round-trip fromReal_toReal in the other.
Claim. Let $x,y$ be elements of the recovered real line LogicReal. Then $x=y$ if and only if toReal$(x)=$toReal$(y)$, where toReal is the canonical comparison map into the standard reals.
background
LogicReal wraps Mathlib's Bourbaki completion of the rationals, taking its input from the equivalence LogicRat ≃ ℚ recovered from the Law of Logic. The map toReal realizes the comparison equivalence CompareReals.compareEquiv while fromReal supplies the inverse transport. The module documentation states that algebra on LogicReal is obtained by pullback along toReal so every downstream theorem reduces to an existing real theorem.
proof idea
The proof constructs the biconditional explicitly. One direction is the congruence of toReal. The converse applies fromReal to the assumed equality of images and rewrites both sides via the two instances of fromReal_toReal.
why it matters
This lemma is invoked by fourteen downstream declarations, including the transported addition laws add_assoc' and add_comm' as well as the transcendental identities expL_logL and coshL_eq_exp. It implements the transport-first API of the RealsFromLogic module and supplies the embedding step required once the rationals have been recovered from the Law of Logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.