case a
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S✝ : Type v
x✝ y : R
inst✝ : CommRing S✝
S T : Ideal R
H : S ≤ T
x : R
⊢ ↑(RingHom.comp (factor S T H) (mk S)) x = ↑(mk T) x
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S✝ : Type v
x y : R
inst✝ : CommRing S✝
S T : Ideal R
H : S ≤ T
⊢ RingHom.comp (factor S T H) (mk S) = mk T
ext x
no goals
case a
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S✝ : Type v
x✝ y : R
inst✝ : CommRing S✝
S T : Ideal R
H : S ≤ T
x : R
⊢ ↑(RingHom.comp (factor S T H) (mk S)) x = ↑(mk T) x
rw [RingHom.comp_apply, factor_mk]