case none
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
y : β
f : (a : α) → a ∈ none → Option β
⊢ pbind none f = some y ↔ ∃ z H, f z H = some y

case some
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ pbind (some x) f = some y ↔ ∃ z H, f z H = some y
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : (a : α) → a ∈ x → Option β
y : β
⊢ pbind x f = some y ↔ ∃ z H, f z H = some y
rcases x with (_|x)
case none
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
y : β
f : (a : α) → a ∈ none → Option β
⊢ ∀ (x : α) (x_1 : x ∈ none), ¬f x x_1 = some y
case none
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
y : β
f : (a : α) → a ∈ none → Option β
⊢ pbind none f = some y ↔ ∃ z H, f z H = some y
simp only [pbind, false_iff, not_exists]
case none
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
y : β
f : (a : α) → a ∈ none → Option β
z : α
h : z ∈ none
⊢ ¬f z h = some y
case none
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
y : β
f : (a : α) → a ∈ none → Option β
⊢ ∀ (x : α) (x_1 : x ∈ none), ¬f x x_1 = some y
intro z h
no goals
case none
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
y : β
f : (a : α) → a ∈ none → Option β
z : α
h : z ∈ none
⊢ ¬f z h = some y
simp at h
case some
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ f x (_ : some x = some x) = some y ↔ ∃ z H, f z H = some y
case some
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ pbind (some x) f = some y ↔ ∃ z H, f z H = some y
simp only [pbind]
case some
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ (∃ z H, f z H = some y) → f x (_ : some x = some x) = some y
case some
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ f x (_ : some x = some x) = some y ↔ ∃ z H, f z H = some y
refine ⟨λ h => ⟨x, rfl, h⟩, ?_⟩
case some.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
z : α
H : z ∈ some x
hz : f z H = some y
⊢ f x (_ : some x = some x) = some y
case some
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ (∃ z H, f z H = some y) → f x (_ : some x = some x) = some y
rintro ⟨z, H, hz⟩
case some.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
z : α
H✝ : z ∈ some x
hz : f z H✝ = some y
H : x = z
⊢ f x (_ : some x = some x) = some y
case some.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
z : α
H : z ∈ some x
hz : f z H = some y
⊢ f x (_ : some x = some x) = some y
simp only [mem_def, Option.some_inj] at H
no goals
case some.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.11629
δ : Type ?u.11632
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
z : α
H✝ : z ∈ some x
hz : f z H✝ = some y
H : x = z
⊢ f x (_ : some x = some x) = some y
simpa [H] using hz