awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f p : R[X]
⊢ Eq (α :=
    HasQuotient.Quotient (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)) (B :=
      Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
      (Ideal.map (R := R[X]) (F :=
        R[X] →+* 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)) (span {f})))
    ((quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f :
          (a : AdjoinRoot f ⧸ Ideal.map (mk f) (Ideal.map C I)) →
            (R[X] ⧸ Ideal.map C I) ⧸ Ideal.map (Ideal.Quotient.mk (Ideal.map C I)) (span {f}))
        ((Ideal.Quotient.mk (Ideal.map (R := R[X]) (mk f) (Ideal.map (F := R →+* R[X]) C I)) :
            (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (mk f) (Ideal.map C I))
          ((mk f : (a : R[X]) → AdjoinRoot f) p)) :
      HasQuotient.Quotient (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)) (B :=
        Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
        (Ideal.map (R := R[X]) (F :=
          R[X] →+* 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)) (span {f})))
    ((quotQuotMk (Ideal.map (F := R →+* R[X]) C I) (span {f}) :
          (a : R[X]) → (R[X] ⧸ Ideal.map C I) ⧸ Ideal.map (Ideal.Quotient.mk (Ideal.map C I)) (span {f}))
        p :
      HasQuotient.Quotient (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)) (B :=
        Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
        (Ideal.map (R := R[X]) (F :=
          R[X] →+* 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)) (span {f})))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f p : R[X]
⊢ Eq (α :=
    HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f))
      (Ideal.map (R := R[X]) (mk f) (Ideal.map (F := R →+* R[X]) C I)))
    (((quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f).symm :
          (a : (R[X] ⧸ Ideal.map C I) ⧸ Ideal.map (Ideal.Quotient.mk (Ideal.map C I)) (span {f})) →
            AdjoinRoot f ⧸ Ideal.map (mk f) (Ideal.map C I))
        ((quotQuotMk (Ideal.map (F := R →+* R[X]) C I) (span {f}) :
            (a : R[X]) → (R[X] ⧸ Ideal.map C I) ⧸ Ideal.map (Ideal.Quotient.mk (Ideal.map C I)) (span {f}))
          p) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f))
        (Ideal.map (R := R[X]) (mk f) (Ideal.map (F := R →+* R[X]) C I)))
    ((Ideal.Quotient.mk
            (Ideal.map (R := R[X]) (F := R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {f}))
              (Ideal.Quotient.mk (span {f})) (Ideal.map (F := R →+* R[X]) C I)) :
          (a : R[X] ⧸ span {f}) → (R[X] ⧸ span {f}) ⧸ Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))
        ((mk f : (a : R[X]) → AdjoinRoot f) p) :
      HasQuotient.Quotient (HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {f})) (B :=
        Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {f})))
        (Ideal.map (R := R[X]) (F := R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {f}))
          (Ideal.Quotient.mk (span {f})) (Ideal.map (F := R →+* R[X]) C I)))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f p : R[X]
⊢ Eq (α :=
    HasQuotient.Quotient (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)) (B :=
      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)))))
    ((quotQuotEquivComm I f :
          (a : (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f}) →
            (R[X] ⧸ Ideal.map C I) ⧸ span {(Ideal.Quotient.mk (Ideal.map C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f})
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f}) :
            (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
          (Polynomial.map (Ideal.Quotient.mk I) p)) :
      HasQuotient.Quotient (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)) (B :=
        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.Quotient.mk
            (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)))) :
          (a : R[X] ⧸ Ideal.map C I) →
            (R[X] ⧸ Ideal.map C I) ⧸ span {(Ideal.Quotient.mk (Ideal.map C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f})
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) p) :
      HasQuotient.Quotient (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)) (B :=
        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)))))

Tactic:
simp only [Polynomial.quotQuotEquivComm, quotientEquiv_mk,
    polynomialQuotientEquivQuotientPolynomial_map_mk]

Premises used: Ideal.quotientEquiv_mk, Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk, AdjoinRoot.Polynomial.quotQuotEquivComm
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f p : R[X]
⊢ Eq (α := HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    (((quotQuotEquivComm I f).symm :
          (a :
              (R[X] ⧸ Ideal.map C I) ⧸
                span {(Ideal.Quotient.mk (Ideal.map C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f}) →
            (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        ((Ideal.Quotient.mk
              (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)))) :
            (a : R[X] ⧸ Ideal.map C I) →
              (R[X] ⧸ Ideal.map C I) ⧸ span {(Ideal.Quotient.mk (Ideal.map C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f})
          ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) p)) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f}) :
          (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        (Polynomial.map (Ideal.Quotient.mk I) p) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))

Tactic:
simp only [Polynomial.quotQuotEquivComm, quotientEquiv_symm_mk,
    polynomialQuotientEquivQuotientPolynomial_symm_mk]

Premises used: Ideal.quotientEquiv_symm_mk, Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk, AdjoinRoot.Polynomial.quotQuotEquivComm
-- 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
      (Set.image (α := R[X])
        (⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I)) : (a : R[X]) → R[X] ⧸ Ideal.map C I) {f}))
    (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))))
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)))
    (Ideal.map (R := R[X]) (F := R[X] →+* 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)) (span {f}))
    (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))))

Tactic:
rw [map_span, Set.image_singleton]

