Coq proof that type isomorphism relationship is transitive
You can make the proof a lot shorter by giving a constructor for the class Isomorphism and by destructing your arguments instead of inverting them:

Class Isomorphism A B :=
  MkIsomorphism {
    from: A -&gt; B;
    to: B -&gt; A;
    from_to x: from (to x) = x;
    to_from x: to (from x) = x
  }.


Definition compose {A B C} (f : B -&gt; C) (g : A -&gt; B) (x : A) : C
  := f (g x).

Definition trans {A B C} :
  Isomorphism A B -&gt; Isomorphism B C -&gt; Isomorphism A C.
Proof.
intros [AtoB BtoA AtoBtoA BtoAtoB] [BtoC CtoB BtoCtoB CtoBtoC].
apply MkIsomorphism
  with (from := compose BtoC AtoB)
       (to   := compose BtoA CtoB);
intro x; unfold compose.
 - rewrite AtoBtoA, BtoCtoB; reflexivity.
 - rewrite CtoBtoC, BtoAtoB; reflexivity.
Defined.