typeclass instance issues in !4#2280

Stream: mathlib4

[Arien Malec]

In !4#2280, there's the local definitions:

@[to_additive
      "Addition of ultrafilters given by\n`∀ᶠ m in U+V, p m ↔ ∀ᶠ m in U, ∀ᶠ m' in V, p (m+m')`."]
def Ultrafilter.hasMul {M} [Mul M] : Mul (Ultrafilter M) where mul U V := (· * ·) <$> U <*> V

attribute [local instance] Ultrafilter.hasMul Ultrafilter.hasAdd

/- We could have taken this as the definition of `U * V`, but then we would have to prove that it
defines an ultrafilter. -/
@[to_additive]
theorem Ultrafilter.eventually_mul {M} [Mul M] (U V : Ultrafilter M) (p : M → Prop) :
    (∀ᶠ m in ↑(U * V), p m) ↔ ∀ᶠ m in U, ∀ᶠ m' in V, p (m * m') :=
  Iff.rfl

Later, in Ultrafilter.semigroup (line 70, marked by a -- porting note), we get a very slow typechecking. If I turn on set_option trace.Meta.synthInstance true, we get a very convoluted typechecking for Ultrafilter.hasMul, ending in result Semigroup.toMul and for Ultrafilter.eventually_mul we get an even longer typechecking with far more failure ending in exactly the same place.

But the instances should be short-circuited by the attribute [local instance]....

Later at line 139 exists_idempotent_ultrafilter_le_FP we have a very odd proof state, where Lean 4 claims there are no goals, but what's really happening is that Lean can't fill in the placeholders at obtain ⟨U, hU, U_idem⟩ := exists_idempotent_in_compact_subsemigroup _ S _ _ _. It takes some work to get Lean to realize that's what's happening but it's easiest to see if you do a have h := <lhs>.

After some experimentation, I think what's happening is that there's a timeout here in filling in the placeholders, and it leaves the tactic state confused? Certainly, if, e.g., I replace one of the placeholders with (by library_search), I get an actual timeout. I believe if we fix typeclass resolution for Ultrafilter we'll fix this issue as well...

[Arien Malec]

(The third and final issue at line 190 is one where the types check similarly on Lean 3 and Lean 4 but Lean 4 doesn't believe the types are as desired).

[Arien Malec]

Can I throw all this in the general https://github.com/leanprover/lean4/issues/2055 bucket?