Apply failing to infer a function for ~Finset.le_sup

Stream: lean4

[Geoffrey Irving]

I was trying to make bound know about Finset.le_sup at least in the Finset.univ case, but I am running into apply failures:

import Mathlib.Data.Finset.Lattice.Fold
import Mathlib.Data.Fintype.Basic
import Mathlib.Tactic.Bound

variable {α β : Type} [Fintype α]

/-- Failed attempt at a version of `Finset.le_sup` that works inside `bound` -/
@[bound] lemma Finset.le_univ_sup [SemilatticeSup β] [OrderBot β] (f : α → β) {x : α} :
    f x ≤ Finset.univ.sup fun x ↦ f x := by
  apply Finset.le_sup (Finset.mem_univ x)

/-- If we use `f` directly, `bound` works -/
lemma bound_works {n : ℕ} (f : Fin n → ℕ) (x : Fin n) : f x ≤ Finset.univ.sup fun x ↦ f x := by
  bound

/-- If we have a fancier expression, `bound` fails -/
lemma bound_fails (f : α → ℕ) (x : α) : (f x) ^ 2 ≤ Finset.univ.sup fun x ↦ (f x) ^ 2 := by
  -- apply Finset.le_univ_sup (f := fun x ↦ (f x) ^ 2)  -- Works
  bound  -- Fails

/-- Indeed, `apply` already fails for the fancy expression version -/
lemma apply_fails (f : α → ℕ) (x : α) : (f x) ^ 2 ≤ Finset.univ.sup fun x ↦ (f x) ^ 2 := by
  -- apply Finset.le_univ_sup (f := fun x ↦ (f x) ^ 2)  -- Works
  apply Finset.le_univ_sup  -- Fails

Presumably the problem is that apply (and thus the apply machinery inside aesop on which bound is built) do not know to infer the function from the RHS of the equality goal first, before looking at the LHS. I initially tried to fix this with no_index, but with hindsight it is unsurprising that this has no effect given that apply also fails.

Is there a way to write the Finset.le_univ_sup lemma such that the bare apply and the bound work?

[Geoffrey Irving]

@Eric Wieser Do you know how to make this kind of thing infer?

[Jovan Gerbscheid]

If you replace the ≤ by a ≥ and swap the two arguments, it will work.

The reason is that unifying the Finset.univ.sup fun x => f x (or just Finset.univ.sup f) instantiates the f. But if it first tries to unify the f x, unification doesn't know what to do and does an incorrect instantiation. So the problem is the order in which the subexpressions are unified.

[Eric Wieser]

A mechanism to steer the unification order without writing the inequality backwards would be nice here, but maybe one doesn't exist

[Jovan Gerbscheid]

Yes, I don't think this exists.

[Jovan Gerbscheid]

Writing the equality backwards only helps if it is backwards in both the lemma and the goal, because otherwise ≥gets unfolded to ≤, so that isn't really a useful solution here.

[Geoffrey Irving]

If we can't mess with the order, is there a way to make the LHS f not unifiable at all, so that it looks like a black box until the RHS f infers and only then unfolds?

[Jovan Gerbscheid]

I think you're suggesting the same as Eric: a way to tell lean do unification in a different order.