How to use omit?

Stream: new members

[Michael Novak]

Lean suggest I use omit of some unnecessary assumption in a lemma, but I don't understand where exactly I can put this line. Do you have a link for some documentation of this tacitc?

[Weiyi Wang]

omit (var) in
theorem foo : ...

omit [TypeClass T] in
theorem foo :...

[Weiyi Wang]

I don't know where the doc is but I often search mathlib code base to find examples

[Michael Novak]

for some reason I get a red error line under the word omit when I do it like this

[Michael Novak]

Oh, that was because I had documentation string before it. Now when I put it before the documentation string it works. Thank you very much for the help!