Theorem: flformat_to_fformat (HOLFloat/Float.lean)

State before:
float : flformat
⊢ is_valid_fformat ↑float
Tactic:
apply And.intro
State after:
case left
float : flformat
⊢ 1 < (↑float).r

case right
float : flformat
⊢ (↑float).r % 2 = 0 ∧ 0 < (↑float).p

State before:
float : flformat
⊢ 1 < (↑float).r
Tactic:
case left => 
  exact float.prop.left
State after:
no goals

State before:
float : flformat
⊢ (↑float).r % 2 = 0 ∧ 0 < (↑float).p
Tactic:
case right => 
  apply And.intro
  case left  =>
    exact float.prop.right.left
  case right =>
    apply Int.one_lt_zero_lt
    exact float.prop.right.right
State after:
no goals

State before:
float : flformat
⊢ 1 < (↑float).r
Tactic:
exact float.prop.left
State after:
no goals

State before:
float : flformat
⊢ (↑float).r % 2 = 0 ∧ 0 < (↑float).p
Tactic:
apply And.intro
State after:
case left
float : flformat
⊢ (↑float).r % 2 = 0

case right
float : flformat
⊢ 0 < (↑float).p

State before:
float : flformat
⊢ (↑float).r % 2 = 0
Tactic:
case left  =>
  exact float.prop.right.left
State after:
no goals

State before:
float : flformat
⊢ 0 < (↑float).p
Tactic:
case right =>
  apply Int.one_lt_zero_lt
  exact float.prop.right.right
State after:
no goals

State before:
float : flformat
⊢ (↑float).r % 2 = 0
Tactic:
exact float.prop.right.left
State after:
no goals

State before:
float : flformat
⊢ 0 < (↑float).p
Tactic:
apply Int.one_lt_zero_lt
State after:
case a
float : flformat
⊢ 1 < (↑float).p

State before:
case a
float : flformat
⊢ 1 < (↑float).p
Tactic:
exact float.prop.right.right
State after:
no goals