style(Geometry/Manifold): remove superfluous indentation in doc-strin…

…gs (#22117)

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Style.20.3Abicycle.3A.20.3A.20indenting.20second.20lines.20in.20doc-strings)

Mathlib/Geometry/Manifold/ChartedSpace.lean

@@ -677,7 +677,7 @@ theorem ChartedSpace.locallyConnectedSpace [LocallyConnectedSpace H] : LocallyCo
     exact hsconn.isPreconnected.image _ ((e x).continuousOn_symm.mono hssubset)
 
 /-- If a topological space `M` admits an atlas with locally path-connected charts,
-  then `M` itself is locally path-connected. -/
+then `M` itself is locally path-connected. -/
 theorem ChartedSpace.locPathConnectedSpace [LocPathConnectedSpace H] : LocPathConnectedSpace M := by
   refine ⟨fun x ↦ ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨u, hu⟩ ↦ Filter.mem_of_superset hu.1.1 hu.2⟩⟩⟩
   let e := chartAt H x
@@ -1090,8 +1090,8 @@ instance hasGroupoid_continuousGroupoid : HasGroupoid M (continuousGroupoid H) :
   rw [continuousGroupoid, mem_groupoid_of_pregroupoid]
   simp only [and_self_iff]
 
-/-- If `G` is closed under restriction, the transition function between
-  the restriction of two charts `e` and `e'` lies in `G`. -/
+/-- If `G` is closed under restriction, the transition function between the restriction of two
+charts `e` and `e'` lies in `G`. -/
 theorem StructureGroupoid.trans_restricted {e e' : PartialHomeomorph M H} {G : StructureGroupoid H}
     (he : e ∈ atlas H M) (he' : e' ∈ atlas H M)
     [HasGroupoid M G] [ClosedUnderRestriction G] {s : Opens M} (hs : Nonempty s) :
@@ -1261,14 +1261,14 @@ protected instance instChartedSpace : ChartedSpace H s where
     use x
 
 /-- If `s` is a non-empty open subset of `M`, every chart of `s` is the restriction
- of some chart on `M`. -/
+of some chart on `M`. -/
 lemma chart_eq {s : Opens M} (hs : Nonempty s) {e : PartialHomeomorph s H} (he : e ∈ atlas H s) :
     ∃ x : s, e = (chartAt H (x : M)).subtypeRestr hs := by
   rcases he with ⟨xset, ⟨x, hx⟩, he⟩
   exact ⟨x, mem_singleton_iff.mp (by convert he)⟩
 
 /-- If `t` is a non-empty open subset of `H`,
-  every chart of `t` is the restriction of some chart on `H`. -/
+every chart of `t` is the restriction of some chart on `H`. -/
 -- XXX: can I unify this with `chart_eq`?
 lemma chart_eq' {t : Opens H} (ht : Nonempty t) {e' : PartialHomeomorph t H}
     (he' : e' ∈ atlas H t) : ∃ x : t, e' = (chartAt H ↑x).subtypeRestr ht := by

Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

