Theorem: float_ipow_le_real_2 (HOLFloat/Float_theorem.lean)

State before:
fmt : flformat
x : ℝ
⊢ 0 < x → ∃ e, x ≤ ↑(↑fmt).r ^ e
Tactic:
intros
State after:
fmt : flformat
x : ℝ
a✝ : 0 < x
⊢ ∃ e, x ≤ ↑(↑fmt).r ^ e

State before:
fmt : flformat
x : ℝ
a✝ : 0 < x
⊢ ∃ e, x ≤ ↑(↑fmt).r ^ e
Tactic:
apply ipow_le_real
State after:
case a
fmt : flformat
x : ℝ
a✝ : 0 < x
⊢ 2 ≤ ↑(↑fmt).r

State before:
case a
fmt : flformat
x : ℝ
a✝ : 0 < x
⊢ 2 ≤ ↑(↑fmt).r
Tactic:
simp_all only [flformat_radix_le_2_real]
State after:
no goals