simp only [mem_image, mem_image_equiv, Subtype.exists, exists_and_right, exists_eq_right,
  inclusion_mk, Subtype.mk.injEq, exists_and_right, exists_eq_right, exists_and_left,
  subsetEquivSubset, coe_fn_mk, Subtype.mk.injEq, exists_prop]
case h
α✝ : 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
x : β
⊢ x ∈ ↑(⇑(e.subsetEquivSubset has hbt h_eq) '' u) ↔ x ∈ ↑(⇑e '' (inclusion has '' u))
case h
α✝ : 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
x : β
⊢ (x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x) ↔
    ∃ (x_1 : x ∈ t), ∃ a_1, (∃ (x : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u) ∧ ∃ (x_2 : a_1 ∈ s), e ⟨a_1, ⋯⟩ = ⟨x, ⋯⟩