Why does `Set.isWF_iff_no_descending_seq` takes order d...

Stream: mathlib4

[Weiyi Wang]

In https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/WellFoundedSet.html#Set.isWF_iff_no_descending_seq, there is a OrderDual.toDual applied on n. Why is this needed?

[Matt Diamond]

It looks like it's been this way since mathlib3, from this commit

[Yaël Dillies]

This is indeed unnecessary. The story here is that Aaron Anderson introduced that lemma in !3#6113 with statement

theorem is_wf_iff_no_descending_seq :
  is_wf s ↔ ∀ (f : (order_dual ℕ) ↪o α), ¬ (range f) ⊆ s

Then Yury G. Kudryashov changed it to the current type-incorrect statement in !3#11303, probably by replacing the order_hom with strict_anti but keeping the order_dual

[Matt Diamond]

(sorry re: resolving/unresolving, hit the wrong button)

[Yury G. Kudryashov]

I'm sorry for introducing the typo

[Yaël Dillies]

It's my fault for not catching it in review!

[Weiyi Wang]

Ah, I suspected it might be a mistake but also wanted to ask in case it is some special use that I wasn't aware of. I happened to want to use the theorem. I can make a PR for the fix

[Yaël Dillies]

Yes please! Request my review or Yury's and we will make sure it goes through promptly

[Weiyi Wang]

There you go #24776