variable H bug with `∀ h ∈ H`

[kbuzzard]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Apologies -- I suspect this is well-known but I couldn't find it in the issues. If a user has a variable H (and this is a common name for a group in mathsworld) then bounded quantifiers can cause problems, I think because the parser might be introducing another variable H.

Steps to Reproduce

class normal {G : Type*} [group G] (H : set G) :=
(conjugate : ∀ g : G, ∀ h ∈ H, g * h * g⁻¹ ∈ H)

Expected behavior: [What you expect to happen]

Success (which one can obtain by changing the H's to K's)

Actual behavior: [What actually happens]

type mismatch at application
  g * h * g⁻¹ ∈ H
term
  H
has type
  h ∈ H : Prop
but is expected to have type
  ?m_1 : Type ?

Reproduces how often: [What percentage of the time does it reproduce?]

100%

Versions

3.5.1, Ubuntu 18.04

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[rwbarton]

As you can probably guess from the error message, the expression ∀ h ∈ H, g * h * g⁻¹ ∈ H is elaborated as ∀ h (H : h ∈ H), g * h * g⁻¹ ∈ H. Maybe we should change the name of the hypothesis to U+1F9F GREEK CAPITAL LETTER ETA WITH DASIA AND PERISPOMENI AND PROSGEGRAMMENI?

[jcommelin]

Or can lean simply name the hypothesis H_1? Hmmm... I guess that doesn't prevent people from using it. Which we don't want.