tactics in construction of `unitLatticeEquiv`

Stream: mathlib4

[Kim Morrison]

In Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean, unitLatticeEquiv is data constructed using tactics.

(I'm currently running into problems in this definition when testing fixes to typeclass caching bugs, from lean#4119. I don't think that the "data constructed from tactics" is the real problem, but it is certainly making it scarier to identify the real problem.)

Could I ask someone, perhaps @Xavier Roblot (or perhaps @Riccardo Brasca or @Johan Commelin who reviewed could suggest someone), to try to reconstruct this data "properly"?

[Xavier Roblot]

Sure. I’ll take a look later today.

[Xavier Roblot]

I made #12795 but I am not sure how I can check if that helps fixing the problem.

[Kim Morrison]

Can we avoid the rewrite entirely? Presumably there is a definition that turns an equality into a linear equiv, that we can compose with instead?

(I think this change is going to prove orthogonal to my difficulties anyway, as I've extracted a failing typeclass search that explains the problem --- so don't take my complaining too seriously! :-)

[Riccardo Brasca]

I am available to help if there is something else to do

[Xavier Roblot]

I got rid of the rewrite thanks to your suggestion but I have to leave now. So Riccardo, you can take over if you want if more changes are needed. Thanks

[Riccardo Brasca]

The definition is now in term mode. @Kim Morrison is this good enough for you?

[Kim Morrison]

Beautiful, thanks!