bump to nightly-2023-04-04-16

mathlib commit leanprover-community/mathlib@3cacc94

Mathbin/Analysis/Calculus/LagrangeMultipliers.lean

@@ -78,9 +78,8 @@ theorem IsLocalExtrOn.exists_linear_map_of_hasStrictFderivAt
   -- squeezed `simp [mul_comm]` to speed up elaboration
   simp only [mul_comm, Algebra.id.smul_eq_mul, LinearEquiv.trans_apply, LinearEquiv.prod_apply,
     LinearEquiv.refl_apply, LinearMap.ringLmapEquivSelf_symm_apply, LinearMap.coprodEquiv_apply,
-    ContinuousLinearMap.toLinearMap_eq_coe, ContinuousLinearMap.coe_prod,
-    LinearMap.coprod_comp_prod, LinearMap.add_apply, LinearMap.coe_comp,
-    ContinuousLinearMap.coe_coe, LinearMap.coe_smulRight, LinearMap.one_apply]
+    [anonymous], ContinuousLinearMap.coe_prod, LinearMap.coprod_comp_prod, LinearMap.add_apply,
+    LinearMap.coe_comp, ContinuousLinearMap.coe_coe, LinearMap.coe_smulRight, LinearMap.one_apply]
 #align is_local_extr_on.exists_linear_map_of_has_strict_fderiv_at IsLocalExtrOn.exists_linear_map_of_hasStrictFderivAt
 
 /-- Lagrange multipliers theorem: if `φ : E → ℝ` has a local extremum on the set `{x | f x = f x₀}`

Mathbin/Analysis/InnerProductSpace/PiL2.lean

