[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ (fun p => sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)) (p + q) =
    (fun p => sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)) p + (fun p => sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)) q
[PROOFSTEP]
dsimp only
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ (sum (p + q) fun n a => ↑C (a * ↑n) * X ^ (n - 1)) =
    (sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)) + sum q fun n a => ↑C (a * ↑n) * X ^ (n - 1)
[PROOFSTEP]
rw [sum_add_index]
[GOAL]
case hf
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (i : ℕ), ↑C (0 * ↑i) * X ^ (i - 1) = 0
[PROOFSTEP]
simp only [add_mul, forall_const, RingHom.map_add, eq_self_iff_true, zero_mul, RingHom.map_zero]
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (a : ℕ) (b₁ b₂ : R), ↑C ((b₁ + b₂) * ↑a) * X ^ (a - 1) = ↑C (b₁ * ↑a) * X ^ (a - 1) + ↑C (b₂ * ↑a) * X ^ (a - 1)
[PROOFSTEP]
simp only [add_mul, forall_const, RingHom.map_add, eq_self_iff_true, zero_mul, RingHom.map_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
a : R
p : R[X]
⊢ AddHom.toFun
      { toFun := fun p => sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1),
        map_add' :=
          (_ :
            ∀ (p q : R[X]),
              (fun p => sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)) (p + q) =
                (fun p => sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)) p +
                  (fun p => sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)) q) }
      (a • p) =
    ↑(RingHom.id R) a •
      AddHom.toFun
        { toFun := fun p => sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1),
          map_add' :=
            (_ :
              ∀ (p q : R[X]),
                (fun p => sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)) (p + q) =
                  (fun p => sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)) p +
                    (fun p => sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)) q) }
        p
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
a : R
p : R[X]
⊢ (sum (a • p) fun n a => ↑C (a * ↑n) * X ^ (n - 1)) = a • sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)
[PROOFSTEP]
rw [sum_smul_index]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
a : R
p : R[X]
⊢ (sum p fun n a_1 => ↑C (a * a_1 * ↑n) * X ^ (n - 1)) = a • sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)
[PROOFSTEP]
simp only [mul_sum, ← C_mul', mul_assoc, coeff_C_mul, RingHom.map_mul, forall_const, zero_mul, RingHom.map_zero, sum]
[GOAL]
case hf
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
a : R
p : R[X]
⊢ ∀ (i : ℕ), ↑C (0 * ↑i) * X ^ (i - 1) = 0
[PROOFSTEP]
simp only [mul_sum, ← C_mul', mul_assoc, coeff_C_mul, RingHom.map_mul, forall_const, zero_mul, RingHom.map_zero, sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ coeff (↑derivative p) n = coeff p (n + 1) * (↑n + 1)
[PROOFSTEP]
rw [derivative_apply]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ coeff (sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)) n = coeff p (n + 1) * (↑n + 1)
[PROOFSTEP]
simp only [coeff_X_pow, coeff_sum, coeff_C_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (sum p fun a b => b * ↑a * if n = a - 1 then 1 else 0) = coeff p (n + 1) * (↑n + 1)
[PROOFSTEP]
rw [sum, Finset.sum_eq_single (n + 1)]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (coeff p (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = coeff p (n + 1) * (↑n + 1)
case h₀
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ∀ (b : ℕ), b ∈ support p → b ≠ n + 1 → (coeff p b * ↑b * if n = b - 1 then 1 else 0) = 0
case h₁
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ¬n + 1 ∈ support p → (coeff p (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = 0
[PROOFSTEP]
simp only [Nat.add_succ_sub_one, add_zero, mul_one, if_true, eq_self_iff_true]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ coeff p (n + 1) * ↑(n + 1) = coeff p (n + 1) * (↑n + 1)
case h₀
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ∀ (b : ℕ), b ∈ support p → b ≠ n + 1 → (coeff p b * ↑b * if n = b - 1 then 1 else 0) = 0
case h₁
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ¬n + 1 ∈ support p → (coeff p (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = 0
[PROOFSTEP]
norm_cast
[GOAL]
case h₀
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ∀ (b : ℕ), b ∈ support p → b ≠ n + 1 → (coeff p b * ↑b * if n = b - 1 then 1 else 0) = 0
[PROOFSTEP]
intro b
[GOAL]
case h₀
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b✝ : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n b : ℕ
⊢ b ∈ support p → b ≠ n + 1 → (coeff p b * ↑b * if n = b - 1 then 1 else 0) = 0
[PROOFSTEP]
cases b
[GOAL]
case h₀.zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ Nat.zero ∈ support p → Nat.zero ≠ n + 1 → (coeff p Nat.zero * ↑Nat.zero * if n = Nat.zero - 1 then 1 else 0) = 0
[PROOFSTEP]
intros
[GOAL]
case h₀.zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
a✝¹ : Nat.zero ∈ support p
a✝ : Nat.zero ≠ n + 1
⊢ (coeff p Nat.zero * ↑Nat.zero * if n = Nat.zero - 1 then 1 else 0) = 0
[PROOFSTEP]
rw [Nat.cast_zero, mul_zero, zero_mul]
[GOAL]
case h₀.succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ Nat.succ n✝ ∈ support p →
    Nat.succ n✝ ≠ n + 1 → (coeff p (Nat.succ n✝) * ↑(Nat.succ n✝) * if n = Nat.succ n✝ - 1 then 1 else 0) = 0
[PROOFSTEP]
intro _ H
[GOAL]
case h₀.succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
a✝ : Nat.succ n✝ ∈ support p
H : Nat.succ n✝ ≠ n + 1
⊢ (coeff p (Nat.succ n✝) * ↑(Nat.succ n✝) * if n = Nat.succ n✝ - 1 then 1 else 0) = 0
[PROOFSTEP]
rw [Nat.succ_sub_one, if_neg (mt (congr_arg Nat.succ) H.symm), mul_zero]
[GOAL]
case h₁
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ¬n + 1 ∈ support p → (coeff p (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = 0
[PROOFSTEP]
rw [if_pos (add_tsub_cancel_right n 1).symm, mul_one, Nat.cast_add, Nat.cast_one, mem_support_iff]
[GOAL]
case h₁
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ¬coeff p (n + 1) ≠ 0 → coeff p (n + 1) * (↑n + 1) = 0
[PROOFSTEP]
intro h
[GOAL]
case h₁
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
h : ¬coeff p (n + 1) ≠ 0
⊢ coeff p (n + 1) * (↑n + 1) = 0
[PROOFSTEP]
push_neg at h
[GOAL]
case h₁
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
h : coeff p (n + 1) = 0
⊢ coeff p (n + 1) * (↑n + 1) = 0
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
k : ℕ
⊢ (↑derivative)^[k] 0 = 0
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
⊢ (↑derivative)^[Nat.zero] 0 = 0
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
k : ℕ
ih : (↑derivative)^[k] 0 = 0
⊢ (↑derivative)^[Nat.succ k] 0 = 0
[PROOFSTEP]
simp [ih]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n✝ : ℕ
inst✝ : Semiring R
a : R
n : ℕ
⊢ ↑derivative (↑(monomial n) a) = ↑(monomial (n - 1)) (a * ↑n)
[PROOFSTEP]
rw [derivative_apply, sum_monomial_index, C_mul_X_pow_eq_monomial]
[GOAL]
case hf
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n✝ : ℕ
inst✝ : Semiring R
a : R
n : ℕ
⊢ ↑C (0 * ↑n) * X ^ (n - 1) = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
a : R
⊢ ↑derivative (↑C a * X) = ↑C a
[PROOFSTEP]
simp [C_mul_X_eq_monomial, derivative_monomial, Nat.cast_one, mul_one]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n✝ : ℕ
inst✝ : Semiring R
a : R
n : ℕ
⊢ ↑derivative (↑C a * X ^ n) = ↑C (a * ↑n) * X ^ (n - 1)
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, C_mul_X_pow_eq_monomial, derivative_monomial]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
a : R
⊢ ↑derivative (↑C a * X ^ 2) = ↑C (a * 2) * X
[PROOFSTEP]
rw [derivative_C_mul_X_pow, Nat.cast_two, pow_one]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
n : ℕ
⊢ ↑derivative (X ^ n) = ↑C ↑n * X ^ (n - 1)
[PROOFSTEP]
convert derivative_C_mul_X_pow (1 : R) n
[GOAL]
case h.e'_2.h.e'_6
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
n : ℕ
⊢ X ^ n = ↑C 1 * X ^ n
[PROOFSTEP]
simp
[GOAL]
case h.e'_3.h.e'_5.h.e'_6
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
n : ℕ
⊢ ↑n = 1 * ↑n
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
⊢ ↑derivative (X ^ 2) = ↑C 2 * X
[PROOFSTEP]
rw [derivative_X_pow, Nat.cast_two, pow_one]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
a : R
⊢ ↑derivative (↑C a) = 0
[PROOFSTEP]
simp [derivative_apply]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p = 0
⊢ ↑derivative p = 0
[PROOFSTEP]
rw [eq_C_of_natDegree_eq_zero hp, derivative_C]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
⊢ ↑(monomial (1 - 1)) (1 * ↑1) = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
a : R[X]
⊢ ↑derivative (bit0 a) = bit0 (↑derivative a)
[PROOFSTEP]
simp [bit0]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
a : R[X]
⊢ ↑derivative (bit1 a) = bit0 (↑derivative a)
[PROOFSTEP]
simp [bit1]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
c : R
⊢ ↑derivative (X + ↑C c) = 1
[PROOFSTEP]
rw [derivative_add, derivative_X, derivative_C, add_zero]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝³ : Semiring R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
k : ℕ
⊢ (↑derivative)^[k] (s • p) = s • (↑derivative)^[k] p
[PROOFSTEP]
induction' k with k ih generalizing p
[GOAL]
case zero
R : Type u
S✝ : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝³ : Semiring R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
s : S
p✝ p : R[X]
⊢ (↑derivative)^[Nat.zero] (s • p) = s • (↑derivative)^[Nat.zero] p
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S✝ : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝³ : Semiring R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
s : S
p✝ : R[X]
k : ℕ
ih : ∀ (p : R[X]), (↑derivative)^[k] (s • p) = s • (↑derivative)^[k] p
p : R[X]
⊢ (↑derivative)^[Nat.succ k] (s • p) = s • (↑derivative)^[Nat.succ k] p
[PROOFSTEP]
simp [ih]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
a : R
p : R[X]
k : ℕ
⊢ (↑derivative)^[k] (↑C a * p) = ↑C a * (↑derivative)^[k] p
[PROOFSTEP]
simp_rw [← smul_eq_C_mul, iterate_derivative_smul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n ∈ support (↑derivative p)
h1 : coeff p (n + 1) = 0
⊢ coeff (↑derivative p) n = 0
[PROOFSTEP]
rw [coeff_derivative, h1, zero_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
H : p = 0
⊢ degree (↑derivative p) = degree p
[PROOFSTEP]
rw [H, derivative_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p ≠ 0
⊢ natDegree (↑derivative p) < natDegree p
[PROOFSTEP]
cases' eq_or_ne (derivative p) 0 with hp' hp'
[GOAL]
case inl
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p ≠ 0
hp' : ↑derivative p = 0
⊢ natDegree (↑derivative p) < natDegree p
[PROOFSTEP]
rw [hp', Polynomial.natDegree_zero]
[GOAL]
case inl
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p ≠ 0
hp' : ↑derivative p = 0
⊢ 0 < natDegree p
[PROOFSTEP]
exact hp.bot_lt
[GOAL]
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p ≠ 0
hp' : ↑derivative p ≠ 0
⊢ natDegree (↑derivative p) < natDegree p
[PROOFSTEP]
rw [natDegree_lt_natDegree_iff hp']
[GOAL]
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p ≠ 0
hp' : ↑derivative p ≠ 0
⊢ degree (↑derivative p) < degree p
[PROOFSTEP]
exact degree_derivative_lt fun h => hp (h.symm ▸ natDegree_zero)
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ natDegree (↑derivative p) ≤ natDegree p - 1
[PROOFSTEP]
by_cases p0 : p.natDegree = 0
[GOAL]
case pos
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
p0 : natDegree p = 0
⊢ natDegree (↑derivative p) ≤ natDegree p - 1
[PROOFSTEP]
simp [p0, derivative_of_natDegree_zero]
[GOAL]
case neg
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
p0 : ¬natDegree p = 0
⊢ natDegree (↑derivative p) ≤ natDegree p - 1
[PROOFSTEP]
exact Nat.le_pred_of_lt (natDegree_derivative_lt p0)
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
n : ℕ
⊢ ↑derivative ↑n = 0
[PROOFSTEP]
rw [← map_natCast C n]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
n : ℕ
⊢ ↑derivative (↑C ↑n) = 0
[PROOFSTEP]
exact derivative_C
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
x : ℕ
hx : natDegree p < x
⊢ (↑derivative)^[x] p = 0
[PROOFSTEP]
induction' h : p.natDegree using Nat.strong_induction_on with _ ih generalizing p x
[GOAL]
case h
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x✝¹ : ℕ
hx✝ : natDegree p✝ < x✝¹
x✝ : ℕ
h✝ : natDegree p✝ = x✝
n✝ : ℕ
ih : ∀ (m : ℕ), m < n✝ → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative)^[x] p = 0
p : R[X]
x : ℕ
hx : natDegree p < x
h : natDegree p = n✝
⊢ (↑derivative)^[x] p = 0
[PROOFSTEP]
subst h
[GOAL]
case h
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x✝¹ : ℕ
hx✝ : natDegree p✝ < x✝¹
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
x : ℕ
hx : natDegree p < x
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative)^[x] p = 0
⊢ (↑derivative)^[x] p = 0
[PROOFSTEP]
obtain ⟨t, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (pos_of_gt hx).ne'
[GOAL]
case h.intro
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x : ℕ
hx✝ : natDegree p✝ < x
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative)^[x] p = 0
t : ℕ
hx : natDegree p < Nat.succ t
⊢ (↑derivative)^[Nat.succ t] p = 0
[PROOFSTEP]
rw [Function.iterate_succ_apply]
[GOAL]
case h.intro
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x : ℕ
hx✝ : natDegree p✝ < x
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative)^[x] p = 0
t : ℕ
hx : natDegree p < Nat.succ t
⊢ (↑derivative)^[t] (↑derivative p) = 0
[PROOFSTEP]
by_cases hp : p.natDegree = 0
[GOAL]
case pos
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x : ℕ
hx✝ : natDegree p✝ < x
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative)^[x] p = 0
t : ℕ
hx : natDegree p < Nat.succ t
hp : natDegree p = 0
⊢ (↑derivative)^[t] (↑derivative p) = 0
[PROOFSTEP]
rw [derivative_of_natDegree_zero hp, iterate_derivative_zero]
[GOAL]
case neg
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x : ℕ
hx✝ : natDegree p✝ < x
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative)^[x] p = 0
t : ℕ
hx : natDegree p < Nat.succ t
hp : ¬natDegree p = 0
⊢ (↑derivative)^[t] (↑derivative p) = 0
[PROOFSTEP]
have := natDegree_derivative_lt hp
[GOAL]
case neg
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x : ℕ
hx✝ : natDegree p✝ < x
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative)^[x] p = 0
t : ℕ
hx : natDegree p < Nat.succ t
hp : ¬natDegree p = 0
this : natDegree (↑derivative p) < natDegree p
⊢ (↑derivative)^[t] (↑derivative p) = 0
[PROOFSTEP]
exact ih _ this (this.trans_le <| Nat.le_of_lt_succ hx) rfl
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
⊢ natDegree f = 0
[PROOFSTEP]
rcases eq_or_ne f 0 with (rfl | hf)
[GOAL]
case inl
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
h : ↑derivative 0 = 0
⊢ natDegree 0 = 0
[PROOFSTEP]
exact natDegree_zero
[GOAL]
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
⊢ natDegree f = 0
[PROOFSTEP]
rw [natDegree_eq_zero_iff_degree_le_zero]
[GOAL]
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
⊢ degree f ≤ 0
[PROOFSTEP]
by_contra' f_nat_degree_pos
[GOAL]
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < degree f
⊢ False
[PROOFSTEP]
rw [← natDegree_pos_iff_degree_pos] at f_nat_degree_pos
[GOAL]
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
⊢ False
[PROOFSTEP]
let m := f.natDegree - 1
[GOAL]
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
⊢ False
[PROOFSTEP]
have hm : m + 1 = f.natDegree := tsub_add_cancel_of_le f_nat_degree_pos
[GOAL]
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
⊢ False
[PROOFSTEP]
have h2 := coeff_derivative f m
[GOAL]
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
h2 : coeff (↑derivative f) m = coeff f (m + 1) * (↑m + 1)
⊢ False
[PROOFSTEP]
rw [Polynomial.ext_iff] at h
[GOAL]
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), coeff (↑derivative f) n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
h2 : coeff (↑derivative f) m = coeff f (m + 1) * (↑m + 1)
⊢ False
[PROOFSTEP]
rw [h m, coeff_zero, ← Nat.cast_add_one, ← nsmul_eq_mul', eq_comm, smul_eq_zero] at h2
[GOAL]
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), coeff (↑derivative f) n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
h2 : m + 1 = 0 ∨ coeff f (m + 1) = 0
⊢ False
[PROOFSTEP]
replace h2 := h2.resolve_left m.succ_ne_zero
[GOAL]
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), coeff (↑derivative f) n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
h2 : coeff f (m + 1) = 0
⊢ False
[PROOFSTEP]
rw [hm, ← leadingCoeff, leadingCoeff_eq_zero] at h2
[GOAL]
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), coeff (↑derivative f) n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
h2 : f = 0
⊢ False
[PROOFSTEP]
exact hf h2
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ↑derivative (f * g) = sum f fun n a => sum g fun m b => (n + m) • (↑C (a * b) * X ^ (n + m - 1))
[PROOFSTEP]
rw [mul_eq_sum_sum, derivative_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ b in support f, ↑derivative (sum g fun j a => ↑(monomial (b + j)) (coeff f b * a)) =
    sum f fun n a => sum g fun m b => (n + m) • (↑C (a * b) * X ^ (n + m - 1))
[PROOFSTEP]
trans
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ b in support f, ↑derivative (sum g fun j a => ↑(monomial (b + j)) (coeff f b * a)) = ?m.380316
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∀ (x : ℕ), x ∈ support f → ↑derivative (sum g fun j a => ↑(monomial (x + j)) (coeff f x * a)) = ?m.380366 x
R : Type u S : Type v T : Type w ι : Type y A : Type z a b : R n : ℕ inst✝ : Semiring R f g : R[X] ⊢ ℕ → R[X]
[PROOFSTEP]
intro x _
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
x : ℕ
a✝ : x ∈ support f
⊢ ↑derivative (sum g fun j a => ↑(monomial (x + j)) (coeff f x * a)) = ?m.380366 x
R : Type u S : Type v T : Type w ι : Type y A : Type z a b : R n : ℕ inst✝ : Semiring R f g : R[X] ⊢ ℕ → R[X]
[PROOFSTEP]
exact derivative_sum
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ x in support f, ∑ b in support g, ↑derivative ((fun j a => ↑(monomial (x + j)) (coeff f x * a)) b (coeff g b)) =
    sum f fun n a => sum g fun m b => (n + m) • (↑C (a * b) * X ^ (n + m - 1))
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∀ (x : ℕ),
    x ∈ support f →
      ∑ b in support g, ↑derivative ((fun j a => ↑(monomial (x + j)) (coeff f x * a)) b (coeff g b)) =
        (fun n a => sum g fun m b => (n + m) • (↑C (a * b) * X ^ (n + m - 1))) x (coeff f x)
[PROOFSTEP]
intro n _
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝ : n ∈ support f
⊢ ∑ b in support g, ↑derivative ((fun j a => ↑(monomial (n + j)) (coeff f n * a)) b (coeff g b)) =
    (fun n a => sum g fun m b => (n + m) • (↑C (a * b) * X ^ (n + m - 1))) n (coeff f n)
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝ : n ∈ support f
⊢ ∀ (x : ℕ),
    x ∈ support g →
      ↑derivative ((fun j a => ↑(monomial (n + j)) (coeff f n * a)) x (coeff g x)) =
        (fun m b => (n + m) • (↑C (coeff f n * b) * X ^ (n + m - 1))) x (coeff g x)
[PROOFSTEP]
intro m _
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝¹ : n ∈ support f
m : ℕ
a✝ : m ∈ support g
⊢ ↑derivative ((fun j a => ↑(monomial (n + j)) (coeff f n * a)) m (coeff g m)) =
    (fun m b => (n + m) • (↑C (coeff f n * b) * X ^ (n + m - 1))) m (coeff g m)
[PROOFSTEP]
trans
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝¹ : n ∈ support f
m : ℕ
a✝ : m ∈ support g
⊢ ↑derivative ((fun j a => ↑(monomial (n + j)) (coeff f n * a)) m (coeff g m)) = ?m.380816
[PROOFSTEP]
exact congr_arg _ C_mul_X_pow_eq_monomial.symm
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝¹ : n ∈ support f
m : ℕ
a✝ : m ∈ support g
⊢ ↑derivative (↑C (coeff f n * coeff g m) * X ^ (n + m)) =
    (fun m b => (n + m) • (↑C (coeff f n * b) * X ^ (n + m - 1))) m (coeff g m)
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝¹ : n ∈ support f
m : ℕ
a✝ : m ∈ support g
⊢ ↑derivative (↑C (coeff f n * coeff g m) * X ^ (n + m)) = (n + m) • (↑C (coeff f n * coeff g m) * X ^ (n + m - 1))
[PROOFSTEP]
rw [← smul_mul_assoc, smul_C, nsmul_eq_mul']
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
a✝¹ : n ∈ support f
m : ℕ
a✝ : m ∈ support g
⊢ ↑derivative (↑C (coeff f n * coeff g m) * X ^ (n + m)) = ↑C (coeff f n * coeff g m * ↑(n + m)) * X ^ (n + m - 1)
[PROOFSTEP]
exact derivative_C_mul_X_pow _ _
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
f g : R[X]
n : ℕ
hn : n ∈ support f
m : ℕ
hm : m ∈ support g
⊢ (fun m b => (n + m) • (↑C (coeff f n * b) * X ^ (n + m - 1))) m (coeff g m) =
    (fun m b => n • (↑C (coeff f n) * X ^ (n - 1)) * (↑C b * X ^ m) + ↑C (coeff f n) * X ^ n * m • (↑C b * X ^ (m - 1)))
      m (coeff g m)
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
m : ℕ
hm : m ∈ support g
hn : Nat.zero ∈ support f
⊢ (fun m b => (Nat.zero + m) • (↑C (coeff f Nat.zero * b) * X ^ (Nat.zero + m - 1))) m (coeff g m) =
    (fun m b =>
        Nat.zero • (↑C (coeff f Nat.zero) * X ^ (Nat.zero - 1)) * (↑C b * X ^ m) +
          ↑C (coeff f Nat.zero) * X ^ Nat.zero * m • (↑C b * X ^ (m - 1)))
      m (coeff g m)
[PROOFSTEP]
cases m
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
m : ℕ
hm : m ∈ support g
n✝ : ℕ
hn : Nat.succ n✝ ∈ support f
⊢ (fun m b => (Nat.succ n✝ + m) • (↑C (coeff f (Nat.succ n✝) * b) * X ^ (Nat.succ n✝ + m - 1))) m (coeff g m) =
    (fun m b =>
        Nat.succ n✝ • (↑C (coeff f (Nat.succ n✝)) * X ^ (Nat.succ n✝ - 1)) * (↑C b * X ^ m) +
          ↑C (coeff f (Nat.succ n✝)) * X ^ Nat.succ n✝ * m • (↑C b * X ^ (m - 1)))
      m (coeff g m)
[PROOFSTEP]
cases m
[GOAL]
case zero.zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
hn : Nat.zero ∈ support f
hm : Nat.zero ∈ support g
⊢ (fun m b => (Nat.zero + m) • (↑C (coeff f Nat.zero * b) * X ^ (Nat.zero + m - 1))) Nat.zero (coeff g Nat.zero) =
    (fun m b =>
        Nat.zero • (↑C (coeff f Nat.zero) * X ^ (Nat.zero - 1)) * (↑C b * X ^ m) +
          ↑C (coeff f Nat.zero) * X ^ Nat.zero * m • (↑C b * X ^ (m - 1)))
      Nat.zero (coeff g Nat.zero)
[PROOFSTEP]
simp_rw [add_smul, mul_smul_comm, smul_mul_assoc, X_pow_mul_assoc, ← mul_assoc, ← C_mul, mul_assoc, ← pow_add]
[GOAL]
case zero.succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
hn : Nat.zero ∈ support f
n✝ : ℕ
hm : Nat.succ n✝ ∈ support g
⊢ (fun m b => (Nat.zero + m) • (↑C (coeff f Nat.zero * b) * X ^ (Nat.zero + m - 1))) (Nat.succ n✝)
      (coeff g (Nat.succ n✝)) =
    (fun m b =>
        Nat.zero • (↑C (coeff f Nat.zero) * X ^ (Nat.zero - 1)) * (↑C b * X ^ m) +
          ↑C (coeff f Nat.zero) * X ^ Nat.zero * m • (↑C b * X ^ (m - 1)))
      (Nat.succ n✝) (coeff g (Nat.succ n✝))
[PROOFSTEP]
simp_rw [add_smul, mul_smul_comm, smul_mul_assoc, X_pow_mul_assoc, ← mul_assoc, ← C_mul, mul_assoc, ← pow_add]
[GOAL]
case succ.zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
n✝ : ℕ
hn : Nat.succ n✝ ∈ support f
hm : Nat.zero ∈ support g
⊢ (fun m b => (Nat.succ n✝ + m) • (↑C (coeff f (Nat.succ n✝) * b) * X ^ (Nat.succ n✝ + m - 1))) Nat.zero
      (coeff g Nat.zero) =
    (fun m b =>
        Nat.succ n✝ • (↑C (coeff f (Nat.succ n✝)) * X ^ (Nat.succ n✝ - 1)) * (↑C b * X ^ m) +
          ↑C (coeff f (Nat.succ n✝)) * X ^ Nat.succ n✝ * m • (↑C b * X ^ (m - 1)))
      Nat.zero (coeff g Nat.zero)
[PROOFSTEP]
simp_rw [add_smul, mul_smul_comm, smul_mul_assoc, X_pow_mul_assoc, ← mul_assoc, ← C_mul, mul_assoc, ← pow_add]
[GOAL]
case succ.succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
n✝¹ : ℕ
hn : Nat.succ n✝¹ ∈ support f
n✝ : ℕ
hm : Nat.succ n✝ ∈ support g
⊢ (fun m b => (Nat.succ n✝¹ + m) • (↑C (coeff f (Nat.succ n✝¹) * b) * X ^ (Nat.succ n✝¹ + m - 1))) (Nat.succ n✝)
      (coeff g (Nat.succ n✝)) =
    (fun m b =>
        Nat.succ n✝¹ • (↑C (coeff f (Nat.succ n✝¹)) * X ^ (Nat.succ n✝¹ - 1)) * (↑C b * X ^ m) +
          ↑C (coeff f (Nat.succ n✝¹)) * X ^ Nat.succ n✝¹ * m • (↑C b * X ^ (m - 1)))
      (Nat.succ n✝) (coeff g (Nat.succ n✝))
[PROOFSTEP]
simp_rw [add_smul, mul_smul_comm, smul_mul_assoc, X_pow_mul_assoc, ← mul_assoc, ← C_mul, mul_assoc, ← pow_add]
[GOAL]
case zero.succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
hn : Nat.zero ∈ support f
n✝ : ℕ
hm : Nat.succ n✝ ∈ support g
⊢ Nat.zero • (↑C (coeff f Nat.zero * coeff g (Nat.succ n✝)) * X ^ (Nat.zero + Nat.succ n✝ - 1)) +
      Nat.succ n✝ • (↑C (coeff f Nat.zero * coeff g (Nat.succ n✝)) * X ^ (Nat.zero + Nat.succ n✝ - 1)) =
    Nat.zero • (↑C (coeff f Nat.zero * coeff g (Nat.succ n✝)) * X ^ (Nat.succ n✝ + (Nat.zero - 1))) +
      Nat.succ n✝ • (↑C (coeff f Nat.zero * coeff g (Nat.succ n✝)) * X ^ (Nat.succ n✝ - 1 + Nat.zero))
[PROOFSTEP]
simp [Nat.add_succ, Nat.succ_add, Nat.succ_sub_one, zero_smul, add_comm]
[GOAL]
case succ.zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
n✝ : ℕ
hn : Nat.succ n✝ ∈ support f
hm : Nat.zero ∈ support g
⊢ Nat.succ n✝ • (↑C (coeff f (Nat.succ n✝) * coeff g Nat.zero) * X ^ (Nat.succ n✝ + Nat.zero - 1)) +
      Nat.zero • (↑C (coeff f (Nat.succ n✝) * coeff g Nat.zero) * X ^ (Nat.succ n✝ + Nat.zero - 1)) =
    Nat.succ n✝ • (↑C (coeff f (Nat.succ n✝) * coeff g Nat.zero) * X ^ (Nat.zero + (Nat.succ n✝ - 1))) +
      Nat.zero • (↑C (coeff f (Nat.succ n✝) * coeff g Nat.zero) * X ^ (Nat.zero - 1 + Nat.succ n✝))
[PROOFSTEP]
simp [Nat.add_succ, Nat.succ_add, Nat.succ_sub_one, zero_smul, add_comm]
[GOAL]
case succ.succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
n✝¹ : ℕ
hn : Nat.succ n✝¹ ∈ support f
n✝ : ℕ
hm : Nat.succ n✝ ∈ support g
⊢ Nat.succ n✝¹ • (↑C (coeff f (Nat.succ n✝¹) * coeff g (Nat.succ n✝)) * X ^ (Nat.succ n✝¹ + Nat.succ n✝ - 1)) +
      Nat.succ n✝ • (↑C (coeff f (Nat.succ n✝¹) * coeff g (Nat.succ n✝)) * X ^ (Nat.succ n✝¹ + Nat.succ n✝ - 1)) =
    Nat.succ n✝¹ • (↑C (coeff f (Nat.succ n✝¹) * coeff g (Nat.succ n✝)) * X ^ (Nat.succ n✝ + (Nat.succ n✝¹ - 1))) +
      Nat.succ n✝ • (↑C (coeff f (Nat.succ n✝¹) * coeff g (Nat.succ n✝)) * X ^ (Nat.succ n✝ - 1 + Nat.succ n✝¹))
[PROOFSTEP]
simp [Nat.add_succ, Nat.succ_add, Nat.succ_sub_one, zero_smul, add_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ (sum f fun n a =>
      sum g fun m b => n • (↑C a * X ^ (n - 1)) * (↑C b * X ^ m) + ↑C a * X ^ n * m • (↑C b * X ^ (m - 1))) =
    ↑derivative f * g + f * ↑derivative g
[PROOFSTEP]
conv =>
  rhs
  congr
  ·rw [← sum_C_mul_X_pow_eq g]
  ·rw [← sum_C_mul_X_pow_eq f]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
| (sum f fun n a =>
      sum g fun m b => n • (↑C a * X ^ (n - 1)) * (↑C b * X ^ m) + ↑C a * X ^ n * m • (↑C b * X ^ (m - 1))) =
    ↑derivative f * g + f * ↑derivative g
[PROOFSTEP]
  rhs
  congr
  ·rw [← sum_C_mul_X_pow_eq g]
  ·rw [← sum_C_mul_X_pow_eq f]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
| (sum f fun n a =>
      sum g fun m b => n • (↑C a * X ^ (n - 1)) * (↑C b * X ^ m) + ↑C a * X ^ n * m • (↑C b * X ^ (m - 1))) =
    ↑derivative f * g + f * ↑derivative g
[PROOFSTEP]
  rhs
  congr
  ·rw [← sum_C_mul_X_pow_eq g]
  ·rw [← sum_C_mul_X_pow_eq f]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
| (sum f fun n a =>
      sum g fun m b => n • (↑C a * X ^ (n - 1)) * (↑C b * X ^ m) + ↑C a * X ^ n * m • (↑C b * X ^ (m - 1))) =
    ↑derivative f * g + f * ↑derivative g
[PROOFSTEP]
rhs
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
| ↑derivative f * g + f * ↑derivative g
[PROOFSTEP]
congr
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
| ↑derivative f * g
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
| f * ↑derivative g
[PROOFSTEP]
·rw [← sum_C_mul_X_pow_eq g]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
| ↑derivative f * g
[PROOFSTEP]
rw [← sum_C_mul_X_pow_eq g]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
| ↑derivative f * g
[PROOFSTEP]
rw [← sum_C_mul_X_pow_eq g]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
| ↑derivative f * g
[PROOFSTEP]
rw [← sum_C_mul_X_pow_eq g]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
| f * ↑derivative g
[PROOFSTEP]
·rw [← sum_C_mul_X_pow_eq f]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
| f * ↑derivative g
[PROOFSTEP]
rw [← sum_C_mul_X_pow_eq f]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
| f * ↑derivative g
[PROOFSTEP]
rw [← sum_C_mul_X_pow_eq f]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
| f * ↑derivative g
[PROOFSTEP]
rw [← sum_C_mul_X_pow_eq f]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ (sum f fun n a =>
      sum g fun m b => n • (↑C a * X ^ (n - 1)) * (↑C b * X ^ m) + ↑C a * X ^ n * m • (↑C b * X ^ (m - 1))) =
    (↑derivative f * sum g fun n a => ↑C a * X ^ n) + (sum f fun n a => ↑C a * X ^ n) * ↑derivative g
[PROOFSTEP]
simp only [sum, sum_add_distrib, Finset.mul_sum, Finset.sum_mul, derivative_apply]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ x in support f, ∑ x_1 in support g, x • (↑C (coeff f x) * X ^ (x - 1)) * (↑C (coeff g x_1) * X ^ x_1) +
      ∑ x in support f, ∑ x_1 in support g, ↑C (coeff f x) * X ^ x * x_1 • (↑C (coeff g x_1) * X ^ (x_1 - 1)) =
    ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1 * ↑x_1) * X ^ (x_1 - 1) * (↑C (coeff g x) * X ^ x) +
      ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1) * X ^ x_1 * (↑C (coeff g x * ↑x) * X ^ (x - 1))
[PROOFSTEP]
simp_rw [← smul_mul_assoc, smul_C, nsmul_eq_mul']
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ x in support f, ∑ x_1 in support g, ↑C (coeff f x * ↑x) * X ^ (x - 1) * (↑C (coeff g x_1) * X ^ x_1) +
      ∑ x in support f, ∑ x_1 in support g, ↑C (coeff f x) * X ^ x * (↑C (coeff g x_1 * ↑x_1) * X ^ (x_1 - 1)) =
    ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1 * ↑x_1) * X ^ (x_1 - 1) * (↑C (coeff g x) * X ^ x) +
      ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1) * X ^ x_1 * (↑C (coeff g x * ↑x) * X ^ (x - 1))
[PROOFSTEP]
rw [Finset.sum_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ y in support g, ∑ x in support f, ↑C (coeff f x * ↑x) * X ^ (x - 1) * (↑C (coeff g y) * X ^ y) +
      ∑ x in support f, ∑ x_1 in support g, ↑C (coeff f x) * X ^ x * (↑C (coeff g x_1 * ↑x_1) * X ^ (x_1 - 1)) =
    ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1 * ↑x_1) * X ^ (x_1 - 1) * (↑C (coeff g x) * X ^ x) +
      ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1) * X ^ x_1 * (↑C (coeff g x * ↑x) * X ^ (x - 1))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
f g : R[X]
⊢ ∑ x in support f, ∑ x_1 in support g, ↑C (coeff f x) * X ^ x * (↑C (coeff g x_1 * ↑x_1) * X ^ (x_1 - 1)) =
    ∑ x in support g, ∑ x_1 in support f, ↑C (coeff f x_1) * X ^ x_1 * (↑C (coeff g x * ↑x) * X ^ (x - 1))
[PROOFSTEP]
rw [Finset.sum_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x (↑derivative p) = sum p fun n a => a * ↑n * x ^ (n - 1)
[PROOFSTEP]
simp_rw [derivative_apply, eval_sum, eval_mul_X_pow, eval_C]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ ↑derivative (map f p) = map f (↑derivative p)
[PROOFSTEP]
let n := max p.natDegree (map f p).natDegree
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ↑derivative (map f p) = map f (↑derivative p)
[PROOFSTEP]
rw [derivative_apply, derivative_apply]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ (sum (map f p) fun n a => ↑C (a * ↑n) * X ^ (n - 1)) = map f (sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1))
[PROOFSTEP]
rw [sum_over_range' _ _ (n + 1) ((le_max_left _ _).trans_lt (lt_add_one _))]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ (sum (map f p) fun n a => ↑C (a * ↑n) * X ^ (n - 1)) = map f (∑ a in range (n + 1), ↑C (coeff p a * ↑a) * X ^ (a - 1))
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0
[PROOFSTEP]
rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∑ a in range (n + 1), ↑C (coeff (map f p) a * ↑a) * X ^ (a - 1) =
    map f (∑ a in range (n + 1), ↑C (coeff p a * ↑a) * X ^ (a - 1))
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0
[PROOFSTEP]
simp only [Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_C, map_mul, coeff_map, map_natCast,
  Polynomial.map_nat_cast, Polynomial.map_pow, map_X]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0
[PROOFSTEP]
all_goals intro n; rw [zero_mul, C_0, zero_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0
[PROOFSTEP]
intro n
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n✝ : ℕ := max (natDegree p) (natDegree (map f p))
n : ℕ
⊢ ↑C (0 * ↑n) * X ^ (n - 1) = 0
[PROOFSTEP]
rw [zero_mul, C_0, zero_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (natDegree p) (natDegree (map f p))
⊢ ∀ (n : ℕ), ↑C (0 * ↑n) * X ^ (n - 1) = 0
[PROOFSTEP]
intro n
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n✝ : ℕ := max (natDegree p) (natDegree (map f p))
n : ℕ
⊢ ↑C (0 * ↑n) * X ^ (n - 1) = 0
[PROOFSTEP]
rw [zero_mul, C_0, zero_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
k : ℕ
⊢ (↑derivative)^[k] (map f p) = map f ((↑derivative)^[k] p)
[PROOFSTEP]
induction' k with k ih generalizing p
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p✝ : R[X]
f : R →+* S
p : R[X]
⊢ (↑derivative)^[Nat.zero] (map f p) = map f ((↑derivative)^[Nat.zero] p)
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p✝ : R[X]
f : R →+* S
k : ℕ
ih : ∀ (p : R[X]), (↑derivative)^[k] (map f p) = map f ((↑derivative)^[k] p)
p : R[X]
⊢ (↑derivative)^[Nat.succ k] (map f p) = map f ((↑derivative)^[Nat.succ k] p)
[PROOFSTEP]
simp only [ih, Function.iterate_succ, Polynomial.derivative_map, Function.comp_apply]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ ↑derivative (↑n * f) = ↑n * ↑derivative f
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
n k : ℕ
f : R[X]
⊢ (↑derivative)^[k] (↑n * f) = ↑n * (↑derivative)^[k] f
[PROOFSTEP]
induction' k with k ih generalizing f
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
n : ℕ
f✝ f : R[X]
⊢ (↑derivative)^[Nat.zero] (↑n * f) = ↑n * (↑derivative)^[Nat.zero] f
[PROOFSTEP]
simp [*]
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
n : ℕ
f✝ : R[X]
k : ℕ
ih : ∀ {f : R[X]}, (↑derivative)^[k] (↑n * f) = ↑n * (↑derivative)^[k] f
f : R[X]
⊢ (↑derivative)^[Nat.succ k] (↑n * f) = ↑n * (↑derivative)^[Nat.succ k] f
[PROOFSTEP]
simp [*]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
⊢ n ∈ support (↑derivative p) ↔ n + 1 ∈ support p
[PROOFSTEP]
suffices ¬p.coeff (n + 1) * (n + 1 : ℕ) = 0 ↔ coeff p (n + 1) ≠ 0 by
  simpa only [mem_support_iff, coeff_derivative, Ne.def, Nat.cast_succ]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
this : ¬coeff p (n + 1) * ↑(n + 1) = 0 ↔ coeff p (n + 1) ≠ 0
⊢ n ∈ support (↑derivative p) ↔ n + 1 ∈ support p
[PROOFSTEP]
simpa only [mem_support_iff, coeff_derivative, Ne.def, Nat.cast_succ]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
⊢ ¬coeff p (n + 1) * ↑(n + 1) = 0 ↔ coeff p (n + 1) ≠ 0
[PROOFSTEP]
rw [← nsmul_eq_mul', smul_eq_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
⊢ ¬(n + 1 = 0 ∨ coeff p (n + 1) = 0) ↔ coeff p (n + 1) ≠ 0
[PROOFSTEP]
simp only [Nat.succ_ne_zero, false_or_iff]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ degree (↑derivative p) = ↑(natDegree p - 1)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ degree (↑derivative p) ≤ ↑(natDegree p - 1)
[PROOFSTEP]
rw [derivative_apply]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ degree (sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)) ≤ ↑(natDegree p - 1)
[PROOFSTEP]
apply le_trans (degree_sum_le _ _) (Finset.sup_le _)
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ ∀ (b : ℕ), b ∈ support p → degree ((fun n a => ↑C (a * ↑n) * X ^ (n - 1)) b (coeff p b)) ≤ ↑(natDegree p - 1)
[PROOFSTEP]
intro n hn
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
n : ℕ
hn : n ∈ support p
⊢ degree ((fun n a => ↑C (a * ↑n) * X ^ (n - 1)) n (coeff p n)) ≤ ↑(natDegree p - 1)
[PROOFSTEP]
simp only [Nat.cast_withBot]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
n : ℕ
hn : n ∈ support p
⊢ degree (↑C (coeff p n * ↑n) * X ^ (n - 1)) ≤ ↑(natDegree p - 1)
[PROOFSTEP]
apply le_trans (degree_C_mul_X_pow_le _ _) (WithBot.coe_le_coe.2 (tsub_le_tsub_right _ _))
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
n : ℕ
hn : n ∈ support p
⊢ n ≤ natDegree p
[PROOFSTEP]
apply le_natDegree_of_mem_supp _ hn
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ ↑(natDegree p - 1) ≤ degree (↑derivative p)
[PROOFSTEP]
refine' le_sup _
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ natDegree p - 1 ∈ support (↑derivative p)
[PROOFSTEP]
rw [mem_support_derivative, tsub_add_cancel_of_le, mem_support_iff]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ coeff p (natDegree p) ≠ 0
[PROOFSTEP]
show ¬leadingCoeff p = 0
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ ¬leadingCoeff p = 0
[PROOFSTEP]
rw [leadingCoeff_eq_zero]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ ¬p = 0
[PROOFSTEP]
intro h
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
h : p = 0
⊢ False
[PROOFSTEP]
rw [h, natDegree_zero] at hp
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < 0
h : p = 0
⊢ False
[PROOFSTEP]
exact lt_irrefl 0 (lt_of_le_of_lt (zero_le _) hp)
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ 1 ≤ natDegree p
[PROOFSTEP]
exact hp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
k : ℕ
p : R[X]
⊢ ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ ∀ (m : ℕ),
    coeff ((↑derivative)^[Nat.zero] p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ Nat.zero), i) • coeff p (m + Nat.zero)
[PROOFSTEP]
simp [add_zero, forall_const, one_smul, Ico_self, eq_self_iff_true, Function.iterate_zero_apply, prod_empty]
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
⊢ ∀ (m : ℕ),
    coeff ((↑derivative)^[Nat.succ k] p) m =
      (∏ i in Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)), i) • coeff p (m + Nat.succ k)
[PROOFSTEP]
intro m
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ coeff ((↑derivative)^[Nat.succ k] p) m =
    (∏ i in Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)), i) • coeff p (m + Nat.succ k)
[PROOFSTEP]
rw [Function.iterate_succ_apply', coeff_derivative, ih (m + 1), ← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul,
  mul_comm]
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ ((∏ i in Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k), i) * (m + 1)) • coeff p (m + 1 + k) =
    (∏ i in Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)), i) • coeff p (m + Nat.succ k)
