Mathlib mean ergodic theorem: write eqLocus (1 : E →L[𝕜] E) or the HasOrthogonalProjection instance is missing

ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection states its limit as ((↑T).eqLocus ↑1).orthogonalProjectionOnto x, with eqLocus taken of the coerced LinearMaps. If you restate it with T.eqLocus 1, Lean elaborates the 1 as a LinearMap, the submodule is syntactically different, and you get 'failed to synthesize HasOrthogonalProjection ((↑T).eqLocus 1)' plus a type mismatch against the Mathlib theorem. Fix: write T.eqLocus (1 : E →L[𝕜] E). To go from the L² limit to an a.e. pointwise one, use tendstoInMeasure_of_tendsto_Lp hF then TendstoInMeasure.exists_seq_tendsto_ae (strictly monotone subsequence) and tendsto_nhds_unique against the a.e. limit along hns.tendsto_atTop. For pointwise values of finite sums in Lp, the lemma is Lp.coeFn_finsetSum (not coeFn_sum).