[GOAL]
n : ℕ
⊢ hermite (n + 1) = X * hermite n - ↑derivative (hermite n)
[PROOFSTEP]
rw [hermite]
[GOAL]
n : ℕ
⊢ hermite n = (fun p => X * p - ↑derivative p)^[n] 1
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
⊢ hermite Nat.zero = (fun p => X * p - ↑derivative p)^[Nat.zero] 1
[PROOFSTEP]
rfl
[GOAL]
case succ
n : ℕ
ih : hermite n = (fun p => X * p - ↑derivative p)^[n] 1
⊢ hermite (Nat.succ n) = (fun p => X * p - ↑derivative p)^[Nat.succ n] 1
[PROOFSTEP]
rw [Function.iterate_succ_apply', ← ih, hermite_succ]
[GOAL]
⊢ hermite 1 = X
[PROOFSTEP]
rw [hermite_succ, hermite_zero]
[GOAL]
⊢ X * ↑C 1 - ↑derivative (↑C 1) = X
[PROOFSTEP]
simp only [map_one, mul_one, derivative_one, sub_zero]
[GOAL]
n : ℕ
⊢ coeff (hermite (n + 1)) 0 = -coeff (hermite n) 1
[PROOFSTEP]
simp [coeff_derivative]
[GOAL]
n k : ℕ
⊢ coeff (hermite (n + 1)) (k + 1) = coeff (hermite n) k - (↑k + 2) * coeff (hermite n) (k + 2)
[PROOFSTEP]
rw [hermite_succ, coeff_sub, coeff_X_mul, coeff_derivative, mul_comm]
[GOAL]
n k : ℕ
⊢ coeff (hermite n) k - (↑(k + 1) + 1) * coeff (hermite n) (k + 1 + 1) =
    coeff (hermite n) k - (↑k + 2) * coeff (hermite n) (k + 2)
[PROOFSTEP]
norm_cast
[GOAL]
n k : ℕ
hnk : n < k
⊢ coeff (hermite n) k = 0
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt hnk
[GOAL]
case intro
n k : ℕ
hnk : n < n + k + 1
⊢ coeff (hermite n) (n + k + 1) = 0
[PROOFSTEP]
clear hnk
[GOAL]
case intro
n k : ℕ
⊢ coeff (hermite n) (n + k + 1) = 0
[PROOFSTEP]
induction' n with n ih generalizing k
[GOAL]
case intro.zero
k✝ k : ℕ
⊢ coeff (hermite Nat.zero) (Nat.zero + k + 1) = 0
[PROOFSTEP]
apply coeff_C
[GOAL]
case intro.succ
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (hermite n) (n + k + 1) = 0
k : ℕ
⊢ coeff (hermite (Nat.succ n)) (Nat.succ n + k + 1) = 0
[PROOFSTEP]
have : n + k + 1 + 2 = n + (k + 2) + 1 := by ring
[GOAL]
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (hermite n) (n + k + 1) = 0
k : ℕ
⊢ n + k + 1 + 2 = n + (k + 2) + 1
[PROOFSTEP]
ring
[GOAL]
case intro.succ
k✝ n : ℕ
ih : ∀ (k : ℕ), coeff (hermite n) (n + k + 1) = 0
k : ℕ
this : n + k + 1 + 2 = n + (k + 2) + 1
⊢ coeff (hermite (Nat.succ n)) (Nat.succ n + k + 1) = 0
[PROOFSTEP]
rw [Nat.succ_eq_add_one, coeff_hermite_succ_succ, add_right_comm, this, ih k, ih (k + 2), mul_zero, sub_zero]
[GOAL]
n : ℕ
⊢ coeff (hermite n) n = 1
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
⊢ coeff (hermite Nat.zero) Nat.zero = 1
[PROOFSTEP]
apply coeff_C
[GOAL]
case succ
n : ℕ
ih : coeff (hermite n) n = 1
⊢ coeff (hermite (Nat.succ n)) (Nat.succ n) = 1
[PROOFSTEP]
rw [coeff_hermite_succ_succ, ih, coeff_hermite_of_lt, mul_zero, sub_zero]
[GOAL]
case succ
n : ℕ
ih : coeff (hermite n) n = 1
⊢ n < n + 2
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ degree (hermite n) = ↑n
[PROOFSTEP]
rw [degree_eq_of_le_of_coeff_ne_zero]
[GOAL]
case pn
n : ℕ
⊢ degree (hermite n) ≤ ↑n
case p1 n : ℕ ⊢ coeff (hermite n) n ≠ 0
[PROOFSTEP]
simp_rw [degree_le_iff_coeff_zero, Nat.cast_lt]
[GOAL]
case pn
n : ℕ
⊢ ∀ (m : ℕ), n < m → coeff (hermite n) m = 0
[PROOFSTEP]
rintro m hnm
[GOAL]
case pn
n m : ℕ
hnm : n < m
⊢ coeff (hermite n) m = 0
[PROOFSTEP]
exact coeff_hermite_of_lt hnm
[GOAL]
case p1
n : ℕ
⊢ coeff (hermite n) n ≠ 0
[PROOFSTEP]
simp [coeff_hermite_self n]
[GOAL]
n : ℕ
⊢ leadingCoeff (hermite n) = 1
[PROOFSTEP]
rw [← coeff_natDegree, natDegree_hermite, coeff_hermite_self]
[GOAL]
n k : ℕ
hnk : Odd (n + k)
⊢ coeff (hermite n) k = 0
[PROOFSTEP]
induction' n with n ih generalizing k
[GOAL]
case zero
n k✝ : ℕ
hnk✝ : Odd (n + k✝)
k : ℕ
hnk : Odd (Nat.zero + k)
⊢ coeff (hermite Nat.zero) k = 0
[PROOFSTEP]
rw [Nat.zero_eq, zero_add k] at hnk 
[GOAL]
case zero
n k✝ : ℕ
hnk✝ : Odd (n + k✝)
k : ℕ
hnk : Odd k
⊢ coeff (hermite Nat.zero) k = 0
[PROOFSTEP]
exact coeff_hermite_of_lt hnk.pos
[GOAL]
case succ
n✝ k✝ : ℕ
hnk✝ : Odd (n✝ + k✝)
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → coeff (hermite n) k = 0
k : ℕ
hnk : Odd (Nat.succ n + k)
⊢ coeff (hermite (Nat.succ n)) k = 0
[PROOFSTEP]
cases' k with k
[GOAL]
case succ.zero
n✝ k : ℕ
hnk✝ : Odd (n✝ + k)
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → coeff (hermite n) k = 0
hnk : Odd (Nat.succ n + Nat.zero)
⊢ coeff (hermite (Nat.succ n)) Nat.zero = 0
[PROOFSTEP]
rw [Nat.succ_add_eq_succ_add] at hnk 
[GOAL]
case succ.zero
n✝ k : ℕ
hnk✝ : Odd (n✝ + k)
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → coeff (hermite n) k = 0
hnk : Odd (n + Nat.succ Nat.zero)
⊢ coeff (hermite (Nat.succ n)) Nat.zero = 0
[PROOFSTEP]
rw [coeff_hermite_succ_zero, ih hnk, neg_zero]
[GOAL]
case succ.succ
n✝ k✝ : ℕ
hnk✝ : Odd (n✝ + k✝)
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → coeff (hermite n) k = 0
k : ℕ
hnk : Odd (Nat.succ n + Nat.succ k)
⊢ coeff (hermite (Nat.succ n)) (Nat.succ k) = 0
[PROOFSTEP]
rw [coeff_hermite_succ_succ, ih, ih, mul_zero, sub_zero]
[GOAL]
case succ.succ
n✝ k✝ : ℕ
hnk✝ : Odd (n✝ + k✝)
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → coeff (hermite n) k = 0
k : ℕ
hnk : Odd (Nat.succ n + Nat.succ k)
⊢ Odd (n + (k + 2))
[PROOFSTEP]
rwa [Nat.succ_add_eq_succ_add] at hnk 
[GOAL]
case succ.succ
n✝ k✝ : ℕ
hnk✝ : Odd (n✝ + k✝)
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → coeff (hermite n) k = 0
k : ℕ
hnk : Odd (Nat.succ n + Nat.succ k)
⊢ Odd (n + k)
[PROOFSTEP]
rw [(by rw [Nat.succ_add, Nat.add_succ] : n.succ + k.succ = n + k + 2)] at hnk 
[GOAL]
n✝ k✝ : ℕ
hnk✝ : Odd (n✝ + k✝)
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → coeff (hermite n) k = 0
k : ℕ
hnk : Odd (Nat.succ n + Nat.succ k)
⊢ Nat.succ n + Nat.succ k = n + k + 2
[PROOFSTEP]
rw [Nat.succ_add, Nat.add_succ]
[GOAL]
case succ.succ
n✝ k✝ : ℕ
hnk✝ : Odd (n✝ + k✝)
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → coeff (hermite n) k = 0
k : ℕ
hnk : Odd (n + k + 2)
⊢ Odd (n + k)
[PROOFSTEP]
exact (Nat.odd_add.mp hnk).mpr even_two
[GOAL]
x✝ : ℕ
⊢ coeff (hermite (2 * 0 + x✝)) x✝ = (-1) ^ 0 * ↑(2 * 0 - 1)‼ * ↑(Nat.choose (2 * 0 + x✝) x✝)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ coeff (hermite (2 * (n + 1) + 0)) 0 = (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + 0) 0)
[PROOFSTEP]
convert coeff_hermite_succ_zero (2 * n + 1) using 1
  -- porting note: ring_nf did not solve the goal on line 165