[PROOFSTEP]
apply congr_arg₂
[GOAL]
case succ.hx
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ (∏ i in Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k), i) * (m + 1) =
    ∏ i in Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)), i
[PROOFSTEP]
have set_eq : Ico m.succ (m + k.succ.succ) = Ico (m + 1).succ (m + 1 + k.succ) ∪ {m + 1} :=
  by
  simp_rw [← Nat.Ico_succ_singleton, union_comm, Nat.succ_eq_add_one, add_comm (k + 1), add_assoc]
  rw [Ico_union_Ico_eq_Ico] <;> simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)) = Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k) ∪ {m + 1}
[PROOFSTEP]
simp_rw [← Nat.Ico_succ_singleton, union_comm, Nat.succ_eq_add_one, add_comm (k + 1), add_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ Ico (m + 1) (m + (1 + (k + 1))) = Ico (m + 1) (m + (1 + 1)) ∪ Ico (m + (1 + 1)) (m + (1 + (k + 1)))
[PROOFSTEP]
rw [Ico_union_Ico_eq_Ico]
[GOAL]
case hab
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ m + 1 ≤ m + (1 + 1)
[PROOFSTEP]
simp
[GOAL]
case hbc
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ m + (1 + 1) ≤ m + (1 + (k + 1))
[PROOFSTEP]
simp
[GOAL]
case succ.hx
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
set_eq : Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)) = Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k) ∪ {m + 1}
⊢ (∏ i in Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k), i) * (m + 1) =
    ∏ i in Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)), i
