Algebra.Algebra.Operations !4#2568

Stream: mathlib4

[Eric Wieser]

I have this file mostly building, but:

• It needs to be re-ported tomorrow on the latest mathport
• Unsurprisingly it runs into lean4#2074 and only works for now with etaExperiment true
• While trying to workaround lean4#1926, I seem to have run into a hygiene issue with suffices?

[Eric Wieser]

I've left review comments for each

[Eric Wieser]

The last one is particularly worrying, the error is

application type mismatch
  h_lean4_1926_aux.mpr
argument has type
  x ∈ M ^ Nat.succ n ↔ x ∈ M ^ n * M
but function has type
  (x✝¹ ∈ M ^ Nat.succ n ↔ x✝¹ ∈ M ^ n * M) → x✝¹ ∈ M ^ n * M → x✝¹ ∈ M ^ Nat.succ n
All Messages (4)

but the goal view never shows x✝¹

[Johan Commelin]

Thanks for taking on this file!

[Johan Commelin]

Re •₂: do you mean that none of the other 2074-workarounds seem to work?

[Johan Commelin]

I see, you need it once

[Johan Commelin]

I fixed the remaining errors, and worked around the eta issue.