no goals
α✝ : Type ?u.9780
β : Type ?u.9783
γ : Type ?u.9786
α : Type u_1
⊢ (↑Option.none).Dom ↔ Option.isSome Option.none = true
simp [ofOption, none]
no goals
α✝ : Type ?u.9780
β : Type ?u.9783
γ : Type ?u.9786
α : Type u_1
a : α
⊢ (↑(Option.some a)).Dom ↔ Option.isSome (Option.some a) = true
simp [ofOption]