[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → B
p : MvPolynomial σ R
⊢ ↑(aeval x) (↑(map (algebraMap R A)) p) = ↑(aeval x) p
[PROOFSTEP]
rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
⊢ ↑(aeval (↑(algebraMap A B) ∘ x)) p = ↑(algebraMap A B) (↑(aeval x) p)
[PROOFSTEP]
rw [aeval_def, aeval_def, ← coe_eval₂Hom, ← coe_eval₂Hom, map_eval₂Hom, ← IsScalarTower.algebraMap_eq]
  -- Porting note: added
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
⊢ ↑(eval₂Hom (algebraMap R B) (↑(algebraMap A B) ∘ x)) p =
    ↑(eval₂Hom (algebraMap R B) fun i => ↑(algebraMap A B) (x i)) p
[PROOFSTEP]
simp only [Function.comp]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Nontrivial B
x : σ → A
p : MvPolynomial σ R
⊢ ↑(aeval (↑(algebraMap A B) ∘ x)) p = 0 ↔ ↑(aeval x) p = 0
[PROOFSTEP]
rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero, iff_false_intro (one_ne_zero' B),
  or_false_iff]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
h : Function.Injective ↑(algebraMap A B)
⊢ ↑(aeval (↑(algebraMap A B) ∘ x)) p = 0 ↔ ↑(aeval x) p = 0
[PROOFSTEP]
rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : σ → { x // x ∈ S }
p : MvPolynomial σ R
⊢ ↑(aeval fun i => ↑(x i)) p = ↑(↑(aeval x) p)
[PROOFSTEP]
convert aeval_algebraMap_apply A x p
