-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Ideal (goal)
Goal:
A : Type u_3
σ : Type u_4
inst : CommRing A
I : Ideal (MvPolynomial σ A)
d : MvPolynomial σ A
h :
  Eq (α := MvPolynomial σ A ⧸ I)
    ((Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) d : MvPolynomial σ A ⧸ I)
    (eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
        (fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)) d :
      MvPolynomial σ A ⧸ I)
h₁ :
  Eq (α := MvPolynomial σ A ⧸ I)
    ((Ideal.Quotient.mkₐ A I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) d : MvPolynomial σ A ⧸ I)
    (eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
        (fun (d : σ) ↦ (Ideal.Quotient.mkₐ A I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)) d :
      MvPolynomial σ A ⧸ I)
h₂ :
  Eq (α := MvPolynomial σ A ⧸ I)
    ((aeval fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d) :
          (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I)
        d :
      MvPolynomial σ A ⧸ I)
    (eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
        (fun (d : σ) ↦
          (aeval fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d) :
              (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I)
            (X d))
        d :
      MvPolynomial σ A ⧸ I)
h₃ :
  Eq (α := MvPolynomial σ A ⧸ I)
    ((aeval fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d) :
          (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I)
        d :
      MvPolynomial σ A ⧸ I)
    (eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
        (fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)) d :
      MvPolynomial σ A ⧸ I)
h₄ :
  Eq (α := MvPolynomial σ A ⧸ I)
    (({
            toRingHom :=
              eval₂Hom (algebraMap A (MvPolynomial σ A ⧸ I)) fun (d : σ) ↦
                (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d),
            commutes' := ⋯ } :
          (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I)
        d :
      MvPolynomial σ A ⧸ I)
    (eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
        (fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)) d :
      MvPolynomial σ A ⧸ I)
⊢ OneHom.toFun
      (↑(↑(Ideal.Quotient.mk I) : MvPolynomial σ A →* MvPolynomial σ A ⧸ I) :
        OneHom (MvPolynomial σ A) (MvPolynomial σ A ⧸ I))
      d =
    eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
      (fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)) d
have h₅ : Eq (α := MvPolynomial σ A ⧸ I)
  ((eval₂Hom (algebraMap A (MvPolynomial σ A ⧸ I)) fun (d : σ) ↦
          (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d) :
        (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I)
      d :
    MvPolynomial σ A ⧸ I)
  (eval₂ (algebraMap A (MvPolynomial σ A ⧸ I))
      (fun (d : σ) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial σ A) → MvPolynomial σ A ⧸ I) (X d)) d :
    MvPolynomial σ A ⧸ I)
Tactic: simp_rw [RingHom.toFun_eq_coe, ← Ideal.Quotient.mkₐ_eq_mk A, mkₐ_eq_aeval, aeval_X, aeval,
    AlgHom.coe_mk, coe_eval₂Hom]