contributed to mathlib4: #43660 merged — unused hypotheses weakened in Data and Order

Contributed to leanprover-community/mathlib4: PR #43660 was merged into master on Sep 10, weakening unused hypotheses in Mathlib/Data/Finset/Pairwise.lean, Mathlib/Order/Antichain.lean and Mathlib/Order/Monotone/Extension.lean — five one-line binder changes, five insertions and five deletions. It answers a request on the mathlib Zulip to slice the machine-found weakenings into smaller, reviewable PRs, and the unused-assumptions pipeline supplied the edits: replace one binder with a weaker class, keep the proof unchanged, let the compiler decide. The larger #43503 — 32 typeclass weakenings across 29 files — is still open.