@@ -887,9 +887,9 @@ noncomputable def LinearIsometry.extend (L : S →ₗᵢ[𝕜] V) : V →ₗᵢ[
     rw [← sq_eq_sq (norm_nonneg _) (norm_nonneg _), norm_sq_eq_add_norm_sq_projection x S]
     simp only [sq, Mx_decomp]
     rw [norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (L (p1 x)) (L3 (p2 x)) Mx_orth]
-    simp only [LinearIsometry.norm_map, p1, p2, ContinuousLinearMap.toLinearMap_eq_coe,
-      add_left_inj, mul_eq_mul_left_iff, norm_eq_zero, true_or_iff, eq_self_iff_true,
-      ContinuousLinearMap.coe_coe, Submodule.coe_norm, Submodule.coe_eq_zero]
+    simp only [LinearIsometry.norm_map, p1, p2, [anonymous], add_left_inj, mul_eq_mul_left_iff,
+      norm_eq_zero, true_or_iff, eq_self_iff_true, ContinuousLinearMap.coe_coe, Submodule.coe_norm,
+      Submodule.coe_eq_zero]
   exact
     { toLinearMap := M
       norm_map' := M_norm_map }
@@ -898,8 +898,7 @@ noncomputable def LinearIsometry.extend (L : S →ₗᵢ[𝕜] V) : V →ₗᵢ[
 theorem LinearIsometry.extend_apply (L : S →ₗᵢ[𝕜] V) (s : S) : L.extend s = L s :=
   by
   haveI : CompleteSpace S := FiniteDimensional.complete 𝕜 S
-  simp only [LinearIsometry.extend, ContinuousLinearMap.toLinearMap_eq_coe, ←
-    LinearIsometry.coe_toLinearMap]
+  simp only [LinearIsometry.extend, [anonymous], ← LinearIsometry.coe_toLinearMap]
   simp only [add_right_eq_self, LinearIsometry.coe_toLinearMap,
     LinearIsometryEquiv.coe_toLinearIsometry, LinearIsometry.coe_comp, Function.comp_apply,
     orthogonalProjection_mem_subspace_eq_self, LinearMap.coe_comp, ContinuousLinearMap.coe_coe,

Mathbin/Analysis/InnerProductSpace/Projection.lean

@@ -705,8 +705,8 @@ def reflection : E ≃ₗᵢ[𝕜] E :=
       convert norm_sub_eq_norm_add this using 2
       · rw [LinearEquiv.coe_mk, reflectionLinearEquiv, LinearEquiv.toFun_eq_coe,
           LinearEquiv.coe_ofInvolutive, LinearMap.sub_apply, LinearMap.id_apply, bit0,
-          LinearMap.add_apply, LinearMap.comp_apply, Submodule.subtype_apply,
-          ContinuousLinearMap.toLinearMap_eq_coe, ContinuousLinearMap.coe_coe]
+          LinearMap.add_apply, LinearMap.comp_apply, Submodule.subtype_apply, [anonymous],
+          ContinuousLinearMap.coe_coe]
         dsimp [w, v]
         abel
       · simp only [add_sub_cancel'_right, eq_self_iff_true] }
@@ -1220,8 +1220,8 @@ theorem LinearIsometryEquiv.reflections_generate_dim_aux [FiniteDimensional ℝ
     symm
     ext x
     have := LinearMap.congr_fun (linear_map.ker_eq_top.mp this) x
-    simpa only [sub_eq_zero, ContinuousLinearMap.toLinearMap_eq_coe, ContinuousLinearMap.coe_sub,
-      LinearMap.sub_apply, LinearMap.zero_apply] using this
+    simpa only [sub_eq_zero, [anonymous], ContinuousLinearMap.coe_sub, LinearMap.sub_apply,
+      LinearMap.zero_apply] using this
   · -- Inductive step.  Let `W` be the fixed subspace of `φ`.  We suppose its complement to have
     -- dimension at most n + 1.
     let W := ker (ContinuousLinearMap.id ℝ F - φ)

Mathbin/Analysis/NormedSpace/Dual.lean

@@ -102,7 +102,7 @@ theorem double_dual_bound (x : E) : ‖(inclusionInDoubleDual 𝕜 E) x‖ ≤ 
 
 /-- The dual pairing as a bilinear form. -/
 def dualPairing : Dual 𝕜 E →ₗ[𝕜] E →ₗ[𝕜] 𝕜 :=
-  ContinuousLinearMap.coeLm 𝕜
+  ContinuousLinearMap.coeLM 𝕜
 #align normed_space.dual_pairing NormedSpace.dualPairing
 
 @[simp]

Mathbin/Analysis/NormedSpace/FiniteDimension.lean

@@ -178,7 +178,7 @@ theorem ContinuousLinearMap.continuous_det : Continuous fun f : E →L[𝕜] E =
     refine' Continuous.matrix_det _
     exact
       ((LinearMap.toMatrix b b).toLinearMap.comp
-          (ContinuousLinearMap.coeLm 𝕜)).continuous_of_finiteDimensional
+          (ContinuousLinearMap.coeLM 𝕜)).continuous_of_finiteDimensional
   · unfold LinearMap.det
     simpa only [h, MonoidHom.one_apply, dif_neg, not_false_iff] using continuous_const
 #align continuous_linear_map.continuous_det ContinuousLinearMap.continuous_det

Mathbin/Analysis/NormedSpace/Multilinear.lean

@@ -1027,17 +1027,17 @@ def ContinuousLinearEquiv.compContinuousMultilinearMapL (g : G ≃L[𝕜] G') :
     left_inv := by
       intro f
       ext1 m
-      simp only [comp_continuous_multilinear_mapL, ContinuousLinearEquiv.coe_def_rev,
-        to_linear_map_eq_coe, LinearMap.toFun_eq_coe, coe_coe, LinearMap.mkContinuous₂_apply,
-        LinearMap.mk₂_apply, comp_continuous_multilinear_map_coe, ContinuousLinearEquiv.coe_coe,
-        Function.comp_apply, ContinuousLinearEquiv.symm_apply_apply]
+      simp only [comp_continuous_multilinear_mapL, [anonymous], to_linear_map_eq_coe,
+        LinearMap.toFun_eq_coe, coe_coe, LinearMap.mkContinuous₂_apply, LinearMap.mk₂_apply,
+        comp_continuous_multilinear_map_coe, ContinuousLinearEquiv.coe_coe, Function.comp_apply,
+        ContinuousLinearEquiv.symm_apply_apply]
     right_inv := by
       intro f
       ext1 m
-      simp only [comp_continuous_multilinear_mapL, ContinuousLinearEquiv.coe_def_rev,
-        to_linear_map_eq_coe, LinearMap.mkContinuous₂_apply, LinearMap.mk₂_apply,
-        LinearMap.toFun_eq_coe, coe_coe, comp_continuous_multilinear_map_coe,
-        ContinuousLinearEquiv.coe_coe, Function.comp_apply, ContinuousLinearEquiv.apply_symm_apply]
+      simp only [comp_continuous_multilinear_mapL, [anonymous], to_linear_map_eq_coe,
+        LinearMap.mkContinuous₂_apply, LinearMap.mk₂_apply, LinearMap.toFun_eq_coe, coe_coe,
+        comp_continuous_multilinear_map_coe, ContinuousLinearEquiv.coe_coe, Function.comp_apply,
+        ContinuousLinearEquiv.apply_symm_apply]
     continuous_toFun := (compContinuousMultilinearMapL 𝕜 _ _ _ g.toContinuousLinearMap).Continuous
     continuous_invFun :=
       (compContinuousMultilinearMapL 𝕜 _ _ _ g.symm.toContinuousLinearMap).Continuous }
@@ -1201,8 +1201,8 @@ theorem norm_comp_continuous_linearIsometry_le (g : ContinuousMultilinearMap 
   by
   apply op_norm_le_bound _ (norm_nonneg _) fun m => _
   apply (g.le_op_norm _).trans _
-  simp only [ContinuousLinearMap.toLinearMap_eq_coe, ContinuousLinearMap.coe_coe,
-    LinearIsometry.coe_toContinuousLinearMap, LinearIsometry.norm_map]
+  simp only [[anonymous], ContinuousLinearMap.coe_coe, LinearIsometry.coe_toContinuousLinearMap,
+    LinearIsometry.norm_map]
 #align continuous_multilinear_map.norm_comp_continuous_linear_isometry_le ContinuousMultilinearMap.norm_comp_continuous_linearIsometry_le
 
 theorem norm_comp_continuous_linearIsometryEquiv (g : ContinuousMultilinearMap 𝕜 E₁ G)
@@ -1269,15 +1269,14 @@ def compContinuousLinearMapEquivL (f : ∀ i, E i ≃L[𝕜] E₁ i) :
     left_inv := by
       intro g
       ext1 m
-      simp only [ContinuousLinearMap.toLinearMap_eq_coe, LinearMap.toFun_eq_coe,
-        ContinuousLinearMap.coe_coe, comp_continuous_linear_mapL_apply,
-        comp_continuous_linear_map_apply, ContinuousLinearEquiv.coe_coe,
-        ContinuousLinearEquiv.apply_symm_apply]
+      simp only [[anonymous], LinearMap.toFun_eq_coe, ContinuousLinearMap.coe_coe,
+        comp_continuous_linear_mapL_apply, comp_continuous_linear_map_apply,
+        ContinuousLinearEquiv.coe_coe, ContinuousLinearEquiv.apply_symm_apply]
     right_inv := by
       intro g
       ext1 m
-      simp only [ContinuousLinearMap.toLinearMap_eq_coe, comp_continuous_linear_mapL_apply,
-        LinearMap.toFun_eq_coe, ContinuousLinearMap.coe_coe, comp_continuous_linear_map_apply,
+      simp only [[anonymous], comp_continuous_linear_mapL_apply, LinearMap.toFun_eq_coe,
+        ContinuousLinearMap.coe_coe, comp_continuous_linear_map_apply,
         ContinuousLinearEquiv.coe_coe, ContinuousLinearEquiv.symm_apply_apply] }
 #align continuous_multilinear_map.comp_continuous_linear_map_equivL ContinuousMultilinearMap.compContinuousLinearMapEquivL