left

Summary

There are two ways to prove ⊢ P ∨ Q; you can either prove P or you can prove Q. If you want to prove P then use the left tactic, which changes ⊢ P ∨ Q to ⊢ P.

Details

It’s a theorem in Lean that P → P ∨ Q. The left tactic applies this theorem, thus reducing a goal of the form ⊢ P ∨ Q to the goal ⊢ P.

Further notes

See also right. More generally, if your goal is an inductive type with two constructors, left applies the first constructor, and right applies the second one.