feat(Tactic): nonempty attribute#39782

robin-carlier wants to merge 4 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

robin-carlier:nonempty_attrrobin-carlier/mathlib4:nonempty_attrCopy head branch name to clipboard