[GOAL]
case h.e'_3
n : ℕ
⊢ (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + 0) 0) = -coeff (hermite (2 * n + 1)) 1
[PROOFSTEP]
rw [coeff_hermite_explicit n 1, (by rw [Nat.left_distrib, mul_one, Nat.succ_sub_one] : 2 * (n + 1) - 1 = 2 * n + 1),
  Nat.doubleFactorial_add_one, Nat.choose_zero_right, Nat.choose_one_right, pow_succ]
[GOAL]
n : ℕ
⊢ 2 * (n + 1) - 1 = 2 * n + 1
[PROOFSTEP]
rw [Nat.left_distrib, mul_one, Nat.succ_sub_one]
[GOAL]
case h.e'_3
n : ℕ
⊢ -1 * (-1) ^ n * ↑((2 * n + 1) * (2 * n - 1)‼) * ↑1 = -((-1) ^ n * ↑(2 * n - 1)‼ * ↑(2 * n + 1))
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_3
n : ℕ
⊢ -1 * (-1) ^ n * ((2 * ↑n + 1) * ↑(2 * n - 1)‼) * 1 = -((-1) ^ n * ↑(2 * n - 1)‼ * (2 * ↑n + 1))
[PROOFSTEP]
ring
[GOAL]
n k : ℕ
⊢ coeff (hermite (2 * (n + 1) + (k + 1))) (k + 1) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + (k + 1)) (k + 1))
[PROOFSTEP]
let hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * (2 * n - 1)‼ * Nat.choose (2 * n + k) k
[GOAL]
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
⊢ coeff (hermite (2 * (n + 1) + (k + 1))) (k + 1) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + (k + 1)) (k + 1))
[PROOFSTEP]
have hermite_explicit_recur :
  ∀ n k : ℕ, hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (k + 2) * hermite_explicit n (k + 2) :=
  by
  intro n k
  simp only
    -- Factor out (-1)'s.
  rw [mul_comm (↑k + _ : ℤ), sub_eq_add_neg]
  nth_rw 3 [neg_eq_neg_one_mul]
  simp only [mul_assoc, ← mul_add, pow_succ]
  congr 2
    -- Factor out double factorials.
  norm_cast
    -- porting note: ring_nf did not solve the goal on line 186
  rw [(by rw [Nat.left_distrib, mul_one, Nat.succ_sub_one] : 2 * (n + 1) - 1 = 2 * n + 1), Nat.doubleFactorial_add_one,
    mul_comm (2 * n + 1)]
  simp only [mul_assoc, ← mul_add]
  congr 1
    -- Match up binomial coefficients using `Nat.choose_succ_right_eq`.
  rw [(by ring : 2 * (n + 1) + (k + 1) = 2 * n + 1 + (k + 1) + 1), (by ring : 2 * (n + 1) + k = 2 * n + 1 + (k + 1)),
    (by ring : 2 * n + (k + 2) = 2 * n + 1 + (k + 1))]
  rw [Nat.choose, Nat.choose_succ_right_eq (2 * n + 1 + (k + 1)) (k + 1), Nat.add_sub_cancel, Int.negSucc_eq]
    -- porting note: ring could not solve the goal so the lines 195, 198-200 were added.
  ring_nf
  simp only [sub_eq_add_neg, ← neg_mul, ← right_distrib _ _ ((-(1 : ℤ)) ^ n), ← neg_add]
  norm_cast
  simp only [← add_assoc, add_comm]
