Theorem: fformat_radix_lt_0 (HOLFloat/Fixed_theroem.lean)

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

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

State before:
h : fformat
h₁ : 1 < (↑h).r
⊢ 0 < (↑h).r
Tactic:
have h₂ : 0 < (1 : Int) := by trivial
State after:
h : fformat
h₁ : 1 < (↑h).r
h₂ : 0 < 1
⊢ 0 < (↑h).r

State before:
h : fformat
h₁ : 1 < (↑h).r
h₂ : 0 < 1
⊢ 0 < (↑h).r
Tactic:
apply Int.lt_trans h₂ h₁
State after:
no goals

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