Trace product for rank-one sums

import Mathlib

namespace Conway99Formal.CubicMetric
end Conway99Formal.CubicMetric

set_option autoImplicit false

open Conway99Formal.CubicMetric

theorem Conway99Formal.CubicMetric.rank_one_trace_product {T I : Type*} [Fintype T] [Fintype I]
    [DecidableEq I] (tau : T → I → ℝ) (a b : T → ℝ)
    (F H : Matrix I I ℝ)
    (hF : ∀ i j, F i j = -(∑ t, a t * tau t i * tau t j) / 3)
    (hH : ∀ i j, H i j = -(∑ t, b t * tau t i * tau t j) / 3) :
    9 * Matrix.trace (F * H) =
      ∑ t, ∑ u, a t * (∑ i, tau t i * tau u i) ^ 2 * b u := by sorry