-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
I : Ideal R
f : R[X]
rw :
  Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
    (span
      (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
          HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
    (span
      (Set.image (α := (R ⧸ I)[X])
        (⇑(↑I.polynomialQuotientEquivQuotientPolynomial : (R ⧸ I)[X] →+* R[X] ⧸ Ideal.map C I) :
          (a : (R ⧸ I)[X]) → R[X] ⧸ Ideal.map C I)
        {Polynomial.map (Ideal.Quotient.mk I) f}))
rw₁ :
  Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
    (span
      (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
          HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
    (span
      (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
        (((↑I.polynomialQuotientEquivQuotientPolynomial : (R ⧸ I)[X] →+* R[X] ⧸ Ideal.map C I) :
              (a : (R ⧸ I)[X]) → R[X] ⧸ Ideal.map C I)
            (Polynomial.map (Ideal.Quotient.mk I) f) :
          HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
rw₂ :
  Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
    (span
      (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
          HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
    (span
      (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
        ((I.polynomialQuotientEquivQuotientPolynomial : (a : (R ⧸ I)[X]) → R[X] ⧸ Ideal.map C I)
            (Polynomial.map (Ideal.Quotient.mk I) f) :
          HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
rw₃ rw₄ :
  Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
    (span
      (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
          HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
    (span
      (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
          HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
⊢ Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
    (span
      (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
          HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
    (Ideal.map (R := (R ⧸ I)[X]) (F :=
      (R ⧸ I)[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
      (↑I.polynomialQuotientEquivQuotientPolynomial : (R ⧸ I)[X] →+* R[X] ⧸ Ideal.map C I)
      (span {Polynomial.map (Ideal.Quotient.mk I) f}))

Tactic:
rw [map_span, Set.image_singleton, RingEquiv.coe_toRingHom,
        polynomialQuotientEquivQuotientPolynomial_map_mk I f]

Premises used: Set.image_singleton, Ideal.map_span, Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk, RingEquiv.coe_toRingHom