the H bug (or not a bug)

Stream: general

[Yury G. Kudryashov]

Currently expressions like ⋃ x ∈ s, f x add (H : x ∈ s) to the context. Manifolds use H as a variable name for the model space, and this creates conflicts similar to the a bug. Should we use the same strange symbol for (_ : x ∈ s) or ban H as a variable name?

[Johan Commelin]

It would be great if Lean would look at the name of the variable var in var > 0 or var \in s, and use hvar.

[Johan Commelin]

I think that's a predictable rule that will avoid 99.5% of all conflicts.