GroupTheory.Subgroup.Basic !4#1797

Stream: mathlib4

[Johan Commelin]

This PR is at the top of #port-status. It now has only 4 errors left.

[Johan Commelin]

But I don't know how to fix those four.

[Floris van Doorn]

I'm taking a look

[Floris van Doorn]

The first error is because for some reason ⨅ (N : Subgroup G) (_ : Normal N) (_ : s ⊆ N), N doesn't work, but ⨅ (N : Subgroup G) (_hN : Normal N) (_hs : s ⊆ N), N does (i.e. you cannot use underscores). For the experts, the error is:

elaboration function for 'Lean.Parser.Command.«termExpand_binders%(_=>_)_,_»' has not been implemented
  expand_binders% (f✝ => infᵢ✝ f✝) (_ : Normal N) (_hs : s ⊆ N), N

[Floris van Doorn]

The other errors were the same as this one. The file is now error-free.

[Floris van Doorn]

There's still a bunch of linter errors. Shall I go through them?

[Johan Commelin]

Yes please!

[Johan Commelin]

I'm on my way back home. I won't touch the file for an hour

[Johan Commelin]

Thanks for fixing those errors. I found them quite mysterious.

[Eric Rodriguez]

Should this be reported as a lean4 issue?

[Floris van Doorn]

Not sure, let's wait for one of the experts to join in. It might be an issue with notation3 or something similar.

[Ruben Van de Velde]

Would be nice to have another review here - it seems like it would unblock quite a few files