Fintype disappears for decreasing_by

Stream: mathlib4

[Pim Otte]

In the code below, I just need to prove termination (the sorry's in the body are for brevity). I don't really understand why I don't have [Fintype α] there, while I do have [PartialOrder α]. Can I get that in some way?

import Mathlib.Data.Set.Card

theorem chainInFintypeHasMax {α : Type} [Fintype α] [PartialOrder α] {c : Set α} [hnc : Nonempty c] (hic : IsChain (. ≤ .) c) :
  ∃ m ∈ c, ∀ a ∈ c, a ≤ m := by
    by_contra! hc
    obtain ⟨ g , hg ⟩ := hnc
    obtain hcemp | hcnemp := (c \ {g}).eq_empty_or_nonempty
    · sorry
    · have cGch : IsChain (. ≤ .) (c \ {g}) := by sorry
      haveI instNonEmp : Nonempty ↑(c \ {g}) := Set.Nonempty.to_subtype hcnemp
      obtain ⟨ m , hm ⟩ := chainInFintypeHasMax cGch
      sorry
termination_by c.ncard
decreasing_by
· simp_wf
  -- Where did Fintype α go?
  haveI : Fintype c := setFintype c
  rw [Set.ncard_eq_toFinset_card]

[Pim Otte]

I ended up resolving this by defining a version with Finset and doing the recursion there, if someone knows I'm still interested in what is going on here

[Kyle Miller]

It looks like the issue is that the Fintype instance is used nowhere in the definition, and it's being cleared. (@Joachim Breitner Do you know if the termination argument intentionally clears unused arguments?)

One workaround is to add have := ‹Fintype α› somewhere inside, but that's not great.

[Joachim Breitner]

There is a call to docs#Lean.MVarId.cleanup in WF.Fix.lean, but I would have expected that to keep theFintype assumption (if it is still around by that time)