Theorem: ieee_to_flformat (HOLFloat/IEEE.lean)

State before:
fmt : ieee_format
⊢ is_valid_flformat (mk_format fmt)
Tactic:
have h := fmt.prop
State after:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ is_valid_flformat (mk_format fmt)

State before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ is_valid_flformat (mk_format fmt)
Tactic:
apply And.intro
State after:
case left
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ 1 < (mk_format fmt).r

case right
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ (mk_format fmt).r % 2 = 0 ∧ 1 < (mk_format fmt).p

State before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ 1 < (mk_format fmt).r
Tactic:
case left =>
  apply h.left
State after:
no goals

State before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ (mk_format fmt).r % 2 = 0 ∧ 1 < (mk_format fmt).p
Tactic:
case right =>
  apply And.intro
  case left =>
    apply h.right.left
  case right =>
    apply h.right.right.left
State after:
no goals

State before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ 1 < (mk_format fmt).r
Tactic:
apply h.left
State after:
no goals

State before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ (mk_format fmt).r % 2 = 0 ∧ 1 < (mk_format fmt).p
Tactic:
apply And.intro
State after:
case left
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ (mk_format fmt).r % 2 = 0

case right
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ 1 < (mk_format fmt).p

State before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ (mk_format fmt).r % 2 = 0
Tactic:
case left =>
  apply h.right.left
State after:
no goals

State before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ 1 < (mk_format fmt).p
Tactic:
case right =>
  apply h.right.right.left
State after:
no goals

State before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ (mk_format fmt).r % 2 = 0
Tactic:
apply h.right.left
State after:
no goals

State before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ 1 < (mk_format fmt).p
Tactic:
apply h.right.right.left
State after:
no goals