disable instance search in `apply`

Stream: lean4

[Scott Morrison]

In Lean 3 I could use apply_with ... { instances := ff }, to allow deferring instances as goals when using apply:

import group_theory.submonoid.operations

#print submonoid.map
-- Π {M : Type u_1} {N : Type u_2} [_inst_1 : mul_one_class M] [_inst_2 : mul_one_class N]
--   {F : Type u_4} [mc : monoid_hom_class F M N], F → submonoid M → submonoid N

example {M N : Type} [monoid M] [monoid N] (f : M →* N) : submonoid M → submonoid N :=
begin
  apply_with submonoid.map { instances := ff }
  -- Goals are now:
  -- ⊢ monoid_hom_class ?m_1 M N
  -- ⊢ ?m_1
  -- ⊢ Type
end

If I understand correctly, there is not currently a way to do this in Lean 4 (whether plumbing or porcelain)?

It looks like we would need to change synthAppInstances, adding a configuration option that allowed for failures in synthInstance.

[Scott Morrison]

lean4#2274

[Jujian Zhang]

As this will make !4#5046 closer to its mathlib3 original, should I wait for lean4#2274