feat(LinearAlgebra/AffineSpace): affine maps/equivs determined by values on spanning sets (#30949)

This PR adds extensionality lemmas showing that affine maps and equivalences are uniquely determined by their values on any set that affinely spans the entire space.

All theorems are in `Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic`:

- `AffineMap.linear_eqOn_vectorSpan`: If two affine maps agree on a set, their linear parts agree on the vector span
- `AffineMap.eqOn_affineSpan`: Two affine maps which agree on a set, agree on its affine span
- `AffineMap.ext_on`: If two affine maps agree on a set that spans the entire space, they are equal
- `AffineEquiv.ext_on`: If two affine equivalences agree on a set that spans the entire space, they are equal (generalized to work between different spaces)

Extracted from #30854.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: jessealama

Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean

@@ -594,10 +594,40 @@ theorem span_eq_top_of_surjective {s : Set P₁} (hf : Function.Surjective f)
     (h : affineSpan k s = ⊤) : affineSpan k (f '' s) = ⊤ := by
   rw [← AffineSubspace.map_span, h, map_top_of_surjective f hf]
 
+/-- If two affine maps agree on a set, their linear parts agree on the vector span of that set. -/
+theorem linear_eqOn_vectorSpan {V₂ P₂ : Type*} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂]
+    {s : Set P₁} {f g : P₁ →ᵃ[k] P₂}
+    (h_agree : s.EqOn f g) : Set.EqOn f.linear g.linear (vectorSpan k s) := by
+  simp only [vectorSpan_def]
+  apply LinearMap.eqOn_span
+  rintro - ⟨x, hx, y, hy, rfl⟩
+  simp [h_agree hx, h_agree hy]
+
+/-- Two affine maps which agree on a set, agree on its affine span. -/
+theorem eqOn_affineSpan {V₂ P₂ : Type*} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂]
+    {s : Set P₁} {f g : P₁ →ᵃ[k] P₂}
+    (h_agree : s.EqOn f g) : Set.EqOn f g (affineSpan k s) := by
+  rcases s.eq_empty_or_nonempty with rfl | ⟨q, hq⟩; · simp
+  rintro - ⟨x, hx, y, hy, rfl⟩
+  simp [h_agree hx, linear_eqOn_vectorSpan h_agree hy]
+
+/-- If two affine maps agree on a set that spans the entire space, then they are equal. -/
+theorem ext_on {V₂ P₂ : Type*} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂]
+    {s : Set P₁} {f g : P₁ →ᵃ[k] P₂}
+    (h_span : affineSpan k s = ⊤)
+    (h_agree : s.EqOn f g) : f = g := by
+  simpa [h_span]  using eqOn_affineSpan h_agree
+
 end AffineMap
 
 namespace AffineEquiv
 
+/-- If two affine equivalences agree on a set that spans the entire space, then they are equal. -/
+theorem ext_on {V₂ P₂ : Type*} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂]
+    {s : Set P₁} (h_span : affineSpan k s = ⊤)
+    (T₁ T₂ : P₁ ≃ᵃ[k] P₂) (h_agree : s.EqOn T₁ T₂) : T₁ = T₂ :=
+  (AffineEquiv.toAffineMap_inj).mp <| AffineMap.ext_on h_span h_agree
+
 section ofEq
 variable (S₁ S₂ : AffineSubspace k P₁) [Nonempty S₁] [Nonempty S₂]