non defeq in mathlib4#735

Stream: mathlib4

[Scott Morrison]

mathlib4#735 has a few "open issues", for which I've created issues either on mathlib4 or lean4:

• https://github.com/leanprover/lean4/issues/1886
• https://github.com/leanprover-community/mathlib4/issues/739
• https://github.com/leanprover-community/mathlib4/issues/740

[Scott Morrison]

The one remaining issue that we may want to study before merging is at https://github.com/leanprover-community/mathlib4/pull/735/files#diff-556dc9aa9cefaa23300eba8051b7dba60bdb7f576071cd8e791e228eaf8bc57eR206

[Scott Morrison]

Here we need to use Units.val_inv_eq_inv_val.{u_1} : ∀ {M : Type u_1} [inst : DivisionMonoid M] (u : Mˣ), ↑u⁻¹ = (↑u)⁻¹ after a convert, where previously convert just closed the goal.

[Ruben Van de Velde]

Scott Morrison said:

The one remaining issue that we may want to study before merging is at https://github.com/leanprover-community/mathlib4/pull/735/files#diff-556dc9aa9cefaa23300eba8051b7dba60bdb7f576071cd8e791e228eaf8bc57eR206

Was lean3 too smart or lean4 too dumb?

[Scott Morrison]

Well, I suspect it is neither, and we have inadvertently changed something so this is no longer a defeq.

[Jireh Loreaux]

Not at my machine, but a good place to check might be dubious translations in algebra.group.units in the most recent mathport