R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval₂ (RingHom.id R) (x + y) f =
    sum f fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval (x + y) f = sum f fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)
unfold eval
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (sum f fun e a => ↑(RingHom.id R) a * (x + y) ^ e) =
    sum f fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval₂ (RingHom.id R) (x + y) f =
    sum f fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)
rw [eval₂_eq_sum]
case e_f.h.h
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
n : ℕ
z : R
⊢ ↑(RingHom.id R) z * (x + y) ^ n = z * (x ^ n + ↑n * x ^ (n - 1) * y + ↑(Polynomial.polyBinomAux1 x y n z) * y ^ 2)
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (sum f fun e a => ↑(RingHom.id R) a * (x + y) ^ e) =
    sum f fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)
congr with (n z)
no goals
case e_f.h.h
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
n : ℕ
z : R
⊢ ↑(RingHom.id R) z * (x + y) ^ n = z * (x ^ n + ↑n * x ^ (n - 1) * y + ↑(Polynomial.polyBinomAux1 x y n z) * y ^ 2)
apply (polyBinomAux1 x y _ _).property