Comment Comment by tux3 Lean tactics can handle obvious things automatically, for some value of "obvious". parent tux3 13 days ago
