WF.Fix: Does not deduplicate goals when lambdas are duplicated

It seems that #3024 does not work as well as I hoped.

This definition from mathlib

/-- Auxiliary definition to show `exists_seq_of_forall_finset_exists`. -/
noncomputable def seqOfForallFinsetExistsAux {α : Type*} [DecidableEq α] (P : α → Prop)
    (r : α → α → Prop) (h : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y) : ℕ → α
  | n =>
    Classical.choose
      (h
        (Finset.image (fun i : Fin n => seqOfForallFinsetExistsAux P r h i)
          (Finset.univ : Finset (Fin n))))
  decreasing_by all_goals exact i.2

has only one recursive call, but shows three proof obligations:

3 goals
a✝: ℕ
n: ℕ := a✝
i: Fin n
⊢ (invImage (fun a ↦ sizeOf a) instWellFoundedRelation).1 (↑i) a✝

α: Type u_4
inst✝: DecidableEq α
P: α → Prop
r: α → α → Prop
h: ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
a✝²: ℕ
a✝¹: (y : ℕ) → (invImage (fun a ↦ sizeOf a) instWellFoundedRelation).1 y a✝² → α
n: ℕ := a✝²
a✝: ∀ x ∈ image (fun i ↦ a✝¹ ↑i _) univ, P x
i: Fin n
⊢ (invImage (fun a ↦ sizeOf a) instWellFoundedRelation).1 (↑i) a✝²

a✝: ℕ
n: ℕ := a✝
i: Fin n
⊢ (invImage (fun a ↦ sizeOf a) instWellFoundedRelation).1 (↑i) a✝

At least the first and the last should deduplicate nicely.

The second is also subsumed, but strangely the context is extended “on top” rather than below, which I find strange. Probably it's present in both, and .cleanup is leaving it in place because a✝¹ drags it in.

This is the elaborated term in its full glory:

      let n := a✝¹;
      @Classical.choose α
        (fun x ↦
          (∀ (x : α),
              @Membership.mem α (Finset α) (@Finset.instMembershipFinset α) x
                  (@Finset.image (Fin n) α (fun a b ↦ inst✝ a b)
                    (fun i ↦ @seqOfForallFinsetExistsAux α (fun a b ↦ inst✝ a b) P r h ↑i)
                    (@Finset.univ (Fin n) (Fin.fintype n))) →
                P x) →
            P x ∧
              ∀ (x_1 : α),
                @Membership.mem α (Finset α) (@Finset.instMembershipFinset α) x_1
                    (@Finset.image (Fin n) α (fun a b ↦ inst✝ a b)
                      (fun i ↦ @seqOfForallFinsetExistsAux α (fun a b ↦ inst✝ a b) P r h ↑i)
                      (@Finset.univ (Fin n) (Fin.fintype n))) →
                  r x_1 x)
        (h
          (@Finset.image (Fin n) α (fun a b ↦ inst✝ a b)
            (fun i ↦ @seqOfForallFinsetExistsAux α (fun a b ↦ inst✝ a b) P r h ↑i)
            (@Finset.univ (Fin n) (Fin.fintype n)))) 

Versions

Observed on #3040 at the time of writing.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start at WF.Fix and reproduce the duplicated-lambda example from mathlib using the #3040 setup. Compare the generated proof obligations and elaborated term; done means equivalent obligations are deduplicated, including the first and last, with the second subsumed as described.