∀ {R : Type w₁} [inst : CommRing R] {A : Type w₂} [inst_1 : CommRing A] [inst_2 : Algebra R A] (B : Type w₃)
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FinitePresentation R A],
  Algebra.FinitePresentation B (TensorProduct R B A)