Theorem: ipow_le_real (HOLFloat/Common.lean)

State before:
r z : ℝ
⊢ 2 ≤ r → ∃ e, z ≤ r ^ e
Tactic:
intros h
State after:
r z : ℝ
h : 2 ≤ r
⊢ ∃ e, z ≤ r ^ e

State before:
r z : ℝ
h : 2 ≤ r
⊢ ∃ e, z ≤ r ^ e
Tactic:
sorry
State after:
no goals