Theorem: fformat_radix_ne_0 (HOLFloat/Fixed_theroem.lean)

State before:
⊢ ∀ (fmt : fformat), (↑fmt).r ≠ 0
Tactic:
intro h
State after:
h : fformat
⊢ (↑h).r ≠ 0

State before:
h : fformat
⊢ (↑h).r ≠ 0
Tactic:
have h₁ := h.prop.left
State after:
h : fformat
h₁ : 1 < (↑h).r
⊢ (↑h).r ≠ 0

State before:
h : fformat
h₁ : 1 < (↑h).r
⊢ (↑h).r ≠ 0
Tactic:
apply gt_zero_ne_zero
State after:
case a
h : fformat
h₁ : 1 < (↑h).r
⊢ 1 < (↑h).r

State before:
case a
h : fformat
h₁ : 1 < (↑h).r
⊢ 1 < (↑h).r
Tactic:
trivial
State after:
no goals