[Merged by Bors] - chore(Data/Finset/Max): use to_dual - #43289

[Merged by Bors] - chore(Data/Finset/Max): use to_dual#43289

JovanGerb wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

JovanGerb:Jovan-to_dual-Finset.maxJovanGerb/mathlib4:Jovan-to_dual-Finset.maxCopy head branch name to clipboard