case none
α : Type u_1
β : Type u_2
γ : Type ?u.11082
δ : Type ?u.11085
p : α → Prop
f✝ : (a : α) → p a → β
f : (a : α) → a ∈ none → Option β
h' : ∀ (a : α) (H : a ∈ none), f a H = none → none = none
⊢ pbind none f = none ↔ none = none

case some
α : Type u_1
β : Type u_2
γ : Type ?u.11082
δ : Type ?u.11085
p : α → Prop
f✝ : (a : α) → p a → β
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
⊢ pbind (some val✝) f = none ↔ some val✝ = none
α : Type u_1
β : Type u_2
γ : Type ?u.11082
δ : Type ?u.11085
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : (a : α) → a ∈ x → Option β
h' : ∀ (a : α) (H : a ∈ x), f a H = none → x = none
⊢ pbind x f = none ↔ x = none
cases x
no goals
case none
α : Type u_1
β : Type u_2
γ : Type ?u.11082
δ : Type ?u.11085
p : α → Prop
f✝ : (a : α) → p a → β
f : (a : α) → a ∈ none → Option β
h' : ∀ (a : α) (H : a ∈ none), f a H = none → none = none
⊢ pbind none f = none ↔ none = none
simp
case some
α : Type u_1
β : Type u_2
γ : Type ?u.11082
δ : Type ?u.11085
p : α → Prop
f✝ : (a : α) → p a → β
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
⊢ ¬f val✝ (_ : some val✝ = some val✝) = none
case some
α : Type u_1
β : Type u_2
γ : Type ?u.11082
δ : Type ?u.11085
p : α → Prop
f✝ : (a : α) → p a → β
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
⊢ pbind (some val✝) f = none ↔ some val✝ = none
simp only [pbind, iff_false]
case some
α : Type u_1
β : Type u_2
γ : Type ?u.11082
δ : Type ?u.11085
p : α → Prop
f✝ : (a : α) → p a → β
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
h : f val✝ (_ : some val✝ = some val✝) = none
⊢ False
case some
α : Type u_1
β : Type u_2
γ : Type ?u.11082
δ : Type ?u.11085
p : α → Prop
f✝ : (a : α) → p a → β
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
⊢ ¬f val✝ (_ : some val✝ = some val✝) = none
intro h
no goals
case some
α : Type u_1
β : Type u_2
γ : Type ?u.11082
δ : Type ?u.11085
p : α → Prop
f✝ : (a : α) → p a → β
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
h : f val✝ (_ : some val✝ = some val✝) = none
⊢ False
cases h' _ rfl h