[PROOFSTEP]
rw [set_eq, prod_union, prod_singleton]
[GOAL]
case succ.hx
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
set_eq : Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)) = Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k) ∪ {m + 1}
⊢ Disjoint (Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k)) {m + 1}
[PROOFSTEP]
rw [disjoint_singleton_right, mem_Ico]
[GOAL]
case succ.hx
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
set_eq : Ico (Nat.succ m) (m + Nat.succ (Nat.succ k)) = Ico (Nat.succ (m + 1)) (m + 1 + Nat.succ k) ∪ {m + 1}
⊢ ¬(Nat.succ (m + 1) ≤ m + 1 ∧ m + 1 < m + 1 + Nat.succ k)
[PROOFSTEP]
exact fun h => (Nat.lt_succ_self _).not_le h.1
[GOAL]
case succ.hy
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in Ico (Nat.succ m) (m + Nat.succ k), i) • coeff p (m + k)
m : ℕ
⊢ coeff p (m + 1 + k) = coeff p (m + Nat.succ k)
[PROOFSTEP]
exact congr_arg _ (Nat.succ_add m k)
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
k : ℕ
p : R[X]
⊢ ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in range k, (m + k - i)) • coeff p (m + k)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ ∀ (m : ℕ), coeff ((↑derivative)^[Nat.zero] p) m = (∏ i in range Nat.zero, (m + Nat.zero - i)) • coeff p (m + Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in range k, (m + k - i)) • coeff p (m + k)
⊢ ∀ (m : ℕ),
    coeff ((↑derivative)^[Nat.succ k] p) m =
      (∏ i in range (Nat.succ k), (m + Nat.succ k - i)) • coeff p (m + Nat.succ k)
