case none
α✝ : Type ?u.10143
β : Type ?u.10146
γ : Type ?u.10149
α : Type u_1
h₁ : (↑Option.none).Dom
h₂ : { Dom := Option.isSome Option.none = true, get := Option.get Option.none }.Dom
⊢ get (↑Option.none) h₁ = get { Dom := Option.isSome Option.none = true, get := Option.get Option.none } h₂

case some
α✝ : Type ?u.10143
β : Type ?u.10146
γ : Type ?u.10149
α : Type u_1
val✝ : α
h₁ : (↑(Option.some val✝)).Dom
h₂ : { Dom := Option.isSome (Option.some val✝) = true, get := Option.get (Option.some val✝) }.Dom
⊢ get (↑(Option.some val✝)) h₁ =
    get { Dom := Option.isSome (Option.some val✝) = true, get := Option.get (Option.some val✝) } h₂
α✝ : Type ?u.10143
β : Type ?u.10146
γ : Type ?u.10149
α : Type u_1
o : Option α
h₁ : (↑o).Dom
h₂ : { Dom := Option.isSome o = true, get := Option.get o }.Dom
⊢ get (↑o) h₁ = get { Dom := Option.isSome o = true, get := Option.get o } h₂
cases o
case some
α✝ : Type ?u.10143
β : Type ?u.10146
γ : Type ?u.10149
α : Type u_1
val✝ : α
h₁ : (↑(Option.some val✝)).Dom
h₂ : { Dom := Option.isSome (Option.some val✝) = true, get := Option.get (Option.some val✝) }.Dom
⊢ get (↑(Option.some val✝)) h₁ =
    get { Dom := Option.isSome (Option.some val✝) = true, get := Option.get (Option.some val✝) } h₂
case none
α✝ : Type ?u.10143
β : Type ?u.10146
γ : Type ?u.10149
α : Type u_1
h₁ : (↑Option.none).Dom
h₂ : { Dom := Option.isSome Option.none = true, get := Option.get Option.none }.Dom
⊢ get (↑Option.none) h₁ = get { Dom := Option.isSome Option.none = true, get := Option.get Option.none } h₂

case some
α✝ : Type ?u.10143
β : Type ?u.10146
γ : Type ?u.10149
α : Type u_1
val✝ : α
h₁ : (↑(Option.some val✝)).Dom
h₂ : { Dom := Option.isSome (Option.some val✝) = true, get := Option.get (Option.some val✝) }.Dom
⊢ get (↑(Option.some val✝)) h₁ =
    get { Dom := Option.isSome (Option.some val✝) = true, get := Option.get (Option.some val✝) } h₂
. simp at h₂
no goals
case some
α✝ : Type ?u.10143
β : Type ?u.10146
γ : Type ?u.10149
α : Type u_1
val✝ : α
h₁ : (↑(Option.some val✝)).Dom
h₂ : { Dom := Option.isSome (Option.some val✝) = true, get := Option.get (Option.some val✝) }.Dom
⊢ get (↑(Option.some val✝)) h₁ =
    get { Dom := Option.isSome (Option.some val✝) = true, get := Option.get (Option.some val✝) } h₂
. rfl
no goals
case none
α✝ : Type ?u.10143
β : Type ?u.10146
γ : Type ?u.10149
α : Type u_1
h₁ : (↑Option.none).Dom
h₂ : { Dom := Option.isSome Option.none = true, get := Option.get Option.none }.Dom
⊢ get (↑Option.none) h₁ = get { Dom := Option.isSome Option.none = true, get := Option.get Option.none } h₂
simp at h₂
no goals
case some
α✝ : Type ?u.10143
β : Type ?u.10146
γ : Type ?u.10149
α : Type u_1
val✝ : α
h₁ : (↑(Option.some val✝)).Dom
h₂ : { Dom := Option.isSome (Option.some val✝) = true, get := Option.get (Option.some val✝) }.Dom
⊢ get (↑(Option.some val✝)) h₁ =
    get { Dom := Option.isSome (Option.some val✝) = true, get := Option.get (Option.some val✝) } h₂
rfl