[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
⊢ (x + y) ^ 0 = x ^ 0 + ↑0 * x ^ (0 - 1) * y + 0 * y ^ 2
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
⊢ (x + y) ^ 1 = x ^ 1 + ↑1 * x ^ (1 - 1) * y + 0 * y ^ 2
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
⊢ { k // (x + y) ^ (n + 2) = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 2 - 1) * y + k * y ^ 2 }
[PROOFSTEP]
cases' (powAddExpansion x y (n + 1)) with z hz
[GOAL]
case mk
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ { k // (x + y) ^ (n + 2) = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 2 - 1) * y + k * y ^ 2 }
[PROOFSTEP]
exists x * z + (n + 1) * x ^ n + z * y
[GOAL]
case mk
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) ^ (n + 2) = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 2 - 1) * y + (x * z + (↑n + 1) * x ^ n + z * y) * y ^ 2
[PROOFSTEP]
calc
  (x + y) ^ (n + 2) = (x + y) * (x + y) ^ (n + 1) := by ring
  _ = (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2) := by rw [hz]
  _ = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 1) * y + (x * z + (n + 1) * x ^ n + z * y) * y ^ 2 :=
    by
    push_cast
    ring!
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) ^ (n + 2) = (x + y) * (x + y) ^ (n + 1)
[PROOFSTEP]
ring
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) * (x + y) ^ (n + 1) = (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2)
[PROOFSTEP]
rw [hz]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2) =
    x ^ (n + 2) + ↑(n + 2) * x ^ (n + 1) * y + (x * z + (↑n + 1) * x ^ n + z * y) * y ^ 2
[PROOFSTEP]
push_cast
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) * (x ^ (n + 1) + (↑n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2) =
    x ^ (n + 2) + (↑n + 2) * x ^ (n + 1) * y + (x * z + (↑n + 1) * x ^ n + z * y) * y ^ 2
[PROOFSTEP]
ring!
[GOAL]
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
x y : R
e : ℕ
a : R
⊢ { k // a * (x + y) ^ e = a * (x ^ e + ↑e * x ^ (e - 1) * y + k * y ^ 2) }
[PROOFSTEP]
exists (powAddExpansion x y e).val
[GOAL]
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
x y : R
e : ℕ
a : R
⊢ a * (x + y) ^ e = a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(powAddExpansion x y e) * y ^ 2)
[PROOFSTEP]
congr
[GOAL]
case e_a
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
x y : R
e : ℕ
a : R
⊢ (x + y) ^ e = x ^ e + ↑e * x ^ (e - 1) * y + ↑(powAddExpansion x y e) * y ^ 2
[PROOFSTEP]
apply (powAddExpansion _ _ _).property
[GOAL]
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)
[PROOFSTEP]
unfold eval
[GOAL]
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)
[PROOFSTEP]
rw [eval₂_eq_sum]
[GOAL]
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)
[PROOFSTEP]
congr with (n z)
[GOAL]
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)
[PROOFSTEP]
apply (polyBinomAux1 x y _ _).property
[GOAL]
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) + sum f fun e a => a * ↑e * x ^ (e - 1) * y) +
      sum f fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2
[PROOFSTEP]
rw [poly_binom_aux2]
[GOAL]
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 => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)) =
    ((sum f fun e a => a * x ^ e) + sum f fun e a => a * ↑e * x ^ (e - 1) * y) +
      sum f fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2
[PROOFSTEP]
simp [left_distrib, sum_add, mul_assoc]
[GOAL]
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
⊢ { k // eval (x + y) f = eval x f + eval x (↑derivative f) * y + k * y ^ 2 }
[PROOFSTEP]
exists f.sum fun e a => a * (polyBinomAux1 x y e a).val
[GOAL]
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 =
    eval x f + eval x (↑derivative f) * y + (sum f fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a)) * y ^ 2