[PROOFSTEP]
intro m
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in range k, (m + k - i)) • coeff p (m + k)
m : ℕ
⊢ coeff ((↑derivative)^[Nat.succ k] p) m = (∏ i in range (Nat.succ k), (m + Nat.succ k - i)) • coeff p (m + Nat.succ k)
[PROOFSTEP]
calc
  (derivative^[k + 1] p).coeff m = (∏ i in range k, (m + k.succ - i)) • p.coeff (m + k.succ) * (m + 1) := by
    rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]
  _ = ((∏ i in range k, (m + k.succ - i)) * (m + 1)) • p.coeff (m + k.succ) := by
    rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul, mul_comm]
  _ = (∏ i in range k.succ, (m + k.succ - i)) • p.coeff (m + k.succ) := by
    rw [prod_range_succ, add_tsub_assoc_of_le k.le_succ, Nat.succ_sub le_rfl, tsub_self]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in range k, (m + k - i)) • coeff p (m + k)
m : ℕ
⊢ coeff ((↑derivative)^[k + 1] p) m = (∏ i in range k, (m + Nat.succ k - i)) • coeff p (m + Nat.succ k) * (↑m + 1)
[PROOFSTEP]
rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in range k, (m + k - i)) • coeff p (m + k)
m : ℕ
⊢ (∏ i in range k, (m + Nat.succ k - i)) • coeff p (m + Nat.succ k) * (↑m + 1) =
    ((∏ i in range k, (m + Nat.succ k - i)) * (m + 1)) • coeff p (m + Nat.succ k)
