no goals
α : Type u_1
β : Type u_2
γ : Type ?u.13574
δ : Type ?u.13577
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : (a : α) → p a → β
x : Option (Option α)
H : ∀ (a : Option α), a ∈ x → ∀ (a_2 : α), a_2 ∈ a → p a_2
⊢ join (pmap (pmap f) x H) = pmap f (join x) (_ : ∀ (a : α), a ∈ join x → p a)
rcases x with (_ | _ | x) <;> simp