-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_mul {f g : R[X]} : derivative (f * g) = derivative f * g + f * derivative g

Proof state:
case h_monomial.h_monomial.succ.succ
R : Type u
inst✝ : Semiring R
a b : R
m n : ℕ
⊢ (monomial (m + 1 + n)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + n)) (a * (b * ↑(n + 1))) =
    (monomial (m + (n + 1))) (a * (b * ↑(m + 1))) + (monomial (m + 1 + n)) (a * (b * ↑(n + 1)))

Tactic:
rw [add_assoc, add_comm n 1]

Result:
no goals

Proof state:
case h_add
R : Type u
inst✝ : Semiring R
g p✝ q✝ : R[X]
a✝¹ : derivative (p✝ * g) = derivative p✝ * g + p✝ * derivative g
a✝ : derivative (q✝ * g) = derivative q✝ * g + q✝ * derivative g
⊢ derivative ((p✝ + q✝) * g) = derivative (p✝ + q✝) * g + (p✝ + q✝) * derivative g

Tactic:
simp only [add_mul, map_add, add_assoc, add_left_comm, *]

Result:
no goals

Proof state:
case h_monomial.h_monomial
R : Type u
inst✝ : Semiring R
m : ℕ
a : R
n : ℕ
b : R
⊢ derivative ((monomial m) a * (monomial n) b) =
    derivative ((monomial m) a) * (monomial n) b + (monomial m) a * derivative ((monomial n) b)

Tactic:
simp only [monomial_mul_monomial, derivative_monomial]

Result:
case h_monomial.h_monomial
R : Type u
inst✝ : Semiring R
m : ℕ
a : R
n : ℕ
b : R
⊢ (monomial (m + n - 1)) (a * b * ↑(m + n)) =
    (monomial (m - 1 + n)) (a * ↑m * b) + (monomial (m + (n - 1))) (a * (b * ↑n))

Proof state:
case h_monomial.h_monomial.succ
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
b : R
m : ℕ
⊢ (monomial (m + 1 + n - 1)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + n - 1)) (a * (b * ↑n)) =
    (monomial (m + 1 - 1 + n)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + (n - 1))) (a * (b * ↑n))

Tactic:
cases n with
| zero => simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]
| succ n =>
simp only [Nat.add_succ_sub_one, add_tsub_cancel_right]
rw [add_assoc, add_comm n 1]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
f g : R[X]
⊢ derivative (f * g) = derivative f * g + f * derivative g

Tactic:
induction f using Polynomial.induction_on' with
| h_add => simp only [add_mul, map_add, add_assoc, add_left_comm, *]
| h_monomial m a =>
induction g using Polynomial.induction_on' with
| h_add => simp only [mul_add, map_add, add_assoc, add_left_comm, *]
| h_monomial n b =>
simp only [monomial_mul_monomial, derivative_monomial]
simp only [mul_assoc, (Nat.cast_commute _ _).eq, Nat.cast_add, mul_add, map_add]
cases m with
| zero => simp only [zero_add, Nat.cast_zero, mul_zero, map_zero]
| succ m =>
cases n with
| zero => simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]
| succ n =>
simp only [Nat.add_succ_sub_one, add_tsub_cancel_right]
rw [add_assoc, add_comm n 1]

Result:
no goals

Proof state:
case h_monomial.h_monomial.zero
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
b : R
⊢ (monomial (0 + n - 1)) (a * (b * ↑0)) + (monomial (0 + n - 1)) (a * (b * ↑n)) =
    (monomial (0 - 1 + n)) (a * (b * ↑0)) + (monomial (0 + (n - 1))) (a * (b * ↑n))

Tactic:
simp only [zero_add, Nat.cast_zero, mul_zero, map_zero]

Result:
no goals

Proof state:
case h_monomial.h_monomial
R : Type u
inst✝ : Semiring R
m : ℕ
a : R
n : ℕ
b : R
⊢ (monomial (m + n - 1)) (a * (b * ↑m)) + (monomial (m + n - 1)) (a * (b * ↑n)) =
    (monomial (m - 1 + n)) (a * (b * ↑m)) + (monomial (m + (n - 1))) (a * (b * ↑n))