[PROOFSTEP]
rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul, mul_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), coeff ((↑derivative)^[k] p) m = (∏ i in range k, (m + k - i)) • coeff p (m + k)
m : ℕ
⊢ ((∏ i in range k, (m + Nat.succ k - i)) * (m + 1)) • coeff p (m + Nat.succ k) =
    (∏ i in range (Nat.succ k), (m + Nat.succ k - i)) • coeff p (m + Nat.succ k)
[PROOFSTEP]
rw [prod_range_succ, add_tsub_assoc_of_le k.le_succ, Nat.succ_sub le_rfl, tsub_self]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
n : ℕ
p q : R[X]
⊢ (↑derivative)^[n] (p * q) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q)
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ (↑derivative)^[Nat.zero] (p * q) =
    ∑ k in range (Nat.succ Nat.zero), Nat.choose Nat.zero k • ((↑derivative)^[Nat.zero - k] p * (↑derivative)^[k] q)
[PROOFSTEP]
simp [Finset.range]
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH :
  (↑derivative)^[n] (p * q) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q)
⊢ (↑derivative)^[Nat.succ n] (p * q) =
    ∑ k in range (Nat.succ (Nat.succ n)),
      Nat.choose (Nat.succ n) k • ((↑derivative)^[Nat.succ n - k] p * (↑derivative)^[k] q)
[PROOFSTEP]
calc
  derivative^[n + 1] (p * q) =
      derivative (∑ k : ℕ in range n.succ, n.choose k • (derivative^[n - k] p * derivative^[k] q)) :=
    by rw [Function.iterate_succ_apply', IH]
  _ =
      (∑ k : ℕ in range n.succ, n.choose k • (derivative^[n - k + 1] p * derivative^[k] q)) +
        ∑ k : ℕ in range n.succ, n.choose k • (derivative^[n - k] p * derivative^[k + 1] q) :=
    by
    simp_rw [derivative_sum, derivative_smul, derivative_mul, Function.iterate_succ_apply', smul_add, sum_add_distrib]
  _ =
      (∑ k : ℕ in range n.succ, n.choose k.succ • (derivative^[n - k] p * derivative^[k + 1] q)) +
          1 • (derivative^[n + 1] p * derivative^[0] q) +
        ∑ k : ℕ in range n.succ, n.choose k • (derivative^[n - k] p * derivative^[k + 1] q) :=
    ?_
  _ =
      ((∑ k : ℕ in range n.succ, n.choose k • (derivative^[n - k] p * derivative^[k + 1] q)) +
          ∑ k : ℕ in range n.succ, n.choose k.succ • (derivative^[n - k] p * derivative^[k + 1] q)) +
        1 • (derivative^[n + 1] p * derivative^[0] q) :=
    by rw [add_comm, add_assoc]
  _ =
      (∑ i : ℕ in range n.succ, (n + 1).choose (i + 1) • (derivative^[n + 1 - (i + 1)] p * derivative^[i + 1] q)) +
        1 • (derivative^[n + 1] p * derivative^[0] q) :=
    by simp_rw [Nat.choose_succ_succ, Nat.succ_sub_succ, add_smul, sum_add_distrib]
  _ = ∑ k : ℕ in range n.succ.succ, n.succ.choose k • (derivative^[n.succ - k] p * derivative^[k] q) := by
    rw [sum_range_succ' _ n.succ, Nat.choose_zero_right, tsub_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH :
  (↑derivative)^[n] (p * q) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q)
⊢ (↑derivative)^[n + 1] (p * q) =
    ↑derivative (∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q))
[PROOFSTEP]
rw [Function.iterate_succ_apply', IH]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH :
  (↑derivative)^[n] (p * q) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q)
⊢ ↑derivative (∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q)) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k + 1] p * (↑derivative)^[k] q) +
      ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k + 1] q)
[PROOFSTEP]
simp_rw [derivative_sum, derivative_smul, derivative_mul, Function.iterate_succ_apply', smul_add, sum_add_distrib]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH :
  (↑derivative)^[n] (p * q) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q)
⊢ ∑ k in range (Nat.succ n), Nat.choose n (Nat.succ k) • ((↑derivative)^[n - k] p * (↑derivative)^[k + 1] q) +
        1 • ((↑derivative)^[n + 1] p * (↑derivative)^[0] q) +
      ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k + 1] q) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k + 1] q) +
        ∑ k in range (Nat.succ n), Nat.choose n (Nat.succ k) • ((↑derivative)^[n - k] p * (↑derivative)^[k + 1] q) +
      1 • ((↑derivative)^[n + 1] p * (↑derivative)^[0] q)
[PROOFSTEP]
rw [add_comm, add_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH :
  (↑derivative)^[n] (p * q) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q)
