Mysterious (kernel) declaration has metavariables 'mul2'

Stream: mathlib4

[Daniel Weber]

Where do the metavariables in this definition come from?

import Mathlib

-- (kernel) declaration has metavariables 'mul2'
def mul2 : ℕ ↪ ℕ := ⟨fun x : ℕ ↦ 2 * x, mul_right_injective₀ nofun⟩

-- (kernel) declaration has metavariables 'mul2''
def mul2' : ℕ ↪ ℕ where
  toFun x := 2 * x
  inj' := mul_right_injective₀ nofun

it works when using (by nofun) instead of a plain nofun

[Daniel Weber]

Here's a Mathlib-free minimization:

opaque Injective {α β : Type} (f : α → β) : Prop

theorem mul_right_injective {M₀ : Type} [Mul M₀] [Zero M₀] {a : M₀} (ha : a ≠ 0) :
  Injective fun (x : M₀) ↦ a * x := sorry

-- (kernel) declaration has metavariables 'mul2'
def mul2 : { f : Nat → Nat // Injective f } := ⟨fun x : Nat ↦ 2 * x, mul_right_injective nofun⟩

[Miyahara Kō]

In this case, it seems that nofun makes a metavariable:

set_option trace.Elab.step.result true in
set_option pp.match false in
set_option pp.proofs true in
/-
[Elab.step.result]
  { toFun := fun x => 2 * x,
    inj' := mul_right_injective₀ fun a => mul2.match_1 MulZeroClass.toZero ?m.768 (fun a => False) a }
-/
def mul2 : ℕ ↪ ℕ := ⟨fun x : ℕ ↦ 2 * x, mul_right_injective₀ nofun⟩

This is an issue of Lean, I will create an issue.

[Miyahara Kō]

The issue was already created: lean4#5925

[Daniel Weber]

Is this the same issue?

[Miyahara Kō]

Not exactly the same issue, but similar in that nofun is creating a metavariable.
I have commented our example to lean4#5925 now.

[Daniel Weber]

Is this the same issue?

[Miyahara Kō]

I thought it would be better to comment our example in the same issue instead of creating different issues, since the name of lean4#5925 is 'A “declaration has metavariables” error', which is the same as this situation.
@Daniel Weber Would it be better to create different issues?