Theorem: Set.image_val_image_val_eq (Matroid/ForMathlib/PreimageVal.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s : Set α
x : Set ↑s
⊢ ↑((fun x => ⟨f ↑x, ⋯⟩) '' x) = f '' ↑x
Tactic:
aesop
State after:
no goals