no goals
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_3
R₂ : Type ?u.1587950
A : Type u_1
B : Type u_2
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
J : Ideal B
f : A →ₐ[R₁] B
H : I ≤ comap f J
x : A
⊢ ↑(AlgHom.comp (quotientMapₐ J f H) (Quotient.mkₐ R₁ I)) x = ↑(AlgHom.comp (Quotient.mkₐ R₁ J) f) x
simp only [quotient_map_mkₐ, Quotient.mkₐ_eq_mk, AlgHom.comp_apply]