α : Type u_1
β : Type ?u.11858
γ : Type ?u.11861
ι : Sort ?u.11864
ι' : Sort ?u.11867
f : α → β
g : β → γ
p : α → Prop
s : Set (Subtype p)
t : Set α
s_eq : s = Subtype.val ⁻¹' t
x : α
h : p x
⊢ { val := x, property := h } ∈ Subtype.val ⁻¹' t ↔ x ∈ t
α : Type u_1
β : Type ?u.11858
γ : Type ?u.11861
ι : Sort ?u.11864
ι' : Sort ?u.11867
f : α → β
g : β → γ
p : α → Prop
s : Set (Subtype p)
t : Set α
s_eq : s = Subtype.val ⁻¹' t
x : α
h : p x
⊢ { val := x, property := h } ∈ s ↔ x ∈ t
rw [s_eq]
no goals
α : Type u_1
β : Type ?u.11858
γ : Type ?u.11861
ι : Sort ?u.11864
ι' : Sort ?u.11867
f : α → β
g : β → γ
p : α → Prop
s : Set (Subtype p)
t : Set α
s_eq : s = Subtype.val ⁻¹' t
x : α
h : p x
⊢ { val := x, property := h } ∈ Subtype.val ⁻¹' t ↔ x ∈ t
simp
no goals
α : Type u_1
β : Type ?u.11858
γ : Type ?u.11861
ι : Sort ?u.11864
ι' : Sort ?u.11867
f : α → β
g : β → γ
p : α → Prop
s : Set (Subtype p)
t : Set α
h : ∀ (x : α) (h : p x), { val := x, property := h } ∈ s ↔ x ∈ t
x✝ : Subtype p
x : α
hx : p x
⊢ { val := x, property := hx } ∈ s ↔ { val := x, property := hx } ∈ Subtype.val ⁻¹' t
simp [h]