∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] (H : LieSubalgebra K L) [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] (a a_1 : ↥H),
  ((LieAlgebra.IsKilling.cartanEquivDual H) a) a_1 =
    (LinearMap.trace K L) ((LieModule.toEnd K (↥H) L) a * (LieModule.toEnd K (↥H) L) a_1)