Inner centered commutator of raw commutator

lemma inner_centered_commutator_of_raw_commutator :    centeredCommutatorExpectation A B ψ hψB = Complex.I * c := by  let a : H := A ψ  let b : H := B ⟨ψ, hψB⟩  let μa : ℝ := expectedValue A ψ  let μb : ℝ := expectedValue B ⟨ψ, hψB⟩  have hμa_right : ⟪(ψ : H), a⟫_ℂ = (μa : ℂ) := by    simpa [a, μa] using expectedValue_eq_inner A hA ψ  have hμa_left : ⟪a, (ψ : H)⟫_ℂ = (μa : ℂ) := by    have h_symm : ⟪a, (ψ : H)⟫_ℂ = ⟪(ψ : H), a⟫_ℂ := by      simpa [a] using hA ψ ψ    simpa [h_symm] using hμa_right  have hμb_right : ⟪(ψ : H), b⟫_ℂ = (μb : ℂ) := by    simpa [b, μb] using expectedValue_eq_inner B hB ⟨ψ, hψB⟩  have hμb_left : ⟪b, (ψ : H)⟫_ℂ = (μb : ℂ) := by    have h_symm : ⟪b, (ψ : H)⟫_ℂ = ⟪(ψ : H), b⟫_ℂ := by      simpa [b] using hB ⟨ψ, hψB⟩ ⟨ψ, hψB⟩    simpa [h_symm] using hμb_right  calc    centeredCommutatorExpectation A B ψ hψB =      ⟪centered A ψ, centered B ⟨ψ, hψB⟩⟫_ℂ -        ⟪centered B ⟨ψ, hψB⟩, centered A ψ⟫_ℂ := by          rfl    _ =      ⟪a - (μa : ℂ) • (ψ : H), b - (μb : ℂ) • (ψ : H)⟫_ℂ -        ⟪b - (μb : ℂ) • (ψ : H), a - (μa : ℂ) • (ψ : H)⟫_ℂ := by          rfl    _ = ⟪a, b⟫_ℂ - ⟪b, a⟫_ℂ :=      sub_expectation_commutator_eq_raw (ψ : H) a b μa μb        hμa_right hμa_left hμb_right hμb_left hψ_norm    _ = Complex.I * c :=      raw_commutator_eq_of_symmetric A B hA hB ψ hψB hBA hAB        (by simpa [rawCommutatorExpectation] using h_raw)