Commit 2024-11-04 17:01 016dfafc
View on Github →feat(Data/Finset/Max): max'/min' union (#18601)
Continues https://github.com/leanprover-community/mathlib4/pull/18545. Though, I'm unsure if I should simply ignore the earlier variable declaration variable (s : Finset α) (H : s.Nonempty) {x : α} and continue as is.