Reassocating a calc proof

Stream: lean4

[Robin Carlier]

import Mathlib.CategoryTheory.Iso

open CategoryTheory
variable {C : Type*} [Category C]

def test {x y z t : C} (e₁ : x ≅ y) (e₂ : y ≅ z) (e₃ : z ≅ t) : x ≅ t :=
  calc x ≅ _ := e₁
       _ ≅ _ := e₂
       _ ≅ t := e₃

lemma test_eq {x y z t : C} (e₁ : x ≅ y) (e₂ : y ≅ z) (e₃ : z ≅ t) :
    test e₁ e₂ e₃ = e₁ ≪≫ e₂ ≪≫ e₃ :=
  rfl --fails

lemma test_eq' {x y z t : C} (e₁ : x ≅ y) (e₂ : y ≅ z) (e₃ : z ≅ t) :
    test e₁ e₂ e₃ = (e₁ ≪≫ e₂) ≪≫ e₃ :=
  rfl --works

There are cases (e.g composition of (iso)morphisms) where it is most natural to associate things "on the right" rather than "on the left". The example above shows that terms generated by calc are associated "in the wrong order".
Is there a way to tell calc to associate it in the other direction? Admittedly, calc only knows about the Trans instance, so not about associativity of the relation, so I don’t know if it’s even possible... This should just be about how terms are constructed, and calc doesn’t need to know about associativity of the relation.

[Robin Carlier]

Or perhaps this has nothing to do with calc and shows that the Trans instance on isos needs to be improved?

[Kenny Lau]

@Robin Carlier well... calc is usually for proofs, where the "direction" doesn't matter

[Kenny Lau]

are you facing a problem that cannot be solved by just using ≪≫?

[Robin Carlier]

Not facing such a problem right now (though admittedly the proofs here (edit : or here) would be quite ugly, or at least way less readable, without calc), but if you ripgrep for calc in Mathlib/CategoryTheory, you will see there are several instances where calc is used to construct isomorphisms, or equivalences, and so possibly the terms constructed here are "wrong", or at least not naturally in nice simp normal forms.

This is not a big deal, because some of these isomorphisms are "intermediary" constructions, and those that are not might have a @[simps!] attribute that will make their components have the right form (and then aesop_cat calls ext on natural isomorphisms so automation is happy with that), but I still find this a bit unsatisfying and could be easily fixed if calc had an option to construct the term with the reverse association condition, it would make it more viable as a tool for constructing stuff in category theory than it is now.

[Robin Carlier]

(also, by definition there should be no such thing of "something ≪≫ can’t do but calc can", just like we could manually use Eq.trans everywhere.)