Lean tactics can handle obvious things automatically, for some value of "obvious".