no goals
k : Type u_1
V₁ : Type u_4
P₁ : Type u_2
V₂ : Type u_5
P₂ : Type u_3
V₃ : Type ?u.642758
P₃ : Type ?u.642761
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 : P₁ ≃ᵃ[k] P₂
s : Set P₂
⊢ comap (↑f) (affineSpan k s) = affineSpan k (↑f ⁻¹' s)
rw [← map_symm, map_span, AffineEquiv.coe_coe, f.image_symm]