[PROOFSTEP]
rw [poly_binom_aux3]
[GOAL]
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 => a * x ^ e) + sum f fun e a => a * ↑e * x ^ (e - 1) * y) +
      sum f fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2) =
    eval x f + eval x (↑derivative f) * y + (sum f fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a)) * y ^ 2
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
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 => a * x ^ e) = eval x f
[PROOFSTEP]
rw [← eval_eq_sum]
[GOAL]
case e_a.e_a
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 => a * ↑e * x ^ (e - 1) * y) = eval x (↑derivative f) * y
[PROOFSTEP]
rw [derivative_eval]
[GOAL]
case e_a.e_a
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 => a * ↑e * x ^ (e - 1) * y) = (sum f fun n a => a * ↑n * x ^ (n - 1)) * y
[PROOFSTEP]
exact Finset.sum_mul.symm
[GOAL]
case e_a
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 => a * ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2) =
    (sum f fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a)) * y ^ 2
[PROOFSTEP]
exact Finset.sum_mul.symm
[GOAL]
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
x y : R
⊢ x ^ 0 - y ^ 0 = 0 * (x - y)
[PROOFSTEP]
simp
[GOAL]
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
x y : R
⊢ x ^ 1 - y ^ 1 = 1 * (x - y)
[PROOFSTEP]
simp
[GOAL]
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
x y : R
k : ℕ
⊢ { z // x ^ (k + 2) - y ^ (k + 2) = z * (x - y) }
[PROOFSTEP]
cases' @powSubPowFactor x y (k + 1) with z hz
[GOAL]
case mk
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
x y : R
k : ℕ
z : R
hz : x ^ (k + 1) - y ^ (k + 1) = z * (x - y)
⊢ { z // x ^ (k + 2) - y ^ (k + 2) = z * (x - y) }
[PROOFSTEP]
exists z * x + y ^ (k + 1)
[GOAL]
case mk
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
x y : R
k : ℕ
z : R
hz : x ^ (k + 1) - y ^ (k + 1) = z * (x - y)
⊢ x ^ (k + 2) - y ^ (k + 2) = (z * x + y ^ (k + 1)) * (x - y)
[PROOFSTEP]
linear_combination (norm := ring) x * hz
[GOAL]
case a
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
x y : R
k : ℕ
z : R
hz : x ^ (k + 1) - y ^ (k + 1) = z * (x - y)
⊢ x ^ (k + 2) - y ^ (k + 2) - (z * x + y ^ (k + 1)) * (x - y) - (x * (x ^ (k + 1) - y ^ (k + 1)) - x * (z * (x - y))) =
    0
[PROOFSTEP]
ring
[GOAL]
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
⊢ { z // eval x f - eval y f = z * (x - y) }
[PROOFSTEP]
refine' ⟨f.sum fun i r => r * (powSubPowFactor x y i).val, _⟩
[GOAL]
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 f - eval y f = (sum f fun i r => r * ↑(powSubPowFactor x y i)) * (x - y)
[PROOFSTEP]
delta eval
[GOAL]
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 f - eval₂ (RingHom.id R) y f = (sum f fun i r => r * ↑(powSubPowFactor x y i)) * (x - y)
[PROOFSTEP]
rw [eval₂_eq_sum, eval₂_eq_sum]
[GOAL]
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 ^ e) - sum f fun e a => ↑(RingHom.id R) a * y ^ e) =
    (sum f fun i r => r * ↑(powSubPowFactor x y i)) * (x - y)
[PROOFSTEP]
simp only [sum, ← Finset.sum_sub_distrib, Finset.sum_mul]
[GOAL]
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
⊢ (Finset.sum (support f) fun x_1 =>
      ↑(RingHom.id R) (coeff f x_1) * x ^ x_1 - ↑(RingHom.id R) (coeff f x_1) * y ^ x_1) =
    Finset.sum (support f) fun x_1 => coeff f x_1 * ↑(powSubPowFactor x y x_1) * (x - y)
[PROOFSTEP]
dsimp
[GOAL]
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
⊢ (Finset.sum (support f) fun x_1 => coeff f x_1 * x ^ x_1 - coeff f x_1 * y ^ x_1) =
    Finset.sum (support f) fun x_1 => coeff f x_1 * ↑(powSubPowFactor x y x_1) * (x - y)
[PROOFSTEP]
congr with i
[GOAL]
case e_f.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
i : ℕ
⊢ coeff f i * x ^ i - coeff f i * y ^ i = coeff f i * ↑(powSubPowFactor x y i) * (x - y)
[PROOFSTEP]
rw [mul_assoc, ← (powSubPowFactor x y _).prop, mul_sub]