⊢ ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k + 1] q) +
        ∑ k in range (Nat.succ n), Nat.choose n (Nat.succ k) • ((↑derivative)^[n - k] p * (↑derivative)^[k + 1] q) +
      1 • ((↑derivative)^[n + 1] p * (↑derivative)^[0] q) =
    ∑ i in range (Nat.succ n),
        Nat.choose (n + 1) (i + 1) • ((↑derivative)^[n + 1 - (i + 1)] p * (↑derivative)^[i + 1] q) +
      1 • ((↑derivative)^[n + 1] p * (↑derivative)^[0] q)
[PROOFSTEP]
simp_rw [Nat.choose_succ_succ, Nat.succ_sub_succ, add_smul, sum_add_distrib]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH :
  (↑derivative)^[n] (p * q) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q)
⊢ ∑ i in range (Nat.succ n),
        Nat.choose (n + 1) (i + 1) • ((↑derivative)^[n + 1 - (i + 1)] p * (↑derivative)^[i + 1] q) +
      1 • ((↑derivative)^[n + 1] p * (↑derivative)^[0] q) =
    ∑ k in range (Nat.succ (Nat.succ n)),
      Nat.choose (Nat.succ n) k • ((↑derivative)^[Nat.succ n - k] p * (↑derivative)^[k] q)
[PROOFSTEP]
rw [sum_range_succ' _ n.succ, Nat.choose_zero_right, tsub_zero]
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH :
  (↑derivative)^[n] (p * q) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q)
⊢ ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k + 1] p * (↑derivative)^[k] q) +
      ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k + 1] q) =
    ∑ k in range (Nat.succ n), Nat.choose n (Nat.succ k) • ((↑derivative)^[n - k] p * (↑derivative)^[k + 1] q) +
        1 • ((↑derivative)^[n + 1] p * (↑derivative)^[0] q) +
      ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k + 1] q)
[PROOFSTEP]
congr
[GOAL]
case succ.e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH :
  (↑derivative)^[n] (p * q) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q)
⊢ ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k + 1] p * (↑derivative)^[k] q) =
    ∑ k in range (Nat.succ n), Nat.choose n (Nat.succ k) • ((↑derivative)^[n - k] p * (↑derivative)^[k + 1] q) +
      1 • ((↑derivative)^[n + 1] p * (↑derivative)^[0] q)
[PROOFSTEP]
refine' (sum_range_succ' _ _).trans (congr_arg₂ (· + ·) _ _)
[GOAL]
case succ.e_a.refine'_1
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH :
  (↑derivative)^[n] (p * q) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q)
⊢ ∑ k in range n, Nat.choose n (k + 1) • ((↑derivative)^[n - (k + 1) + 1] p * (↑derivative)^[k + 1] q) =
    ∑ k in range (Nat.succ n), Nat.choose n (Nat.succ k) • ((↑derivative)^[n - k] p * (↑derivative)^[k + 1] q)
[PROOFSTEP]
rw [sum_range_succ, Nat.choose_succ_self, zero_smul, add_zero]
[GOAL]
case succ.e_a.refine'_1
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH :
  (↑derivative)^[n] (p * q) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q)
⊢ ∑ k in range n, Nat.choose n (k + 1) • ((↑derivative)^[n - (k + 1) + 1] p * (↑derivative)^[k + 1] q) =
    ∑ x in range n, Nat.choose n (Nat.succ x) • ((↑derivative)^[n - x] p * (↑derivative)^[x + 1] q)
[PROOFSTEP]
refine' sum_congr rfl fun k hk => _
[GOAL]
case succ.e_a.refine'_1
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH :
  (↑derivative)^[n] (p * q) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q)
k : ℕ
hk : k ∈ range n
⊢ Nat.choose n (k + 1) • ((↑derivative)^[n - (k + 1) + 1] p * (↑derivative)^[k + 1] q) =
    Nat.choose n (Nat.succ k) • ((↑derivative)^[n - k] p * (↑derivative)^[k + 1] q)
[PROOFSTEP]
rw [mem_range] at hk
[GOAL]
case succ.e_a.refine'_1
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH :
  (↑derivative)^[n] (p * q) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q)
k : ℕ
hk : k < n
⊢ Nat.choose n (k + 1) • ((↑derivative)^[n - (k + 1) + 1] p * (↑derivative)^[k + 1] q) =
    Nat.choose n (Nat.succ k) • ((↑derivative)^[n - k] p * (↑derivative)^[k + 1] q)
[PROOFSTEP]
congr
[GOAL]
case succ.e_a.refine'_1.e_a.e_a.e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH :
  (↑derivative)^[n] (p * q) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q)
k : ℕ
hk : k < n
⊢ n - (k + 1) + 1 = n - k
[PROOFSTEP]
rw [tsub_add_eq_add_tsub (Nat.succ_le_of_lt hk), Nat.succ_sub_succ]
[GOAL]
case succ.e_a.refine'_2
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH :
  (↑derivative)^[n] (p * q) =
    ∑ k in range (Nat.succ n), Nat.choose n k • ((↑derivative)^[n - k] p * (↑derivative)^[k] q)
⊢ Nat.choose n 0 • ((↑derivative)^[n - 0 + 1] p * (↑derivative)^[0] q) =
    1 • ((↑derivative)^[n + 1] p * (↑derivative)^[0] q)
[PROOFSTEP]
rw [Nat.choose_zero_right, tsub_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ ↑derivative (p ^ (Nat.zero + 1)) = ↑C (↑Nat.zero + 1) * p ^ Nat.zero * ↑derivative p
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : ↑derivative (p ^ (n + 1)) = ↑C (↑n + 1) * p ^ n * ↑derivative p
⊢ ↑derivative (p ^ (Nat.succ n + 1)) = ↑C (↑(Nat.succ n) + 1) * p ^ Nat.succ n * ↑derivative p
[PROOFSTEP]
rw [pow_succ', derivative_mul, ih, Nat.add_one, mul_right_comm, C_add, add_mul, add_mul, pow_succ', ← mul_assoc, C_1,
  one_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : ↑derivative (p ^ (n + 1)) = ↑C (↑n + 1) * p ^ n * ↑derivative p
⊢ (↑C ↑n * p ^ n * p + p ^ n * p) * ↑derivative p + p ^ n * p * ↑derivative p =
    ↑C (↑(Nat.succ n) + 1) * p ^ n * p * ↑derivative p
[PROOFSTEP]
simp [add_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ ↑derivative (p ^ Nat.zero) = ↑C ↑Nat.zero * p ^ (Nat.zero - 1) * ↑derivative p
[PROOFSTEP]
rw [pow_zero, derivative_one, Nat.cast_zero, C_0, zero_mul, zero_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
⊢ ↑derivative (p ^ Nat.succ n) = ↑C ↑(Nat.succ n) * p ^ (Nat.succ n - 1) * ↑derivative p
[PROOFSTEP]
rw [p.derivative_pow_succ n, n.succ_sub_one, n.cast_succ]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p : R[X]
⊢ ↑derivative (p ^ 2) = ↑C 2 * p * ↑derivative p
[PROOFSTEP]
rw [derivative_pow_succ, Nat.cast_one, one_add_one_eq_two, pow_one]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
f : R[X]
n m : ℕ
c : R
hm : m ≠ 0
⊢ ↑n ∣ eval c ((↑derivative)^[m] (f ^ n))
[PROOFSTEP]
obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hm
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : Nat.succ m ≠ 0
⊢ ↑n ∣ eval c ((↑derivative)^[Nat.succ m] (f ^ n))
[PROOFSTEP]
rw [Function.iterate_succ_apply, derivative_pow, mul_assoc, C_eq_nat_cast, iterate_derivative_nat_cast_mul, eval_mul,
  eval_nat_cast]
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : Nat.succ m ≠ 0
⊢ ↑n ∣ ↑n * eval c ((↑derivative)^[m] (f ^ (n - 1) * ↑derivative f))
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n k : ℕ
⊢ (↑derivative)^[k] (X ^ n) = ↑(Nat.descFactorial n k) * X ^ (n - k)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n : ℕ
⊢ (↑derivative)^[Nat.zero] (X ^ n) = ↑(Nat.descFactorial n Nat.zero) * X ^ (n - Nat.zero)
[PROOFSTEP]
erw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n k : ℕ
ih : (↑derivative)^[k] (X ^ n) = ↑(Nat.descFactorial n k) * X ^ (n - k)
⊢ (↑derivative)^[Nat.succ k] (X ^ n) = ↑(Nat.descFactorial n (Nat.succ k)) * X ^ (n - Nat.succ k)
[PROOFSTEP]
rw [Function.iterate_succ_apply', ih, derivative_nat_cast_mul, derivative_X_pow, C_eq_nat_cast, Nat.succ_eq_add_one,
  Nat.descFactorial_succ, Nat.sub_sub, Nat.cast_mul]
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n k : ℕ
ih : (↑derivative)^[k] (X ^ n) = ↑(Nat.descFactorial n k) * X ^ (n - k)
⊢ ↑(Nat.descFactorial n k) * (↑(n - k) * X ^ (n - (k + 1))) = ↑(n - k) * ↑(Nat.descFactorial n k) * X ^ (n - (k + 1))
[PROOFSTEP]
simp [mul_comm, mul_assoc, mul_left_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n k : ℕ
⊢ (↑derivative)^[k] (X ^ n) = ↑C ↑(Nat.descFactorial n k) * X ^ (n - k)
[PROOFSTEP]
rw [iterate_derivative_X_pow_eq_nat_cast_mul n k, C_eq_nat_cast]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n k : ℕ
⊢ (↑derivative)^[k] (X ^ n) = ↑(Nat.descFactorial n k) • X ^ (n - k)
[PROOFSTEP]
rw [iterate_derivative_X_pow_eq_C_mul n k, smul_eq_C_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
c : R
m : ℕ
⊢ ↑derivative ((X + ↑C c) ^ m) = ↑C ↑m * (X + ↑C c) ^ (m - 1)
[PROOFSTEP]
rw [derivative_pow, derivative_X_add_C, mul_one]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
c : R
⊢ ↑derivative ((X + ↑C c) ^ 2) = ↑C 2 * (X + ↑C c)
[PROOFSTEP]
rw [derivative_sq, derivative_X_add_C, mul_one]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n k : ℕ
c : R
⊢ (↑derivative)^[k] ((X + ↑C c) ^ n) = ↑(∏ i in range k, (n - i)) * (X + ↑C c) ^ (n - k)
[PROOFSTEP]
induction' k with k IH
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n : ℕ
c : R
⊢ (↑derivative)^[Nat.zero] ((X + ↑C c) ^ n) = ↑(∏ i in range Nat.zero, (n - i)) * (X + ↑C c) ^ (n - Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n : ℕ
c : R
k : ℕ
IH : (↑derivative)^[k] ((X + ↑C c) ^ n) = ↑(∏ i in range k, (n - i)) * (X + ↑C c) ^ (n - k)
⊢ (↑derivative)^[Nat.succ k] ((X + ↑C c) ^ n) = ↑(∏ i in range (Nat.succ k), (n - i)) * (X + ↑C c) ^ (n - Nat.succ k)
[PROOFSTEP]
simp only [Function.iterate_succ_apply', IH, derivative_mul, zero_mul, derivative_nat_cast, zero_add,
  Finset.prod_range_succ, C_eq_nat_cast, Nat.sub_sub, ← mul_assoc, derivative_X_add_C_pow, Nat.succ_eq_add_one,
  Nat.cast_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
⊢ ↑derivative (comp p q) = ↑derivative q * comp (↑derivative p) q
[PROOFSTEP]
induction p using Polynomial.induction_on'
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
q p✝ q✝ : R[X]
a✝¹ : ↑derivative (comp p✝ q) = ↑derivative q * comp (↑derivative p✝) q
a✝ : ↑derivative (comp q✝ q) = ↑derivative q * comp (↑derivative q✝) q
⊢ ↑derivative (comp (p✝ + q✝) q) = ↑derivative q * comp (↑derivative (p✝ + q✝)) q
[PROOFSTEP]
simp [*, mul_add]
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ ↑derivative (comp (↑(monomial n✝) a✝) q) = ↑derivative q * comp (↑derivative (↑(monomial n✝) a✝)) q
[PROOFSTEP]
simp only [derivative_pow, derivative_mul, monomial_comp, derivative_monomial, derivative_C, zero_mul, C_eq_nat_cast,
  zero_add, RingHom.map_mul]
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ ↑C a✝ * (↑n✝ * q ^ (n✝ - 1) * ↑derivative q) = ↑derivative q * (↑C a✝ * ↑n✝ * q ^ (n✝ - 1))
[PROOFSTEP]
ring
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ ↑derivative (eval₂ C q (↑C r)) = eval₂ C q (↑derivative (↑C r)) * ↑derivative q
[PROOFSTEP]
rw [eval₂_C, derivative_C, eval₂_zero, zero_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q p₁ p₂ : R[X]
ih₁ : ↑derivative (eval₂ C q p₁) = eval₂ C q (↑derivative p₁) * ↑derivative q
ih₂ : ↑derivative (eval₂ C q p₂) = eval₂ C q (↑derivative p₂) * ↑derivative q
⊢ ↑derivative (eval₂ C q (p₁ + p₂)) = eval₂ C q (↑derivative (p₁ + p₂)) * ↑derivative q
[PROOFSTEP]
rw [eval₂_add, derivative_add, ih₁, ih₂, derivative_add, eval₂_add, add_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih : ↑derivative (eval₂ C q (↑C r * X ^ n)) = eval₂ C q (↑derivative (↑C r * X ^ n)) * ↑derivative q
⊢ ↑derivative (eval₂ C q (↑C r * X ^ (n + 1))) = eval₂ C q (↑derivative (↑C r * X ^ (n + 1))) * ↑derivative q
[PROOFSTEP]
rw [pow_succ', ← mul_assoc, eval₂_mul, eval₂_X, derivative_mul, ih, @derivative_mul _ _ _ X, derivative_X, mul_one,
  eval₂_add, @eval₂_mul _ _ _ _ X, eval₂_X, add_mul, mul_right_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s : Multiset ι
f : ι → R[X]
⊢ ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
[PROOFSTEP]
refine' Multiset.induction_on s (by simp) fun i s h => _
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s : Multiset ι
f : ι → R[X]
⊢ ↑derivative (Multiset.prod (Multiset.map f 0)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase 0 i)) * ↑derivative (f i)) 0)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
⊢ ↑derivative (Multiset.prod (Multiset.map f (i ::ₘ s))) =
    Multiset.sum
      (Multiset.map (fun i_1 => Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) i_1)) * ↑derivative (f i_1))
        (i ::ₘ s))
[PROOFSTEP]
rw [Multiset.map_cons, Multiset.prod_cons, derivative_mul, Multiset.map_cons _ i s, Multiset.sum_cons,
  Multiset.erase_cons_head, mul_comm (derivative (f i))]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
⊢ Multiset.prod (Multiset.map f s) * ↑derivative (f i) + f i * ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.prod (Multiset.map f s) * ↑derivative (f i) +
      Multiset.sum
        (Multiset.map (fun i_1 => Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) i_1)) * ↑derivative (f i_1))
          s)
[PROOFSTEP]
congr
[GOAL]
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
⊢ f i * ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum
      (Multiset.map (fun i_1 => Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) i_1)) * ↑derivative (f i_1)) s)
