no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.251441
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace G
A : E →L[𝕜] F
x : E
y : F
⊢ inner (↑(↑adjointAux A) y) x = inner y (↑A x)
rw [adjointAux_apply, toDual_symm_apply, toSesqForm_apply_coe, coe_comp', innerSL_apply_coe,
  Function.comp_apply]