Italics in Lean Infoview panel

Stream: lean4

[Anthony Bordg]

How do you reproduce italics that are sometimes used for naming implicit instances in the Lean Infoview panel, e.g. inst\textdied : Category C?
Apparently copy-pasting from the Infoview panel in VS Code doesn't preserve formatting.

[Anthony Bordg]

One can input the first characters using \Mi, e.g. \Mii. But, I don't know how to produce the italicized dagger ✝?

[Rémy Degenne]

My understanding is that the point of that dagger is to indicate that this is an auto-generated name and to prevent you from using it. Auto-generated names are very brittle: they can change for a variety of reasons in code above the current proof.
Instead, you should give a name to that instance when you introduce it (in the lemma statement, presumably?). Write [hC : Category C], then use the name hC.
I am not familiar with the category theory library but in general it's surprising that you need to refer to instances by name like that.

[Yaël Dillies]

You can also write \<Category C\>

[Ruben Van de Velde]

\f<

[Anthony Bordg]

Rémy Degenne said:

Instead, you should give a name to that instance when you introduce it (in the lemma statement, presumably?). Write [hC : Category C], then use the name hC.

Any alternative to naming my instance, which seems unecessary?
For instance, I have the following tactic state.

C : Type w
  inst✝ : SmallCategory C
  J : GrothendieckTopology C
  ⊢ ∃ C_1 x J_1 l, (inducedPresentation J_1 l).IsEquivalence

Use C, _, J doesn't work, so how to refer to inst✝ without being able to use this auto-generated name?

[Rémy Degenne]

inferInstance. Or what Yaël and Ruben wrote.

[Rémy Degenne]

If you provided a small #mwe, it would be easier for us to fill the gap and show you a working solution.

[Anthony Bordg]

inferInstance does the job. Thanks.

[Rémy Degenne]

And if you need to get an instance while in tactic mode, the tactic is infer_instance.

[Eric Wieser]

Just to answer the original question: the italics are just a formatting choice in the info view, like the use of the yellow color; it's not something that it makes sense to try and type in the editor

[Anthony Bordg]

I was misled by the fact that I was unable to use the name of the assumption, after all that's what a name is used for :), so I thought the formatting, here italics, matters. I know understand that these auto-generated names shouldn't be used.

[Kyle Miller]

Here's a "secret of the dagger": names that aren't supposed to be referred to have a macro scope affixed to the end.

open Lean
#eval show MetaM String from do return toString <| Syntax.getId (← `(x))
-- "x._@.Mathlib.foo._hyg.1"

The whole macro scope suffix gets rendered as a dagger when pretty printed

#eval show Elab.Command.CommandElabM Unit from do logInfo m!"{← `(x)}"
-- x✝

This is to say that even if dagger were something you could type, what you actually would need is to be able to type this whole secret macro scope.