@[simp]

theorem Set.image_val_image_val_eq {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (x : Set ↑s) : Subtype.val '' (fun (x : ↑s) => ⟨f ↑x, ⋯⟩) '' x = f '' Subtype.val '' x

theorem Set.image_val_eq_coe {α : Type u_1} (s : Set α) (x : Set ↑s) : (fun (a : ↑s) => ↑a) '' x = Subtype.val '' x

@[simp]

theorem Set.image_val_image_eq {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set ↑s) (f : α → β) : (fun (x : ↑s) => f ↑x) '' t = f '' Subtype.val '' t

theorem Set.Subset.eq_image_val {α : Type u_1} {s x : Set α} (hsx : x ⊆ s) : ∃ (y : Set ↑s), x = Subtype.val '' y

theorem Set.Subset.image_val_preimage_val_eq {α : Type u_1} {s x : Set α} (hsx : x ⊆ s) : Subtype.val '' Subtype.val ⁻¹' x = x