no goals
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
V₃ : Type ?u.542331
P₃ : Type ?u.542334
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f✝ f : P₁ →ᵃ[k] P₂
x : P₂
s : AffineSubspace k P₁
⊢ x ∈ map f s ↔ ∃ y, y ∈ s ∧ ↑f y = x
simpa only [bex_def] using mem_image_iff_bex