no goals
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type ?u.1436024
R₂ : Type ?u.1436027
A : Type ?u.1436030
B : Type ?u.1436033
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
hf : Function.Surjective ↑f
x✝ : S ⧸ I
x : S
hx : ↑(Quotient.mk I) x = x✝
y : R
hy : ↑f y = x
⊢ ↑(quotientMap I f H) (↑(Quotient.mk J) y) = x✝
simp [hx, hy]