∀ {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 = ⊤) (a : ↥A) (b : ↥B),
  (H.mulMapLeftOfSupEqTop H') (a ⊗ₜ[R] b) = ↑a * ↑b