Theorem: fformat_radix_ipow_le_0 (HOLFloat/Fixed_theroem.lean)

State before:
fmt : fformat
e : ℤ
⊢ (↑fmt).r ^ e ≠ 0
Tactic:
simp [HPow.hPow, Pow.pow, pow_int]
State after:
fmt : fformat
e : ℤ
⊢ ¬↑(↑fmt).r ^ e = 0

State before:
fmt : fformat
e : ℤ
⊢ ¬↑(↑fmt).r ^ e = 0
Tactic:
cases e with
| ofNat n =>
  simp [pow_ne_zero]
| negSucc n =>
simp_all only [zpow_negSucc, inv_eq_zero, add_pos_iff, or_true, pow_eq_zero_iff, Int.cast_eq_zero, fformat_radix_lt_1,
  gt_zero_ne_zero, not_false_iff]
State after:
no goals

State before:
case ofNat
fmt : fformat
n : ℕ
⊢ ¬↑(↑fmt).r ^ Int.ofNat n = 0
Tactic:
simp [pow_ne_zero]
State after:
no goals

State before:
case negSucc
fmt : fformat
n : ℕ
⊢ ¬↑(↑fmt).r ^ Int.negSucc n = 0
Tactic:
simp_all only [zpow_negSucc, inv_eq_zero, add_pos_iff, or_true, pow_eq_zero_iff, Int.cast_eq_zero, fformat_radix_lt_1,
gt_zero_ne_zero, not_false_iff]
State after:
no goals