R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
key : ↑derivative ((X - ↑C a) * (f /ₘ (X - ↑C a))) = ↑derivative (f - f %ₘ (X - ↑C a))
⊢ f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
⊢ f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
have key := by apply congrArg derivative <| X_sub_C_mul_divByMonic_eq_sub_modByMonic f a
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
key : ↑derivative ((X - ↑C a) * (f /ₘ (X - ↑C a))) = ↑derivative (f - ↑C (eval a f))
⊢ f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
key : ↑derivative ((X - ↑C a) * (f /ₘ (X - ↑C a))) = ↑derivative (f - f %ₘ (X - ↑C a))
⊢ f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
rw [modByMonic_X_sub_C_eq_C_eval] at key
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
key :
  (1 - ↑derivative (↑C a)) * (f /ₘ (X - ↑C a)) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) =
    ↑derivative f - ↑derivative (↑C (eval a f))
⊢ f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
key : ↑derivative ((X - ↑C a) * (f /ₘ (X - ↑C a))) = ↑derivative (f - ↑C (eval a f))
⊢ f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
rw [derivative_mul,derivative_sub,derivative_X,derivative_sub] at key
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
key : f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f - ↑derivative (↑C (eval a f))
⊢ f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
key :
  (1 - ↑derivative (↑C a)) * (f /ₘ (X - ↑C a)) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) =
    ↑derivative f - ↑derivative (↑C (eval a f))
⊢ f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
rw [derivative_C,sub_zero,one_mul] at key
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
key : f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
⊢ f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
key : f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f - ↑derivative (↑C (eval a f))
⊢ f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
rw [derivative_C,sub_zero] at key
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
key : f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
⊢ f /ₘ (X - ↑C a) + (X - ↑C a) * ↑derivative (f /ₘ (X - ↑C a)) = ↑derivative f
assumption
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
⊢ ?m.1889975
apply congrArg derivative <| X_sub_C_mul_divByMonic_eq_sub_modByMonic f a