-- Mathlib/RingTheory/Polynomial/HilbertPoly.lean
lemma hilbertPoly_add_left (p q : F[X]) (d : ℕ) :
    hilbertPoly (p + q) d = hilbertPoly p d + hilbertPoly q d

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

Tactic:
exact sum_add_index _ _ _ (fun _ => zero_smul ..) (fun _ _ _ => add_smul ..)

Result:
no goals

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

Tactic:
simp only [← coeff_add]

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

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

Tactic:
delta hilbertPoly

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

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

Tactic:
induction d with
| zero => simp only [add_zero]
| succ d _ =>
    simp only [← coeff_add]
    rw [← sum_def _ fun _ r => r • _]
    exact sum_add_index _ _ _ (fun _ => zero_smul ..) (fun _ _ _ => add_smul ..)

Result:
no goals

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

Tactic:
rw [← sum_def _ fun _ r => r • _]

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

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

Tactic:
simp only [add_zero]

Result:
no goals