Custom Simps Projection

Stream: mathlib4

[Aaron Liu]

Sometime I find a comment

/-- See Note [custom simps projection] -/

Where is this note? I can't find it anywhere.

[Kenny Lau]

Felix Weilacher said:

Several declarations named Simps.apply have "See Note [custom simps projection]" as a docstring. Where can I find this note?

[Kenny Lau]

Kim Morrison said:

file#Mathlib/Tactic/Simps/Basic

particularly line 814

[Aaron Liu]

Thanks!

[Kenny Lau]

I wish @[simps!] supported real custom simps projection

[Aaron Liu]

Is there a way I could have found that out myself?

[Kenny Lau]

Kim Morrison said:

(I found this by grepping for library_note.*custom simps projection

[Kenny Lau]

Read the whole thread lol, that's all from me