-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
i : ι
rw :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
      ((aeval fun (o : Option ι) ↦
            o.elim Polynomial.X fun (s : ι) ↦
              (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s) :
          (a : MvPolynomial (Option ι) R) → Polynomial (MvPolynomial ι R))
        (X (some i))))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
      ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)))
rw₁ :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
      ((some i).elim Polynomial.X fun (s : ι) ↦
        (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s)))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
      ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)))
rw₂ :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
      ((Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X i)))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
      ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)))
rw₃ :
  Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
        (((↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x))) :
            (a : MvPolynomial ι R) → ↥(adjoin R (range x)))
          (X i)) :
      Polynomial ↥(adjoin R (range x)))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
        ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)) :
      Polynomial ↥(adjoin R (range x)))
⊢ Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
    ((hx.mvPolynomialOptionEquivPolynomialAdjoin : (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
        (X (some i)) :
      Polynomial ↥(adjoin R (range x)))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
        ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)) :
      Polynomial ↥(adjoin R (range x)))
have rw₄ : Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
  ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
      ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)) :
    Polynomial ↥(adjoin R (range x)))
  ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
      ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) (X i)) :
    Polynomial ↥(adjoin R (range x)))
Tactic: rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim,
    Polynomial.map_C, RingHom.coe_coe]