Theorem: float_normalize_real (HOLFloat/Float_theorem.lean)

State before:
fmt : flformat
x : ℝ
⊢ x < 0 → x = greatest_m fmt x * ↑(↑fmt).r ^ greatest_e fmt x + greatest_r fmt x
Tactic:
intro h
State after:
fmt : flformat
x : ℝ
h : x < 0
⊢ x = greatest_m fmt x * ↑(↑fmt).r ^ greatest_e fmt x + greatest_r fmt x

State before:
fmt : flformat
x : ℝ
h : x < 0
⊢ x = greatest_m fmt x * ↑(↑fmt).r ^ greatest_e fmt x + greatest_r fmt x
Tactic:
sorry
State after:
no goals