case none
α : Type u_1
β : Type ?u.7014
γ : Type ?u.7017
δ : Type ?u.7020
a b : α
h : none ≠ ⊥
⊢ ↑(unbot none h) = none

case some
α : Type u_1
β : Type ?u.7014
γ : Type ?u.7017
δ : Type ?u.7020
a b val✝ : α
h : Option.some val✝ ≠ ⊥
⊢ ↑(unbot (Option.some val✝) h) = Option.some val✝
α : Type u_1
β : Type ?u.7014
γ : Type ?u.7017
δ : Type ?u.7020
a b : α
x : WithBot α
h : x ≠ ⊥
⊢ ↑(unbot x h) = x
cases x
case some
α : Type u_1
β : Type ?u.7014
γ : Type ?u.7017
δ : Type ?u.7020
a b val✝ : α
h : Option.some val✝ ≠ ⊥
⊢ ↑(unbot (Option.some val✝) h) = Option.some val✝
case none
α : Type u_1
β : Type ?u.7014
γ : Type ?u.7017
δ : Type ?u.7020
a b : α
h : none ≠ ⊥
⊢ ↑(unbot none h) = none

case some
α : Type u_1
β : Type ?u.7014
γ : Type ?u.7017
δ : Type ?u.7020
a b val✝ : α
h : Option.some val✝ ≠ ⊥
⊢ ↑(unbot (Option.some val✝) h) = Option.some val✝
exact (h rfl).elim
no goals
case some
α : Type u_1
β : Type ?u.7014
γ : Type ?u.7017
δ : Type ?u.7020
a b val✝ : α
h : Option.some val✝ ≠ ⊥
⊢ ↑(unbot (Option.some val✝) h) = Option.some val✝
rfl