case h.h
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1573756
B' : Type ?u.1573759
a b : R
n : ℕ
inst✝¹⁰ : CommSemiring A'
inst✝⁹ : Semiring B'
inst✝⁸ : CommSemiring R
p q : R[X]
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type ?u.1573972
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
x : A
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Algebra S A'
inst✝ : Algebra S B'
g : R →ₐ[S] A'
y : A'
s : S
⊢ ↑(aevalTower (AlgHom.id S S) s) X = ↑(aeval s) X
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1573756
B' : Type ?u.1573759
a b : R
n : ℕ
inst✝¹⁰ : CommSemiring A'
inst✝⁹ : Semiring B'
inst✝⁸ : CommSemiring R
p q : R[X]
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type ?u.1573972
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
x : A
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Algebra S A'
inst✝ : Algebra S B'
g : R →ₐ[S] A'
y : A'
⊢ aevalTower (AlgHom.id S S) = aeval
ext s
no goals
case h.h
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1573756
B' : Type ?u.1573759
a b : R
n : ℕ
inst✝¹⁰ : CommSemiring A'
inst✝⁹ : Semiring B'
inst✝⁸ : CommSemiring R
p q : R[X]
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
B : Type ?u.1573972
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
x : A
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Algebra S A'
inst✝ : Algebra S B'
g : R →ₐ[S] A'
y : A'
s : S
⊢ ↑(aevalTower (AlgHom.id S S) s) X = ↑(aeval s) X
simp only [eval_X, aevalTower_X, coe_aeval_eq_eval]