∀ {A : Type u_8} {B : Type u_9} {C : Type u_10} {D : Type u_11} [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : CommRing C] [inst_3 : CommRing D] [inst_4 : Algebra A B] [inst_5 : Algebra A C] [inst_6 : Algebra A D]
  (FA : Type u_12) (FB : Type u_13) (FC : Type u_14) (FD : Type u_15) [inst_7 : Field FA] [inst_8 : Field FB]
  [inst_9 : Field FC] [inst_10 : Field FD] [inst_11 : Algebra A FA] [inst_12 : Algebra B FB] [inst_13 : Algebra C FC]
  [inst_14 : Algebra D FD] [inst_15 : IsFractionRing A FA] [inst_16 : IsFractionRing B FB]
  [inst_17 : IsFractionRing C FC] [inst_18 : IsFractionRing D FD] [inst_19 : Algebra A FB]
  [inst_20 : IsScalarTower A B FB] [inst_21 : Algebra A FC] [inst_22 : IsScalarTower A C FC] [inst_23 : Algebra A FD]
  [inst_24 : IsScalarTower A D FD] [inst_25 : Algebra FA FB] [inst_26 : IsScalarTower A FA FB] [inst_27 : Algebra FA FC]
  [inst_28 : IsScalarTower A FA FC] [inst_29 : Algebra FA FD] [inst_30 : IsScalarTower A FA FD] (f : B ≃ₐ[A] C)
  (g : C ≃ₐ[A] D),
  IsFractionRing.fieldEquivOfAlgEquiv FA FB FD (f.trans g) =
    (IsFractionRing.fieldEquivOfAlgEquiv FA FB FC f).trans (IsFractionRing.fieldEquivOfAlgEquiv FA FC FD g)