chore: rename a bunch of stuff (#18886)

These are (in my opinion) improperly named things that I encountered over time. Happy to remove any of them if there are disagreements.
* Remove manual instance names `IccManifold` and `Icc_smooth_manifold`. They're improper because the former is a `ChartedSpace` instance, while the latter is a `SmoothManifoldWithCorners` instance. As instances, they also probably shouldn't come up so high when searching for "Manifold" in the docs. Their names are now automatically generated, just like the two instances below them.
* Rename `ManifoldWithCorners.metrizableSpace` to `Manifold.metrizableSpace`.
* Rename `apply_(h)fdifferential` to `(h)fdifferential_apply`. This is to match the semantics of e.g. `ite_apply` and `apply_ite`.

Author: winstonyin

Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean

@@ -47,7 +47,7 @@ theorem ae_eq_zero_of_integral_smooth_smul_eq_zero [SigmaCompactSpace M]
   have := ChartedSpace.locallyCompactSpace H M
   have := I.secondCountableTopology
   have := ChartedSpace.secondCountable_of_sigma_compact H M
-  have := ManifoldWithCorners.metrizableSpace I M
+  have := Manifold.metrizableSpace I M
   let _ : MetricSpace M := TopologicalSpace.metrizableSpaceMetric M
   -- it suffices to show that the integral of the function vanishes on any compact set `s`
   apply ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero' hf (fun s hs ↦ Eq.symm ?_)

Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean

@@ -204,25 +204,25 @@ theorem left_invariant : 𝒅ₕ (smoothLeftMul_one I g) (evalAt (1 : G) X) = ev
 
 theorem evalAt_mul : evalAt (g * h) X = 𝒅ₕ (L_apply I g h) (evalAt h X) := by
   ext f
-  rw [← left_invariant, apply_hfdifferential, apply_hfdifferential, L_mul, fdifferential_comp,
-    apply_fdifferential]
+  rw [← left_invariant, hfdifferential_apply, hfdifferential_apply, L_mul, fdifferential_comp,
+    fdifferential_apply]
   -- Porting note: more aggressive here
   erw [LinearMap.comp_apply]
   -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-  erw [apply_fdifferential, ← apply_hfdifferential, left_invariant]
+  erw [fdifferential_apply, ← hfdifferential_apply, left_invariant]
 
 theorem comp_L : (X f).comp (𝑳 I g) = X (f.comp (𝑳 I g)) := by
   ext h
-  rw [ContMDiffMap.comp_apply, L_apply, ← evalAt_apply, evalAt_mul, apply_hfdifferential,
-    apply_fdifferential, evalAt_apply]
+  rw [ContMDiffMap.comp_apply, L_apply, ← evalAt_apply, evalAt_mul, hfdifferential_apply,
+    fdifferential_apply, evalAt_apply]
 
 instance : Bracket (LeftInvariantDerivation I G) (LeftInvariantDerivation I G) where
   bracket X Y :=
     ⟨⁅(X : Derivation 𝕜 C^∞⟮I, G; 𝕜⟯ C^∞⟮I, G; 𝕜⟯), Y⁆, fun g => by
       ext f
       have hX := Derivation.congr_fun (left_invariant' g X) (Y f)
       have hY := Derivation.congr_fun (left_invariant' g Y) (X f)
-      rw [apply_hfdifferential, apply_fdifferential, Derivation.evalAt_apply] at hX hY ⊢
+      rw [hfdifferential_apply, fdifferential_apply, Derivation.evalAt_apply] at hX hY ⊢
       rw [comp_L] at hX hY
       rw [Derivation.commutator_apply, SmoothMap.coe_sub, Pi.sub_apply, coe_derivation]
       rw [coe_derivation] at hX hY ⊢

Mathlib/Geometry/Manifold/DerivationBundle.lean

@@ -150,14 +150,16 @@ scoped[Manifold] notation "𝒅" => fdifferential
 scoped[Manifold] notation "𝒅ₕ" => hfdifferential
 
 @[simp]
-theorem apply_fdifferential (f : C^∞⟮I, M; I', M'⟯) {x : M} (v : PointDerivation I x)
+theorem fdifferential_apply (f : C^∞⟮I, M; I', M'⟯) {x : M} (v : PointDerivation I x)
     (g : C^∞⟮I', M'; 𝕜⟯) : 𝒅 f x v g = v (g.comp f) :=
   rfl
+@[deprecated (since := "2024-11-11")] alias apply_fdifferential := fdifferential_apply
 
 @[simp]
-theorem apply_hfdifferential {f : C^∞⟮I, M; I', M'⟯} {x : M} {y : M'} (h : f x = y)
+theorem hfdifferential_apply {f : C^∞⟮I, M; I', M'⟯} {x : M} {y : M'} (h : f x = y)
     (v : PointDerivation I x) (g : C^∞⟮I', M'; 𝕜⟯) : 𝒅ₕ h v g = 𝒅 f x v g :=
   rfl
+@[deprecated (since := "2024-11-11")] alias apply_hfdifferential := hfdifferential_apply
 
 variable {E'' : Type*} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type*}
   [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type*} [TopologicalSpace M'']

Mathlib/Geometry/Manifold/Instances/Real.lean

@@ -320,7 +320,7 @@ def IccRightChart (x y : ℝ) [h : Fact (x < y)] :
 /-- Charted space structure on `[x, y]`, using only two charts taking values in
 `EuclideanHalfSpace 1`.
 -/
-instance IccManifold (x y : ℝ) [h : Fact (x < y)] :
+instance IccChartedSpace (x y : ℝ) [h : Fact (x < y)] :
     ChartedSpace (EuclideanHalfSpace 1) (Icc x y) where
   atlas := {IccLeftChart x y, IccRightChart x y}
   chartAt z := if z.val < y then IccLeftChart x y else IccRightChart x y
@@ -335,7 +335,7 @@ instance IccManifold (x y : ℝ) [h : Fact (x < y)] :
 
 /-- The manifold structure on `[x, y]` is smooth.
 -/
-instance Icc_smooth_manifold (x y : ℝ) [Fact (x < y)] :
+instance Icc_smoothManifoldWithCorners (x y : ℝ) [Fact (x < y)] :
     SmoothManifoldWithCorners (𝓡∂ 1) (Icc x y) := by
   have M : ContDiff ℝ ∞ (show EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1)
       from fun z i => -z i + (y - x)) :=
@@ -373,8 +373,8 @@ instance Icc_smooth_manifold (x y : ℝ) [Fact (x < y)] :
   ·-- `e = right chart`, `e' = right chart`
     exact (mem_groupoid_of_pregroupoid.mpr (symm_trans_mem_contDiffGroupoid _)).1
 
-/-! Register the manifold structure on `Icc 0 1`, and also its zero and one. -/
-
+/-! Register the manifold structure on `Icc 0 1`. These are merely special cases of
+`IccChartedSpace` and `Icc_smoothManifoldWithCorners`. -/
 
 section
 

Mathlib/Geometry/Manifold/Metrizable.lean

@@ -19,11 +19,13 @@ open TopologicalSpace
 
 /-- A σ-compact Hausdorff topological manifold over a finite dimensional real vector space is
 metrizable. -/
-theorem ManifoldWithCorners.metrizableSpace {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+theorem Manifold.metrizableSpace {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
     [FiniteDimensional ℝ E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H)
     (M : Type*) [TopologicalSpace M] [ChartedSpace H M] [SigmaCompactSpace M] [T2Space M] :
     MetrizableSpace M := by
   haveI := I.locallyCompactSpace; haveI := ChartedSpace.locallyCompactSpace H M
   haveI := I.secondCountableTopology
   haveI := ChartedSpace.secondCountable_of_sigma_compact H M
   exact metrizableSpace_of_t3_second_countable M
+@[deprecated (since := "2024-11-11")] alias ManifoldWithCorners.metrizableSpace :=
+  Manifold.metrizableSpace