[PROOFSTEP]
rw [h, ← AddMonoidHom.coe_mulLeft, (AddMonoidHom.mulLeft (f i)).map_multiset_sum _, AddMonoidHom.coe_mulLeft]
[GOAL]
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
⊢ Multiset.sum
      (Multiset.map (HMul.hMul (f i))
        (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)) =
    Multiset.sum
      (Multiset.map (fun i_1 => Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) i_1)) * ↑derivative (f i_1)) s)
[PROOFSTEP]
simp only [Function.comp_apply, Multiset.map_map]
[GOAL]
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
⊢ Multiset.sum
      (Multiset.map (fun x => f i * (Multiset.prod (Multiset.map f (Multiset.erase s x)) * ↑derivative (f x))) s) =
    Multiset.sum
      (Multiset.map (fun x => Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) x)) * ↑derivative (f x)) s)
[PROOFSTEP]
refine' congr_arg _ (Multiset.map_congr rfl fun j hj => _)
[GOAL]
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
j : ι
hj : j ∈ s
⊢ f i * (Multiset.prod (Multiset.map f (Multiset.erase s j)) * ↑derivative (f j)) =
    Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) j)) * ↑derivative (f j)
[PROOFSTEP]
rw [← mul_assoc, ← Multiset.prod_cons, ← Multiset.map_cons]
[GOAL]
case e_a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
j : ι
hj : j ∈ s
⊢ Multiset.prod (Multiset.map f (i ::ₘ Multiset.erase s j)) * ↑derivative (f j) =
    Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) j)) * ↑derivative (f j)
[PROOFSTEP]
by_cases hij : i = j
[GOAL]
case pos
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
j : ι
hj : j ∈ s
hij : i = j
⊢ Multiset.prod (Multiset.map f (i ::ₘ Multiset.erase s j)) * ↑derivative (f j) =
    Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) j)) * ↑derivative (f j)
[PROOFSTEP]
simp [hij, ← Multiset.prod_cons, ← Multiset.map_cons, Multiset.cons_erase hj]
[GOAL]
case neg
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  ↑derivative (Multiset.prod (Multiset.map f s)) =
    Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f (Multiset.erase s i)) * ↑derivative (f i)) s)
j : ι
hj : j ∈ s
hij : ¬i = j
⊢ Multiset.prod (Multiset.map f (i ::ₘ Multiset.erase s j)) * ↑derivative (f j) =
    Multiset.prod (Multiset.map f (Multiset.erase (i ::ₘ s) j)) * ↑derivative (f j)
[PROOFSTEP]
simp [hij]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
c : R
⊢ ↑derivative (X - ↑C c) = 1
[PROOFSTEP]
rw [derivative_sub, derivative_X, derivative_C, sub_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
k : ℕ
f g : R[X]
⊢ (↑derivative)^[k] (f - g) = (↑derivative)^[k] f - (↑derivative)^[k] g
[PROOFSTEP]
induction' k with k ih generalizing f g
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
f✝ g✝ f g : R[X]
⊢ (↑derivative)^[Nat.zero] (f - g) = (↑derivative)^[Nat.zero] f - (↑derivative)^[Nat.zero] g
[PROOFSTEP]
simp [*]
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
f✝ g✝ : R[X]
k : ℕ
ih : ∀ {f g : R[X]}, (↑derivative)^[k] (f - g) = (↑derivative)^[k] f - (↑derivative)^[k] g
f g : R[X]
⊢ (↑derivative)^[Nat.succ k] (f - g) = (↑derivative)^[Nat.succ k] f - (↑derivative)^[Nat.succ k] g
[PROOFSTEP]
simp [*]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Ring R
n : ℤ
⊢ ↑derivative ↑n = 0
[PROOFSTEP]
rw [← C_eq_int_cast n]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Ring R
n : ℤ
⊢ ↑derivative (↑C ↑n) = 0
[PROOFSTEP]
exact derivative_C
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Ring R
n : ℤ
f : R[X]
⊢ ↑derivative (↑n * f) = ↑n * ↑derivative f
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Ring R
n : ℤ
k : ℕ
f : R[X]
⊢ (↑derivative)^[k] (↑n * f) = ↑n * (↑derivative)^[k] f
[PROOFSTEP]
induction' k with k ih generalizing f
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Ring R
n : ℤ
f✝ f : R[X]
⊢ (↑derivative)^[Nat.zero] (↑n * f) = ↑n * (↑derivative)^[Nat.zero] f
[PROOFSTEP]
simp [*]
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Ring R
n : ℤ
f✝ : R[X]
k : ℕ
ih : ∀ {f : R[X]}, (↑derivative)^[k] (↑n * f) = ↑n * (↑derivative)^[k] f
f : R[X]
⊢ (↑derivative)^[Nat.succ k] (↑n * f) = ↑n * (↑derivative)^[Nat.succ k] f
[PROOFSTEP]
simp [*]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p : R[X]
⊢ ↑derivative (comp p (1 - X)) = -comp (↑derivative p) (1 - X)
[PROOFSTEP]
simp [derivative_comp]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p : R[X]
k : ℕ
⊢ (↑derivative)^[k] (comp p (1 - X)) = (-1) ^ k * comp ((↑derivative)^[k] p) (1 - X)
[PROOFSTEP]
induction' k with k ih generalizing p
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ p : R[X]
⊢ (↑derivative)^[Nat.zero] (comp p (1 - X)) = (-1) ^ Nat.zero * comp ((↑derivative)^[Nat.zero] p) (1 - X)
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ : R[X]
k : ℕ
ih : ∀ (p : R[X]), (↑derivative)^[k] (comp p (1 - X)) = (-1) ^ k * comp ((↑derivative)^[k] p) (1 - X)
p : R[X]
⊢ (↑derivative)^[Nat.succ k] (comp p (1 - X)) = (-1) ^ Nat.succ k * comp ((↑derivative)^[Nat.succ k] p) (1 - X)
[PROOFSTEP]
simp [ih (derivative p), iterate_derivative_neg, derivative_comp, pow_succ]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
S : Multiset R
r : R
hr : r ∈ S
⊢ eval r (↑derivative (Multiset.prod (Multiset.map (fun a => X - ↑C a) S))) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase S r))
[PROOFSTEP]
nth_rw 1 [← Multiset.cons_erase hr]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
S : Multiset R
r : R
hr : r ∈ S
⊢ eval r (↑derivative (Multiset.prod (Multiset.map (fun a => X - ↑C a) (r ::ₘ Multiset.erase S r)))) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase S r))
[PROOFSTEP]
have := (evalRingHom r).map_multiset_prod (Multiset.map (fun a => X - C a) (S.erase r))
[GOAL]
R : Type u
S✝ : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
S : Multiset R
r : R
hr : r ∈ S
this :
  ↑(evalRingHom r) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (Multiset.erase S r))) =
    Multiset.prod (Multiset.map (↑(evalRingHom r)) (Multiset.map (fun a => X - ↑C a) (Multiset.erase S r)))
