fix(Analysis/InnerProductSpace): define instInnerProductSpaceRealComplex as RCLike.toInnerProductSpaceReal

Previously `instInnerProductSpaceRealComplex` was defined as
`InnerProductSpace.complexToReal`, which internally uses
`NormedSpace.restrictScalars ℝ ℂ ℂ`. The `Module ℝ ℂ` from that path
disagrees with `Algebra.toModule ℝ ℂ` at `.instances` transparency,
causing `rw [one_smul]` to fail with
`set_option backward.isDefEq.respectTransparency true`.

The fix moves the instance to after `RCLike.toInnerProductSpaceReal`
and defines it as `RCLike.toInnerProductSpaceReal` directly. The
`NormedSpace ℝ ℂ` in `RCLike.toInnerProductSpaceReal` is synthesized
in a context with only `[RCLike 𝕜]`, so synthesis finds
`NormedAlgebra.toNormedSpace` (non-leaky) rather than
`NormedSpace.complexToReal = RestrictScalars.normedSpace` (leaky).

The two instances were already proven equal by `rfl` in the existing
file (since `InnerProductSpace.complexToReal = InnerProductSpace.rclikeToReal ℂ ℂ`
and `RCLike.toInnerProductSpaceReal` use the same underlying `Inner.rclikeToReal`);
this PR just makes the canonical non-leaky one the definition.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: kim-em

Mathlib/Analysis/InnerProductSpace/Basic.lean

@@ -957,12 +957,6 @@ def InnerProductSpace.complexToReal [SeminormedAddCommGroup G] [InnerProductSpac
     InnerProductSpace ℝ G :=
   InnerProductSpace.rclikeToReal ℂ G
 
-instance : InnerProductSpace ℝ ℂ := InnerProductSpace.complexToReal
-
-@[simp]
-protected theorem Complex.inner (w z : ℂ) : ⟪w, z⟫_ℝ = (z * conj w).re :=
-  rfl
-
 end RCLikeToReal
 
 /-- An `RCLike` field is a real inner product space. -/
@@ -976,12 +970,22 @@ noncomputable instance RCLike.toInnerProductSpaceReal : InnerProductSpace ℝ 
     show re (_ * _) = _ * re (_ * _) by
       simp only [mul_re, conj_re, conj_im, conj_trivial, smul_re, smul_im]; ring
 
--- The instance above does not create diamonds for concrete `𝕜`:
+-- The instance above directly subsumes the complexToReal construction for ℂ.
+-- We define this here (after `RCLike.toInnerProductSpaceReal`) rather than above, so that
+-- `fast_instance%` and instance synthesis can find the canonical non-leaky form.
+noncomputable instance : InnerProductSpace ℝ ℂ := RCLike.toInnerProductSpaceReal
+
+-- Check that this does not create diamonds for concrete `𝕜`:
 example : (innerProductSpace : InnerProductSpace ℝ ℝ) = RCLike.toInnerProductSpaceReal := rfl
 example :
     (instInnerProductSpaceRealComplex : InnerProductSpace ℝ ℂ) = RCLike.toInnerProductSpaceReal :=
   rfl
 
+open scoped InnerProductSpace in
+@[simp]
+protected theorem Complex.inner (w z : ℂ) : ⟪w, z⟫_ℝ = (z * conj w).re :=
+  rfl
+
 section IsPosSemidef
 
 variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]

MathlibTest/InnerProductSpaceRealComplex.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2024 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import Mathlib.Analysis.InnerProductSpace.Basic
+
+/-!
+# Test: `instInnerProductSpaceRealComplex` is canonical at `instances` transparency
+
+Previously `instInnerProductSpaceRealComplex` was defined as `InnerProductSpace.complexToReal`,
+which goes through `NormedSpace.restrictScalars ℝ ℂ ℂ`. The `Module ℝ ℂ` arising from that path
+disagrees with `Algebra.toModule ℝ ℂ` at `.instances` transparency, causing `rw [one_smul]` to
+fail with `set_option backward.isDefEq.respectTransparency true`.
+
+The fix redefines `instInnerProductSpaceRealComplex := RCLike.toInnerProductSpaceReal`, whose
+`NormedSpace ℝ ℂ` comes from `NormedAlgebra.toNormedSpace` (via `RCLike.toNormedAlgebra`),
+so its `Module ℝ ℂ` agrees with `Algebra.toModule` at `.instances` transparency.
+-/
+
+-- The `Module ℝ ℂ` from `InnerProductSpace ℝ ℂ` now agrees with `Algebra.toModule` at instances
+-- transparency.
+example : (inferInstance : InnerProductSpace ℝ ℂ).toNormedSpace.toModule =
+    (inferInstance : Algebra ℝ ℂ).toModule := by
+  with_reducible_and_instances rfl
+
+-- As a consequence, `rw [one_smul]` works with strict transparency.
+set_option backward.isDefEq.respectTransparency true in
+example (z : ℂ) : (1 : ℝ) • z = z := by
+  rw [one_smul]