[GOAL]
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
⊢ ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
[PROOFSTEP]
intro n k
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
[PROOFSTEP]
simp only
  -- Factor out (-1)'s.
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + (k + 1)) (k + 1)) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + k) k) -
      (↑k + 2) * ((-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + (k + 2)) (k + 2)))
[PROOFSTEP]
rw [mul_comm (↑k + _ : ℤ), sub_eq_add_neg]
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + (k + 1)) (k + 1)) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + k) k) +
      -((-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + (k + 2)) (k + 2)) * (↑k + 2))
[PROOFSTEP]
nth_rw 3 [neg_eq_neg_one_mul]
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + (k + 1)) (k + 1)) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + k) k) +
      -((-1 * 1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + (k + 2)) (k + 2)) * (↑k + 2))
[PROOFSTEP]
simp only [mul_assoc, ← mul_add, pow_succ]
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ -1 * ((-1) ^ n * (↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + (k + 1)) (k + 1)))) =
    -1 * ((-1) ^ n * (↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + k) k))) +
      -((-1 * 1) ^ n * (↑(2 * n - 1)‼ * (↑(Nat.choose (2 * n + (k + 2)) (k + 2)) * (↑k + 2))))
[PROOFSTEP]
congr 2
  -- Factor out double factorials.
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ -1 * ((-1) ^ n * (↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + (k + 1)) (k + 1)))) =
    -1 * ((-1) ^ n * (↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + k) k))) +
      -((-1 * 1) ^ n * (↑(2 * n - 1)‼ * (↑(Nat.choose (2 * n + (k + 2)) (k + 2)) * (↑k + 2))))
