no goals
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsIntegralClosure A R B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
x : R
h : optParam (IsIntegral R (↑(algebraMap R B) x)) (_ : IsIntegral R (↑(algebraMap R ((fun x => B) x)) x))
⊢ ↑(algebraMap A B) (mk' A (↑(algebraMap R B) x) h) = ↑(algebraMap A B) (↑(algebraMap R A) x)
rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply]