{A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : CommSemiring B] →
          [inst_2 : CommSemiring C] →
            [inst_3 : Algebra A B] →
              [inst_4 : Algebra B C] →
                [inst_5 : Algebra A C] → [IsScalarTower A B C] → (b : B) → Algebra ↥A[b] ↥A[(algebraMap B C) b]