Tactic:
cases m with
| zero => simp only [zero_add, Nat.cast_zero, mul_zero, map_zero]
| succ m =>
cases n with
| zero => simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]
| succ n =>
simp only [Nat.add_succ_sub_one, add_tsub_cancel_right]
rw [add_assoc, add_comm n 1]

Result:
no goals

Proof state:
case h_monomial.h_monomial.succ.succ
R : Type u
inst✝ : Semiring R
a b : R
m n : ℕ
⊢ (monomial (m + 1 + (n + 1) - 1)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + (n + 1) - 1)) (a * (b * ↑(n + 1))) =
    (monomial (m + 1 - 1 + (n + 1))) (a * (b * ↑(m + 1))) + (monomial (m + 1 + (n + 1 - 1))) (a * (b * ↑(n + 1)))

Tactic:
simp only [Nat.add_succ_sub_one, add_tsub_cancel_right]

Result:
case h_monomial.h_monomial.succ.succ
R : Type u
inst✝ : Semiring R
a b : R
m n : ℕ
⊢ (monomial (m + 1 + n)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + n)) (a * (b * ↑(n + 1))) =
    (monomial (m + (n + 1))) (a * (b * ↑(m + 1))) + (monomial (m + 1 + n)) (a * (b * ↑(n + 1)))

Proof state:
case h_monomial
R : Type u
inst✝ : Semiring R
g : R[X]
m : ℕ
a : R
⊢ derivative ((monomial m) a * g) = derivative ((monomial m) a) * g + (monomial m) a * derivative g

Tactic:
induction g using Polynomial.induction_on' with
| h_add => simp only [mul_add, map_add, add_assoc, add_left_comm, *]
| h_monomial n b =>
simp only [monomial_mul_monomial, derivative_monomial]
simp only [mul_assoc, (Nat.cast_commute _ _).eq, Nat.cast_add, mul_add, map_add]
cases m with
| zero => simp only [zero_add, Nat.cast_zero, mul_zero, map_zero]
| succ m =>
cases n with
| zero => simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]
| succ n =>
simp only [Nat.add_succ_sub_one, add_tsub_cancel_right]
rw [add_assoc, add_comm n 1]

Result:
no goals

Proof state:
case h_monomial.h_monomial.succ.zero
R : Type u
inst✝ : Semiring R
a b : R
m : ℕ
⊢ (monomial (m + 1 + 0 - 1)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + 0 - 1)) (a * (b * ↑0)) =
    (monomial (m + 1 - 1 + 0)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + (0 - 1))) (a * (b * ↑0))

Tactic:
simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]

Result:
no goals

Proof state:
case h_monomial.h_monomial
R : Type u
inst✝ : Semiring R
m : ℕ
a : R
n : ℕ
b : R
⊢ (monomial (m + n - 1)) (a * b * ↑(m + n)) =
    (monomial (m - 1 + n)) (a * ↑m * b) + (monomial (m + (n - 1))) (a * (b * ↑n))

Tactic:
simp only [mul_assoc, (Nat.cast_commute _ _).eq, Nat.cast_add, mul_add, map_add]

Result:
case h_monomial.h_monomial
R : Type u
inst✝ : Semiring R
m : ℕ
a : R
n : ℕ
b : R
⊢ (monomial (m + n - 1)) (a * (b * ↑m)) + (monomial (m + n - 1)) (a * (b * ↑n)) =
    (monomial (m - 1 + n)) (a * (b * ↑m)) + (monomial (m + (n - 1))) (a * (b * ↑n))

Proof state:
case h_monomial.h_add
R : Type u
inst✝ : Semiring R
m : ℕ
a : R
p✝ q✝ : R[X]
a✝¹ : derivative ((monomial m) a * p✝) = derivative ((monomial m) a) * p✝ + (monomial m) a * derivative p✝
a✝ : derivative ((monomial m) a * q✝) = derivative ((monomial m) a) * q✝ + (monomial m) a * derivative q✝
⊢ derivative ((monomial m) a * (p✝ + q✝)) =
    derivative ((monomial m) a) * (p✝ + q✝) + (monomial m) a * derivative (p✝ + q✝)

Tactic:
simp only [mul_add, map_add, add_assoc, add_left_comm, *]

Result:
no goals