[PROOFSTEP]
norm_cast
  -- porting note: ring_nf did not solve the goal on line 186
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * (n + 1) - 1)‼ * Nat.choose (2 * (n + 1) + (k + 1)) (k + 1))) =
    Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * (n + 1) - 1)‼ * Nat.choose (2 * (n + 1) + k) k)) +
      -((Int.negSucc 0 * 1) ^ n * ↑((2 * n - 1)‼ * (Nat.choose (2 * n + (k + 2)) (k + 2) * (k + 2))))
[PROOFSTEP]
rw [(by rw [Nat.left_distrib, mul_one, Nat.succ_sub_one] : 2 * (n + 1) - 1 = 2 * n + 1), Nat.doubleFactorial_add_one,
  mul_comm (2 * n + 1)]
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ 2 * (n + 1) - 1 = 2 * n + 1
[PROOFSTEP]
rw [Nat.left_distrib, mul_one, Nat.succ_sub_one]
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * n - 1)‼ * (2 * n + 1) * Nat.choose (2 * (n + 1) + (k + 1)) (k + 1))) =
    Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * n - 1)‼ * (2 * n + 1) * Nat.choose (2 * (n + 1) + k) k)) +
      -((Int.negSucc 0 * 1) ^ n * ↑((2 * n - 1)‼ * (Nat.choose (2 * n + (k + 2)) (k + 2) * (k + 2))))
[PROOFSTEP]
simp only [mul_assoc, ← mul_add]
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * n - 1)‼ * ((2 * n + 1) * Nat.choose (2 * (n + 1) + (k + 1)) (k + 1)))) =
    Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * n - 1)‼ * ((2 * n + 1) * Nat.choose (2 * (n + 1) + k) k))) +
      -((Int.negSucc 0 * 1) ^ n * ↑((2 * n - 1)‼ * (Nat.choose (2 * n + (k + 2)) (k + 2) * (k + 2))))
