Missing simp for adjoin

Stream: mathlib4

[Martha Hartt]

In the following example, it seems we miss some simp lemmas that would allow to remove the change.

import Mathlib.FieldTheory.Adjoin
import Mathlib.Data.Real.Basic

example (a : ℝ )(b:ℝ ): ℚ⟮a⟯ ≤ ℚ⟮b, a⟯:= by
  apply IntermediateField.adjoin.mono
  change {a} ⊆ {b, a}
  simp

Or am I missing something?

[Thomas Browning]

I wonder if this fancy notation setup might be the culprit for the lack of simp lemmas:
https://github.com/leanprover-community/mathlib4/blob/b5e7466176ae76668b236b23537586b69d88f07e/Mathlib/FieldTheory/Adjoin.lean#L458-L476

[Patrick Massot]

Yes, the whole discussion is about that fancy notation. The apply IntermediateField.adjoin.mono line gives an inscrutable goal because of this so either this should be restated or we should have simp lemmas turning the inscrutable goal into what her change is describing.

[Eric Rodriguez]

Yes, this should be fixable with simp lemmas for the notation, right? I'm not sure if this is possible without that stuff, though, considering the new Lean4 notation parser

[Eric Rodriguez]

cc @Kyle Miller who wrote the notation in lean3

[Eric Wieser]

I would guess that lean4's notation lets us do something much simpler than rolling our own set notation

[Eric Wieser]

Is there an easy way to ask Lean "Where's the notation for {a, b, c} defined?"?

[Damiano Testa]

In this case, it seems to be defined just below docs4#Sep, here. However, I found it by expecting that it would have been close to wherever I would land by Ctrl-clicking on the infoview...

[Damiano Testa]

I thought that there was a way to do this systematically, something like #check notation or #print notation, but I am failing to find it on Zulip or to guess it correctly in Lean.

[Sebastian Ullrich]

If it is part of a valid term, Ctrl+click in the editor (e.g. on the braces) should work

[Damiano Testa]

Yes, I can confirm: Ctrl+clicking on the braces does take me to where the notation is defined. However, you have to aim just right! :direct_hit:

[Kyle Miller]

Since this typeclass-based notation was my fault, here's a new version that gives pristine set notations: mathlib4#5110

Now the change does nothing at all:

example (a : ℝ )(b:ℝ ): ℚ⟮a⟯ ≤ ℚ⟮b, a⟯:= by
  apply IntermediateField.adjoin.mono
  change {a} ⊆ {b, a}
  simp

[Yury G. Kudryashov]

At least in Lean 4, we can write a notation so that Q(a, b) = adjoin K {a, b} and Q(a) = adjoin K {a} (I know I use wrong parentheses).

[Mario Carneiro]

you don't even need fancy parentheses for this

[Kyle Miller]

@Yury G. Kudryashov That's exactly the effect of my PR (now merged)