chore(linear_algebra/alternating,topology/algebra/module/multilinear)…

…: add a fun_like instance (#18766)




Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

src/analysis/analytic/inverse.lean

@@ -170,7 +170,7 @@ begin
   { simp only [right_inv_coeff_one] },
   simp only [right_inv, neg_inj],
   rw remove_zero_comp_of_pos _ _ (add_pos_of_nonneg_of_pos (n.zero_le) zero_lt_two),
-  congrm i.symm.to_continuous_linear_map.comp_continuous_multilinear_map (p.comp (λ k, _) _),
+  congr' 2 with k,
   by_cases hk : k < n+2; simp [hk, IH]
 end
 

src/analysis/calculus/cont_diff_def.lean

@@ -571,7 +571,8 @@ begin
         change ((p' y 0) (init (@cons 0 (λ i, E) z 0))) (@cons 0 (λ i, E) z 0 (last 0))
           = ((p' y 0) 0) z,
         unfold_coes,
-        congr },
+        congr,
+        dec_trivial },
       { convert (Hp'.mono (inter_subset_left v u)).congr (λ x hx, Hp'.zero_eq x hx.1),
         { ext x y,
           change p' x 0 (init (@snoc 0 (λ i : fin 1, E) 0 y)) y = p' x 0 0 y,

src/analysis/normed_space/multilinear.lean

@@ -820,7 +820,7 @@ variables {𝕜 ι}
 
 lemma mk_pi_field_apply_one_eq_self (f : continuous_multilinear_map 𝕜 (λ(i : ι), 𝕜) G) :
   continuous_multilinear_map.mk_pi_field 𝕜 ι (f (λi, 1)) = f :=
-to_multilinear_map_inj f.to_multilinear_map.mk_pi_ring_apply_one_eq_self
+to_multilinear_map_injective f.to_multilinear_map.mk_pi_ring_apply_one_eq_self
 
 @[simp] lemma norm_mk_pi_field (z : G) : ‖continuous_multilinear_map.mk_pi_field 𝕜 ι z‖ = ‖z‖ :=
 (multilinear_map.mk_continuous_norm_le _ (norm_nonneg z) _).antisymm $
@@ -830,7 +830,7 @@ lemma mk_pi_field_eq_iff {z₁ z₂ : G} :
   continuous_multilinear_map.mk_pi_field 𝕜 ι z₁ = continuous_multilinear_map.mk_pi_field 𝕜 ι z₂ ↔
   z₁ = z₂ :=
 begin
-  rw [← to_multilinear_map_inj.eq_iff],
+  rw [← to_multilinear_map_injective.eq_iff],
   exact multilinear_map.mk_pi_ring_eq_iff
 end
 
@@ -1225,7 +1225,7 @@ end
 
 @[simp] lemma continuous_multilinear_map.uncurry_curry_left
   (f : continuous_multilinear_map 𝕜 Ei G) : f.curry_left.uncurry_left = f :=
-continuous_multilinear_map.to_multilinear_map_inj $ f.to_multilinear_map.uncurry_curry_left
+continuous_multilinear_map.to_multilinear_map_injective $ f.to_multilinear_map.uncurry_curry_left
 
 variables (𝕜 Ei G)
 

src/linear_algebra/alternating.lean

@@ -80,7 +80,12 @@ open function
 /-! Basic coercion simp lemmas, largely copied from `ring_hom` and `multilinear_map` -/
 section coercions
 
-instance : has_coe_to_fun (alternating_map R M N ι) (λ _, (ι → M) → N) := ⟨λ x, x.to_fun⟩
+instance fun_like : fun_like (alternating_map R M N ι) (ι → M) (λ _, N) :=
+{ coe := alternating_map.to_fun,
+  coe_injective' := λ f g h, by { cases f, cases g, congr' } }
+
+-- shortcut instance
+instance : has_coe_to_fun (alternating_map R M N ι) (λ _, (ι → M) → N) := ⟨fun_like.coe⟩
 
 initialize_simps_projections alternating_map (to_fun → apply)
 
@@ -96,14 +101,14 @@ theorem congr_arg (f : alternating_map R M N ι) {x y : ι → M} (h : x = y) :
 congr_arg (λ x : ι → M, f x) h
 
 theorem coe_injective : injective (coe_fn : alternating_map R M N ι → ((ι → M) → N)) :=
-λ f g h, by { cases f, cases g, cases h, refl }
+fun_like.coe_injective
 
 @[simp, norm_cast] theorem coe_inj {f g : alternating_map R M N ι} :
   (f : (ι → M) → N) = g ↔ f = g :=
 coe_injective.eq_iff
 
 @[ext] theorem ext {f f' : alternating_map R M N ι} (H : ∀ x, f x = f' x) : f = f' :=
-coe_injective (funext H)
+fun_like.ext _ _ H
 
 theorem ext_iff {f g : alternating_map R M N ι} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ h x, h ▸ rfl, λ h, ext h⟩

src/topology/algebra/module/multilinear.lean

@@ -63,8 +63,19 @@ variables [semiring R]
   [topological_space M₂] [topological_space M₃] [topological_space M₄]
 (f f' : continuous_multilinear_map R M₁ M₂)
 
+theorem to_multilinear_map_injective :
+  function.injective (continuous_multilinear_map.to_multilinear_map :
+    continuous_multilinear_map R M₁ M₂ → multilinear_map R M₁ M₂)
+| ⟨f, hf⟩ ⟨g, hg⟩ rfl := rfl
+
+instance continuous_map_class :
+  continuous_map_class (continuous_multilinear_map R M₁ M₂) (Π i, M₁ i) M₂ :=
+{ coe := λ f, f.to_fun,
+  coe_injective' := λ f g h, to_multilinear_map_injective $ multilinear_map.coe_injective h,
+  map_continuous := continuous_multilinear_map.cont }
+
 instance : has_coe_to_fun (continuous_multilinear_map R M₁ M₂) (λ _, (Π i, M₁ i) → M₂) :=
-⟨λ f, f.to_fun⟩
+⟨λ f, f⟩
 
 /-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
   because it is a composition of multiple projections. -/
@@ -77,16 +88,11 @@ initialize_simps_projections continuous_multilinear_map
 
 @[simp] lemma coe_coe : (f.to_multilinear_map : (Π i, M₁ i) → M₂) = f := rfl
 
-theorem to_multilinear_map_inj :
-  function.injective (continuous_multilinear_map.to_multilinear_map :
-    continuous_multilinear_map R M₁ M₂ → multilinear_map R M₁ M₂)
-| ⟨f, hf⟩ ⟨g, hg⟩ rfl := rfl
-
 @[ext] theorem ext {f f' : continuous_multilinear_map R M₁ M₂} (H : ∀ x, f x = f' x) : f = f' :=
-to_multilinear_map_inj $ multilinear_map.ext H
+fun_like.ext _ _ H
 
 theorem ext_iff {f f' : continuous_multilinear_map R M₁ M₂} : f = f' ↔ ∀ x, f x = f' x :=
-by rw [← to_multilinear_map_inj.eq_iff, multilinear_map.ext_iff]; refl
+by rw [← to_multilinear_map_injective.eq_iff, multilinear_map.ext_iff]; refl
 
 @[simp] lemma map_add [decidable_eq ι] (m : Πi, M₁ i) (i : ι) (x y : M₁ i) :
   f (update m i (x + y)) = f (update m i x) + f (update m i y) :=
@@ -142,7 +148,7 @@ instance [distrib_mul_action R'ᵐᵒᵖ M₂] [is_central_scalar R' M₂] :
 ⟨λ c₁ f, ext $ λ x, op_smul_eq_smul _ _⟩
 
 instance : mul_action R' (continuous_multilinear_map A M₁ M₂) :=
-function.injective.mul_action to_multilinear_map to_multilinear_map_inj (λ _ _, rfl)
+function.injective.mul_action to_multilinear_map to_multilinear_map_injective (λ _ _, rfl)
 
 end has_smul
 
@@ -159,7 +165,7 @@ instance : has_add (continuous_multilinear_map R M₁ M₂) :=
 rfl
 
 instance add_comm_monoid : add_comm_monoid (continuous_multilinear_map R M₁ M₂) :=
-to_multilinear_map_inj.add_comm_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)
+to_multilinear_map_injective.add_comm_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)
 
 /-- Evaluation of a `continuous_multilinear_map` at a vector as an `add_monoid_hom`. -/
 def apply_add_hom (m : Π i, M₁ i) : continuous_multilinear_map R M₁ M₂ →+ M₂ :=
@@ -359,7 +365,7 @@ instance : has_sub (continuous_multilinear_map R M₁ M₂) :=
 @[simp] lemma sub_apply (m : Πi, M₁ i) : (f - f') m = f m - f' m := rfl
 
 instance : add_comm_group (continuous_multilinear_map R M₁ M₂) :=
-to_multilinear_map_inj.add_comm_group _
+to_multilinear_map_injective.add_comm_group _
   rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
 
 end topological_add_group
@@ -398,7 +404,7 @@ variables {R' R'' A : Type*} [monoid R'] [monoid R''] [semiring A]
 instance [has_continuous_add M₂] : distrib_mul_action R' (continuous_multilinear_map A M₁ M₂) :=
 function.injective.distrib_mul_action
   ⟨to_multilinear_map, to_multilinear_map_zero, to_multilinear_map_add⟩
-  to_multilinear_map_inj (λ _ _, rfl)
+  to_multilinear_map_injective (λ _ _, rfl)
 
 end distrib_mul_action
 
@@ -414,7 +420,7 @@ variables {R' A : Type*} [semiring R'] [semiring A]
 pointwise addition and scalar multiplication. -/
 instance : module R' (continuous_multilinear_map A M₁ M₂) :=
 function.injective.module _ ⟨to_multilinear_map, to_multilinear_map_zero, to_multilinear_map_add⟩
-  to_multilinear_map_inj (λ _ _, rfl)
+  to_multilinear_map_injective (λ _ _, rfl)
 
 /-- Linear map version of the map `to_multilinear_map` associating to a continuous multilinear map
 the corresponding multilinear map. -/