awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
this : n + k + 1 + 2 = n + (k + 2) + 1
succ : (hermite n).coeff (n + 1 + k) - HAdd.hAdd (α := ℤ) (↑(n + 1 + k) : ℤ) 2 * (hermite n).coeff (n + 1 + k + 2) = 0
⊢ (hermite (n + 1)).coeff (n + 1 + k + 1) = 0
have succ₁ : (hermite n).coeff (n + k + 1) - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * (hermite n).coeff (n + k + 1 + 2) = 0
Tactic: rw [coeff_hermite_succ_succ, add_right_comm, this, ih k, ih (k + 2), mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
this : n + k + 1 + 2 = n + (k + 2) + 1
succ : (hermite n).coeff (n + 1 + k) - HAdd.hAdd (α := ℤ) (↑(n + 1 + k) : ℤ) 2 * (hermite n).coeff (n + 1 + k + 2) = 0
succ₁ : (hermite n).coeff (n + k + 1) - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * (hermite n).coeff (n + k + 1 + 2) = 0
⊢ (hermite (n + 1)).coeff (n + 1 + k + 1) = 0
have succ₂ : (hermite n).coeff (n + k + 1) - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * (hermite n).coeff (n + (k + 2) + 1) = 0
Tactic: rw [coeff_hermite_succ_succ, add_right_comm, this, ih k, ih (k + 2), mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
this : n + k + 1 + 2 = n + (k + 2) + 1
succ : (hermite n).coeff (n + 1 + k) - HAdd.hAdd (α := ℤ) (↑(n + 1 + k) : ℤ) 2 * (hermite n).coeff (n + 1 + k + 2) = 0
succ₁ : (hermite n).coeff (n + k + 1) - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * (hermite n).coeff (n + k + 1 + 2) = 0
succ₂ :
  (hermite n).coeff (n + k + 1) - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * (hermite n).coeff (n + (k + 2) + 1) = 0
⊢ (hermite (n + 1)).coeff (n + 1 + k + 1) = 0
have succ₃ : 0 - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * (hermite n).coeff (n + (k + 2) + 1) = 0
Tactic: rw [coeff_hermite_succ_succ, add_right_comm, this, ih k, ih (k + 2), mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
this : n + k + 1 + 2 = n + (k + 2) + 1
succ : (hermite n).coeff (n + 1 + k) - HAdd.hAdd (α := ℤ) (↑(n + 1 + k) : ℤ) 2 * (hermite n).coeff (n + 1 + k + 2) = 0
succ₁ : (hermite n).coeff (n + k + 1) - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * (hermite n).coeff (n + k + 1 + 2) = 0
succ₂ :
  (hermite n).coeff (n + k + 1) - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * (hermite n).coeff (n + (k + 2) + 1) = 0
succ₃ : 0 - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * (hermite n).coeff (n + (k + 2) + 1) = 0
⊢ (hermite (n + 1)).coeff (n + 1 + k + 1) = 0
have succ₄ : 0 - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * 0 = 0
Tactic: rw [coeff_hermite_succ_succ, add_right_comm, this, ih k, ih (k + 2), mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
this : n + k + 1 + 2 = n + (k + 2) + 1
succ : (hermite n).coeff (n + 1 + k) - HAdd.hAdd (α := ℤ) (↑(n + 1 + k) : ℤ) 2 * (hermite n).coeff (n + 1 + k + 2) = 0
succ₁ : (hermite n).coeff (n + k + 1) - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * (hermite n).coeff (n + k + 1 + 2) = 0
succ₂ :
  (hermite n).coeff (n + k + 1) - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * (hermite n).coeff (n + (k + 2) + 1) = 0
succ₃ : 0 - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * (hermite n).coeff (n + (k + 2) + 1) = 0
succ₄ : 0 - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * 0 = 0
⊢ (hermite (n + 1)).coeff (n + 1 + k + 1) = 0
have succ₅ : HSub.hSub (α := ℤ) 0 0 = 0
Tactic: rw [coeff_hermite_succ_succ, add_right_comm, this, ih k, ih (k + 2), mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
this : n + k + 1 + 2 = n + (k + 2) + 1
succ : (hermite n).coeff (n + 1 + k) - HAdd.hAdd (α := ℤ) (↑(n + 1 + k) : ℤ) 2 * (hermite n).coeff (n + 1 + k + 2) = 0
succ₁ : (hermite n).coeff (n + k + 1) - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * (hermite n).coeff (n + k + 1 + 2) = 0
succ₂ :
  (hermite n).coeff (n + k + 1) - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * (hermite n).coeff (n + (k + 2) + 1) = 0
succ₃ : 0 - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * (hermite n).coeff (n + (k + 2) + 1) = 0
succ₄ : 0 - HAdd.hAdd (α := ℤ) (↑(n + k + 1) : ℤ) 2 * 0 = 0
succ₅ : HSub.hSub (α := ℤ) 0 0 = 0
⊢ (hermite (n + 1)).coeff (n + 1 + k + 1) = 0
have succ₆ : Eq (α := ℤ) 0 0
Tactic: rw [coeff_hermite_succ_succ, add_right_comm, this, ih k, ih (k + 2), mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n k : ℕ
⊢ (hermite n).coeff (n + k + 1) = 0
have zero : ∀ (k : ℕ), (hermite 0).coeff (0 + k + 1) = 0
Tactic: induction n generalizing k with
  | zero => exact coeff_C
  | succ n ih =>
    have : n + k + 1 + 2 = n + (k + 2) + 1 := by ring
    rw [coeff_hermite_succ_succ, add_right_comm, this, ih k, ih (k + 2), mul_zero, sub_zero]
Cleared hypotheses: n, k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n k : ℕ
zero : ∀ (k : ℕ), (hermite 0).coeff (0 + k + 1) = 0
⊢ (hermite n).coeff (n + k + 1) = 0
have succ : ∀ (n : ℕ) (ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0) (k : ℕ), (hermite (n + 1)).coeff (n + 1 + k + 1) = 0
Tactic: induction n generalizing k with
  | zero => exact coeff_C
  | succ n ih =>
    have : n + k + 1 + 2 = n + (k + 2) + 1 := by ring
    rw [coeff_hermite_succ_succ, add_right_comm, this, ih k, ih (k + 2), mul_zero, sub_zero]
Cleared hypotheses: n, k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : (hermite n).coeff n = 1
⊢ (hermite (n + 1)).coeff (n + 1) = 1
have succ : n < n + 2
Tactic: rw [coeff_hermite_succ_succ, ih, coeff_hermite_of_lt, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
⊢ (hermite n).coeff n = 1
have zero : (hermite 0).coeff 0 = 1
Tactic: induction n with
  | zero => exact coeff_C
  | succ n ih =>
    rw [coeff_hermite_succ_succ, ih, coeff_hermite_of_lt, mul_zero, sub_zero]
    simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
zero : (hermite 0).coeff 0 = 1
⊢ (hermite n).coeff n = 1
have succ : ∀ (n : ℕ) (ih : (hermite n).coeff n = 1), (hermite (n + 1)).coeff (n + 1) = 1
Tactic: induction n with
  | zero => exact coeff_C
  | succ n ih =>
    rw [coeff_hermite_succ_succ, ih, coeff_hermite_of_lt, mul_zero, sub_zero]
    simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
⊢ (hermite n).degree = (↑n : WithBot ℕ)
have pn : (hermite n).degree ≤ (↑n : WithBot ℕ)
Tactic: rw [degree_eq_of_le_of_coeff_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
pn : (hermite n).degree ≤ (↑n : WithBot ℕ)
⊢ (hermite n).degree = (↑n : WithBot ℕ)
have p1 : (hermite n).coeff n ≠ 0
Tactic: rw [degree_eq_of_le_of_coeff_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
⊢ (hermite n).degree ≤ (↑n : WithBot ℕ)
have pn : ∀ (m : ℕ), n < m → (hermite n).coeff m = 0
Tactic: simp_rw [degree_le_iff_coeff_zero, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
⊢ (hermite n).leadingCoeff = 1
have rw : (hermite n).coeff (hermite n).natDegree = 1
Tactic: rw [← coeff_natDegree, natDegree_hermite, coeff_hermite_self]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
rw : (hermite n).coeff (hermite n).natDegree = 1
⊢ (hermite n).leadingCoeff = 1
have rw₁ : (hermite n).coeff n = 1
Tactic: rw [← coeff_natDegree, natDegree_hermite, coeff_hermite_self]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
rw : (hermite n).coeff (hermite n).natDegree = 1
rw₁ : (hermite n).coeff n = 1
⊢ (hermite n).leadingCoeff = 1
have rw₂ : Eq (α := ℤ) 1 1
Tactic: rw [← coeff_natDegree, natDegree_hermite, coeff_hermite_self]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (hypothesis)
Goal:
k : ℕ
hnk : Odd (0 + k)
⊢ (hermite 0).coeff k = 0
have hnk₁ : Odd k
Tactic: rw [zero_add k] at hnk
Cleared hypotheses: hnk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0
hnk : Odd (n + Nat.succ 0)
⊢ (hermite (n + 1)).coeff 0 = 0
have succ : -(hermite n).coeff 1 = 0
Tactic: rw [coeff_hermite_succ_zero, ih hnk, neg_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0
hnk : Odd (n + Nat.succ 0)
succ : -(hermite n).coeff 1 = 0
⊢ (hermite (n + 1)).coeff 0 = 0
have succ₁ : Eq (α := ℤ) (-0) 0
Tactic: rw [coeff_hermite_succ_zero, ih hnk, neg_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0
hnk : Odd (n + Nat.succ 0)
succ : -(hermite n).coeff 1 = 0
succ₁ : Eq (α := ℤ) (-0) 0
⊢ (hermite (n + 1)).coeff 0 = 0
have succ₂ : Eq (α := ℤ) 0 0
Tactic: rw [coeff_hermite_succ_zero, ih hnk, neg_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ (hermite (n + 1)).coeff (k + 1) = 0
have succ : Odd (n + (k + 2))
Tactic: rw [coeff_hermite_succ_succ, ih, ih, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
succ : Odd (n + (k + 2))
⊢ (hermite (n + 1)).coeff (k + 1) = 0
have succ₁ : Odd (n + k)
Tactic: rw [coeff_hermite_succ_succ, ih, ih, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ Odd (n + (k + 2))
have succ : ∀ (hnk : Odd (n + (k + 1).succ)), Odd (n + (k + 2))
Tactic: rwa [Nat.succ_add_eq_add_succ] at hnk
Cleared hypotheses: hnk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ n.succ + k.succ = n + k + 2
have rw : (n + k.succ).succ = n + k + 2
Tactic: rw [Nat.succ_add, Nat.add_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
rw : (n + k.succ).succ = n + k + 2
⊢ n.succ + k.succ = n + k + 2
have rw₁ : (n + k).succ.succ = n + k + 2
Tactic: rw [Nat.succ_add, Nat.add_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (hypothesis)
Goal:
n : ℕ
ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ Odd (n + k)
have hnk₁ : Odd (n + k + 2)
Tactic: rw [(by rw [Nat.succ_add, Nat.add_succ] : n.succ + k.succ = n + k + 2)] at hnk
Cleared hypotheses: hnk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + k)
⊢ (hermite (n + 1)).coeff k = 0
have succ : ∀ (hnk : Odd (n + 1 + 0)), (hermite (n + 1)).coeff 0 = 0
Tactic: cases k with
    | zero =>
      rw [Nat.succ_add_eq_add_succ] at hnk
      rw [coeff_hermite_succ_zero, ih hnk, neg_zero]
    | succ k =>
      rw [coeff_hermite_succ_succ, ih, ih, mul_zero, sub_zero]
      · rwa [Nat.succ_add_eq_add_succ] at hnk
      · rw [(by rw [Nat.succ_add, Nat.add_succ] : n.succ + k.succ = n + k + 2)] at hnk
        exact (Nat.odd_add.mp hnk).mpr even_two
Cleared hypotheses: k, hnk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + k)
succ : ∀ (hnk : Odd (n + 1 + 0)), (hermite (n + 1)).coeff 0 = 0
⊢ (hermite (n + 1)).coeff k = 0
have succ₁ : ∀ (k : ℕ) (hnk : Odd (n + 1 + (k + 1))), (hermite (n + 1)).coeff (k + 1) = 0
Tactic: cases k with
    | zero =>
      rw [Nat.succ_add_eq_add_succ] at hnk
      rw [coeff_hermite_succ_zero, ih hnk, neg_zero]
    | succ k =>
      rw [coeff_hermite_succ_succ, ih, ih, mul_zero, sub_zero]
      · rwa [Nat.succ_add_eq_add_succ] at hnk
      · rw [(by rw [Nat.succ_add, Nat.add_succ] : n.succ + k.succ = n + k + 2)] at hnk
        exact (Nat.odd_add.mp hnk).mpr even_two
Cleared hypotheses: k, hnk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n k : ℕ
hnk : Odd (n + k)
⊢ (hermite n).coeff k = 0
have zero : ∀ {k : ℕ} (hnk : Odd (0 + k)), (hermite 0).coeff k = 0
Tactic: induction n generalizing k with
  | zero =>
    rw [zero_add k] at hnk
    exact coeff_hermite_of_lt hnk.pos
  | succ n ih =>
    cases k with
    | zero =>
      rw [Nat.succ_add_eq_add_succ] at hnk
      rw [coeff_hermite_succ_zero, ih hnk, neg_zero]
    | succ k =>
      rw [coeff_hermite_succ_succ, ih, ih, mul_zero, sub_zero]
      · rwa [Nat.succ_add_eq_add_succ] at hnk
      · rw [(by rw [Nat.succ_add, Nat.add_succ] : n.succ + k.succ = n + k + 2)] at hnk
        exact (Nat.odd_add.mp hnk).mpr even_two
Cleared hypotheses: n, k, hnk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n k : ℕ
hnk : Odd (n + k)
zero : ∀ {k : ℕ} (hnk : Odd (0 + k)), (hermite 0).coeff k = 0
⊢ (hermite n).coeff k = 0
have succ : ∀ (n : ℕ) (ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0) {k : ℕ} (hnk : Odd (n + 1 + k)),
  (hermite (n + 1)).coeff k = 0
Tactic: induction n generalizing k with
  | zero =>
    rw [zero_add k] at hnk
    exact coeff_hermite_of_lt hnk.pos
  | succ n ih =>
    cases k with
    | zero =>
      rw [Nat.succ_add_eq_add_succ] at hnk
      rw [coeff_hermite_succ_zero, ih hnk, neg_zero]
    | succ k =>
      rw [coeff_hermite_succ_succ, ih, ih, mul_zero, sub_zero]
      · rwa [Nat.succ_add_eq_add_succ] at hnk
      · rw [(by rw [Nat.succ_add, Nat.add_succ] : n.succ + k.succ = n + k + 2)] at hnk
        exact (Nat.odd_add.mp hnk).mpr even_two
Cleared hypotheses: n, k, hnk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
⊢ (hermite (2 * (n + 1) + 0)).coeff 0 =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + 0).choose 0) : ℤ)
have h : HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + 0).choose 0) : ℤ) =
  -(hermite (2 * n + 1)).coeff 1
Tactic: convert! coeff_hermite_succ_zero (2 * n + 1) using 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
⊢ HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + 0).choose 0) : ℤ) =
    -(hermite (2 * n + 1)).coeff 1
have h : HPow.hPow (α := ℤ) (-1) n * -1 * (↑((2 * n + 1) * (2 * n - 1)‼) : ℤ) * (↑1 : ℤ) =
  -(HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑(2 * n + 1) : ℤ))
Tactic: rw [coeff_hermite_explicit n 1, (by grind : 2 * (n + 1) - 1 = 2 * n + 1),
      Nat.doubleFactorial_add_one, Nat.choose_zero_right,
      Nat.choose_one_right, pow_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
⊢ HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + k).choose k) : ℤ) -
      HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 *
        (HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + (k + 2)).choose (k + 2)) : ℤ))
