awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
x y : R
rw :
  Eq (α := Ideal R[X])
    (Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) x : R[X])) ⊔
      Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])})
    (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])} ⊔
      Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) x : R[X])))
rw₁ rw₂ :
  Eq (α := Ideal R[X])
    (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])} ⊔
      Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) x : R[X])))
    (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])} ⊔
      Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) x : R[X])))
⊢ Eq (α := Ideal R[X])
    (Ideal.span
      (insert (α := R[X]) ((C : (a : R) → R[X]) x : R[X])
        {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}))
    (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])} ⊔
      Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) x : R[X])))

Tactic:
rw [Ideal.span_insert, sup_comm]

Premises used: sup_comm, Ideal.span_insert
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
x y : R
simp :
  Eq (α := Ideal R)
    (Ideal.span
      (singleton (α := R)
        (((↑(quotientSpanXSubCAlgEquiv y) : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y} →+* R) :
              (a : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y}) → R)
            ((Ideal.Quotient.mkₐ R (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}) :
                  (a : R[X]) → R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y})
                ((C : (a : R) → R[X]) x) :
              HasQuotient.Quotient R[X] (B := Ideal R[X])
                (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])})) :
          R)))
    (Ideal.span {x})
⊢ Eq (α := Ideal R)
    (Ideal.map (R :=
      HasQuotient.Quotient R[X] (B := Ideal R[X])
        (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}))
      (F :=
      HasQuotient.Quotient R[X] (B := Ideal R[X])
          (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}) →+*
        R)
      (↑(quotientSpanXSubCAlgEquiv y) : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y} →+* R)
      (Ideal.map (R := R[X]) (F :=
        R[X] →ₐ[R]
          HasQuotient.Quotient R[X] (B := Ideal R[X])
            (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}))
        (Ideal.Quotient.mkₐ R (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}))
        (Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) x : R[X])))))
    (Ideal.span {x})

Tactic:
simp only [Ideal.map_span, Set.image_singleton]

Premises used: Set.image_singleton, Ideal.map_span
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
x y : R
e_s :
  ((↑(quotientSpanXSubCAlgEquiv y) : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y} →+* R) :
        (a : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y}) → R)
      ((Ideal.Quotient.mkₐ R (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}) :
            (a : R[X]) → R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y})
          ((C : (a : R) → R[X]) x) :
        HasQuotient.Quotient R[X] (B := Ideal R[X])
          (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])})) =
    x
⊢ Eq (α := Ideal R)
    (Ideal.span
      (singleton (α := R)
        (((↑(quotientSpanXSubCAlgEquiv y) : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y} →+* R) :
              (a : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y}) → R)
            ((Ideal.Quotient.mkₐ R (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}) :
                  (a : R[X]) → R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y})
                ((C : (a : R) → R[X]) x) :
              HasQuotient.Quotient R[X] (B := Ideal R[X])
                (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])})) :
          R)))
    (Ideal.span {x})

Tactic:
congr 2
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
x y : R
⊢ ((↑(quotientSpanXSubCAlgEquiv y) : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y} →+* R) :
        (a : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y}) → R)
      ((Ideal.Quotient.mkₐ R (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}) :
            (a : R[X]) → R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y})
          ((C : (a : R) → R[X]) x) :
        HasQuotient.Quotient R[X] (B := Ideal R[X])
          (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])})) =
    x

Tactic:
eval_C

Premises used: Polynomial.eval, Polynomial.eval_C, Quotient.liftOn', AddCon.liftOn, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
x y : R
⊢ ((↑(quotientSpanXSubCAlgEquiv y) : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y} →+* R) :
        (a : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y}) → R)
      ((Ideal.Quotient.mkₐ R (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])}) :
            (a : R[X]) → R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) y})
          ((C : (a : R) → R[X]) x) :
        HasQuotient.Quotient R[X] (B := Ideal R[X])
          (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) y : R[X])})) =
    x

Tactic:
exact eval_C

