no goals
R : Type u_1
A : Type u_3
B : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
x y : B
hx : IsIntegral R x
hy : IsIntegral R y
⊢ ↑(algebraMap A B) (mk' A (x + y) (_ : IsIntegral R (x + y))) = ↑(algebraMap A B) (mk' A x hx + mk' A y hy)
simp only [algebraMap_mk', RingHom.map_add]