Transitivity of additive equivalences

Stream: new members

[Marcus Zibrowius]

If I read the source code correctly, each of Equiv.trans, MulEquiv.trans and AddEquiv.trans should qualify as trans-lemmas. If I read the documentation of the trans tactic correctly, I should therefore by able to apply this tactic to each of the above equivalences. But this only appears to work with vanilla equivalences:

import Mathlib

variable (L M N : Type) [AddMonoid L] [AddMonoid M] [AddMonoid N] [Monoid L] [Monoid M] [Monoid N]

example : L ≃ N := by
  trans M -- looks ok
  sorry

example : L ≃* N := by
  trans M -- gives an error
  sorry

example : L ≃+ N := by
  trans M -- gives an error
  sorry

Am I making a mistake here?

[Mario Carneiro]

note that there is a bug in the trans tactic and it's currently being rewritten; see batteries#1223

[Marcus Zibrowius]

The error message I get is much simpler:

transitivity lemmas only apply to binary relations and non-dependent arrows, not
L ≃* N

But of course I’m happy to wait and see whether the current rewrite will also fix my issue.