@@ -368,7 +368,7 @@ theorem contMDiffWithinAt_iff_of_mem_maximalAtlas {x : M} (he : e ∈ maximalAtl
   (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_indep_chart he hx he' hy
 
 /-- An alternative formulation of `contMDiffWithinAt_iff_of_mem_maximalAtlas`
-  if the set if `s` lies in `e.source`. -/
+if the set if `s` lies in `e.source`. -/
 theorem contMDiffWithinAt_iff_image {x : M} (he : e ∈ maximalAtlas I n M)
     (he' : e' ∈ maximalAtlas I' n M')
     (hs : s ⊆ e.source) (hx : x ∈ e.source) (hy : f x ∈ e'.source) :
@@ -434,10 +434,10 @@ theorem contMDiffOn_iff_of_mem_maximalAtlas' (he : e ∈ maximalAtlas I n M)
     (e.continuousOn_writtenInExtend_iff hs h2s).1 h.continuousOn
 
 /-- If the set where you want `f` to be `C^n` lies entirely in a single chart, and `f` maps it
-  into a single chart, the fact that `f` is `C^n` on that set can be expressed by purely looking in
-  these charts.
-  Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure
-  that this set lies in `(extChartAt I x).target`. -/
+into a single chart, the fact that `f` is `C^n` on that set can be expressed by purely looking in
+these charts.
+Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure
+that this set lies in `(extChartAt I x).target`. -/
 theorem contMDiffOn_iff_of_subset_source {x : M} {y : M'} (hs : s ⊆ (chartAt H x).source)
     (h2s : MapsTo f s (chartAt H' y).source) :
     ContMDiffOn I I' n f s ↔
@@ -447,10 +447,10 @@ theorem contMDiffOn_iff_of_subset_source {x : M} {y : M'} (hs : s ⊆ (chartAt H
     h2s
 
 /-- If the set where you want `f` to be `C^n` lies entirely in a single chart, and `f` maps it
-  into a single chart, the fact that `f` is `C^n` on that set can be expressed by purely looking in
-  these charts.
-  Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure
-  that this set lies in `(extChartAt I x).target`. -/
+into a single chart, the fact that `f` is `C^n` on that set can be expressed by purely looking in
+these charts.
+Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure
+that this set lies in `(extChartAt I x).target`. -/
 theorem contMDiffOn_iff_of_subset_source' {x : M} {y : M'} (hs : s ⊆ (extChartAt I x).source)
     (h2s : MapsTo f s (extChartAt I' y).source) :
     ContMDiffOn I I' n f s ↔

Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean

@@ -137,7 +137,7 @@ lemma IsIntegralCurve.continuous (hγ : IsIntegralCurve γ v) : Continuous γ :=
 variable [IsManifold I 1 M]
 
 /-- If `γ` is an integral curve of a vector field `v`, then `γ t` is tangent to `v (γ t)` when
-  expressed in the local chart around the initial point `γ t₀`. -/
+expressed in the local chart around the initial point `γ t₀`. -/
 lemma IsIntegralCurveOn.hasDerivAt (hγ : IsIntegralCurveOn γ v s) {t : ℝ} (ht : t ∈ s)
     (hsrc : γ t ∈ (extChartAt I (γ t₀)).source) :
     HasDerivAt ((extChartAt I (γ t₀)) ∘ γ)

Mathlib/Geometry/Manifold/IntegralCurve/UniformTime.lean

@@ -34,7 +34,7 @@ variable
   [T2Space M] {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} {s s' : Set ℝ} {t₀ : ℝ}
 
 /-- This is the uniqueness theorem of integral curves applied to a real-indexed family of integral
-  curves with the same starting point. -/
+curves with the same starting point. -/
 lemma eqOn_of_isIntegralCurveOn_Ioo [BoundarylessManifold I M]
     (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) {x : M}
     (γ : ℝ → ℝ → M) (hγx : ∀ a, γ a 0 = x) (hγ : ∀ a > 0, IsIntegralCurveOn (γ a) v (Ioo (-a) a))
@@ -48,9 +48,8 @@ lemma eqOn_of_isIntegralCurveOn_Ioo [BoundarylessManifold I M]
   · apply Ioo_subset_Ioo <;> linarith
 
 /-- For a family of integral curves `γ : ℝ → ℝ → M` with the same starting point `γ 0 = x` such that
-  each `γ a` is defined on `Ioo (-a) a`, the global curve `γ_ext := fun t ↦ γ (|t| + 1) t` agrees
-  with each `γ a` on `Ioo (-a) a`. This will help us show that `γ_ext` is a global integral
-  curve. -/
+each `γ a` is defined on `Ioo (-a) a`, the global curve `γ_ext := fun t ↦ γ (|t| + 1) t` agrees
+with each `γ a` on `Ioo (-a) a`. This will help us show that `γ_ext` is a global integral curve. -/
 lemma eqOn_abs_add_one_of_isIntegralCurveOn_Ioo [BoundarylessManifold I M]
     (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) {x : M}
     (γ : ℝ → ℝ → M) (hγx : ∀ a, γ a 0 = x) (hγ : ∀ a > 0, IsIntegralCurveOn (γ a) v (Ioo (-a) a))
@@ -63,8 +62,8 @@ lemma eqOn_abs_add_one_of_isIntegralCurveOn_Ioo [BoundarylessManifold I M]
       (neg_lt_self_iff.mp <| lt_trans ht.1 ht.2) (not_lt.mp hlt) ht |>.symm
 
 /-- For a family of integral curves `γ : ℝ → ℝ → M` with the same starting point `γ 0 = x` such that
-  each `γ a` is defined on `Ioo (-a) a`, the function `γ_ext := fun t ↦ γ (|t| + 1) t` is a global
-  integral curve. -/
+each `γ a` is defined on `Ioo (-a) a`, the function `γ_ext := fun t ↦ γ (|t| + 1) t` is a global
+integral curve. -/
 lemma isIntegralCurve_abs_add_one_of_isIntegralCurveOn_Ioo [BoundarylessManifold I M]
     (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) {x : M}
     (γ : ℝ → ℝ → M) (hγx : ∀ a, γ a 0 = x) (hγ : ∀ a > 0, IsIntegralCurveOn (γ a) v (Ioo (-a) a)) :
@@ -82,8 +81,8 @@ lemma isIntegralCurve_abs_add_one_of_isIntegralCurveOn_Ioo [BoundarylessManifold
     exact Ioo_mem_nhds this.1 this.2
 
 /-- The existence of a global integral curve is equivalent to the existence of a family of local
-  integral curves `γ : ℝ → ℝ → M` with the same starting point `γ 0 = x` such that each `γ a` is
-  defined on `Ioo (-a) a`. -/
+integral curves `γ : ℝ → ℝ → M` with the same starting point `γ 0 = x` such that each `γ a` is
+defined on `Ioo (-a) a`. -/
 lemma exists_isIntegralCurve_iff_exists_isIntegralCurveOn_Ioo [BoundarylessManifold I M]
     (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) (x : M) :
     (∃ γ, γ 0 = x ∧ IsIntegralCurve γ v) ↔
@@ -94,9 +93,9 @@ lemma exists_isIntegralCurve_iff_exists_isIntegralCurveOn_Ioo [BoundarylessManif
     isIntegralCurve_abs_add_one_of_isIntegralCurveOn_Ioo hv γ hγx (fun a _ ↦  hγ a)⟩
 
 /-- Let `γ` and `γ'` be integral curves defined on `Ioo a b` and `Ioo a' b'`, respectively. Then,
-  `piecewise (Ioo a b) γ γ'` is equal to `γ` and `γ'` in their respective domains.
-  `Set.piecewise_eqOn` shows the equality for `γ` by definition, while this lemma shows the equality
-  for `γ'` by the uniqueness of integral curves. -/
+`piecewise (Ioo a b) γ γ'` is equal to `γ` and `γ'` in their respective domains.
+`Set.piecewise_eqOn` shows the equality for `γ` by definition, while this lemma shows the equality
+for `γ'` by the uniqueness of integral curves. -/
 lemma eqOn_piecewise_of_isIntegralCurveOn_Ioo [BoundarylessManifold I M]
     (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M)))
     {a b a' b' : ℝ} (hγ : IsIntegralCurveOn γ v (Ioo a b))
@@ -117,12 +116,12 @@ lemma eqOn_piecewise_of_isIntegralCurveOn_Ioo [BoundarylessManifold I M]
 
 /-- The extension of an integral curve by another integral curve is an integral curve.
 
-  If two integral curves are defined on overlapping open intervals, and they agree at a point in
-  their common domain, then they can be patched together to form a longer integral curve.
+If two integral curves are defined on overlapping open intervals, and they agree at a point in
+their common domain, then they can be patched together to form a longer integral curve.
 
-  This is stated for manifolds without boundary for simplicity. We actually only need to assume that
-  the images of `γ` and `γ'` lie in the interior of the manifold. TODO: Generalise to manifolds with
-  boundary. -/
+This is stated for manifolds without boundary for simplicity. We actually only need to assume that
+the images of `γ` and `γ'` lie in the interior of the manifold.
+TODO: Generalise to manifolds with boundary. -/
 lemma isIntegralCurveOn_piecewise [BoundarylessManifold I M]
     (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M)))
     {a b a' b' : ℝ} (hγ : IsIntegralCurveOn γ v (Ioo a b))
@@ -145,10 +144,10 @@ lemma isIntegralCurveOn_piecewise [BoundarylessManifold I M]
       eqOn_piecewise_of_isIntegralCurveOn_Ioo hv hγ hγ' ht₀ h⟩
 
 /-- If there exists `ε > 0` such that the local integral curve at each point `x : M` is defined at
-  least on an open interval `Ioo (-ε) ε`, then every point on `M` has a global integral
-  curve passing through it.
+least on an open interval `Ioo (-ε) ε`, then every point on `M` has a global integral curve
+passing through it.
 
-  See Lemma 9.15, [J.M. Lee (2012)][lee2012]. -/
+See Lemma 9.15, [J.M. Lee (2012)][lee2012]. -/
 lemma exists_isIntegralCurve_of_isIntegralCurveOn [BoundarylessManifold I M]
     {v : (x : M) → TangentSpace I x}
     (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M)))

Mathlib/Geometry/Manifold/IsManifold/Basic.lean

@@ -194,7 +194,7 @@ protected def symm : PartialEquiv E H :=
   I.toPartialEquiv.symm
 
 /-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
-  because it is a composition of multiple projections. -/
+because it is a composition of multiple projections. -/
 def Simps.apply (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*) [NormedAddCommGroup E]
     [NormedSpace 𝕜 E] (H : Type*) [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : H → E :=
   I
@@ -480,8 +480,8 @@ end ModelWithCornersProd
 section Boundaryless
 
 /-- Property ensuring that the model with corners `I` defines manifolds without boundary. This
-  differs from the more general `BoundarylessManifold`, which requires every point on the manifold
-  to be an interior point. -/
+differs from the more general `BoundarylessManifold`, which requires every point on the manifold
+to be an interior point. -/
 class ModelWithCorners.Boundaryless {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
     [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
     (I : ModelWithCorners 𝕜 E H) : Prop where
@@ -569,7 +569,7 @@ def contDiffPregroupoid : Pregroupoid H where
 
 variable (n I) in
 /-- Given a model with corners `(E, H)`, we define the groupoid of invertible `C^n` transformations
-  of `H` as the invertible maps that are `C^n` when read in `E` through `I`. -/
+of `H` as the invertible maps that are `C^n` when read in `E` through `I`. -/
 def contDiffGroupoid : StructureGroupoid H :=
   Pregroupoid.groupoid (contDiffPregroupoid n I)
 

Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean

@@ -154,7 +154,7 @@ lemma interior_extend_target_subset_interior_range :
   exact inter_subset_right
 
 /-- If `y ∈ f.target` and `I y ∈ interior (range I)`,
-  then `I y` is an interior point of `(I ∘ f).target`. -/
+then `I y` is an interior point of `(I ∘ f).target`. -/
 lemma mem_interior_extend_target {y : H} (hy : y ∈ f.target)
     (hy' : I y ∈ interior (range I)) : I y ∈ interior (f.extend I).target := by
   rw [f.extend_target, interior_inter, (f.open_target.preimage I.continuous_symm).interior_eq,
@@ -781,7 +781,7 @@ variable
   {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
 
 /-- A finite-dimensional manifold modelled on a locally compact field
-  (such as ℝ, ℂ or the `p`-adic numbers) is locally compact. -/
+(such as ℝ, ℂ or the `p`-adic numbers) is locally compact. -/
 lemma Manifold.locallyCompact_of_finiteDimensional
     (I : ModelWithCorners 𝕜 E H) [LocallyCompactSpace 𝕜] [FiniteDimensional 𝕜 E] :
     LocallyCompactSpace M := by
@@ -811,8 +811,7 @@ lemma LocallyCompactSpace.of_locallyCompact_manifold (I : ModelWithCorners 𝕜
   exact interior_mono (extChartAt_target_subset_range x) hy
 
 /-- Riesz's theorem applied to manifolds: a locally compact manifolds must be modelled on a
-  finite-dimensional space. This is the converse to
-  `Manifold.locallyCompact_of_finiteDimensional`. -/
+finite-dimensional space. This is the converse to `Manifold.locallyCompact_of_finiteDimensional`. -/
 theorem FiniteDimensional.of_locallyCompact_manifold
     [CompleteSpace 𝕜] (I : ModelWithCorners 𝕜 E H) [Nonempty M] [LocallyCompactSpace M] :
     FiniteDimensional 𝕜 E := by

Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean

@@ -131,7 +131,7 @@ lemma _root_.range_mem_nhds_isInteriorPoint {x : M} (h : I.IsInteriorPoint x) :
   exact ⟨interior (range I), interior_subset, isOpen_interior, h⟩
 
 /-- Type class for manifold without boundary. This differs from `ModelWithCorners.Boundaryless`,
-  which states that the `ModelWithCorners` maps to the whole model vector space. -/
+which states that the `ModelWithCorners` maps to the whole model vector space. -/
 class _root_.BoundarylessManifold {𝕜 : Type*} [NontriviallyNormedField 𝕜]
     {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
     {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)

Mathlib/Geometry/Manifold/LocalDiffeomorph.lean

@@ -133,12 +133,12 @@ end PartialDiffeomorph
 variable {M N}
 
 /-- `f : M → N` is called a **`C^n` local diffeomorphism at *x*** iff there exist
-  open sets `U ∋ x` and `V ∋ f x` and a diffeomorphism `Φ : U → V` such that `f = Φ` on `U`. -/
+open sets `U ∋ x` and `V ∋ f x` and a diffeomorphism `Φ : U → V` such that `f = Φ` on `U`. -/
 def IsLocalDiffeomorphAt (f : M → N) (x : M) : Prop :=
   ∃ Φ : PartialDiffeomorph I J M N n, x ∈ Φ.source ∧ EqOn f Φ Φ.source
 
 /-- `f : M → N` is called a **`C^n` local diffeomorphism on *s*** iff it is a local diffeomorphism
-  at each `x : s`. -/
+at each `x : s`. -/
 def IsLocalDiffeomorphOn (f : M → N) (s : Set M) : Prop :=
   ∀ x : s, IsLocalDiffeomorphAt I J n f x
 

Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

@@ -296,7 +296,7 @@ theorem mdifferentiableWithinAt_iff_of_mem_maximalAtlas {x : M} (he : e ∈ maxi
   differentiableWithinAt_localInvariantProp.liftPropWithinAt_indep_chart he hx he' hy
 
 /-- An alternative formulation of `mdifferentiableWithinAt_iff_of_mem_maximalAtlas`
-  if the set if `s` lies in `e.source`. -/
+if the set if `s` lies in `e.source`. -/
 theorem mdifferentiableWithinAt_iff_image {x : M} (he : e ∈ maximalAtlas I 1 M)
     (he' : e' ∈ maximalAtlas I' 1 M') (hs : s ⊆ e.source) (hx : x ∈ e.source)
     (hy : f x ∈ e'.source) :
@@ -365,10 +365,10 @@ theorem mdifferentiableOn_iff_of_mem_maximalAtlas' (he : e ∈ maximalAtlas I 1
     (e.continuousOn_writtenInExtend_iff hs h2s).1 h.continuousOn
 
 /-- If the set where you want `f` to be smooth lies entirely in a single chart, and `f` maps it
-  into a single chart, the smoothness of `f` on that set can be expressed by purely looking in
-  these charts.
-  Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure
-  that this set lies in `(extChartAt I x).target`. -/
+into a single chart, the smoothness of `f` on that set can be expressed by purely looking in
+these charts.
+Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure
+that this set lies in `(extChartAt I x).target`. -/
 theorem mdifferentiableOn_iff_of_subset_source {x : M} {y : M'} (hs : s ⊆ (chartAt H x).source)
     (h2s : MapsTo f s (chartAt H' y).source) :
     MDifferentiableOn I I' f s ↔
@@ -378,10 +378,10 @@ theorem mdifferentiableOn_iff_of_subset_source {x : M} {y : M'} (hs : s ⊆ (cha
     (chart_mem_maximalAtlas y) hs h2s
 
 /-- If the set where you want `f` to be smooth lies entirely in a single chart, and `f` maps it
-  into a single chart, the smoothness of `f` on that set can be expressed by purely looking in
-  these charts.
-  Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure
-  that this set lies in `(extChartAt I x).target`. -/
+into a single chart, the smoothness of `f` on that set can be expressed by purely looking in
+these charts.
+Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure
+that this set lies in `(extChartAt I x).target`. -/
 theorem mdifferentiableOn_iff_of_subset_source' {x : M} {y : M'} (hs : s ⊆ (extChartAt I x).source)
     (h2s : MapsTo f s (extChartAt I' y).source) :
     MDifferentiableOn I I' f s ↔

Mathlib/Geometry/Manifold/PartitionOfUnity.lean

@@ -213,7 +213,7 @@ section finsupport
 variable {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M)
 
 /-- The support of a smooth partition of unity at a point `x₀` as a `Finset`.
-  This is the set of `i : ι` such that `x₀ ∈ support f i`, i.e. `f i ≠ x₀`. -/
+This is the set of `i : ι` such that `x₀ ∈ support f i`, i.e. `f i ≠ x₀`. -/
 def finsupport : Finset ι := ρ.toPartitionOfUnity.finsupport x₀
 
 @[simp]
@@ -245,7 +245,7 @@ theorem finite_tsupport : {i | x₀ ∈ tsupport (ρ i)}.Finite :=
   ρ.toPartitionOfUnity.finite_tsupport _
 
 /-- The tsupport of a partition of unity at a point `x₀` as a `Finset`.
-  This is the set of `i : ι` such that `x₀ ∈ tsupport f i`. -/
+This is the set of `i : ι` such that `x₀ ∈ tsupport f i`. -/
 def fintsupport (x : M) : Finset ι :=
   (ρ.finite_tsupport x).toFinset