α : Type u_1
β : Type u_2
γ : Type ?u.7041
δ : Type ?u.7044
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha✝ : a ∈ x
ha : x = some a
⊢ pmap f x h = some (f a (_ : p a))
α : Type u_1
β : Type u_2
γ : Type ?u.7041
δ : Type ?u.7044
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha : a ∈ x
⊢ f a (_ : p a) ∈ pmap f x h
rw [mem_def] at ha ⊢
α : Type u_1
β : Type u_2
γ : Type ?u.7041
δ : Type ?u.7044
p : α → Prop
f : (a : α) → p a → β
a : α
h : ∀ (a_1 : α), a_1 ∈ some a → p a_1
ha : a ∈ some a
⊢ pmap f (some a) h = some (f a (_ : p a))
α : Type u_1
β : Type u_2
γ : Type ?u.7041
δ : Type ?u.7044
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha✝ : a ∈ x
ha : x = some a
⊢ pmap f x h = some (f a (_ : p a))
subst ha
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.7041
δ : Type ?u.7044
p : α → Prop
f : (a : α) → p a → β
a : α
h : ∀ (a_1 : α), a_1 ∈ some a → p a_1
ha : a ∈ some a
⊢ pmap f (some a) h = some (f a (_ : p a))
rfl