simp [has hva, hva, hvu]
case h.mp.intro.intro.intro.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hxb : ↑(e ⟨v, ⋯⟩) ∈ b
⊢ ∃ (x : ↑(e ⟨v, ⋯⟩) ∈ t), ∃ a_1, (∃ (x : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u) ∧ ∃ (x_1 : a_1 ∈ s), e ⟨a_1, ⋯⟩ = ⟨↑(e ⟨v, ⋯⟩), ⋯⟩
no goals