found a "(kernel) declaration has metavariables"

Stream: mathlib4

[yannis monbru]

Hi, while working, I found some issue : there is no goal in my lemma but the kernel says it's not done. Here is a minimal example.

import Mathlib.CategoryTheory.EqToHom

open CategoryTheory

variable (B : Type ) [Category B]

variable (G : B ⥤ B)

lemma foo : G = G := by
  apply CategoryTheory.Functor.ext --(h_map := ?_)
  --sorry
  intro U V f
  apply Functor.congr_hom

It seems that the issue is comming from the implicit use of aesop_cat in order to infer the argument h_map in Functor.ext, because if we uncomment the commented part (a sorry is added because the order of the goals are reversed) the issue disapear.

Moreover, i tried to reproduce the issue with a copy of category independent of Mathlib and in this case there is no more issue.

(maybe @Jannis Limperg could be interested)

[Andrew Yang]

This also works

lemma foo : G = G := by
  apply CategoryTheory.Functor.ext
  intro U V f
  apply Functor.congr_hom rfl

So maybe the second apply is also fishy?

[yannis monbru]

What i can tell is that the second apply try to prove the same statement than aesop_cat two line before

[Aaron Liu]

Seems to be some weird interaction between the other goal being in the type unifying with a new metavariable that solves both the other goal and the new metavariable while creating a new one