-- Mathlib/RingTheory/Polynomial/HilbertPoly.lean
lemma hilbertPoly_smul (a : F) (p : F[X]) (d : ℕ) :
    hilbertPoly (a • p) d = a • hilbertPoly p d

Proof state:
case succ
F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i) =
    a •
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i
⊢ ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i = a • ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i

Tactic:
rw [← sum_def _ fun _ r => r • _, ← sum_def _ fun _ r => r • _, Polynomial.smul_sum,
  sum_smul_index' _ _ _ fun i => zero_smul F (preHilbertPoly F d i)]

Result:
case succ
F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i) =
    a •
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i
⊢ (p.sum fun n a_1 => (a • a_1) • preHilbertPoly F d n) = p.sum fun n a_1 => a • a_1 • preHilbertPoly F d n

Proof state:
case succ
F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i) =
    a •
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i
⊢ (p.sum fun n a_1 => (a • a_1) • preHilbertPoly F d n) = p.sum fun n a_1 => a • a_1 • preHilbertPoly F d n

Tactic:
simp only [smul_assoc]

Result:
no goals

Proof state:
F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
⊢ (a • p).hilbertPoly d = a • p.hilbertPoly d

Tactic:
delta hilbertPoly

Result:
F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
⊢ (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i) =
    a •
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i

Proof state:
case succ
F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i) =
    a •
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i
⊢ (match d + 1 with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i) =
    a •
      match d + 1 with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i

Tactic:
simp only

Result:
case succ
F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i) =
    a •
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i
⊢ ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i = a • ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i

Proof state:
F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
⊢ (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i) =
    a •
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i

Tactic:
induction d with
| zero => simp only [smul_zero]
| succ d _ =>
    simp only
    rw [← sum_def _ fun _ r => r • _, ← sum_def _ fun _ r => r • _, Polynomial.smul_sum,
      sum_smul_index' _ _ _ fun i => zero_smul F (preHilbertPoly F d i)]
    simp only [smul_assoc]

Result:
no goals

Proof state:
case zero
F : Type u_1
inst✝ : Field F
a : F
p : F[X]
⊢ (match 0 with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i) =
    a •
      match 0 with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i

Tactic:
simp only [smul_zero]

Result:
no goals