∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  (H : A.LinearDisjoint ↥B) (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤) {ι : Type u_1} (b : Module.Basis ι F ↥A) (i : ι),
  (H.basisOfBasisLeft H' b) i = (algebraMap (↥A) E) (b i)