no goals
R : Type u_2
A : Type u_3
B : Type u_4
S : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
b : B
⊢ ↑(productMap f g) (↑includeRight b) = ↑g b
simp