doc: mention left and right to prove disjunction (#899)

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

Author: ia0

Manual/BasicProps.lean

@@ -113,6 +113,7 @@ Because {lean}`Sum` is a type, it is possible to check _which_ constructor was u
 In other words, because {lean}`Or` is not a {tech}[subsingleton], its proofs cannot be used as part of a computation.
 
 In a {ref "tactics"}[tactic] proof, disjunctions can be proved using either constructor ({name}`Or.inl` or {name}`Or.inr`) explicitly via {tactic}`apply`.
+The {tactic}`left` and {tactic}`right` tactics select the left and right disjuncts.
 Assumptions of disjunctions in the context can be simplified using {tactic}`cases`, pattern matching with {tactic (show := "match")}`Lean.Parser.Tactic.match`, or {tactic}`rcases`.
 
 {docstring Or}