chore(Analysis/InnerProductSpace/Reproducing): clarify TODO (leanprover-community#37693)

Author: Maldooor

Mathlib/Analysis/InnerProductSpace/Reproducing.lean

@@ -28,7 +28,7 @@ positive semidefinite matrices.
 
 ## TODO
 
-- Privatize `RKHS.OfKernel`
+- Privatize `RKHS.H₀`
 
 ## References
 * [Paulsen, Vern I. and Raghupathi, Mrinal,
@@ -94,7 +94,6 @@ lemma continuous_eval (x : X) : Continuous (fun (f : H) ↦ f x) := by
 
 variable (H) [CompleteSpace H] [CompleteSpace V]
 
---TODO: make private
 /-- The kernel functions of a reproducing kernel Hilbert space are the adjoint of
 the point evaluation. -/
 def kerFun (x : X) : V →L[𝕜] H := (.proj x ∘L coeCLM 𝕜).adjoint
@@ -243,7 +242,8 @@ private lemma inner_H₀_def (f g : H₀ K) :
 
 variable (K) in
 /-- The reproducing kernel Hilbert space generated by a positive semidefinite matrix.
-TODO: Privatize. -/
+TODO: Make nonexposed def once deriving is fixed. See
+https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency/near/578850754 -/
 abbrev OfKernel := UniformSpace.Completion (H₀ K)
 --deriving SeminormedAddCommGroup, InnerProductSpace 𝕜, CompleteSpace