match ap with
| Subtype.mk a' p =>
  simp
  apply And.intro
  . exact p
  . match (ex a' p) with
    | Exists.intro b ⟨pb, qb⟩ => exists (Subtype.mk b pb)
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
ap : { x // P x }
⊢ ∃ b, P ap.val ∧ Q ap.val b.val
no goals