⊢ eval r (↑derivative (Multiset.prod (Multiset.map (fun a => X - ↑C a) (r ::ₘ Multiset.erase S r)))) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase S r))
[PROOFSTEP]
simpa using this
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
c : R
m : ℕ
⊢ ↑derivative ((X - ↑C c) ^ m) = ↑C ↑m * (X - ↑C c) ^ (m - 1)
[PROOFSTEP]
rw [derivative_pow, derivative_X_sub_C, mul_one]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
c : R
⊢ ↑derivative ((X - ↑C c) ^ 2) = ↑C 2 * (X - ↑C c)
[PROOFSTEP]
rw [derivative_sq, derivative_X_sub_C, mul_one]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommRing R
n k : ℕ
c : R
⊢ (↑derivative)^[k] ((X - ↑C c) ^ n) = ↑(∏ i in range k, (n - i)) * (X - ↑C c) ^ (n - k)
[PROOFSTEP]
rw [sub_eq_add_neg, ← C_neg, iterate_derivative_X_add_pow]


[GOAL]
α : Type u_1
s : Set α
a : α
⊢ op a ∈ Set.op s ↔ a ∈ s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
s : Set αᵒᵖ
a : αᵒᵖ
⊢ a.unop ∈ Set.unop s ↔ a ∈ s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
x : α
⊢ Set.op {x} = {op x}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ Set.op {x} ↔ x✝ ∈ {op x}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ Set.op {x} → x✝ ∈ {op x}
[PROOFSTEP]
apply unop_injective
[GOAL]
case h.mpr
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ {op x} → x✝ ∈ Set.op {x}
[PROOFSTEP]
apply op_injective
[GOAL]
α : Type u_1
x : αᵒᵖ
⊢ Set.unop {x} = {x.unop}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ Set.unop {x} ↔ x✝ ∈ {x.unop}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ Set.unop {x} → x✝ ∈ {x.unop}
[PROOFSTEP]
apply op_injective
[GOAL]
case h.mpr
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {x.unop} → x✝ ∈ Set.unop {x}
[PROOFSTEP]
apply unop_injective
[GOAL]
α : Type u_1
x : α
⊢ Set.unop {op x} = {x}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
x x✝ : α
⊢ x✝ ∈ Set.unop {op x} ↔ x✝ ∈ {x}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
x x✝ : α
⊢ x✝ ∈ Set.unop {op x} → x✝ ∈ {x}
[PROOFSTEP]
apply op_injective
[GOAL]
case h.mpr
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {x} → x✝ ∈ Set.unop {op x}
[PROOFSTEP]
apply unop_injective
[GOAL]
α : Type u_1
x : αᵒᵖ
⊢ Set.op {x.unop} = {x}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ Set.op {x.unop} ↔ x✝ ∈ {x}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ Set.op {x.unop} → x✝ ∈ {x}
[PROOFSTEP]
apply unop_injective
[GOAL]
case h.mpr
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {x} → x✝ ∈ Set.op {x.unop}
[PROOFSTEP]
apply op_injective


[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
s s₁ s₂ t t₁ t₂ u v : Set α
a b c : α
⊢ c ∈ s ⊻ t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = c
[PROOFSTEP]
simp [(· ⊻ ·)]
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α
a b c : α
s t : Set α
⊢ image2 (fun x x_1 => x ⊔ x_1) s t = s ⊻ t
[PROOFSTEP]
have : (s ×ˢ t).image (uncurry (· ⊔ ·)) = Set.image2 (fun x x_1 => x ⊔ x_1) s t := by
  simp only [ge_iff_le, image_uncurry_prod]
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α
a b c : α
s t : Set α
⊢ (uncurry fun x x_1 => x ⊔ x_1) '' s ×ˢ t = image2 (fun x x_1 => x ⊔ x_1) s t
[PROOFSTEP]
simp only [ge_iff_le, image_uncurry_prod]
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α
a b c : α
s t : Set α
this : (uncurry fun x x_1 => x ⊔ x_1) '' s ×ˢ t = image2 (fun x x_1 => x ⊔ x_1) s t
⊢ image2 (fun x x_1 => x ⊔ x_1) s t = s ⊻ t
[PROOFSTEP]
rw [← this]
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α
a b c : α
s t : Set α
this : (uncurry fun x x_1 => x ⊔ x_1) '' s ×ˢ t = image2 (fun x x_1 => x ⊔ x_1) s t
⊢ (uncurry fun x x_1 => x ⊔ x_1) '' s ×ˢ t = s ⊻ t
[PROOFSTEP]
exact image_uncurry_prod _ _ _
[GOAL]
α : Type u_1
inst✝ : SemilatticeInf α
s s₁ s₂ t t₁ t₂ u v : Set α
a b c : α
⊢ c ∈ s ⊼ t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = c
[PROOFSTEP]
simp [(· ⊼ ·)]
[GOAL]
α : Type u_1
inst✝ : SemilatticeInf α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α
a b c : α
s t : Set α
⊢ image2 (fun x x_1 => x ⊓ x_1) s t = s ⊼ t
[PROOFSTEP]
have : (s ×ˢ t).image (uncurry (· ⊓ ·)) = Set.image2 (fun x x_1 => x ⊓ x_1) s t := by
  simp only [@ge_iff_le, @Set.image_uncurry_prod]
[GOAL]
α : Type u_1
inst✝ : SemilatticeInf α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α
a b c : α
s t : Set α
⊢ (uncurry fun x x_1 => x ⊓ x_1) '' s ×ˢ t = image2 (fun x x_1 => x ⊓ x_1) s t
[PROOFSTEP]
simp only [@ge_iff_le, @Set.image_uncurry_prod]
[GOAL]
α : Type u_1
inst✝ : SemilatticeInf α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α
a b c : α
s t : Set α
this : (uncurry fun x x_1 => x ⊓ x_1) '' s ×ˢ t = image2 (fun x x_1 => x ⊓ x_1) s t
⊢ image2 (fun x x_1 => x ⊓ x_1) s t = s ⊼ t
[PROOFSTEP]
rw [← this]
[GOAL]
α : Type u_1
inst✝ : SemilatticeInf α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Set α
a b c : α
s t : Set α
this : (uncurry fun x x_1 => x ⊓ x_1) '' s ×ˢ t = image2 (fun x x_1 => x ⊓ x_1) s t
⊢ (uncurry fun x x_1 => x ⊓ x_1) '' s ×ˢ t = s ⊼ t
[PROOFSTEP]
exact image_uncurry_prod _ _ _
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
⊢ upperClosure (s ⊻ t) = upperClosure s ⊔ upperClosure t
[PROOFSTEP]
ext a
[GOAL]
case a.h
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ a ∈ ↑(upperClosure (s ⊻ t)) ↔ a ∈ ↑(upperClosure s ⊔ upperClosure t)
[PROOFSTEP]
simp only [SetLike.mem_coe, mem_upperClosure, Set.mem_sups, exists_and_left, exists_prop, UpperSet.coe_sup,
  Set.mem_inter_iff]
[GOAL]
case a.h
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = a_1) ∧ a_1 ≤ a) ↔ (∃ a_1, a_1 ∈ s ∧ a_1 ≤ a) ∧ ∃ a_1, a_1 ∈ t ∧ a_1 ≤ a
[PROOFSTEP]
constructor
[GOAL]
case a.h.mp
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = a_1) ∧ a_1 ≤ a) → (∃ a_2, a_2 ∈ s ∧ a_2 ≤ a) ∧ ∃ a_2, a_2 ∈ t ∧ a_2 ≤ a
[PROOFSTEP]
rintro ⟨_, ⟨b, hb, c, hc, rfl⟩, ha⟩
[GOAL]
case a.h.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : b ⊔ c ≤ a
⊢ (∃ a_1, a_1 ∈ s ∧ a_1 ≤ a) ∧ ∃ a_1, a_1 ∈ t ∧ a_1 ≤ a
[PROOFSTEP]
exact ⟨⟨b, hb, le_sup_left.trans ha⟩, c, hc, le_sup_right.trans ha⟩
[GOAL]
case a.h.mpr
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ ((∃ a_1, a_1 ∈ s ∧ a_1 ≤ a) ∧ ∃ a_1, a_1 ∈ t ∧ a_1 ≤ a) → ∃ a_2, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = a_2) ∧ a_2 ≤ a
[PROOFSTEP]
rintro ⟨⟨b, hb, hab⟩, c, hc, hac⟩
[GOAL]
case a.h.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : SemilatticeSup α
s t : Set α
a b : α
hb : b ∈ s
hab : b ≤ a
c : α
hc : c ∈ t
hac : c ≤ a
⊢ ∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = a_1) ∧ a_1 ≤ a
[PROOFSTEP]
exact ⟨_, ⟨b, hb, c, hc, rfl⟩, sup_le hab hac⟩
[GOAL]
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
⊢ lowerClosure (s ⊼ t) = lowerClosure s ⊓ lowerClosure t
[PROOFSTEP]
ext a
[GOAL]
case a.h
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ ↑(lowerClosure (s ⊼ t)) ↔ a ∈ ↑(lowerClosure s ⊓ lowerClosure t)
[PROOFSTEP]
simp only [SetLike.mem_coe, mem_lowerClosure, Set.mem_infs, exists_and_left, exists_prop, LowerSet.coe_sup,
  Set.mem_inter_iff]
[GOAL]
case a.h
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = a_1) ∧ a ≤ a_1) ↔ a ∈ lowerClosure s ⊓ lowerClosure t
[PROOFSTEP]
constructor
[GOAL]
case a.h.mp
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = a_1) ∧ a ≤ a_1) → a ∈ lowerClosure s ⊓ lowerClosure t
[PROOFSTEP]
rintro ⟨_, ⟨b, hb, c, hc, rfl⟩, ha⟩
[GOAL]
case a.h.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : a ≤ b ⊓ c
⊢ a ∈ lowerClosure s ⊓ lowerClosure t
[PROOFSTEP]
exact ⟨⟨b, hb, ha.trans inf_le_left⟩, c, hc, ha.trans inf_le_right⟩
[GOAL]
case a.h.mpr
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ lowerClosure s ⊓ lowerClosure t → ∃ a_2, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = a_2) ∧ a ≤ a_2
[PROOFSTEP]
rintro ⟨⟨b, hb, hab⟩, c, hc, hac⟩
[GOAL]
case a.h.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
hab : a ≤ b
c : α
hc : c ∈ t
hac : a ≤ c
⊢ ∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = a_1) ∧ a ≤ a_1
[PROOFSTEP]
exact ⟨_, ⟨b, hb, c, hc, rfl⟩, le_inf hab hac⟩