Theorem: float_radix_ipow_lt_0 (HOLFloat/Float_theorem.lean)

State before:
fmt : flformat
e : ℤ
⊢ 0 < ↑(↑fmt).r ^ e
Tactic:
have h : 0 < fmt.val.r := by apply Int.one_lt_zero_lt; exact fmt.prop.left
State after:
fmt : flformat
e : ℤ
h : 0 < (↑fmt).r
⊢ 0 < ↑(↑fmt).r ^ e

State before:
fmt : flformat
e : ℤ
h : 0 < (↑fmt).r
⊢ 0 < ↑(↑fmt).r ^ e
Tactic:
apply ipow_lt_zero
State after:
case a
fmt : flformat
e : ℤ
h : 0 < (↑fmt).r
⊢ 0 < ↑(↑fmt).r

State before:
case a
fmt : flformat
e : ℤ
h : 0 < (↑fmt).r
⊢ 0 < ↑(↑fmt).r
Tactic:
simp_all only [Int.one_lt_zero_le_iff, zero_add, Int.cast_pos]
State after:
no goals

State before:
fmt : flformat
e : ℤ
⊢ 0 < (↑fmt).r
Tactic:
apply Int.one_lt_zero_lt
State after:
case a
fmt : flformat
e : ℤ
⊢ 1 < (↑fmt).r

State before:
case a
fmt : flformat
e : ℤ
⊢ 1 < (↑fmt).r
Tactic:
exact fmt.prop.left
State after:
no goals