Theorem: WithTop.isSome_iff_lt_top (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type
inst✝ : PartialOrder ι
x : WithTop ι
⊢ Option.isSome x = true ↔ x < ⊤
Tactic:
rw [← not_iff_not, Bool.eq_false_eq_not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none,
  lt_top_iff_ne_top, Ne, Classical.not_not]
State after:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type
inst✝ : PartialOrder ι
x : WithTop ι
⊢ x = none ↔ x = ⊤

State before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type
inst✝ : PartialOrder ι
x : WithTop ι
⊢ x = none ↔ x = ⊤
Tactic:
rfl
State after:
no goals