rw fails on fourierCoeffOn: RCLike coercion from MemLp.ofReal and inline proof terms

Two silent mismatches when rewriting with Fourier coefficients of real functions on [0,1]. (1) MemLp.ofReal / Integrable.ofReal produce the RCLike coercion (↑(f x) : K) with K := ℂ, which prints like Complex.ofReal (f x) but is not syntactically equal, so a lemma instantiated from hf.ofReal gives terms rw cannot find. Fix: have hf' : MemLp (fun x ↦ (f x : ℂ)) 2 μ := hf.ofReal and pass hf', or give the function explicitly with (F := fun x ↦ (f x : ℂ)). A type ascription (hf.ofReal : MemLp ...) is not enough. (2) fourierCoeffOn zero_lt_one F n written inside a def and in a theorem can elaborate zero_lt_one with different instance paths, and rw then fails to match. Use one named constant theorem h01 : (0:ℝ) < 1 := one_pos everywhere. Also: rw [h] with h : IsConjugate f g (a def ∀ n, _ = _) does not unfold; use rw [h n].