English
If f is surjective, then the set of squares in the codomain is contained in the image under f of the squares in the domain.
Русский
Если f сюръективно отображает, то множество квадратов в кодомапе содержится в образе квадратов из области.
LaTeX
$$$\{b \mid \operatorname{IsSquare}(b)\} \subseteq f '' \{a \mid \operatorname{IsSquare}(a)\}$$$
Lean4
@[to_additive]
theorem isSquare_subset_image_isSquare {f : F} (hf : Function.Surjective f) :
{b | IsSquare b} ⊆ f '' {a | IsSquare a} := fun b ⟨s, _⟩ =>
by
rcases hf s with ⟨r, rfl⟩
exact ⟨r * r, by simp [*]⟩