Where is Subtype.val turned into a coe?

Stream: general

[Johan Commelin]

For a PR I'm working on, I need to figure out where Subtype.val is turned into a coe. And I realised that I don't know how to answer that question...
What's the tool for that?

[Damiano Testa]

Can you #synth Coe (Subtype Nat) or something similar? (On mobile)

[Johan Commelin]

I have not managed to trick #synth into giving me this info

[Yaël Dillies]

What do you mean by "turn into a coe"? It could mean two things

[Kevin Buzzard]

Right -- there's the attribute and the instance

[Johan Commelin]

Where is \u first made to work for Subtype.val.

[Johan Commelin]

I know there are two things, but that still doesn't help me figure out where those things are...

[Kevin Buzzard]

It also doesn't help me to figure out which of those things is what you're looking for because I still don't understand the lean 4 coercion system :-) Do you need both for the up arrow to work?

[Ruben Van de Velde]

You need the instance to be able to type ↑, and the attribute for lean to output the ↑ back to you

[Ruben Van de Velde]

It's docs#subtypeCoe and it uses CoeOut instead of Coe

[Ruben Van de Velde]

I don't understand the difference

[Andrew Yang]

According to my superficial understanding, Coe (Subtype p) α looks at α and finds Subtype p, and CoeOut (Subtype p) α looks at Subtype p and finds α. But the former isn't possible, so the latter it is.

[Johan Commelin]

Ruben Van de Velde said:

It's docs#subtypeCoe and it uses CoeOut instead of Coe

Awesome! Thanks for finding this for me

[Ruben Van de Velde]

I used loogle "Coe", Subtype

[Johan Commelin]

My next question is: why is this coe not found in https://github.com/leanprover-community/mathlib4/actions/runs/9945993507/job/27475513441?pr=14769

[Ruben Van de Velde]

That's not the issue

theorem Subtype.mono_coe [Preorder α] (t : Set α) : Monotone ((↑ ·) : Subtype t → α) := -- works
  fun _ _ ↦ id

theorem Subtype.mono_coe' [Preorder α] (t : Set α) : Monotone ((↑) : Subtype t → α) := -- fails
  fun _ _ ↦ id

[Ruben Van de Velde]

And the docstring for Mathlib.Tactic.Coe has

Defines notations for coercions.
1. `↑ t` is defined in core.
2. `(↑)` is equivalent to the eta-reduction of `(↑ ·)`

[Ruben Van de Velde]

I pushed the import

[Johan Commelin]

Aah, very good find!

[Johan Commelin]

Awesome! CI is now happy with

chore(Data/Bool): merge Init.Data.Bool.* into Data.Bool.Basic #14769