Theorem: Option.coe_part_dom (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
x : Option α
⊢ (↑x).Dom ↔ isSome x = true
Tactic:
cases x <;> simp
State after:
no goals