Premises used: Polynomial.eval_C
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hq : q.Monic
rw :
  q ∣ p ↔
    Eq (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
      ((Ideal.Quotient.mk (Ideal.span {q}) : (a : R[X]) → R[X] ⧸ Ideal.span {q}) p :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
      (0 : HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
rw₁ rw₂ : q ∣ p ↔ q ∣ p
⊢ p %ₘ q = 0 ↔
    Eq (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
      ((Ideal.Quotient.mk (Ideal.span {q}) : (a : R[X]) → R[X] ⧸ Ideal.span {q}) p :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))
      (0 : HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {q}))

Tactic:
rw [modByMonic_eq_zero_iff_dvd hq, Ideal.Quotient.eq_zero_iff_dvd]

Premises used: Polynomial.modByMonic_eq_zero_iff_dvd, Ideal.Quotient.eq_zero_iff_dvd
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
ha : a ∈ I
rw : Membership.mem (α := R[X]) (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) ((C : (a : R) → R[X]) a : R[X])
⊢ Eq (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
    ((RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C : (a : R) → R[X] ⧸ map C I) a :
      HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
    (0 : HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))

Tactic:
rw [RingHom.comp_apply, Quotient.eq_zero_iff_mem]

Premises used: Ideal.Quotient.eq_zero_iff_mem, RingHom.comp_apply
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ Membership.mem (α := R[X]) (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) ((C : (a : R) → R[X]) a : R[X])

Tactic:
mem_map_of_mem _ ha

Premises used: Ideal.mem_map_of_mem, Set.Mem
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ Membership.mem (α := R[X]) (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) ((C : (a : R) → R[X]) a : R[X])

Tactic:
exact mem_map_of_mem _ ha

Premises used: Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
rw :
  Eq (α := (R ⧸ I)[X])
    ((eval₂RingHom (RingHom.comp C (Quotient.mk I)) X : (a : R[X]) → (R ⧸ I)[X])
      (a.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a))
    0
⊢ Eq (α := (R ⧸ I)[X]) ((eval₂RingHom (RingHom.comp C (Quotient.mk I)) X : (a : R[X]) → (R ⧸ I)[X]) a : (R ⧸ I)[X])
    (0 : (R ⧸ I)[X])

Tactic:
rw [← sum_monomial_eq a]

Premises used: Polynomial.sum_monomial_eq
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
rw :
  Eq (α := (R ⧸ I)[X])
    (a.sum fun (n : ℕ) (a : R) ↦ eval₂ (RingHom.comp C (Quotient.mk I)) X ((monomial n : (a : R) → R[X]) a)) 0
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X (a.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a) = 0

Tactic:
rw [eval₂_sum]

Premises used: Polynomial.eval₂_sum
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
⊢ Eq (α := (R ⧸ I)[X])
    (a.sum fun (n : ℕ) (a : R) ↦ eval₂ (RingHom.comp C (Quotient.mk I)) X ((monomial n : (a : R) → R[X]) a)) 0

Tactic:
Finset.sum_eq_zero fun n _ => ?_

Premises used: Finset.sum_eq_zero, Polynomial.sum
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
refine :
  ∀ n ∈ a.support,
    Eq.{u_1 + 1} (α := (R ⧸ I)[X])
      ((fun (n : ℕ) (a : R) ↦ eval₂ (RingHom.comp C (Quotient.mk I)) X ((monomial n : (a : R) → R[X]) a)) n (a.coeff n))
      0
⊢ Eq (α := (R ⧸ I)[X])
    (a.sum fun (n : ℕ) (a : R) ↦ eval₂ (RingHom.comp C (Quotient.mk I)) X ((monomial n : (a : R) → R[X]) a)) 0

Tactic:
refine Finset.sum_eq_zero fun n _ => ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
n : ℕ
h : n ∈ a.support
rw :
  HMul.hMul (α := (R ⧸ I)[X]) ((RingHom.comp C (Quotient.mk I) : (a : R) → (R ⧸ I)[X]) (a.coeff n) : (R ⧸ I)[X])
      (HPow.hPow (α := (R ⧸ I)[X]) X n) =
    0
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X ((monomial n : (a : R) → R[X]) (a.coeff n)) = 0

Tactic:
rw [eval₂_monomial (C.comp (Quotient.mk I)) X]

Premises used: Polynomial.C, Polynomial.eval₂_monomial, Ideal.Quotient.mk, RingHom.comp, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
n : ℕ
h : n ∈ a.support
⊢ HMul.hMul (α := (R ⧸ I)[X]) ((RingHom.comp C (Quotient.mk I) : (a : R) → (R ⧸ I)[X]) (a.coeff n) : (R ⧸ I)[X])
      (HPow.hPow (α := (R ⧸ I)[X]) X n) =
    0

Tactic:
mul_eq_zero_of_left (Polynomial.ext fun m => ?_) (X ^ n)

Premises used: Polynomial.ext, mul_eq_zero_of_left, HPow.hPow, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
n : ℕ
h : n ∈ a.support
refine :
  ∀ (m : ℕ),
    Eq.{u_1 + 1} (α := R ⧸ I) (coeff ((RingHom.comp C (Quotient.mk I) : (a : R) → (R ⧸ I)[X]) (a.coeff n)) m)
      (coeff 0 m)
⊢ HMul.hMul (α := (R ⧸ I)[X]) ((RingHom.comp C (Quotient.mk I) : (a : R) → (R ⧸ I)[X]) (a.coeff n) : (R ⧸ I)[X])
      (HPow.hPow (α := (R ⧸ I)[X]) X n) =
    0

Tactic:
refine mul_eq_zero_of_left (Polynomial.ext fun m => ?_) (X ^ n)

Premises used: Polynomial.ext, mul_eq_zero_of_left, HPow.hPow, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
n : ℕ
h : n ∈ a.support
m : ℕ
rw : Eq (α := R ⧸ I) (if m = 0 then (Quotient.mk I : (a : R) → R ⧸ I) (a.coeff n) else 0 : R ⧸ I) (coeff 0 m : R ⧸ I)
⊢ Eq.{u_1 + 1} (α := R ⧸ I) (coeff ((RingHom.comp C (Quotient.mk I) : (a : R) → (R ⧸ I)[X]) (a.coeff n)) m) (coeff 0 m)

Tactic:
rw [RingHom.comp_apply, coeff_C]

Premises used: Polynomial.coeff_C, RingHom.comp_apply
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
n : ℕ
h : n ∈ a.support
m : ℕ
pos :
  ∀ (h : m = 0),
    Eq (α := R ⧸ I) (if m = 0 then (Quotient.mk I : (a : R) → R ⧸ I) (a.coeff n) else 0 : R ⧸ I) (coeff 0 m : R ⧸ I)
neg :
  ∀ (h : ¬m = 0),
    Eq (α := R ⧸ I) (if m = 0 then (Quotient.mk I : (a : R) → R ⧸ I) (a.coeff n) else 0 : R ⧸ I) (coeff 0 m : R ⧸ I)
⊢ Eq (α := R ⧸ I) (if m = 0 then (Quotient.mk I : (a : R) → R ⧸ I) (a.coeff n) else 0 : R ⧸ I) (coeff 0 m : R ⧸ I)

Tactic:
by_cases h : m = 0
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
n : ℕ
h_1 : n ∈ a.support
m : ℕ
h : m = 0
⊢ Eq (α := R ⧸ I) (if m = 0 then (Quotient.mk I : (a : R) → R ⧸ I) (a.coeff n) else 0 : R ⧸ I) (coeff 0 m : R ⧸ I)

Tactic:
simpa [h] using Quotient.eq_zero_iff_mem.2 ((mem_map_C_iff.1 ha) n)

Premises used: Iff.mpr, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_map_C_iff, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R[X]
ha : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) a
n : ℕ
h_1 : n ∈ a.support
m : ℕ
h : ¬m = 0
⊢ Eq (α := R ⧸ I) (if m = 0 then (Quotient.mk I : (a : R) → R ⧸ I) (a.coeff n) else 0 : R ⧸ I) (coeff 0 m : R ⧸ I)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
⊢ (Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
        (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
      ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
            ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
          (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
        f) =
    f

Tactic:
Polynomial.induction_on' f ?_ ?_

Premises used: Polynomial.induction_on'
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
refine_1 :
  ∀ (p q : (R ⧸ I)[X]),
    (Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
            (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
          ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
                ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
              (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
            p) =
        p →
      (Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
              (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
            ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
                  ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
                (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
              q) =
          q →
        (Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
              (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
            ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
                  ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
                (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
              (p + q)) =
          p + q
refine_2 :
  ∀ (n : ℕ) (a : R ⧸ I),
    Eq (α := (R ⧸ I)[X])
      ((Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
            (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
          ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
                ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
              (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
            ((monomial n : (a : R ⧸ I) → (R ⧸ I)[X]) a)) :
        (R ⧸ I)[X])
      ((monomial n : (a : R ⧸ I) → (R ⧸ I)[X]) a : (R ⧸ I)[X])
⊢ (Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
        (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
      ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
            ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
          (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
        f) =
    f

Tactic:
refine Polynomial.induction_on' f ?_ ?_
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f p q : (R ⧸ I)[X]
hp :
  (Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
        (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
      (eval₂ (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
        ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) p) =
    p
hq :
  (Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
        (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
      (eval₂ (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
        ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) q) =
    q
⊢ (Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
        (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
      ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
            ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
          (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
        (p + q)) =
    p + q

Tactic:
simp only [coe_eval₂RingHom, hp, hq, map_add]

Premises used: map_add, Polynomial.coe_eval₂RingHom
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
n : ℕ
a : R ⧸ I
x : R
⊢ Eq (α := (R ⧸ I)[X])
    ((Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
          (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
        ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
              ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
            (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
          ((monomial n : (a : R ⧸ I) → (R ⧸ I)[X]) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) x))) :
      (R ⧸ I)[X])
    ((monomial n : (a : R ⧸ I) → (R ⧸ I)[X]) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) x) : (R ⧸ I)[X])

Tactic:
simp only [← smul_X_eq_monomial, C_mul', Quotient.lift_mk, Submodule.Quotient.quot_mk_eq_mk,
        Quotient.mk_eq_mk, eval₂_X_pow, eval₂_smul, coe_eval₂RingHom, map_pow, eval₂_C,
        RingHom.coe_comp, map_mul, eval₂_X, Function.comp_apply]

Premises used: Polynomial.eval₂_X_pow, Polynomial.C_mul', map_pow, Ideal.Quotient.lift_mk, map_mul, Polynomial.eval₂_X, RingHom.coe_comp, Ideal.Quotient.mk_eq_mk, Polynomial.eval₂_C, Function.comp_apply, Submodule.Quotient.quot_mk_eq_mk, Polynomial.eval₂_smul, Polynomial.smul_X_eq_monomial, Polynomial.coe_eval₂RingHom
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
x : HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I)
f : R[X]
⊢ Eq (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
    ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
            ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
          (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
        ((Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
            (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
          (Quot.mk (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop) f)) :
      HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
    (Quot.mk (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop) f :
      Quot (α := R[X]) (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop))

Tactic:
Polynomial.induction_on' f ?_ ?_

Premises used: Polynomial.induction_on'
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
x : HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I)
f : R[X]
n : ℕ
a : R
⊢ Eq (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
    ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
            ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
          (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
        ((Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
            (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
          (Quot.mk (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop) ((monomial n : (a : R) → R[X]) a))) :
      HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
    (Quot.mk (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop) ((monomial n : (a : R) → R[X]) a) :
      Quot (α := R[X]) (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop))

Tactic:
simp only [← smul_X_eq_monomial, ← C_mul' a (X ^ n), Quotient.lift_mk,
        Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk,
        coe_eval₂RingHom, map_pow, eval₂_C, RingHom.coe_comp, map_mul, eval₂_X,
        Function.comp_apply]

Premises used: Polynomial.C_mul', map_pow, Ideal.Quotient.lift_mk, map_mul, HPow.hPow, Polynomial.eval₂_X, RingHom.coe_comp, Ideal.Quotient.mk_eq_mk, Polynomial.eval₂_C, Function.comp_apply, Submodule.Quotient.quot_mk_eq_mk, Polynomial.X, Polynomial.smul_X_eq_monomial, Polynomial.coe_eval₂RingHom
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f g : (R ⧸ I)[X]
⊢ (eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
          ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
        (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
      (f * g) =
    HMul.hMul (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I)) (β :=
      HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
      ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
              ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
            (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
          f :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
      ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
              ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
            (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
          g :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))

Tactic:
simp only [coe_eval₂RingHom, eval₂_mul]

Premises used: Polynomial.eval₂_mul, Polynomial.coe_eval₂RingHom