case h
α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ x ∈ val '' {x | ↑x ∈ t} ↔ x ∈ t
α : Type u_1
s t : Set α
h : t ⊆ s
⊢ val '' {x | ↑x ∈ t} = t
ext x
case h
α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ (∃ x_1, x_1 ∈ {x | ↑x ∈ t} ∧ ↑x_1 = x) ↔ x ∈ t
case h
α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ x ∈ val '' {x | ↑x ∈ t} ↔ x ∈ t
rw [Set.mem_image]
no goals
case h
α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ (∃ x_1, x_1 ∈ {x | ↑x ∈ t} ∧ ↑x_1 = x) ↔ x ∈ t
exact ⟨fun ⟨_, hx', hx⟩ => hx ▸ hx', fun hx => ⟨⟨x, h hx⟩, hx, rfl⟩⟩