Assistance in proof

Stream: new members

[Suvendu Kar]

Can Someone please say, how to proceed with the following proof of if A,B are Hilbert-Schmidt operator then A+B also?
lean_HS.png

[Martin Dvořák]

If you provide a copy-pastable code (ideally #mwe) rather than a screenshot with code, people will be more likely to help you.

[Kevin Buzzard]

Do you know a maths proof?

[Notification Bot]

This topic was moved here from #lean4 > Assistance in proof by Scott Morrison.

[Scott Morrison]

I've moved this to the new members thread. (Other suggestions?) I think we should try to preserve lean4 for discussion about the language itself, going forward.