constructor
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, ⋯⟩
case h.mp
α✝ : 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_2, (∃ (x : a_2 ∈ a), ⟨a_2, ⋯⟩ ∈ u) ∧ ∃ (x_2 : a_2 ∈ s), e ⟨a_2, ⋯⟩ = ⟨x, ⋯⟩

case h.mpr
α✝ : 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_1 : x ∈ t), ∃ a_1, (∃ (x : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u) ∧ ∃ (x_2 : a_1 ∈ s), e ⟨a_1, ⋯⟩ = ⟨x, ⋯⟩) →
    x ∈ b ∧ ∃ a_2, ∃ (h : a_2 ∈ a), ⟨a_2, ⋯⟩ ∈ u ∧ ↑(e ⟨a_2, ⋯⟩) = x