-- Mathlib/RingTheory/Polynomial/Quotient.lean
lemma quotientEquivQuotientMvPolynomial_leftInverse (I : Ideal R) :
    Function.LeftInverse
      (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 intro.h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p q : MvPolynomial σ R
hp :
  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
hq :
  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)

Tactic:
rw [Ideal.Quotient.lift_mk] at hp hq ⊢

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

Proof state:
case intro.h_C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
r : 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 r))) =
    (Ideal.Quotient.mk (Ideal.map C I)) (C r)

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

Result:
no goals

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

Tactic:
simp only [hp]

Result:
no goals

Proof state:
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R ⧸ Ideal.map C I
⊢ 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) ⋯) f) =
    f

Tactic:
obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f

Result:
case intro
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : 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)) f)) =
    (Ideal.Quotient.mk (Ideal.map C I)) f

Proof state:
case intro.h_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)

Tactic:
intros p q hp hq

Result:
case intro.h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p q : MvPolynomial σ R
hp :
  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
hq :
  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)

Proof state:
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
⊢ Function.LeftInverse
    (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 ⧸ Ideal.map C I
⊢ 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) ⋯) f) =
    f