chore(Geometry/Manifold): make some doc-strings follow the style guide (#39729)

such as, by them beginning with the object they are defining as a subject.
This will yield much better doc-strings for the differential geometry elaborators in #39677.

It also increases conformance with the [documentation style guide](https://github.com/leanprover/lean4/blob/master/doc/style.md).

Inspired by the MI retreat in Lisbon.

Author: grunweg

Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

@@ -160,18 +160,22 @@ theorem contDiffWithinAtProp_id (x : H) : ContDiffWithinAtProp I I n id univ x :
   · simp only [mfld_simps]
 
 variable (I I') in
-/-- A function is `n` times continuously differentiable within a set at a point in a manifold if
-it is continuous and it is `n` times continuously differentiable in this set around this point, when
-read in the preferred chart at this point.
+/-- `ContMDiffWithinAt I I' n f x` indicates that the function `f : M → M'` between manifolds
+is `n` times continuously differentiable at `x : M` within the set `s`.
+
+`f` is `n` times continuously differentiable within `s` at `x` if it is continuous and it is `n`
+times continuously differentiable in this set around `x`, when read in the preferred chart at `x`.
 The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
 number, `∞`, or `ω`, where `C^ω` corresponds to analytic functions. -/
 def ContMDiffWithinAt (n : ℕ∞ω) (f : M → M') (s : Set M) (x : M) :=
   LiftPropWithinAt (ContDiffWithinAtProp I I' n) f s x
 
 variable (I I') in
-/-- A function is `n` times continuously differentiable at a point in a manifold if
-it is continuous and it is `n` times continuously differentiable around this point, when
-read in the preferred chart at this point.
+/-- `ContMDiffAt I I' n f x` indicates that the function `f : M → M'` between manifolds
+is `n` times continuously differentiable at `x : M`.
+
+`f` is `n` times continuously differentiable at `x` if it is continuous and it is `n` times
+continuously differentiable around `x`, when read in the preferred chart at `x`.
 The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
 number, `∞`, or `ω`, where `C^ω` corresponds to analytic functions. -/
 def ContMDiffAt (n : ℕ∞ω) (f : M → M') (x : M) :=
@@ -185,18 +189,23 @@ theorem contMDiffAt_iff {n : ℕ∞ω} {f : M → M'} {x : M} :
   liftPropAt_iff.trans <| by rw [ContDiffWithinAtProp, preimage_univ, univ_inter]; rfl
 
 variable (I I') in
-/-- A function is `n` times continuously differentiable in a set of a manifold if it is continuous
-and, for any pair of points, it is `n` times continuously differentiable on this set in the charts
+/-- `ContMDiffOn I I' n f s` indicates that the function `f : M → M'` between manifolds
+is `n` times continuously differentiable in a set `s : Set M`.
+
+`f` is `n` times continuously differentiable on `s` if it is continuous on `s` and,
+for any pair of points, it is `n` times continuously differentiable `s` in the charts
 around these points.
 The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
 number, `∞`, or `ω`, where `C^ω` corresponds to analytic functions. -/
 def ContMDiffOn (n : ℕ∞ω) (f : M → M') (s : Set M) :=
   ∀ x ∈ s, ContMDiffWithinAt I I' n f s x
 
 variable (I I') in
-/-- A function is `n` times continuously differentiable in a manifold if it is continuous
-and, for any pair of points, it is `n` times continuously differentiable in the charts
-around these points.
+/-- `ContMDiff I I' n f` indicates that the function `f : M → M'` between manifolds
+is `n` times continuously differentiable.
+
+`f` is `n` times continuously differentiable if it is continuous and, for any pair of points,
+it is `n` times continuously differentiable in the charts around these points.
 The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
 number, `∞`, or `ω`, where `C^ω` corresponds to analytic functions. -/
 def ContMDiff (n : ℕ∞ω) (f : M → M') :=

Mathlib/Geometry/Manifold/MFDeriv/Defs.lean

@@ -316,9 +316,9 @@ def HasMFDerivAt (f : M → M') (x : M) (f' : TangentSpace I x →L[𝕜] Tangen
 
 open Classical in
 variable (I I') in
-/-- Let `f` be a function between two manifolds. Then `mfderivWithin I I' f s x` is the
-derivative of `f` at `x` within `s`, as a continuous linear map from the tangent space at `x` to the
-tangent space at `f x`. -/
+/-- `mfderivWithin I I' f s x`, given a function `f` between two manifolds,
+is the derivative of `f` at `x` within `s`,
+as a continuous linear map from the tangent space at `x` to the tangent space at `f x`. -/
 def mfderivWithin (f : M → M') (s : Set M) (x : M) : TangentSpace I x →L[𝕜] TangentSpace I' (f x) :=
   if MDifferentiableWithinAt I I' f s x then
     (fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((extChartAt I x).symm ⁻¹' s ∩ range I)
@@ -328,21 +328,22 @@ def mfderivWithin (f : M → M') (s : Set M) (x : M) : TangentSpace I x →L[
 
 open Classical in
 variable (I I') in
-/-- Let `f` be a function between two manifolds. Then `mfderiv I I' f x` is the derivative of
-`f` at `x`, as a continuous linear map from the tangent space at `x` to the tangent space at
-`f x`. -/
+/-- `mfderiv I I' f x`, given a function `f` between two manifolds, is the derivative of `f` at `x`,
+as a continuous linear map from the tangent space at `x` to the tangent space at `f x`. -/
 def mfderiv (f : M → M') (x : M) : TangentSpace I x →L[𝕜] TangentSpace I' (f x) :=
   if MDifferentiableAt I I' f x then
     (fderivWithin 𝕜 (writtenInExtChartAt I I' x f : E → E') (range I) ((extChartAt I x) x) :)
   else 0
 
 variable (I I') in
-/-- The derivative within a set, as a map between the tangent bundles -/
+/-- `tangentMapWithin I I' f s` is the derivative of `f : M → M'` within a set `s`,
+as a map between the tangent bundles `TM` and `TM'`. -/
 def tangentMapWithin (f : M → M') (s : Set M) : TangentBundle I M → TangentBundle I' M' := fun p =>
   ⟨f p.1, (mfderivWithin I I' f s p.1 : TangentSpace I p.1 → TangentSpace I' (f p.1)) p.2⟩
 
 variable (I I') in
-/-- The derivative, as a map between the tangent bundles -/
+/-- `tangentMap I I' f` is the derivative of `f : M → M'` as a map between the tangent bundles
+`TM` and `TM'`. -/
 def tangentMap (f : M → M') : TangentBundle I M → TangentBundle I' M' := fun p =>
   ⟨f p.1, (mfderiv I I' f p.1 : TangentSpace I p.1 → TangentSpace I' (f p.1)) p.2⟩
 

Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

@@ -9,22 +9,34 @@ public import Mathlib.Geometry.Manifold.Algebra.SMul
 public import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
 public import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
 
-/-! ## Equivalence of manifold differentiability with the basic definition for functions between
+/-! # Equivalence of manifold differentiability with the basic definition for functions between
 vector spaces
 
 The API in this file is mostly copied from `Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean`,
 providing the same statements for higher smoothness. In this file, we do the same for
 differentiability.
 
-In addition to the above, this file provides
-* results about the differentiability of scalar multiplication (`mfderiv_smul` and friends),
-* `mvfderiv`: the exterior derivative of a vector-valued function, as a section of the
-  cotangent bundle; adds notation `d% f` for `mvfderiv I f` via a custom elaborator scoped to the
-  `Manifold` namespace, with a corresponding delaborator, and
-  adds basic lemmas about `mvfderiv` (such as addition, subtraction, multiplication and constants).
-* `mvfderivWithin` with notation `d[s]f` for `mvfderivWithin I f s` in the `Manifold` namespace:
+## Main definitions
+
+In addition to the above, this file provides two important definitions.
+* `mvfderiv I f x` is the manifold Fréchet derivative at `x : M` of a vector-valued function
+  `f : M → V`, but taking values in the target normed space `V` instead of `TangentSpace% (f x) V`.
+  Mathematically, this uses the global trivialization `T V ≅ V × V`, yielding an identification
+  `T_v V ≅ V` for each `v : V`. In Lean, we post-compose the differential `mfderiv% f x` with
+  `NormedSpace.fromTangentSpace`. If `V` is a field, this coincides with the exterior derivative
+  of `f` as a section of the cotangent bundle.
+  There is notation `d% f` for `mvfderiv I f` via a custom elaborator scoped to the
+  `Manifold` namespace, with a corresponding delaborator,
+* `mvfderivWithin` with notation `d[s] f` for `mvfderivWithin I f s` in the `Manifold` namespace:
   the analogous concept within a set, with analogous API lemmas
 
+## Main results
+
+This file contains
+* results about the differentiability of scalar multiplication (`mfderiv_smul` and friends),
+* basic lemmas about `mvfderiv` (such as addition, subtraction, multiplication and constants),
+* analogous lemmas about `mvfderivWithin`.
+
 -/
 
 public section
@@ -410,8 +422,10 @@ end smul
 /-! ### Exterior derivative of a vector-valued function -/
 
 variable (I) in
-/-- `mvfderiv I J f x` is the exterior derivative of a vector-valued function `g` on `M`,
-as a section of the cotangent bundle.
+/-- `mvfderivWithin I J f s x` is the `mfderiv` of a vector-valued function `f` on `M` at `x`
+within the set `s`, but taking values in the target normed space directly.
+The difference to `mfderivWithin` is explained in the module-docstring for
+`Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean`.
 
 Future: this could be generalised to functions into additive torsors over abelian Lie groups.
 -/
@@ -421,8 +435,10 @@ noncomputable def mvfderivWithin (g : M → F) (s : Set M) :
   fun x ↦ (NormedSpace.fromTangentSpace <| g x).toContinuousLinearMap ∘L (mfderiv[s] g x)
 
 variable (I) in
-/-- The exterior derivative of a vector-valued function on `M`,
-as a section of the cotangent bundle.
+/-- `mvfderiv I J f x` is the `mfderiv` of a vector-valued function `f` on `M` at `x`,
+but taking values in the target normed space directly.
+The difference to `mfderiv` is explained in the module-docstring for
+`Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean`.
 
 Future: this could be generalised to functions into additive torsors over abelian Lie groups.
 -/