refactor(geometry/manifold/cont_mdiff_map): redefine as subtype not s…

…tructure (#19147)

We have a long-running conversation in mathlib about whether function spaces should be implemented as subtypes or as structures.  This PR proposes to change `cont_mdiff_map`, the type of smooth functions between manifolds `M` and `M'`, from a "structure" implementation to a "subtype" implementation.  It honestly seems pretty painless, even though this is a widely used type -- the only change for users is that the field names are now `val` and `property` rather than `to_fun` and `cont_mdiff_to_fun`.

The motivation is to make it possible to make certain constructions about function spaces generic, so that work for the space of smooth functions can be reused for (for example) the spaces of continuous or differentiable functions.

Notably, in #19146 we introduce a generic construction of a sheaf of functions on a manifold whose object over the open set `U` is the subtype of functions satisfying a "local invariant property".  With this PR, when that construction is applied to the property "smoothness", the resulting sheaf has objects which are *by definition* the types `cont_mdiff_map`.   They then inherit algebraic structures for free, see #19094.

src/geometry/manifold/cont_mdiff_map.lean

@@ -33,10 +33,7 @@ variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
 (n : ℕ∞)
 
 /-- Bundled `n` times continuously differentiable maps. -/
-@[protect_proj]
-structure cont_mdiff_map :=
-(to_fun                  : M → M')
-(cont_mdiff_to_fun : cont_mdiff I I' n to_fun)
+def cont_mdiff_map := {f : M → M' // cont_mdiff I I' n f}
 
 /-- Bundled smooth maps. -/
 @[reducible] def smooth_map := cont_mdiff_map I I' M M' ⊤
@@ -52,24 +49,27 @@ namespace cont_mdiff_map
 
 variables {I} {I'} {M} {M'} {n}
 
-instance : has_coe_to_fun C^n⟮I, M; I', M'⟯ (λ _, M → M') := ⟨cont_mdiff_map.to_fun⟩
+instance fun_like : fun_like C^n⟮I, M; I', M'⟯ M (λ _, M') :=
+{ coe := subtype.val,
+  coe_injective' := subtype.coe_injective }
+
+protected lemma cont_mdiff (f : C^n⟮I, M; I', M'⟯) :
+  cont_mdiff I I' n f := f.prop
+
+protected lemma smooth (f : C^∞⟮I, M; I', M'⟯) :
+  smooth I I' f := f.prop
+
 instance : has_coe C^n⟮I, M; I', M'⟯ C(M, M') :=
-⟨λ f, ⟨f, f.cont_mdiff_to_fun.continuous⟩⟩
+⟨λ f, ⟨f, f.cont_mdiff.continuous⟩⟩
 
 attribute [to_additive_ignore_args 21] cont_mdiff_map
-  cont_mdiff_map.has_coe_to_fun cont_mdiff_map.continuous_map.has_coe
+  cont_mdiff_map.fun_like cont_mdiff_map.continuous_map.has_coe
 variables {f g : C^n⟮I, M; I', M'⟯}
 
 @[simp] lemma coe_fn_mk (f : M → M') (hf : cont_mdiff I I' n f) :
-  (mk f hf : M → M') = f :=
+  ((by exact subtype.mk f hf : C^n⟮I, M; I', M'⟯) : M → M') = f :=
 rfl
 
-protected lemma cont_mdiff (f : C^n⟮I, M; I', M'⟯) :
-  cont_mdiff I I' n f := f.cont_mdiff_to_fun
-
-protected lemma smooth (f : C^∞⟮I, M; I', M'⟯) :
-  smooth I I' f := f.cont_mdiff_to_fun
-
 lemma coe_inj ⦃f g : C^n⟮I, M; I', M'⟯⦄ (h : (f : M → M') = g) : f = g :=
 by cases f; cases g; cases h; refl
 
@@ -86,8 +86,8 @@ def id : C^n⟮I, M; I, M⟯ := ⟨id, cont_mdiff_id⟩
 
 /-- The composition of smooth maps, as a smooth map. -/
 def comp (f : C^n⟮I', M'; I'', M''⟯) (g : C^n⟮I, M; I', M'⟯) : C^n⟮I, M; I'', M''⟯ :=
-{ to_fun := λ a, f (g a),
-  cont_mdiff_to_fun := f.cont_mdiff_to_fun.comp g.cont_mdiff_to_fun, }
+{ val := λ a, f (g a),
+  property := f.cont_mdiff.comp g.cont_mdiff, }
 
 @[simp] lemma comp_apply (f : C^n⟮I', M'; I'', M''⟯) (g : C^n⟮I, M; I', M'⟯) (x : M) :
   f.comp g x = f (g x) := rfl

src/geometry/manifold/derivation_bundle.lean

@@ -42,8 +42,8 @@ variables {𝕜 M}
 
 namespace pointed_smooth_map
 
-instance {x : M} : has_coe_to_fun C^∞⟮I, M; 𝕜⟯⟨x⟩ (λ _, M → 𝕜) :=
-cont_mdiff_map.has_coe_to_fun
+instance fun_like {x : M} : fun_like C^∞⟮I, M; 𝕜⟯⟨x⟩ M (λ _, 𝕜) :=
+cont_mdiff_map.fun_like
 instance {x : M} : comm_ring C^∞⟮I, M; 𝕜⟯⟨x⟩ := smooth_map.comm_ring
 instance {x : M} : algebra 𝕜 C^∞⟮I, M; 𝕜⟯⟨x⟩ := smooth_map.algebra
 instance {x : M} : inhabited C^∞⟮I, M; 𝕜⟯⟨x⟩ := ⟨0⟩

src/geometry/manifold/whitney_embedding.lean

@@ -50,8 +50,8 @@ include hi
 
 /-- Smooth embedding of `M` into `(E × ℝ) ^ ι`. -/
 def embedding_pi_tangent : C^∞⟮I, M; 𝓘(ℝ, ι → (E × ℝ)), ι → (E × ℝ)⟯ :=
-{ to_fun := λ x i, (f i x • ext_chart_at I (f.c i) x, f i x),
-  cont_mdiff_to_fun := cont_mdiff_pi_space.2 $ λ i,
+{ val := λ x i, (f i x • ext_chart_at I (f.c i) x, f i x),
+  property := cont_mdiff_pi_space.2 $ λ i,
     ((f i).smooth_smul cont_mdiff_on_ext_chart_at).prod_mk_space ((f i).smooth) }
 
 local attribute [simp] lemma embedding_pi_tangent_coe :