-- Mathlib/RingTheory/Polynomial/Quotient.lean
lemma quotientEquivQuotientMvPolynomial_rightInverse (I : Ideal R) :
    Function.RightInverse
      (eval₂ (Ideal.Quotient.lift I
        ((Ideal.Quotient.mk (Ideal.map C I : Ideal (MvPolynomial σ R))).comp C)
          fun _ hi => quotient_map_C_eq_zero hi)
          fun i => Ideal.Quotient.mk (Ideal.map C I : Ideal (MvPolynomial σ R)) (X i))
      (Ideal.Quotient.lift (Ideal.map C I : Ideal (MvPolynomial σ R))
        (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) fun _ ha => eval₂_C_mk_eq_zero ha)

Proof state:
case h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p q : MvPolynomial σ (R ⧸ I)
hp :
  (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
      (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)) p) =
    p
hq :
  (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
      (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)) q) =
    q
⊢ (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
        (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)) p) +
      (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
        (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)) q) =
    p + q

Tactic:
rw [hp, hq]

Result:
no goals

Proof state:
case h_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ (R ⧸ I)
i : σ
hp :
  (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
      (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)) p) =
    p
⊢ (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
      (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)) (p * X i)) =
    p * X i

Tactic:
simp only [hp, coe_eval₂Hom, Ideal.Quotient.lift_mk, eval₂_mul, RingHom.map_mul, eval₂_X]

Result:
no goals

Proof state:
case h_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
⊢ ∀ (p : MvPolynomial σ (R ⧸ I)) (n : σ),
    (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          (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)) p) =
        p →
      (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          (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)) (p * X n)) =
        p * X n

Tactic:
intros p i hp

Result:
case h_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ (R ⧸ I)
i : σ
hp :
  (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
      (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)) p) =
    p
⊢ (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
      (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)) (p * X i)) =
    p * X i

Proof state:
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
⊢ Function.RightInverse
    (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) ⋯)

Tactic:
intro f

Result:
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
⊢ (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
      (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)) f) =
    f

Proof state:
case h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
⊢ ∀ (p q : MvPolynomial σ (R ⧸ I)),
    (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          (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)) p) =
        p →
      (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            (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)) q) =
          q →
        (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            (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)) (p + q)) =
          p + q

Tactic:
intros p q hp hq

Result:
case h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p q : MvPolynomial σ (R ⧸ I)
hp :
  (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
      (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)) p) =
    p
hq :
  (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
      (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)) q) =
    q
⊢ (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
      (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)) (p + q)) =
    p + q