Theorem: is_greatest_e_exist_greatest_e (HOLFloat/Float_theorem.lean)

State before:
x : ℝ
fmt : flformat
e : ℤ
⊢ x ≠ 0 → is_greatest_e fmt x e → greatest_e fmt x = e
Tactic:
intro hx he
State after:
x : ℝ
fmt : flformat
e : ℤ
hx : x ≠ 0
he : is_greatest_e fmt x e
⊢ greatest_e fmt x = e

State before:
x : ℝ
fmt : flformat
e : ℤ
hx : x ≠ 0
he : is_greatest_e fmt x e
⊢ greatest_e fmt x = e
Tactic:
simp_all only [is_greatest_e, greatest_e]
State after:
x : ℝ
fmt : flformat
e : ℤ
hx : x ≠ 0
he : ↑(↑fmt).r ^ e ≤ abs x ∧ ∀ (e' : ℤ), ↑(↑fmt).r ^ e' ≤ abs x → e' ≤ e
⊢ supₛ { z | ↑(↑fmt).r ^ z ≤ abs x } = e

State before:
x : ℝ
fmt : flformat
e : ℤ
hx : x ≠ 0
he : ↑(↑fmt).r ^ e ≤ abs x ∧ ∀ (e' : ℤ), ↑(↑fmt).r ^ e' ≤ abs x → e' ≤ e
⊢ supₛ { z | ↑(↑fmt).r ^ z ≤ abs x } = e
Tactic:
sorry
State after:
no goals