Premises used: Set.image_singleton, Ideal.map_span
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f p : R[X]
⊢ Eq (α := HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((quotAdjoinRootEquivQuotPolynomialQuot I f :
          (a : AdjoinRoot f ⧸ Ideal.map (of f) I) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I)
          ((mk f : (a : R[X]) → AdjoinRoot f) p)) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f}) :
          (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        (Polynomial.map (Ideal.Quotient.mk I) p) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, Polynomial.map, rfl
-- 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_1 : Ideal R
f_1 f : R[X]
I : Ideal R
x : R
⊢ Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((algebraMap R (HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I)) :
          (a : R) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        x :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) x)) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))

Tactic:
have :
        algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I) x =
          Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I) ((mk f) (C x)) :=
        rfl
-- 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_1 : Ideal R
f_1 f : R[X]
I : Ideal R
x : R
this :
  Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((algebraMap R (HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I)) :
          (a : R) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        x :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) x)) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
rw :
  Eq (α := HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f}) :
          (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        ((C : (a : R ⧸ I) → (R ⧸ I)[X]) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x)) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((@RingHom.comp _ (R ⧸ I)[X] _ _ Semiring.toNonAssocSemiring _
            (algebraMap (R ⧸ I)[X]
              (HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f})))
            (algebraMap R (R ⧸ I)[X]) :
          (a : R) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        x :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
⊢ Eq (α := HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((quotAdjoinRootEquivQuotPolynomialQuot I f :
          (a : AdjoinRoot f ⧸ Ideal.map (of f) I) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        ((algebraMap R (HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I)) :
            (a : R) → AdjoinRoot f ⧸ Ideal.map (of f) I)
          x) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((algebraMap R
            (HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f})) :
          (a : R) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        x :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))

Tactic:
rw [this, quotAdjoinRootEquivQuotPolynomialQuot_mk_of, map_C, Quotient.alg_map_eq]

Premises used: Ideal.Quotient.alg_map_eq, Polynomial.map_C, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of
-- 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_1 : Ideal R
f_1 f : R[X]
I : Ideal R
x : R
this :
  Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((algebraMap R (HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I)) :
          (a : R) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        x :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) x)) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
⊢ Eq (α := HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f}) :
          (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        ((C : (a : R ⧸ I) → (R ⧸ I)[X]) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x)) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((@RingHom.comp _ (R ⧸ I)[X] _ _ Semiring.toNonAssocSemiring _
            (algebraMap (R ⧸ I)[X]
              (HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f})))
            (algebraMap R (R ⧸ I)[X]) :
          (a : R) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        x :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))

Tactic:
simp only [RingHom.comp_apply, Quotient.algebraMap_eq, Polynomial.algebraMap_apply]

Premises used: Polynomial.algebraMap_apply, Ideal.Quotient.algebraMap_eq, RingHom.comp_apply
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
I : Ideal R
rw :
  Eq (α := HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((quotAdjoinRootEquivQuotPolynomialQuot I f :
          (a : AdjoinRoot f ⧸ Ideal.map (of f) I) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I)
          ((mk f : (a : R[X]) → AdjoinRoot f) g)) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f}) :
          (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        (Polynomial.map (Ideal.Quotient.mk I) g) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
rw₁ rw₂ :
  Eq (α := HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f}) :
          (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        (Polynomial.map (Ideal.Quotient.mk I) g) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f}) :
          (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        (Polynomial.map (Ideal.Quotient.mk I) g) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
⊢ Eq (α := HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((quotEquivQuotMap f I :
          (a : AdjoinRoot f ⧸ Ideal.map (of f) I) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I)
          ((mk f : (a : R[X]) → AdjoinRoot f) g)) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f}) :
          (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        (Polynomial.map (Ideal.Quotient.mk I) g) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))

Tactic:
rw [AdjoinRoot.quotEquivQuotMap_apply, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of]

Premises used: AdjoinRoot.quotEquivQuotMap_apply, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
I : Ideal R
rw :
  Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    (((quotAdjoinRootEquivQuotPolynomialQuot I f).symm :
          (a : (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f}) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f}) :
            (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
          (Polynomial.map (Ideal.Quotient.mk I) g)) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((mk f : (a : R[X]) → AdjoinRoot f) g) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
rw₁ rw₂ :
  Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((mk f : (a : R[X]) → AdjoinRoot f) g) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((mk f : (a : R[X]) → AdjoinRoot f) g) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
⊢ Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    (((quotEquivQuotMap f I).symm :
          (a : (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f}) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f}) :
            (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
          (Polynomial.map (Ideal.Quotient.mk I) g)) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((mk f : (a : R[X]) → AdjoinRoot f) g) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))

Tactic:
rw [AdjoinRoot.quotEquivQuotMap_symm_apply,
    AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk]

Premises used: AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk, AdjoinRoot.quotEquivQuotMap_symm_apply
-- 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
inst_1 : CommRing S
inst_2 : Algebra R S
pb : PowerBasis R S
I : Ideal R
x : R
rw :
  Eq (α := AdjoinRoot (minpoly R pb.gen))
    ((AdjoinRoot.mk (minpoly R pb.gen) : (a : R[X]) → AdjoinRoot (minpoly R pb.gen)) (minpoly R pb.gen)) 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := AdjoinRoot (minpoly R pb.gen)) 0 0
⊢ Eq (α := AdjoinRoot (minpoly R pb.gen))
    ((aeval (root (minpoly R pb.gen)) : (a : R[X]) → AdjoinRoot (minpoly R pb.gen)) (minpoly R pb.gen)) 0

Tactic:
rw [AdjoinRoot.aeval_eq, AdjoinRoot.mk_self]

Premises used: AdjoinRoot.aeval_eq, AdjoinRoot.mk_self