-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin
    (hx : AlgebraicIndependent R x) (a : A) :
    RingHom.comp
        (↑(Polynomial.aeval a : Polynomial (adjoin R (Set.range x)) →ₐ[_] A) :
          Polynomial (adjoin R (Set.range x)) →+* A)
        hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom =
      ↑(MvPolynomial.aeval fun o : Option ι => o.elim a x : MvPolynomial (Option ι) R →ₐ[R] A)

Proof state:
case refine_1
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
r : R
⊢ (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (C r)) = (aeval fun o => o.elim a x) (C r)

Tactic:
rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_C, aeval_C, Polynomial.aeval_C,
  IsScalarTower.algebraMap_apply R (adjoin R (range x)) A]

Result:
no goals

Proof state:
case refine_2.some
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
⊢ (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (X (some i))) =
    (aeval fun o => o.elim a x) (X (some i))

Tactic:
rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Polynomial.aeval_C,
  hx.algebraMap_aevalEquiv, aeval_X, aeval_X, Option.elim]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ (↑(Polynomial.aeval a)).comp hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom = ↑(aeval fun o => o.elim a x)

Tactic:
refine MvPolynomial.ringHom_ext ?_ ?_ <;>
  simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom,
    AlgHom.coe_toRingHom, AlgHom.coe_toRingHom]

Result:
case refine_1
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ ∀ (r : R), (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (C r)) = (aeval fun o => o.elim a x) (C r)

case refine_2
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ ∀ (i : Option ι),
    (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (X i)) = (aeval fun o => o.elim a x) (X i)

Proof state:
case refine_2
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ ∀ (i : Option ι),
    (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (X i)) = (aeval fun o => o.elim a x) (X i)

Tactic:
rintro (⟨⟩ | ⟨i⟩)

Result:
case refine_2.none
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (X none)) = (aeval fun o => o.elim a x) (X none)

case refine_2.some
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
⊢ (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (X (some i))) =
    (aeval fun o => o.elim a x) (X (some i))

Proof state:
case refine_1
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ ∀ (r : R), (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (C r)) = (aeval fun o => o.elim a x) (C r)

Tactic:
intro r

Result:
case refine_1
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
r : R
⊢ (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (C r)) = (aeval fun o => o.elim a x) (C r)

Proof state:
case refine_2.none
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (X none)) = (aeval fun o => o.elim a x) (X none)

Tactic:
rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_none, aeval_X, Polynomial.aeval_X,
  Option.elim]

Result:
no goals