Theorem: LeanColls.Indexed.ofFn.arg_cont.semiAdjoint_rule_simple (SciLean/Data/ArrayType/Properties.lean)

State before:
K : Type
inst✝⁶ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁵ : ArrayType Cont Idx Elem
inst✝⁴ : IndexType Idx
inst✝³ : LawfulIndexType Idx
inst✝² : DecidableEq Idx
X : Type
inst✝¹ : SemiInnerProductSpace K X
inst✝ : SemiInnerProductSpace K Elem
⊢ (semiAdjoint K fun f => ofFn f) = fun cont idx => cont[idx]
Tactic:
sorry_proof
State after:
no goals