-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_map [Semiring S] (p : R[X]) (f : R →+* S) :
    derivative (p.map f) = p.derivative.map f

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ derivative (map f p) = map f (derivative p)

Tactic:
let n := max p.natDegree (map f p).natDegree

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ derivative (map f p) = map f (derivative p)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ derivative (map f p) = map f (derivative p)

Tactic:
rw [derivative_apply, derivative_apply]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ ((map f p).sum fun n a => C (a * ↑n) * X ^ (n - 1)) = map f (p.sum fun n a => C (a * ↑n) * X ^ (n - 1))

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ ((map f p).sum fun n a => C (a * ↑n) * X ^ (n - 1)) = map f (p.sum fun n a => C (a * ↑n) * X ^ (n - 1))

Tactic:
rw [sum_over_range' _ _ (n + 1) ((le_max_left _ _).trans_lt (lt_add_one _))]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ ((map f p).sum fun n a => C (a * ↑n) * X ^ (n - 1)) = map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n✝ : ℕ := p.natDegree ⊔ (map f p).natDegree
n : ℕ
⊢ C (0 * ↑n) * X ^ (n - 1) = 0

Tactic:
rw [zero_mul, C_0, zero_mul]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ ((map f p).sum fun n a => C (a * ↑n) * X ^ (n - 1)) = map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))

Tactic:
rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ ∑ a ∈ range (n + 1), C ((map f p).coeff a * ↑a) * X ^ (a - 1) =
    map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0

Tactic:
intro n

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n✝ : ℕ := p.natDegree ⊔ (map f p).natDegree
n : ℕ
⊢ C (0 * ↑n) * X ^ (n - 1) = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0

Tactic:
all_goals intro n; rw [zero_mul, C_0, zero_mul]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ ∑ a ∈ range (n + 1), C ((map f p).coeff a * ↑a) * X ^ (a - 1) =
    map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))

Tactic:
simp only [Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_C, map_mul, coeff_map,
  map_natCast, Polynomial.map_natCast, Polynomial.map_pow, map_X]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ ((map f p).sum fun n a => C (a * ↑n) * X ^ (n - 1)) = map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0

Tactic:
on_goal 1 => rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ ∑ a ∈ range (n + 1), C ((map f p).coeff a * ↑a) * X ^ (a - 1) =
    map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := p.natDegree ⊔ (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0