[Merged by Bors] - chore: remove a redundant instance on trees in set theory#38302

sgouezel wants to merge 1 commit intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

sgouezel:SG_lintTreeesgouezel/mathlib4:SG_lintTreeeCopy head branch name to clipboard