have rw : HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ) =
  HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + k).choose k) : ℤ) +
    -(HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) *
        HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)
Tactic: rw [mul_comm (↑k + _ : ℤ), sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
⊢ HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + k).choose k) : ℤ) +
      -(HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) *
          HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)
have nth_rw : HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ) =
  HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + k).choose k) : ℤ) +
    -1 *
      (HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) *
        HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)
Tactic: nth_rw 3 [neg_eq_neg_one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
⊢ HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + k).choose k) : ℤ) +
      -1 *
        (HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) *
          HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)
have simp : -1 *
    (HPow.hPow (α := ℤ) (-1) n *
      HMul.hMul (α := ℤ) (↑(2 * (n + 1) - 1)‼ : ℤ) (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ)) =
  -1 *
    (HPow.hPow (α := ℤ) (-1) n *
      (HMul.hMul (α := ℤ) (↑(2 * (n + 1) - 1)‼ : ℤ) (↑((2 * (n + 1) + k).choose k) : ℤ) +
        (↑(2 * n - 1)‼ : ℤ) * ((↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) * HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)))
Tactic: simp only [mul_assoc, ← mul_add, pow_succ']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
⊢ -1 *
      (HPow.hPow (α := ℤ) (-1) n *
        HMul.hMul (α := ℤ) (↑(2 * (n + 1) - 1)‼ : ℤ) (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ)) =
    -1 *
      (HPow.hPow (α := ℤ) (-1) n *
        (HMul.hMul (α := ℤ) (↑(2 * (n + 1) - 1)‼ : ℤ) (↑((2 * (n + 1) + k).choose k) : ℤ) +
          (↑(2 * n - 1)‼ : ℤ) * ((↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) * HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)))
have e_a : HMul.hMul (α := ℤ) (↑(2 * (n + 1) - 1)‼ : ℤ) (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ) =
  HMul.hMul (α := ℤ) (↑(2 * (n + 1) - 1)‼ : ℤ) (↑((2 * (n + 1) + k).choose k) : ℤ) +
    (↑(2 * n - 1)‼ : ℤ) * ((↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) * HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
⊢ HMul.hMul (α := ℤ) (↑(2 * (n + 1) - 1)‼ : ℤ) (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ) =
    HMul.hMul (α := ℤ) (↑(2 * (n + 1) - 1)‼ : ℤ) (↑((2 * (n + 1) + k).choose k) : ℤ) +
      (↑(2 * n - 1)‼ : ℤ) * ((↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) * HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)
have e_a : (2 * (n + 1) - 1)‼ * (2 * (n + 1) + (k + 1)).choose (k + 1) =
  (2 * (n + 1) - 1)‼ * (2 * (n + 1) + k).choose k + (2 * n - 1)‼ * ((2 * n + (k + 2)).choose (k + 2) * (k + 2))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
⊢ (2 * (n + 1) - 1)‼ * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * (n + 1) - 1)‼ * (2 * (n + 1) + k).choose k + (2 * n - 1)‼ * ((2 * n + (k + 2)).choose (k + 2) * (k + 2))
have e_a : (2 * n - 1)‼ * (2 * n + 1) * (2 * (n + 1) + (k + 1)).choose (k + 1) =
  (2 * n - 1)‼ * (2 * n + 1) * (2 * (n + 1) + k).choose k + (2 * n - 1)‼ * ((2 * n + (k + 2)).choose (k + 2) * (k + 2))
Tactic: rw [(by grind : 2 * (n + 1) - 1 = 2 * n + 1),
        Nat.doubleFactorial_add_one, mul_comm (2 * n + 1)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
⊢ (2 * n - 1)‼ * (2 * n + 1) * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * n - 1)‼ * (2 * n + 1) * (2 * (n + 1) + k).choose k +
      (2 * n - 1)‼ * ((2 * n + (k + 2)).choose (k + 2) * (k + 2))
have e_a : (2 * n - 1)‼ * ((2 * n + 1) * (2 * (n + 1) + (k + 1)).choose (k + 1)) =
  (2 * n - 1)‼ * ((2 * n + 1) * (2 * (n + 1) + k).choose k + (2 * n + (k + 2)).choose (k + 2) * (k + 2))
Tactic: simp only [mul_assoc, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
⊢ (2 * n - 1)‼ * ((2 * n + 1) * (2 * (n + 1) + (k + 1)).choose (k + 1)) =
    (2 * n - 1)‼ * ((2 * n + 1) * (2 * (n + 1) + k).choose k + (2 * n + (k + 2)).choose (k + 2) * (k + 2))
have e_a : (2 * n + 1) * (2 * (n + 1) + (k + 1)).choose (k + 1) =
  (2 * n + 1) * (2 * (n + 1) + k).choose k + (2 * n + (k + 2)).choose (k + 2) * (k + 2)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
⊢ (2 * n + 1) * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * n + 1) * (2 * (n + 1) + k).choose k + (2 * n + (k + 2)).choose (k + 2) * (k + 2)
have e_a : (2 * n + 1) * (2 * n + 1 + (k + 1) + 1).choose (k + 1) =
  (2 * n + 1) * (2 * n + 1 + (k + 1)).choose k + (2 * n + 1 + (k + 1)).choose (k + 2) * (k + 2)
Tactic: 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))]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
⊢ (2 * n + 1) * (2 * n + 1 + (k + 1) + 1).choose (k + 1) =
    (2 * n + 1) * (2 * n + 1 + (k + 1)).choose k + (2 * n + 1 + (k + 1)).choose (k + 2) * (k + 2)
have e_a : (2 * n + 1) * ((2 * n + 1 + (k + 1)).choose k + (2 * n + 1 + (k + 1)).choose (k + 1)) =
  (2 * n + 1) * (2 * n + 1 + (k + 1)).choose k + (2 * n + 1 + (k + 1)).choose (k + 1) * (2 * n + 1)
Tactic: rw [Nat.choose, Nat.choose_succ_right_eq (2 * n + 1 + (k + 1)) (k + 1), Nat.add_sub_cancel]