no goals
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type ?u.1203035
R₂ : Type ?u.1203038
A : Type ?u.1203041
B : Type ?u.1203044
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
x : R
⊢ ↑(RingHom.comp (quotientMap I f H) (Quotient.mk J)) x = ↑(RingHom.comp (Quotient.mk I) f) x
simp only [Function.comp_apply, RingHom.coe_comp, Ideal.quotientMap_mk]