R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ ↑(quotEquivOfEq (_ : Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I) = Ideal.map (of f) I))
      (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))) x) =
    ↑(Ideal.Quotient.mk (Ideal.map (of f) I)) x
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ ↑(RingEquiv.symm (quotMapOfEquivQuotMapCMapSpanMk I f))
      (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))) x) =
    ↑(Ideal.Quotient.mk (Ideal.map (of f) I)) x
rw [quotMapOfEquivQuotMapCMapSpanMk, Ideal.quotEquivOfEq_symm]
no goals
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ ↑(quotEquivOfEq (_ : Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I) = Ideal.map (of f) I))
      (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))) x) =
    ↑(Ideal.Quotient.mk (Ideal.map (of f) I)) x
exact Ideal.quotEquivOfEq_mk _ _