by is always required to use tactics. However, there exists some syntactic constructions that have the same name as tactics. sorry is a good example: it is both a syntactically valid tactic and a valid expression. They serve the same purpose, and Lean is setup this way so that you can always use sorry no matter the context, but they should not be confused. When you use sorry as an expression, it's, well, an expression, just like true or 3 + 4. When you use it as a tactic, it's a piece of program whose purpose is to generate a piece of a proof.

From a mathematician perspective, you should always use by unless you have a good reason not to.

To expand on Jason Rute's comment,

• The rfl expression is like Eq.refl a (which is a proof of a = a), except that the a is implicitly figured out by Lean. The rfl tactic (that is, the one you have when you do by rfl), on the other hand, is a bit more general. It tries to match the current goal with things that "look like" they should be closed by "reflexivity", which includes goals like a = a, but also P ↔ P.
• The sorry expression is a macro that essentially just produces a proof (or any value, really) for anything, based on a postulated axiom sorryAx. It's a macro, and not just a plain value, because it also setup things so that error reporting is a little bit better, but you can really think of it just as a value with any type. The sorry tactic, on the other hand, is simply a shorthand for exact sorry. So when you do by sorry, it's really the same thing as just sorry.
• as for calc, I'm not exactly sure why there would be an expression version, but, as far as I understand it, it's pretty much equivalent to its tactic counterpart.

by is always required to use tactics. However, there exists some syntactic constructions that have the same name as tactics. sorry is a good example: it is both a syntactically valid tactic and a valid expression. They serve the same purpose, and Lean is setup this way so that you can always use sorry no matter the context, but they should not be confused. When you use sorry as an expression, it's, well, an expression, just like true or 3 + 4. When you use it as a tactic, it's a piece of program whose purpose is to generate a piece of a proof.

From a mathematician perspective, you should always use by unless you have a good reason not to.

To expand on Jason Rute's comment,

• The rfl expression is like Eq.refl a (which is a proof of a = a), except that the a is implicitly figured out by Lean. The rfl tactic (that is, the one you have when you do by rfl), on the other hand, is a bit more general. It tries to match the current goal with things that "look like" that should be closed by "reflexivity", which includes goals like a = a, but also P ↔ P.
• The sorry expression is a macro that essentially just produces a proof (or any value, really) for anything, based on a postulated axiom sorryAx. It's a macro, and not just a plain value, because it also setup things so that error reporting is a little bit better, but you can really think of it just as a value with any type. The sorry tactic, on the other hand, is simply a shorthand for exact sorry. So when you do by sorry, it's really the same thing as just sorry.
• as for calc, I'm not exactly sure why there would be an expression version, but, as far as I understand it, it's pretty much equivalent to its tactic counterpart.

by is always required to use tactics. However, there exists some syntactic constructions that have the same name as tactics. sorry is a good example: it is both a syntactically valid tactic and a valid expression. They serve the same purpose, and Lean is setup this way so that you can always use sorry no matter the context, but they should not be confused. When you use sorry as an expression, it's, well, an expression, just like true or 3 + 4. When you use it as a tactic, it's a piece of program whose purpose is to generate a piece of a proof.

From a mathematician perspective, you should always use by unless you have a good reason not to.

by is always required to use tactics. However, there exists some syntactic constructions that have the same name as tactics. sorry is a good example: it is both a syntactically valid tactic and a valid expression. They serve the same purpose, and Lean is setup this way so that you can always use sorry no matter the context, but they should not be confused. When you use sorry as an expression, it's, well, an expression, just like true or 3 + 4. When you use it as a tactic, it's a piece of program whose purpose is to generate a piece of a proof.

From a mathematician perspective, you should always use by unless you have a good reason not to.

To expand on Jason Rute's comment,

• The rfl expression is like Eq.refl a (which is a proof of a = a), except that the a is implicitly figured out by Lean. The rfl tactic (that is, the one you have when you do by rfl), on the other hand, is a bit more general. It tries to match the current goal with things that "look like" they should be closed by "reflexivity", which includes goals like a = a, but also P ↔ P.
• The sorry expression is a macro that essentially just produces a proof (or any value, really) for anything, based on a postulated axiom sorryAx. It's a macro, and not just a plain value, because it also setup things so that error reporting is a little bit better, but you can really think of it just as a value with any type. The sorry tactic, on the other hand, is simply a shorthand for exact sorry. So when you do by sorry, it's really the same thing as just sorry.
• as for calc, I'm not exactly sure why there would be an expression version, but, as far as I understand it, it's pretty much equivalent to its tactic counterpart.