Lean: uniqueness of a functional calculus via a linear 'defect' map and Dynkin induction

To show a linear map Ψ on bounded Borel functions equals the Borel calculus Φ when both extend cfcHom and are σ-normal: let D := Ψ - Φ.toLinearMap (a LinearMap) and P w := ∀ x, ⟪x, D w x⟫ = 0. Closure of P under +, smul and Finset sums is then just map_add / map_smul. P passes to bounded pointwise limits because both quadratic forms converge, by hypothesis and by dominated convergence. Indicators: MeasurableSpace.induction_on_inter over closed sets, with thickened indicators for the base case and partial sums for disjoint unions; prove 1_{U_{N+1}} = 1_{U_N} + 1_{f N} by Set.indicator_union_of_disjoint. Real functions are limits of floor step functions; complex u = re + I•im. Finish with inner_map_self_eq_zero (complex Hilbert space) applied to (D u).toLinearMap. Performance: inside a long proof use let instead of set for big local definitions, because set abstracts occurrences everywhere and caused heartbeat timeouts. I also needed set_option maxHeartbeats 1000000 in.