Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
⊢ ∀ (a : R),
    eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
        (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
        ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          ((Ideal.Quotient.mk (Ideal.map C I)) (C a))) =
      (Ideal.Quotient.mk (Ideal.map C I)) (C a)

pp: case add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
          ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) p)) =
        (Ideal.Quotient.mk (Ideal.map C I)) p →
      eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
            ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
              ((Ideal.Quotient.mk (Ideal.map C I)) q)) =
          (Ideal.Quotient.mk (Ideal.map C I)) q →
        eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
            ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
              ((Ideal.Quotient.mk (Ideal.map C I)) (p + q))) =
          (Ideal.Quotient.mk (Ideal.map C I)) (p + q)

pp: case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
          ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) p)) =
        (Ideal.Quotient.mk (Ideal.map C I)) p →
      eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
          ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) (p * X n))) =
        (Ideal.Quotient.mk (Ideal.map C I)) (p * X n)

Tactic:
· intro r
    rw [Ideal.Quotient.lift_mk, eval₂Hom_C, RingHom.comp_apply, eval₂_C, Ideal.Quotient.lift_mk,
      RingHom.comp_apply]

Goal state after:
case add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
          ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) p)) =
        (Ideal.Quotient.mk (Ideal.map C I)) p →
      eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
            ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
              ((Ideal.Quotient.mk (Ideal.map C I)) q)) =
          (Ideal.Quotient.mk (Ideal.map C I)) q →
        eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
            ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
              ((Ideal.Quotient.mk (Ideal.map C I)) (p + q))) =
          (Ideal.Quotient.mk (Ideal.map C I)) (p + q)

case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
          ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) p)) =
        (Ideal.Quotient.mk (Ideal.map C I)) p →
      eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
          (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i))
          ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) (p * X n))) =
        (Ideal.Quotient.mk (Ideal.map C I)) (p * X n)