[PROOFSTEP]
congr 1
  -- Match up binomial coefficients using `Nat.choose_succ_right_eq`.
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * n - 1)‼ * ((2 * n + 1) * Nat.choose (2 * (n + 1) + (k + 1)) (k + 1)))) =
    Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * n - 1)‼ * ((2 * n + 1) * Nat.choose (2 * (n + 1) + k) k))) +
      -((Int.negSucc 0 * 1) ^ n * ↑((2 * n - 1)‼ * (Nat.choose (2 * n + (k + 2)) (k + 2) * (k + 2))))
[PROOFSTEP]
rw [(by ring : 2 * (n + 1) + (k + 1) = 2 * n + 1 + (k + 1) + 1), (by ring : 2 * (n + 1) + k = 2 * n + 1 + (k + 1)),
  (by ring : 2 * n + (k + 2) = 2 * n + 1 + (k + 1))]
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ 2 * (n + 1) + (k + 1) = 2 * n + 1 + (k + 1) + 1
[PROOFSTEP]
ring
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ 2 * (n + 1) + k = 2 * n + 1 + (k + 1)
[PROOFSTEP]
ring
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ 2 * n + (k + 2) = 2 * n + 1 + (k + 1)
[PROOFSTEP]
ring
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * n - 1)‼ * ((2 * n + 1) * Nat.choose (2 * n + 1 + (k + 1) + 1) (k + 1)))) =
    Int.negSucc 0 * (Int.negSucc 0 ^ n * ↑((2 * n - 1)‼ * ((2 * n + 1) * Nat.choose (2 * n + 1 + (k + 1)) k))) +
      -((Int.negSucc 0 * 1) ^ n * ↑((2 * n - 1)‼ * (Nat.choose (2 * n + 1 + (k + 1)) (k + 2) * (k + 2))))
[PROOFSTEP]
rw [Nat.choose, Nat.choose_succ_right_eq (2 * n + 1 + (k + 1)) (k + 1), Nat.add_sub_cancel, Int.negSucc_eq]
  -- porting note: ring could not solve the goal so the lines 195, 198-200 were added.
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ -(↑0 + 1) *
      ((-(↑0 + 1)) ^ n *
        ↑((2 * n - 1)‼ *
            ((2 * n + 1) * (Nat.choose (2 * n + 1 + (k + 1)) k + Nat.choose (2 * n + 1 + (k + 1)) (k + 1))))) =
    -(↑0 + 1) * ((-(↑0 + 1)) ^ n * ↑((2 * n - 1)‼ * ((2 * n + 1) * Nat.choose (2 * n + 1 + (k + 1)) k))) +
      -((-(↑0 + 1) * 1) ^ n * ↑((2 * n - 1)‼ * (Nat.choose (2 * n + 1 + (k + 1)) (k + 1) * (2 * n + 1))))
[PROOFSTEP]
ring_nf
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ -(↑(n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k * 2 + n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k) * 2 +
              (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k +
            (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k)) *
        (-1) ^ n) =
    -(↑(n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k * 2 + (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k) * (-1) ^ n) -
      ↑(n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k) * 2 + (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k)) *
        (-1) ^ n
[PROOFSTEP]
simp only [sub_eq_add_neg, ← neg_mul, ← right_distrib _ _ ((-(1 : ℤ)) ^ n), ← neg_add]
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ -↑(n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k * 2 + n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k) * 2 +
              (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k +
            (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k)) *
      (-1) ^ n =
    -(↑(n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k * 2 + (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k) +
          ↑(n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k) * 2 +
              (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k))) *
      (-1) ^ n
[PROOFSTEP]
norm_cast
[GOAL]
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
n k : ℕ
⊢ -↑(n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k * 2 + n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k) * 2 +
              (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k +
            (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k)) *
      Int.negSucc 0 ^ n =
    -↑(n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k * 2 + (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) k +
            (n * (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k) * 2 +
              (n * 2 - 1)‼ * Nat.choose (2 + n * 2 + k) (1 + k))) *
      Int.negSucc 0 ^ n
