∀ {R : Type u_1} (A : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module A M] [inst_7 : Module R N] [inst_8 : IsScalarTower R A M] (f : Module.Dual A M) (g : Module.Dual R N)
  (m : M) (n : N), ((TensorProduct.AlgebraTensorModule.dualDistrib R A M N) (f ⊗ₜ[R] g)) (m ⊗ₜ[R] n) = g n • f m