no goals
k : Type u_5
V₁ : Type u_3
P₁ : Type u_1
V₂ : Type u_4
P₂ : Type u_2
V₃ : Type ?u.579305
P₃ : Type ?u.579308
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₁
hf : Function.Surjective ↑f
h : affineSpan k s = ⊤
⊢ affineSpan k (↑f '' s) = ⊤
rw [← AffineSubspace.map_span, h, map_top_of_surjective f hf]