Theorem: Set.Subset.image_val_preimage_val_eq (Matroid/ForMathlib/PreimageVal.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
s x : Set α
hsx : x ⊆ s
⊢ ↑(s ↓∩ x) = x
Tactic:
simpa
State after:
no goals