[GOAL]
R : Type u_1
inst✝ : CommRing R
x✝ x : R
⊢ ↑(aeval x✝) ((fun a => ↑C a) x) = x
[PROOFSTEP]
exact eval_C
[GOAL]
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ Ideal.span {↑C x, X - ↑C y} = Ideal.span {X - ↑C y} ⊔ ?m.223800 x y
[PROOFSTEP]
rw [Ideal.span_insert, sup_comm]
[GOAL]
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ Ideal.map (↑(quotientSpanXSubCAlgEquiv y))
      (Ideal.map (Ideal.Quotient.mkₐ R (Ideal.span {X - ↑C y})) (Ideal.span {↑C x})) =
    Ideal.span {x}
[PROOFSTEP]
simp only [Ideal.map_span, Set.image_singleton]
[GOAL]
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ Ideal.span {↑↑(quotientSpanXSubCAlgEquiv y) (↑(Ideal.Quotient.mkₐ R (Ideal.span {X - ↑C y})) (↑C x))} = Ideal.span {x}
[PROOFSTEP]
congr 2
[GOAL]
case e_s.e_a
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ ↑↑(quotientSpanXSubCAlgEquiv y) (↑(Ideal.Quotient.mkₐ R (Ideal.span {X - ↑C y})) (↑C x)) = x
[PROOFSTEP]
exact eval_C
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0
[PROOFSTEP]
intro a ha
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0
[PROOFSTEP]
rw [RingHom.comp_apply, Quotient.eq_zero_iff_mem]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ ↑C a ∈ map C I
[PROOFSTEP]
exact mem_map_of_mem _ ha
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0
[PROOFSTEP]
intro a ha
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) a = 0
[PROOFSTEP]
rw [← sum_monomial_eq a]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) (sum a fun n a => ↑(monomial n) a) = 0
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X (sum a fun n a => ↑(monomial n) a) = 0
[PROOFSTEP]
rw [eval₂_sum]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ (sum a fun n a => eval₂ (RingHom.comp C (Quotient.mk I)) X (↑(monomial n) a)) = 0
[PROOFSTEP]
refine' Finset.sum_eq_zero fun n _ => _
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
⊢ (fun n a => eval₂ (RingHom.comp C (Quotient.mk I)) X (↑(monomial n) a)) n (coeff a n) = 0
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X (↑(monomial n) (coeff a n)) = 0
[PROOFSTEP]
rw [eval₂_monomial (C.comp (Quotient.mk I)) X]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
⊢ ↑(RingHom.comp C (Quotient.mk I)) (coeff a n) * X ^ n = 0
[PROOFSTEP]
refine' mul_eq_zero_of_left (Polynomial.ext fun m => _) (X ^ n)
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
m : ℕ
⊢ coeff (↑(RingHom.comp C (Quotient.mk I)) (coeff a n)) m = coeff 0 m
[PROOFSTEP]
erw [coeff_C]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
m : ℕ
⊢ (if m = 0 then ↑(Quotient.mk I) (coeff a n) else 0) = coeff 0 m
[PROOFSTEP]
by_cases h : m = 0
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
m : ℕ
h : m = 0
⊢ (if m = 0 then ↑(Quotient.mk I) (coeff a n) else 0) = coeff 0 m
[PROOFSTEP]
simpa [h] using Quotient.eq_zero_iff_mem.2 ((mem_map_C_iff.1 ha) n)
[GOAL]
case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
m : ℕ
h : ¬m = 0
⊢ (if m = 0 then ↑(Quotient.mk I) (coeff a n) else 0) = coeff 0 m
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ Function.LeftInverse
    ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
        (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
    ↑(eval₂RingHom
        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
        (↑(Quotient.mk (map C I)) X))
[PROOFSTEP]
intro f
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
⊢ ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
      (↑(eval₂RingHom
            (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
              (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
            (↑(Quotient.mk (map C I)) X))
        f) =
    f
[PROOFSTEP]
refine Polynomial.induction_on' f ?_ ?_
[GOAL]
case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
⊢ ∀ (p q : (R ⧸ I)[X]),
    ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
              (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
          (↑(eval₂RingHom
                (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                  (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                (↑(Quotient.mk (map C I)) X))
            p) =
        p →
      ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
            (↑(eval₂RingHom
                  (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                    (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                  (↑(Quotient.mk (map C I)) X))
              q) =
          q →
        ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
            (↑(eval₂RingHom
                  (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                    (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                  (↑(Quotient.mk (map C I)) X))
              (p + q)) =
          p + q
[PROOFSTEP]
intro p q hp hq
[GOAL]
case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p q : (R ⧸ I)[X]
hp :
  ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
      (↑(eval₂RingHom
            (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
              (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
            (↑(Quotient.mk (map C I)) X))
        p) =
    p
hq :
  ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
      (↑(eval₂RingHom
            (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
              (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
            (↑(Quotient.mk (map C I)) X))
        q) =
    q
⊢ ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
      (↑(eval₂RingHom
            (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
              (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
            (↑(Quotient.mk (map C I)) X))
        (p + q)) =
    p + q
[PROOFSTEP]
simp only [coe_eval₂RingHom] at hp hq 
[GOAL]
case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p q : (R ⧸ I)[X]
hp :
  ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
      (eval₂
        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
        (↑(Quotient.mk (map C I)) X) p) =
    p
hq :
  ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
      (eval₂
        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
        (↑(Quotient.mk (map C I)) X) q) =
    q
⊢ ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
      (↑(eval₂RingHom
            (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
              (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
            (↑(Quotient.mk (map C I)) X))
        (p + q)) =
    p + q
[PROOFSTEP]
simp only [coe_eval₂RingHom, hp, hq, RingHom.map_add]
[GOAL]
case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
⊢ ∀ (n : ℕ) (a : R ⧸ I),
    ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
            (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
        (↑(eval₂RingHom
              (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
              (↑(Quotient.mk (map C I)) X))
          (↑(monomial n) a)) =
      ↑(monomial n) a
[PROOFSTEP]
rintro n ⟨x⟩
[GOAL]
case refine_2.mk
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
n : ℕ
a✝ : R ⧸ I
x : R
⊢ ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
      (↑(eval₂RingHom
            (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
              (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
            (↑(Quotient.mk (map C I)) X))
        (↑(monomial n) (Quot.mk Setoid.r x))) =
    ↑(monomial n) (Quot.mk Setoid.r x)
[PROOFSTEP]
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, RingHom.map_pow, eval₂_C, RingHom.coe_comp, RingHom.map_mul, eval₂_X,
  Function.comp_apply]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ Function.RightInverse
    ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
        (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
    ↑(eval₂RingHom
        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
        (↑(Quotient.mk (map C I)) X))
[PROOFSTEP]
rintro ⟨f⟩
[GOAL]
case mk
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f : R[X]
⊢ ↑(eval₂RingHom
          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
          (↑(Quotient.mk (map C I)) X))
      (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
            (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
        (Quot.mk Setoid.r f)) =
    Quot.mk Setoid.r f
[PROOFSTEP]
refine Polynomial.induction_on' f ?_ ?_
[GOAL]
case mk.refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f : R[X]
⊢ ∀ (p q : R[X]),
    ↑(eval₂RingHom
              (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
              (↑(Quotient.mk (map C I)) X))
          (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
            (Quot.mk Setoid.r p)) =
        Quot.mk Setoid.r p →
      ↑(eval₂RingHom
                (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                  (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                (↑(Quotient.mk (map C I)) X))
            (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                  (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
              (Quot.mk Setoid.r q)) =
          Quot.mk Setoid.r q →
        ↑(eval₂RingHom
                (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                  (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                (↑(Quotient.mk (map C I)) X))
            (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                  (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
              (Quot.mk Setoid.r (p + q))) =
          Quot.mk Setoid.r (p + q)
[PROOFSTEP]
intros p q hp hq
[GOAL]
case mk.refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f p q : R[X]
hp :
  ↑(eval₂RingHom
          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
          (↑(Quotient.mk (map C I)) X))
      (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
            (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
        (Quot.mk Setoid.r p)) =
    Quot.mk Setoid.r p
hq :
  ↑(eval₂RingHom
          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
          (↑(Quotient.mk (map C I)) X))
      (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
            (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
        (Quot.mk Setoid.r q)) =
    Quot.mk Setoid.r q
⊢ ↑(eval₂RingHom
          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
          (↑(Quotient.mk (map C I)) X))
      (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
            (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
        (Quot.mk Setoid.r (p + q))) =
    Quot.mk Setoid.r (p + q)
[PROOFSTEP]
simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, map_add, Quotient.lift_mk, coe_eval₂RingHom] at hp hq ⊢
[GOAL]
case mk.refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f p q : R[X]
hp :
  eval₂
      (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
        (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
      (↑(Quotient.mk (map C I)) X) (eval₂ (RingHom.comp C (Quotient.mk I)) X p) =
    ↑(Quotient.mk (map C I)) p
hq :
  eval₂
      (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
        (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
      (↑(Quotient.mk (map C I)) X) (eval₂ (RingHom.comp C (Quotient.mk I)) X q) =
    ↑(Quotient.mk (map C I)) q
⊢ eval₂
        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
        (↑(Quotient.mk (map C I)) X) (eval₂ (RingHom.comp C (Quotient.mk I)) X p) +
      eval₂
        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
        (↑(Quotient.mk (map C I)) X) (eval₂ (RingHom.comp C (Quotient.mk I)) X q) =
    ↑(Quotient.mk (map C I)) p + ↑(Quotient.mk (map C I)) q
[PROOFSTEP]
rw [hp, hq]
[GOAL]
case mk.refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f : R[X]
⊢ ∀ (n : ℕ) (a : R),
    ↑(eval₂RingHom
            (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
              (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
            (↑(Quotient.mk (map C I)) X))
        (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
              (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
          (Quot.mk Setoid.r (↑(monomial n) a))) =
      Quot.mk Setoid.r (↑(monomial n) a)
[PROOFSTEP]
intro n a
[GOAL]
case mk.refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f : R[X]
n : ℕ
a : R
⊢ ↑(eval₂RingHom
          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
          (↑(Quotient.mk (map C I)) X))
      (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
            (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
        (Quot.mk Setoid.r (↑(monomial n) a))) =
    Quot.mk Setoid.r (↑(monomial n) a)
[PROOFSTEP]
simp only [← smul_X_eq_monomial, ← C_mul' a (X ^ n), Quotient.lift_mk, Submodule.Quotient.quot_mk_eq_mk,
  Quotient.mk_eq_mk, eval₂_X_pow, eval₂_smul, coe_eval₂RingHom, RingHom.map_pow, eval₂_C, RingHom.coe_comp,
  RingHom.map_mul, eval₂_X, Function.comp_apply]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f g : (R ⧸ I)[X]
⊢ Equiv.toFun
      {
        toFun :=
          ↑(eval₂RingHom
              (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
              (↑(Quotient.mk (map C I)) X)),
        invFun :=
          ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
              (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0)),
        left_inv :=
          (_ :
            ∀ (f : (R ⧸ I)[X]),
              ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                      (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                  (↑(eval₂RingHom
                        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                        (↑(Quotient.mk (map C I)) X))
                    f) =
                f),
        right_inv :=
          (_ :
            ∀ (x : R[X] ⧸ map C I),
              ↑(eval₂RingHom
                      (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                        (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                      (↑(Quotient.mk (map C I)) X))
                  (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                        (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                    x) =
                x) }
      (f * g) =
    Equiv.toFun
        {
          toFun :=
            ↑(eval₂RingHom
                (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                  (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                (↑(Quotient.mk (map C I)) X)),
          invFun :=
            ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0)),
          left_inv :=
            (_ :
              ∀ (f : (R ⧸ I)[X]),
                ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                        (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                    (↑(eval₂RingHom
                          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                          (↑(Quotient.mk (map C I)) X))
                      f) =
                  f),
          right_inv :=
            (_ :
              ∀ (x : R[X] ⧸ map C I),
                ↑(eval₂RingHom
                        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                        (↑(Quotient.mk (map C I)) X))
                    (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                      x) =
                  x) }
        f *
      Equiv.toFun
        {
          toFun :=
            ↑(eval₂RingHom
                (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                  (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                (↑(Quotient.mk (map C I)) X)),
          invFun :=
            ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0)),
          left_inv :=
            (_ :
              ∀ (f : (R ⧸ I)[X]),
                ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                        (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                    (↑(eval₂RingHom
                          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                          (↑(Quotient.mk (map C I)) X))
                      f) =
                  f),
          right_inv :=
            (_ :
              ∀ (x : R[X] ⧸ map C I),
                ↑(eval₂RingHom
                        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                        (↑(Quotient.mk (map C I)) X))
                    (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                      x) =
                  x) }
        g
[PROOFSTEP]
simp only [coe_eval₂RingHom, eval₂_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f g : (R ⧸ I)[X]
⊢ Equiv.toFun
      {
        toFun :=
          ↑(eval₂RingHom
              (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
              (↑(Quotient.mk (map C I)) X)),
        invFun :=
          ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
              (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0)),
        left_inv :=
          (_ :
            ∀ (f : (R ⧸ I)[X]),
              ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                      (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                  (↑(eval₂RingHom
                        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                        (↑(Quotient.mk (map C I)) X))
                    f) =
                f),
        right_inv :=
          (_ :
            ∀ (x : R[X] ⧸ map C I),
              ↑(eval₂RingHom
                      (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                        (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                      (↑(Quotient.mk (map C I)) X))
                  (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                        (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                    x) =
                x) }
      (f + g) =
    Equiv.toFun
        {
          toFun :=
            ↑(eval₂RingHom
                (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                  (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                (↑(Quotient.mk (map C I)) X)),
          invFun :=
            ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0)),
          left_inv :=
            (_ :
              ∀ (f : (R ⧸ I)[X]),
                ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                        (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                    (↑(eval₂RingHom
                          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                          (↑(Quotient.mk (map C I)) X))
                      f) =
                  f),
          right_inv :=
            (_ :
              ∀ (x : R[X] ⧸ map C I),
                ↑(eval₂RingHom
                        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                        (↑(Quotient.mk (map C I)) X))
                    (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                      x) =
                  x) }
        f +
      Equiv.toFun
        {
          toFun :=
            ↑(eval₂RingHom
                (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                  (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                (↑(Quotient.mk (map C I)) X)),
          invFun :=
            ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0)),
          left_inv :=
            (_ :
              ∀ (f : (R ⧸ I)[X]),
                ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                        (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                    (↑(eval₂RingHom
                          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                          (↑(Quotient.mk (map C I)) X))
                      f) =
                  f),
          right_inv :=
            (_ :
              ∀ (x : R[X] ⧸ map C I),
                ↑(eval₂RingHom
                        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                        (↑(Quotient.mk (map C I)) X))
                    (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                      x) =
                  x) }
        g
[PROOFSTEP]
simp only [eval₂_add, coe_eval₂RingHom]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ ↑(RingEquiv.symm (polynomialQuotientEquivQuotientPolynomial I)) (↑(Quotient.mk (map C I)) f) =
    Polynomial.map (Quotient.mk I) f
[PROOFSTEP]
rw [polynomialQuotientEquivQuotientPolynomial, RingEquiv.symm_mk, RingEquiv.coe_mk, Equiv.coe_fn_mk, Quotient.lift_mk,
  coe_eval₂RingHom, eval₂_eq_eval_map, ← Polynomial.map_map, ← eval₂_eq_eval_map, Polynomial.eval₂_C_X]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ ↑(polynomialQuotientEquivQuotientPolynomial I) (Polynomial.map (Quotient.mk I) f) = ↑(Quotient.mk (map C I)) f
[PROOFSTEP]
apply (polynomialQuotientEquivQuotientPolynomial I).symm.injective
[GOAL]
case a
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ ↑(RingEquiv.symm (polynomialQuotientEquivQuotientPolynomial I))
      (↑(polynomialQuotientEquivQuotientPolynomial I) (Polynomial.map (Quotient.mk I) f)) =
    ↑(RingEquiv.symm (polynomialQuotientEquivQuotientPolynomial I)) (↑(Quotient.mk (map C I)) f)
[PROOFSTEP]
rw [RingEquiv.symm_apply_apply, polynomialQuotientEquivQuotientPolynomial_symm_mk]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ x = 0
[PROOFSTEP]
let i := ((Quotient.mk I).comp C).rangeRestrict
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
⊢ x = 0
[PROOFSTEP]
have hi' : RingHom.ker (Polynomial.mapRingHom i) ≤ I :=
  by
  refine' fun f hf => polynomial_mem_ideal_of_coeff_mem_ideal I f fun n => _
  rw [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]
  rw [RingHom.mem_ker, coe_mapRingHom] at hf 
  replace hf := congr_arg (fun f : Polynomial _ => f.coeff n) hf
  simp only [coeff_map, coeff_zero] at hf 
  rwa [Subtype.ext_iff, RingHom.coe_rangeRestrict] at hf 
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
⊢ RingHom.ker (mapRingHom i) ≤ I
[PROOFSTEP]
refine' fun f hf => polynomial_mem_ideal_of_coeff_mem_ideal I f fun n => _
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
n : ℕ
⊢ coeff f n ∈ comap C I
[PROOFSTEP]
rw [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
n : ℕ
⊢ ↑(RingHom.comp (Quotient.mk I) C) (coeff f n) = 0
[PROOFSTEP]
rw [RingHom.mem_ker, coe_mapRingHom] at hf 
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
hf : Polynomial.map i f = 0
n : ℕ
⊢ ↑(RingHom.comp (Quotient.mk I) C) (coeff f n) = 0
[PROOFSTEP]
replace hf := congr_arg (fun f : Polynomial _ => f.coeff n) hf
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
n : ℕ
hf : (fun f => coeff f n) (Polynomial.map i f) = (fun f => coeff f n) 0
⊢ ↑(RingHom.comp (Quotient.mk I) C) (coeff f n) = 0
[PROOFSTEP]
simp only [coeff_map, coeff_zero] at hf 
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
n : ℕ
hf : ↑(RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)) (coeff f n) = 0
⊢ ↑(RingHom.comp (Quotient.mk I) C) (coeff f n) = 0
[PROOFSTEP]
rwa [Subtype.ext_iff, RingHom.coe_rangeRestrict] at hf 
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
⊢ x = 0
[PROOFSTEP]
obtain ⟨x, hx'⟩ := x
[GOAL]
case mk
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
x : R[X] ⧸ I
hx' : x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx : ↑C { val := x, property := hx' } ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ { val := x, property := hx' } = 0
[PROOFSTEP]
obtain ⟨y, rfl⟩ := RingHom.mem_range.1 hx'
[GOAL]
case mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } = 0
[PROOFSTEP]
refine' Subtype.eq _
[GOAL]
case mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ ↑{ val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } = ↑0
[PROOFSTEP]
simp only [RingHom.comp_apply, Quotient.eq_zero_iff_mem, ZeroMemClass.coe_zero]
[GOAL]
case mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ ↑C y ∈ I
[PROOFSTEP]
suffices C (i y) ∈ I.map (Polynomial.mapRingHom i)
  by
  obtain ⟨f, hf⟩ :=
    mem_image_of_mem_map_of_surjective (Polynomial.mapRingHom i)
      (Polynomial.map_surjective _ (RingHom.rangeRestrict_surjective ((Quotient.mk I).comp C))) this
  refine' sub_add_cancel (C y) f ▸ I.add_mem (hi' _ : C y - f ∈ I) hf.1
  rw [RingHom.mem_ker, RingHom.map_sub, hf.2, sub_eq_zero, coe_mapRingHom, map_C]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
this : ↑C (↑i y) ∈ map (mapRingHom i) I
⊢ ↑C y ∈ I
[PROOFSTEP]
obtain ⟨f, hf⟩ :=
  mem_image_of_mem_map_of_surjective (Polynomial.mapRingHom i)
    (Polynomial.map_surjective _ (RingHom.rangeRestrict_surjective ((Quotient.mk I).comp C))) this
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
this : ↑C (↑i y) ∈ map (mapRingHom i) I
f : R[X]
hf : f ∈ ↑I ∧ ↑(mapRingHom i) f = ↑C (↑i y)
⊢ ↑C y ∈ I
[PROOFSTEP]
refine' sub_add_cancel (C y) f ▸ I.add_mem (hi' _ : C y - f ∈ I) hf.1
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
this : ↑C (↑i y) ∈ map (mapRingHom i) I
f : R[X]
hf : f ∈ ↑I ∧ ↑(mapRingHom i) f = ↑C (↑i y)
⊢ ↑C y - f ∈ RingHom.ker (mapRingHom i)
[PROOFSTEP]
rw [RingHom.mem_ker, RingHom.map_sub, hf.2, sub_eq_zero, coe_mapRingHom, map_C]
[GOAL]
case mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ ↑C (↑i y) ∈ map (mapRingHom i) I
[PROOFSTEP]
exact hx
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
i : R
hi : i ∈ I
⊢ ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0
[PROOFSTEP]
simp only [Function.comp_apply, RingHom.coe_comp, Ideal.Quotient.eq_zero_iff_mem]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
i : R
hi : i ∈ I
⊢ ↑C i ∈ Ideal.map C I
[PROOFSTEP]
exact Ideal.mem_map_of_mem _ hi
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
⊢ ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0
[PROOFSTEP]
rw [as_sum a]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
⊢ ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) (Finset.sum (support a) fun v => ↑(monomial v) (coeff v a)) = 0
[PROOFSTEP]
rw [coe_eval₂Hom, eval₂_sum]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
⊢ (Finset.sum (support a) fun x => eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X (↑(monomial x) (coeff x a))) = 0
[PROOFSTEP]
refine' Finset.sum_eq_zero fun n _ => _
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
⊢ eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X (↑(monomial n) (coeff n a)) = 0
[PROOFSTEP]
simp only [eval₂_monomial, Function.comp_apply, RingHom.coe_comp]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
⊢ (↑C (↑(Ideal.Quotient.mk I) (coeff n a)) * Finsupp.prod n fun n e => X n ^ e) = 0
[PROOFSTEP]
refine' mul_eq_zero_of_left _ _
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
⊢ ↑C (↑(Ideal.Quotient.mk I) (coeff n a)) = 0
[PROOFSTEP]
suffices coeff n a ∈ I by
  rw [← @Ideal.mk_ker R _ I, RingHom.mem_ker] at this 
  simp only [this, C_0]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
this : coeff n a ∈ I
⊢ ↑C (↑(Ideal.Quotient.mk I) (coeff n a)) = 0
[PROOFSTEP]
rw [← @Ideal.mk_ker R _ I, RingHom.mem_ker] at this 
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
this : ↑(Ideal.Quotient.mk I) (coeff n a) = 0
⊢ ↑C (↑(Ideal.Quotient.mk I) (coeff n a)) = 0
[PROOFSTEP]
simp only [this, C_0]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
⊢ coeff n a ∈ I
[PROOFSTEP]
exact mem_map_C_iff.1 ha n
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
⊢ Function.RightInverse
    (eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
    ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
        (_ : ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
[PROOFSTEP]
intro f
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
⊢ ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) f) =
    f
[PROOFSTEP]
apply induction_on f
[GOAL]
case h_C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
⊢ ∀ (a : R ⧸ I),
    ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (eval₂
          (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
            (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
          (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (↑C a)) =
      ↑C a
[PROOFSTEP]
intro r
[GOAL]
case h_C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r✝ : R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
r : R ⧸ I
⊢ ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (↑C r)) =
    ↑C r
[PROOFSTEP]
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
[GOAL]
case h_C.intro
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r✝ : R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
r : R
⊢ ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (↑C (↑(Ideal.Quotient.mk I) r))) =
    ↑C (↑(Ideal.Quotient.mk I) r)
[PROOFSTEP]
rw [eval₂_C, Ideal.Quotient.lift_mk, RingHom.comp_apply, Ideal.Quotient.lift_mk, eval₂Hom_C, RingHom.comp_apply]
[GOAL]
case h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
⊢ ∀ (p q : MvPolynomial σ (R ⧸ I)),
    ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
              (_ :
                ∀ (a : MvPolynomial σ R),
                  a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
          (eval₂
            (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
              (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
            (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
        p →
      ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
                (_ :
                  ∀ (a : MvPolynomial σ R),
                    a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
            (eval₂
              (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
                (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
              (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) q) =
          q →
        ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
                (_ :
                  ∀ (a : MvPolynomial σ R),
                    a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
            (eval₂
              (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
                (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
              (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p + q)) =
          p + q
[PROOFSTEP]
intros p q hp hq
[GOAL]
case h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p q : MvPolynomial σ (R ⧸ I)
hp :
  ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
    p
hq :
  ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) q) =
    q
⊢ ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p + q)) =
    p + q
[PROOFSTEP]
simp only [RingHom.map_add, MvPolynomial.coe_eval₂Hom, coe_eval₂Hom, MvPolynomial.eval₂_add] at hp hq ⊢
[GOAL]
case h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p q : MvPolynomial σ (R ⧸ I)
hp :
  ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
    p
hq :
  ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) q) =
    q
⊢ ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (eval₂
          (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
            (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
          (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) +
      ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (eval₂
          (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
            (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
          (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) q) =
    p + q
[PROOFSTEP]
rw [hp, hq]
[GOAL]
case h_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
⊢ ∀ (p : MvPolynomial σ (R ⧸ I)) (n : σ),
    ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
              (_ :
                ∀ (a : MvPolynomial σ R),
                  a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
          (eval₂
            (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
              (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
            (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
        p →
      ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
              (_ :
                ∀ (a : MvPolynomial σ R),
                  a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
          (eval₂
            (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
              (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
            (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p * X n)) =
        p * X n
[PROOFSTEP]
intros p i hp
[GOAL]
case h_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p : MvPolynomial σ (R ⧸ I)
i : σ
hp :
  ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
    p
⊢ ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p * X i)) =
    p * X i
[PROOFSTEP]
simp only [coe_eval₂Hom] at hp 
[GOAL]
case h_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p : MvPolynomial σ (R ⧸ I)
i : σ
hp :
  ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
    p
⊢ ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p * X i)) =
    p * X i
[PROOFSTEP]
simp only [hp, coe_eval₂Hom, Ideal.Quotient.lift_mk, eval₂_mul, RingHom.map_mul, eval₂_X]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
⊢ Function.LeftInverse
    (eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
    ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
        (_ : ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
[PROOFSTEP]
intro f
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ R ⧸ Ideal.map C I
⊢ eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        f) =
    f
[PROOFSTEP]
obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f
[GOAL]
case intro
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ R
⊢ eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (↑(Ideal.Quotient.mk (Ideal.map C I)) f)) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) f
[PROOFSTEP]
apply induction_on f
[GOAL]
case intro.h_C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ R
⊢ ∀ (a : R),
    eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
        (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
              (_ :
                ∀ (a : MvPolynomial σ R),
                  a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
          (↑(Ideal.Quotient.mk (Ideal.map C I)) (↑C a))) =
      ↑(Ideal.Quotient.mk (Ideal.map C I)) (↑C a)
[PROOFSTEP]
intro r
[GOAL]
case intro.h_C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r✝ : R
I : Ideal R
f : MvPolynomial σ R
r : R
⊢ eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (↑(Ideal.Quotient.mk (Ideal.map C I)) (↑C r))) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) (↑C r)
[PROOFSTEP]
rw [Ideal.Quotient.lift_mk, eval₂Hom_C, RingHom.comp_apply, eval₂_C, Ideal.Quotient.lift_mk, RingHom.comp_apply]
[GOAL]
case intro.h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    eval₂
          (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
            (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
          (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
          (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
                (_ :
                  ∀ (a : MvPolynomial σ R),
                    a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
            (↑(Ideal.Quotient.mk (Ideal.map C I)) p)) =
        ↑(Ideal.Quotient.mk (Ideal.map C I)) p →
      eval₂
            (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
              (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
            (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
            (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
                  (_ :
                    ∀ (a : MvPolynomial σ R),
                      a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
              (↑(Ideal.Quotient.mk (Ideal.map C I)) q)) =
          ↑(Ideal.Quotient.mk (Ideal.map C I)) q →
        eval₂
            (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
              (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
            (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
            (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
                  (_ :
                    ∀ (a : MvPolynomial σ R),
                      a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
              (↑(Ideal.Quotient.mk (Ideal.map C I)) (p + q))) =
          ↑(Ideal.Quotient.mk (Ideal.map C I)) (p + q)
[PROOFSTEP]
intros p q hp hq
[GOAL]
case intro.h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p q : MvPolynomial σ R
hp :
  eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (↑(Ideal.Quotient.mk (Ideal.map C I)) p)) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) p
hq :
  eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (↑(Ideal.Quotient.mk (Ideal.map C I)) q)) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) q
⊢ eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (↑(Ideal.Quotient.mk (Ideal.map C I)) (p + q))) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) (p + q)
[PROOFSTEP]
erw [Ideal.Quotient.lift_mk] at hp hq ⊢
[GOAL]
case intro.h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p q : MvPolynomial σ R
hp :
  eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) p) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) p
hq :
  eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) q) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) q
⊢ eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) (p + q)) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) (p + q)
[PROOFSTEP]
simp only [Submodule.Quotient.quot_mk_eq_mk, eval₂_add, RingHom.map_add, coe_eval₂Hom, Ideal.Quotient.lift_mk,
  Ideal.Quotient.mk_eq_mk] at hp hq ⊢
[GOAL]
case intro.h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p q : MvPolynomial σ R
hp :
  eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X p) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) p
hq :
  eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X q) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) q
⊢ eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X p) +
      eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X q) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) p + ↑(Ideal.Quotient.mk (Ideal.map C I)) q
[PROOFSTEP]
rw [hp, hq]
[GOAL]
case intro.h_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    eval₂
          (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
            (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
          (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
          (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
                (_ :
                  ∀ (a : MvPolynomial σ R),
                    a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
            (↑(Ideal.Quotient.mk (Ideal.map C I)) p)) =
        ↑(Ideal.Quotient.mk (Ideal.map C I)) p →
      eval₂
          (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
            (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
          (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
          (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
                (_ :
                  ∀ (a : MvPolynomial σ R),
                    a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
            (↑(Ideal.Quotient.mk (Ideal.map C I)) (p * X n))) =
        ↑(Ideal.Quotient.mk (Ideal.map C I)) (p * X n)
[PROOFSTEP]
intros p i hp
[GOAL]
case intro.h_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p : MvPolynomial σ R
i : σ
hp :
  eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (↑(Ideal.Quotient.mk (Ideal.map C I)) p)) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) p
⊢ eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (↑(Ideal.Quotient.mk (Ideal.map C I)) (p * X i))) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) (p * X i)
[PROOFSTEP]
simp only [Submodule.Quotient.quot_mk_eq_mk, coe_eval₂Hom, Ideal.Quotient.lift_mk, Ideal.Quotient.mk_eq_mk, eval₂_mul,
  RingHom.map_mul, eval₂_X] at hp ⊢
[GOAL]
case intro.h_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p : MvPolynomial σ R
i : σ
hp :
  eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X p) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) p
⊢ eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X p) *
      ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) p * ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)
[PROOFSTEP]
simp only [hp]
  -- Porting note: this definition was split to avoid timeouts.
