match ex_t with
 | Exists.intro w h =>
   exists w
   simp [equiv]
   exact h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
⊢ ∃ t, Q t
no goals