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)

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)
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)
induction' k with k ih generalizing p
no goals
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)
simp
no goals
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)
simp [ih (derivative p), iterate_derivative_neg, derivative_comp, pow_succ]