[PROOFSTEP]
simp only [← add_assoc, add_comm]
[GOAL]
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ coeff (hermite (2 * (n + 1) + (k + 1))) (k + 1) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑(Nat.choose (2 * (n + 1) + (k + 1)) (k + 1))
[PROOFSTEP]
change _ = hermite_explicit _ _
[GOAL]
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ coeff (hermite (2 * (n + 1) + (k + 1))) (k + 1) = hermite_explicit (n + 1) (k + 1)
[PROOFSTEP]
rw [← add_assoc, coeff_hermite_succ_succ, hermite_explicit_recur]
[GOAL]
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ coeff (hermite (2 * (n + 1) + k)) k - (↑k + 2) * coeff (hermite (2 * (n + 1) + k)) (k + 2) =
    hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
[PROOFSTEP]
congr
[GOAL]
case e_a
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ coeff (hermite (2 * (n + 1) + k)) k = hermite_explicit (n + 1) k
[PROOFSTEP]
rw [coeff_hermite_explicit (n + 1) k]
[GOAL]
case e_a.e_a
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ coeff (hermite (2 * (n + 1) + k)) (k + 2) = hermite_explicit n (k + 2)
[PROOFSTEP]
rw [(by ring : 2 * (n + 1) + k = 2 * n + (k + 2)), coeff_hermite_explicit n (k + 2)]
  -- porting note: Lean 3 worked this out automatically
[GOAL]
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑(Nat.choose (2 * n + k) k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ 2 * (n + 1) + k = 2 * n + (k + 2)
[PROOFSTEP]
ring
[GOAL]
n k : ℕ
hnk : Even (n + k)
⊢ coeff (hermite n) k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(Nat.choose n k)
[PROOFSTEP]
cases' le_or_lt k n with h_le h_lt
[GOAL]
case inl
n k : ℕ
hnk : Even (n + k)
h_le : k ≤ n
⊢ coeff (hermite n) k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(Nat.choose n k)
[PROOFSTEP]
rw [Nat.even_add, ← Nat.even_sub h_le] at hnk 
[GOAL]
case inl
n k : ℕ
hnk : Even (n - k)
h_le : k ≤ n
⊢ coeff (hermite n) k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(Nat.choose n k)
[PROOFSTEP]
obtain ⟨m, hm⟩ := hnk
[GOAL]
case inl.intro
n k : ℕ
h_le : k ≤ n
m : ℕ
hm : n - k = m + m
⊢ coeff (hermite n) k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(Nat.choose n k)
[PROOFSTEP]
rw [(by linarith [by rwa [Nat.sub_eq_iff_eq_add h_le] at hm ] : n = 2 * m + k), Nat.add_sub_cancel,
  Nat.mul_div_cancel_left _ (Nat.succ_pos 1), coeff_hermite_explicit]
[GOAL]
n k : ℕ
h_le : k ≤ n
m : ℕ
hm : n - k = m + m
⊢ n = 2 * m + k
[PROOFSTEP]
linarith [by rwa [Nat.sub_eq_iff_eq_add h_le] at hm ]
[GOAL]
n k : ℕ
h_le : k ≤ n
m : ℕ
hm : n - k = m + m
⊢ ?m.206711
[PROOFSTEP]
rwa [Nat.sub_eq_iff_eq_add h_le] at hm 
[GOAL]
case inr
n k : ℕ
hnk : Even (n + k)
h_lt : n < k
⊢ coeff (hermite n) k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(Nat.choose n k)
[PROOFSTEP]
simp [Nat.choose_eq_zero_of_lt h_lt, coeff_hermite_of_lt h_lt]
[GOAL]
n k : ℕ
⊢ coeff (hermite n) k = if Even (n + k) then (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(Nat.choose n k) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n k : ℕ
h : Even (n + k)
⊢ coeff (hermite n) k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(Nat.choose n k)
case neg n k : ℕ h : ¬Even (n + k) ⊢ coeff (hermite n) k = 0
[PROOFSTEP]
exact coeff_hermite_of_even_add h
[GOAL]
case neg
n k : ℕ
h : ¬Even (n + k)
⊢ coeff (hermite n) k = 0
[PROOFSTEP]
exact coeff_hermite_of_odd_add (Nat.odd_iff_not_even.mpr h)
