case refine'_1
ι : Type u_1
ι' : Type ?u.1231476
R : Type u_2
K : Type ?u.1231482
A : Type u_3
A' : Type ?u.1231488
A'' : Type ?u.1231491
V : Type u
V' : Type ?u.1231496
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a✝ b : R
hx : AlgebraicIndependent R x
a : A
⊢ ∀ (r : R),
    ↑(Polynomial.aeval a) (↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (↑C r)) =
      ↑(aeval fun o => Option.elim o a x) (↑C r)

case refine'_2
ι : Type u_1
ι' : Type ?u.1231476
R : Type u_2
K : Type ?u.1231482
A : Type u_3
A' : Type ?u.1231488
A'' : Type ?u.1231491
V : Type u
V' : Type ?u.1231496
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a✝ b : R
hx : AlgebraicIndependent R x
a : A
⊢ ∀ (i : Option ι),
    ↑(Polynomial.aeval a) (↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (X i)) =
      ↑(aeval fun o => Option.elim o a x) (X i)
ι : Type u_1
ι' : Type ?u.1231476
R : Type u_2
K : Type ?u.1231482
A : Type u_3
A' : Type ?u.1231488
A'' : Type ?u.1231491
V : Type u
V' : Type ?u.1231496
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a✝ b : R
hx : AlgebraicIndependent R x
a : A
⊢ RingHom.comp (↑(Polynomial.aeval a)) (RingEquiv.toRingHom (mvPolynomialOptionEquivPolynomialAdjoin hx)) =
    ↑(aeval fun o => Option.elim o a x)
refine' MvPolynomial.ringHom_ext _ _ <;>
  simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom,
    AlgHom.coe_toRingHom, AlgHom.coe_toRingHom]
case refine'_1
ι : Type u_1
ι' : Type ?u.1231476
R : Type u_2
K : Type ?u.1231482
A : Type u_3
A' : Type ?u.1231488
A'' : Type ?u.1231491
V : Type u
V' : Type ?u.1231496
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a✝ b : R
hx : AlgebraicIndependent R x
a : A
r : R
⊢ ↑(Polynomial.aeval a) (↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (↑C r)) =
    ↑(aeval fun o => Option.elim o a x) (↑C r)
case refine'_1
ι : Type u_1
ι' : Type ?u.1231476
R : Type u_2
K : Type ?u.1231482
A : Type u_3
A' : Type ?u.1231488
A'' : Type ?u.1231491
V : Type u
V' : Type ?u.1231496
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a✝ b : R
hx : AlgebraicIndependent R x
a : A
⊢ ∀ (r : R),
    ↑(Polynomial.aeval a) (↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (↑C r)) =
      ↑(aeval fun o => Option.elim o a x) (↑C r)
intro r
no goals
case refine'_1
ι : Type u_1
ι' : Type ?u.1231476
R : Type u_2
K : Type ?u.1231482
A : Type u_3
A' : Type ?u.1231488
A'' : Type ?u.1231491
V : Type u
V' : Type ?u.1231496
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a✝ b : R
hx : AlgebraicIndependent R x
a : A
r : R
⊢ ↑(Polynomial.aeval a) (↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (↑C r)) =
    ↑(aeval fun o => Option.elim o a x) (↑C r)
rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_C, aeval_C, Polynomial.aeval_C,
  IsScalarTower.algebraMap_apply R (adjoin R (range x)) A]
case refine'_2.none
ι : Type u_1
ι' : Type ?u.1231476
R : Type u_2
K : Type ?u.1231482
A : Type u_3
A' : Type ?u.1231488
A'' : Type ?u.1231491
V : Type u
V' : Type ?u.1231496
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a✝ b : R
hx : AlgebraicIndependent R x
a : A
⊢ ↑(Polynomial.aeval a) (↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (X none)) =
    ↑(aeval fun o => Option.elim o a x) (X none)

case refine'_2.some
ι : Type u_1
ι' : Type ?u.1231476
R : Type u_2
K : Type ?u.1231482
A : Type u_3
A' : Type ?u.1231488
A'' : Type ?u.1231491
V : Type u
V' : Type ?u.1231496
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a✝ b : R
hx : AlgebraicIndependent R x
a : A
i : ι
⊢ ↑(Polynomial.aeval a) (↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (X (some i))) =
    ↑(aeval fun o => Option.elim o a x) (X (some i))
case refine'_2
ι : Type u_1
ι' : Type ?u.1231476
R : Type u_2
K : Type ?u.1231482
A : Type u_3
A' : Type ?u.1231488
A'' : Type ?u.1231491
V : Type u
V' : Type ?u.1231496
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a✝ b : R
hx : AlgebraicIndependent R x
a : A
⊢ ∀ (i : Option ι),
    ↑(Polynomial.aeval a) (↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (X i)) =
      ↑(aeval fun o => Option.elim o a x) (X i)
rintro (⟨⟩ | ⟨i⟩)
no goals
case refine'_2.none
ι : Type u_1
ι' : Type ?u.1231476
R : Type u_2
K : Type ?u.1231482
A : Type u_3
A' : Type ?u.1231488
A'' : Type ?u.1231491
V : Type u
V' : Type ?u.1231496
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a✝ b : R
hx : AlgebraicIndependent R x
a : A
⊢ ↑(Polynomial.aeval a) (↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (X none)) =
    ↑(aeval fun o => Option.elim o a x) (X none)
rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_none, aeval_X, Polynomial.aeval_X,
  Option.elim]
no goals
case refine'_2.some
ι : Type u_1
ι' : Type ?u.1231476
R : Type u_2
K : Type ?u.1231482
A : Type u_3
A' : Type ?u.1231488
A'' : Type ?u.1231491
V : Type u
V' : Type ?u.1231496
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a✝ b : R
hx : AlgebraicIndependent R x
a : A
i : ι
⊢ ↑(Polynomial.aeval a) (↑(mvPolynomialOptionEquivPolynomialAdjoin hx) (X (some i))) =
    ↑(aeval fun o => Option.elim o a x) (X (some i))
rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Polynomial.aeval_C,
  hx.algebraMap_aevalEquiv, aeval_X, aeval_X, Option.elim]