Theorem: SciLean.re_float (SciLean/Core/FloatAsReal.lean)

State before:
a : Float
⊢ ↑(RCLike.re a) = a
Tactic:
sorry_proof
State after:
no goals