fix build

leanprover-community · Sep 4, 2022 · 17c6fca · 17c6fca
1 parent e2f0924
commit 17c6fca
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/analysis/inner_product_space/reproducing_kernel.lean b/src/analysis/inner_product_space/reproducing_kernel.lean
@@ -172,7 +172,7 @@ lemma eval'_eq_eval_adjoint (x : X) : eval' 𝕜 X H₁ x = (eval 𝕜 𝕜 H₁
 begin
   apply (to_dual 𝕜 H₁).injective,
   ext f,
-  simp [eval'_def],
+  simp [continuous_linear_map.adjoint_apply, eval'_def],
 end
 
 lemma scalar_kernel_def (x y : X) :