∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) {ι : Type u_1} (b : Module.Basis ι R ↥A) (i : ι),
  (H.basisOfBasisLeft H' b) i = (algebraMap (↥A) S) (b i)