import Mathlib

namespace ProofExplorer.Jacobian.Library
open Polynomial
variable {R : Type*} [CommRing R]

theorem coeff_mul_0 (p q : R[X]) : (p*q).coeff 0 = p.coeff 0 * q.coeff 0 := by
  simp [Polynomial.coeff_mul, Finset.Nat.sum_antidiagonal_succ]
  all_goals ring

theorem coeff_mul_1 (p q : R[X]) : (p*q).coeff 1 = p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0 := by
  simp [Polynomial.coeff_mul, Finset.Nat.sum_antidiagonal_succ]
  all_goals ring

theorem coeff_mul_2 (p q : R[X]) : (p*q).coeff 2 = p.coeff 0 * q.coeff 2 + p.coeff 1 * q.coeff 1 + p.coeff 2 * q.coeff 0 := by
  simp [Polynomial.coeff_mul, Finset.Nat.sum_antidiagonal_succ]
  all_goals ring

theorem coeff_mul_3 (p q : R[X]) : (p*q).coeff 3 = p.coeff 0 * q.coeff 3 + p.coeff 1 * q.coeff 2 + p.coeff 2 * q.coeff 1 + p.coeff 3 * q.coeff 0 := by
  simp [Polynomial.coeff_mul, Finset.Nat.sum_antidiagonal_succ]
  all_goals ring

theorem coeff_pow_2_0 (p : R[X]) : (p^2).coeff 0 = 1*(p.coeff 0)^2 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_2_1 (p : R[X]) : (p^2).coeff 1 = 2*(p.coeff 0)^1*(p.coeff 1)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_2_2 (p : R[X]) : (p^2).coeff 2 = 1*(p.coeff 1)^2 + 2*(p.coeff 0)^1*(p.coeff 2)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_2_3 (p : R[X]) : (p^2).coeff 3 = 2*(p.coeff 1)^1*(p.coeff 2)^1 + 2*(p.coeff 0)^1*(p.coeff 3)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_3_0 (p : R[X]) : (p^3).coeff 0 = 1*(p.coeff 0)^3 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_3_1 (p : R[X]) : (p^3).coeff 1 = 3*(p.coeff 0)^2*(p.coeff 1)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_3_2 (p : R[X]) : (p^3).coeff 2 = 3*(p.coeff 0)^1*(p.coeff 1)^2 + 3*(p.coeff 0)^2*(p.coeff 2)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_3_3 (p : R[X]) : (p^3).coeff 3 = 1*(p.coeff 1)^3 + 6*(p.coeff 0)^1*(p.coeff 1)^1*(p.coeff 2)^1 + 3*(p.coeff 0)^2*(p.coeff 3)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_4_0 (p : R[X]) : (p^4).coeff 0 = 1*(p.coeff 0)^4 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_4_1 (p : R[X]) : (p^4).coeff 1 = 4*(p.coeff 0)^3*(p.coeff 1)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_4_2 (p : R[X]) : (p^4).coeff 2 = 6*(p.coeff 0)^2*(p.coeff 1)^2 + 4*(p.coeff 0)^3*(p.coeff 2)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_4_3 (p : R[X]) : (p^4).coeff 3 = 4*(p.coeff 0)^1*(p.coeff 1)^3 + 12*(p.coeff 0)^2*(p.coeff 1)^1*(p.coeff 2)^1 + 4*(p.coeff 0)^3*(p.coeff 3)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_5_0 (p : R[X]) : (p^5).coeff 0 = 1*(p.coeff 0)^5 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_5_1 (p : R[X]) : (p^5).coeff 1 = 5*(p.coeff 0)^4*(p.coeff 1)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_5_2 (p : R[X]) : (p^5).coeff 2 = 10*(p.coeff 0)^3*(p.coeff 1)^2 + 5*(p.coeff 0)^4*(p.coeff 2)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_5_3 (p : R[X]) : (p^5).coeff 3 = 10*(p.coeff 0)^2*(p.coeff 1)^3 + 20*(p.coeff 0)^3*(p.coeff 1)^1*(p.coeff 2)^1 + 5*(p.coeff 0)^4*(p.coeff 3)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_6_0 (p : R[X]) : (p^6).coeff 0 = 1*(p.coeff 0)^6 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_6_1 (p : R[X]) : (p^6).coeff 1 = 6*(p.coeff 0)^5*(p.coeff 1)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_6_2 (p : R[X]) : (p^6).coeff 2 = 15*(p.coeff 0)^4*(p.coeff 1)^2 + 6*(p.coeff 0)^5*(p.coeff 2)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_6_3 (p : R[X]) : (p^6).coeff 3 = 20*(p.coeff 0)^3*(p.coeff 1)^3 + 30*(p.coeff 0)^4*(p.coeff 1)^1*(p.coeff 2)^1 + 6*(p.coeff 0)^5*(p.coeff 3)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_7_0 (p : R[X]) : (p^7).coeff 0 = 1*(p.coeff 0)^7 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_7_1 (p : R[X]) : (p^7).coeff 1 = 7*(p.coeff 0)^6*(p.coeff 1)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_7_2 (p : R[X]) : (p^7).coeff 2 = 21*(p.coeff 0)^5*(p.coeff 1)^2 + 7*(p.coeff 0)^6*(p.coeff 2)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

theorem coeff_pow_7_3 (p : R[X]) : (p^7).coeff 3 = 35*(p.coeff 0)^4*(p.coeff 1)^3 + 42*(p.coeff 0)^5*(p.coeff 1)^1*(p.coeff 2)^1 + 7*(p.coeff 0)^6*(p.coeff 3)^1 := by
  simp only [pow_succ, pow_zero, coeff_mul_0, coeff_mul_1, coeff_mul_2, coeff_mul_3]
  norm_num [Polynomial.coeff_one]
  all_goals ring

/-- Numeral rule for partial derivatives, in any finite number of variables. -/
theorem mv_pderiv_numeral {K : Type*} [CommRing K] {n : ℕ}
    (i : Fin n) (m : ℕ) [m.AtLeastTwo] :
    MvPolynomial.pderiv i (no_index (OfNat.ofNat m) : MvPolynomial (Fin n) K) = 0 := by
  exact (MvPolynomial.pderiv i).map_natCast m

/-- Coefficient extraction after multiplication by a variable. -/
theorem mv_coeff_X_mul {K : Type*} [CommSemiring K] {n : ℕ}
    (m : Fin n →₀ ℕ) (i : Fin n) (p : MvPolynomial (Fin n) K) :
    MvPolynomial.coeff m (MvPolynomial.X i * p) =
      if i ∈ m.support then MvPolynomial.coeff (m-Finsupp.single i 1) p else 0 :=
  MvPolynomial.coeff_X_mul' m i p

end ProofExplorer.Jacobian.Library