Theorem: Set.coe_toSubset (Sard/ToSubset.lean)

State before:
X : Type u_1
s t : Set X
⊢ Subtype.val '' s.toSubset t = s ∩ t
Tactic:
ext
State after:
case h
X : Type u_1
s t : Set X
x✝ : X
⊢ x✝ ∈ Subtype.val '' s.toSubset t ↔ x✝ ∈ s ∩ t

State before:
case h
X : Type u_1
s t : Set X
x✝ : X
⊢ x✝ ∈ Subtype.val '' s.toSubset t ↔ x✝ ∈ s ∩ t
Tactic:
sorry
State after:
no goals