awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this_2 : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
h : i < x
rw rw₁ :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x))
⊢ gaussNorm v c p * HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x))

Tactic:
rw [hi_p]
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this_2 : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
h : i < x
hbc :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)

Tactic:
gcongr 1
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this_2 : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
h : i < x
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
c_1 : ℝ
R_1 : Type u_3
inst : Ring R_1
v_1 : AbsoluteValue R_1 ℝ
c : ℝ
R : Type u_3
inst_1 : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hlt_p : ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
hlt_q : ∀ j_1 < j, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j_1) : ℝ) (c ^ j_1) < gaussNorm v c q
hvpq : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
this_1 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
this_2 : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
h : i < x
v₁ :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) ≤
    gaussNorm v c p * HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x))
v₂ :
  gaussNorm v c p * HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x))
v₃ :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)

Tactic:
calc
    v (p.coeff x) * c ^ x * (v (q.coeff (i + j - x)) * c ^ (i + j - x))
    _ ≤ gaussNorm v c p * (v (q.coeff (i + j - x)) * c ^ (i + j - x)) := by
        gcongr
        exact p.le_gaussNorm v hc0 x
    _ = v (p.coeff i) * c ^ i * (v (q.coeff (i + j - x)) * c ^ (i + j - x)) := by
        rw [hi_p]
    _ < v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j) := by
        gcongr 1
        grind

Premises used: HMul.hMul, HSub.hSub, Polynomial.coeff, HPow.hPow, HAdd.hAdd, DFunLike.coe, Polynomial.gaussNorm
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
c : ℝ
R : Type u_3
inst : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
⊢ gaussNorm v c (p * q) = gaussNorm v c p * gaussNorm v c q

Tactic:
le_antisymm (gaussNorm_mul_le v hna p q (le_of_lt hc))
  <| mul_gaussNorm_le_gaussNorm_mul hna hc p q

Premises used: le_of_lt, _private.0.Polynomial.mul_gaussNorm_le_gaussNorm_mul, le_antisymm, Polynomial.gaussNorm_mul_le
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
c : ℝ
R : Type u_3
inst : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
⊢ gaussNorm v c (p + q) ≤ gaussNorm v c p + gaussNorm v c q

Tactic:
grind [isNonarchimedean_gaussNorm v hna (le_of_lt hc) p q, gaussNorm_nonneg]

Premises used: Polynomial.isNonarchimedean_gaussNorm, le_of_lt, Polynomial.gaussNorm_nonneg
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
r : R
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
⊢ gaussNorm.{u_1} (R := R) (⇑v : (a : R) → ℝ) c ((C : (a : R) → R⟦X⟧) r) = (v : (a : R) → ℝ) r

Tactic:
simp [← Polynomial.coe_C, hc]

Premises used: Polynomial.coe_C
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
c : ℝ
r : R
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
n : ℕ
⊢ gaussNorm.{u_1} (R := R) (⇑v : (a : R) → ℝ) c ((monomial n : (a : R) → R⟦X⟧) r) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) r : ℝ) (c ^ n)

Tactic:
simp [← Polynomial.coe_monomial, hc]

Premises used: Polynomial.coe_monomial
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
rw rw₁ :
  HSub.hSub (β := ℤ[X]) (X * hermite n) ((derivative : (a : ℤ[X]) → ℤ[X]) (hermite n) : ℤ[X]) =
    HSub.hSub (β := ℤ[X]) (X * hermite n) ((derivative : (a : ℤ[X]) → ℤ[X]) (hermite n) : ℤ[X])
⊢ hermite (n + 1) = HSub.hSub (β := ℤ[X]) (X * hermite n) ((derivative : (a : ℤ[X]) → ℤ[X]) (hermite n) : ℤ[X])

Tactic:
rw [hermite]

Premises used: Polynomial.hermite
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
⊢ hermite 0 = (fun (p : ℤ[X]) ↦ HSub.hSub (β := ℤ[X]) (X * p) ((derivative : (a : ℤ[X]) → ℤ[X]) p : ℤ[X]))^[0] 1

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
ih : hermite n = (fun (p : ℤ[X]) ↦ HSub.hSub (β := ℤ[X]) (X * p) ((derivative : (a : ℤ[X]) → ℤ[X]) p : ℤ[X]))^[n] 1
succ :
  hermite (n + 1) =
    HMul.hMul (α := ℤ[X]) X
        ((fun (p : ℤ[X]) ↦ HSub.hSub (β := ℤ[X]) (X * p) ((derivative : (a : ℤ[X]) → ℤ[X]) p : ℤ[X]))^[n] 1) -
      (derivative : (a : ℤ[X]) → ℤ[X])
        ((fun (p : ℤ[X]) ↦ HSub.hSub (β := ℤ[X]) (X * p) ((derivative : (a : ℤ[X]) → ℤ[X]) p : ℤ[X]))^[n] 1)
succ₁ : hermite (n + 1) = HSub.hSub (β := ℤ[X]) (X * hermite n) ((derivative : (a : ℤ[X]) → ℤ[X]) (hermite n) : ℤ[X])
succ₂ succ₃ :
  HSub.hSub (β := ℤ[X]) (X * hermite n) ((derivative : (a : ℤ[X]) → ℤ[X]) (hermite n) : ℤ[X]) =
    HSub.hSub (β := ℤ[X]) (X * hermite n) ((derivative : (a : ℤ[X]) → ℤ[X]) (hermite n) : ℤ[X])
⊢ hermite (n + 1) =
    (fun (p : ℤ[X]) ↦ HSub.hSub (β := ℤ[X]) (X * p) ((derivative : (a : ℤ[X]) → ℤ[X]) p : ℤ[X]))^[n + 1] 1

Tactic:
rw [Function.iterate_succ_apply', ← ih, hermite_succ]

Premises used: Function.iterate_succ_apply', Polynomial.hermite_succ
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
zero : hermite 0 = (fun (p : ℤ[X]) ↦ HSub.hSub (β := ℤ[X]) (X * p) ((derivative : (a : ℤ[X]) → ℤ[X]) p : ℤ[X]))^[0] 1
succ :
  ∀ (n : ℕ)
    (ih :
      hermite n = (fun (p : ℤ[X]) ↦ HSub.hSub (β := ℤ[X]) (X * p) ((derivative : (a : ℤ[X]) → ℤ[X]) p : ℤ[X]))^[n] 1),
    hermite (n + 1) =
      (fun (p : ℤ[X]) ↦ HSub.hSub (β := ℤ[X]) (X * p) ((derivative : (a : ℤ[X]) → ℤ[X]) p : ℤ[X]))^[n + 1] 1
⊢ hermite n = (fun (p : ℤ[X]) ↦ HSub.hSub (β := ℤ[X]) (X * p) ((derivative : (a : ℤ[X]) → ℤ[X]) p : ℤ[X]))^[n] 1

Tactic:
induction n with
  | zero => rfl
  | succ n ih => rw [Function.iterate_succ_apply', ← ih, hermite_succ]

Premises used: Function.iterate_succ_apply', Polynomial.hermite_succ
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
⊢ hermite 0 = (C : (a : ℤ) → ℤ[X]) 1

Tactic:
rfl

Premises used: Polynomial.hermite, rfl
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
⊢ HSub.hSub (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))
      ((derivative : (a : ℤ[X]) → ℤ[X]) ((C : (a : ℤ) → ℤ[X]) 1) : ℤ[X]) =
    X

Tactic:
simp only [map_one, mul_one, derivative_one, sub_zero]

Premises used: sub_zero, map_one, mul_one, Polynomial.derivative_one
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
⊢ (hermite (n + 1)).coeff 0 = -(hermite n).coeff 1

Tactic:
simp [coeff_derivative]

Premises used: Polynomial.coeff_derivative
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
rw :
  (hermite n).coeff k - HAdd.hAdd (α := ℤ) (↑(k + 1) : ℤ) 1 * (hermite n).coeff (k + 1 + 1) =
    (hermite n).coeff k - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 * (hermite n).coeff (k + 2)
⊢ (hermite (n + 1)).coeff (k + 1) = (hermite n).coeff k - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 * (hermite n).coeff (k + 2)

Tactic:
rw [hermite_succ, coeff_sub, coeff_X_mul, coeff_derivative, mul_comm]

Premises used: Polynomial.coeff_derivative, Polynomial.hermite_succ, Polynomial.coeff_sub, mul_comm, Polynomial.coeff_X_mul
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  (hermite n).coeff k - (↑(k + 1 + 1) : ℤ) * (hermite n).coeff (k + 1 + 1) =
    (hermite n).coeff k - (↑(k + 2) : ℤ) * (hermite n).coeff (k + 2)
⊢ (hermite n).coeff k - HAdd.hAdd (α := ℤ) (↑(k + 1) : ℤ) 1 * (hermite n).coeff (k + 1 + 1) =
    (hermite n).coeff k - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 * (hermite n).coeff (k + 2)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
hnk : n < k
obtain : ∀ (k : ℕ) (hnk : n < n + k + 1), (hermite n).coeff (n + k + 1) = 0
⊢ (hermite n).coeff k = 0

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt hnk

Premises used: Nat.exists_eq_add_of_lt, rfl
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
k : ℕ
⊢ (hermite 0).coeff (0 + k + 1) = 0

Tactic:
coeff_C

Premises used: Polynomial.coeff_C, Polynomial.hermite, ite
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
k : ℕ
⊢ (hermite 0).coeff (0 + k + 1) = 0

Tactic:
exact coeff_C

Premises used: Polynomial.coeff_C
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
⊢ n + k + 1 + 2 = n + (k + 2) + 1

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
⊢ n + k + 1 + 2 = n + (k + 2) + 1

Tactic:
have : n + k + 1 + 2 = n + (k + 2) + 1 := by ring
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
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
succ₆ succ₇ : Eq (α := ℤ) 0 0
⊢ (hermite (n + 1)).coeff (n + 1 + k + 1) = 0

Tactic:
rw [coeff_hermite_succ_succ, add_right_comm, this, ih k, ih (k + 2), mul_zero, sub_zero]

Premises used: Polynomial.coeff_hermite_succ_succ, sub_zero, add_right_comm, MulZeroClass.mul_zero, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
zero : ∀ (k : ℕ), (hermite 0).coeff (0 + k + 1) = 0
succ :
  ∀ (n : ℕ) (ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0) (k : ℕ), (hermite (n + 1)).coeff (n + 1 + k + 1) = 0
⊢ (hermite n).coeff (n + 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]

Premises used: Polynomial.coeff_hermite_succ_succ, sub_zero, add_right_comm, Polynomial.coeff_C, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
⊢ (hermite 0).coeff 0 = 1

Tactic:
coeff_C

Premises used: Polynomial.coeff_C, Polynomial.hermite, ite
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
⊢ (hermite 0).coeff 0 = 1

Tactic:
exact coeff_C

Premises used: Polynomial.coeff_C
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
ih : (hermite n).coeff n = 1
succ : n < n + 2
⊢ (hermite (n + 1)).coeff (n + 1) = 1

Tactic:
rw [coeff_hermite_succ_succ, ih, coeff_hermite_of_lt, mul_zero, sub_zero]

Premises used: Polynomial.coeff_hermite_succ_succ, sub_zero, MulZeroClass.mul_zero, Polynomial.coeff_hermite_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
ih : (hermite n).coeff n = 1
⊢ n < n + 2

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
zero : (hermite 0).coeff 0 = 1
succ : ∀ (n : ℕ) (ih : (hermite n).coeff n = 1), (hermite (n + 1)).coeff (n + 1) = 1
⊢ (hermite n).coeff n = 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

Premises used: Polynomial.coeff_hermite_succ_succ, sub_zero, Polynomial.coeff_C, MulZeroClass.mul_zero, Polynomial.coeff_hermite_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
pn : (hermite n).degree ≤ (↑n : WithBot ℕ)
p1 : (hermite n).coeff n ≠ 0
⊢ (hermite n).degree = (↑n : WithBot ℕ)

Tactic:
rw [degree_eq_of_le_of_coeff_ne_zero]

Premises used: Polynomial.degree_eq_of_le_of_coeff_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
pn : ∀ (m : ℕ), n < m → (hermite n).coeff m = 0
⊢ (hermite n).degree ≤ (↑n : WithBot ℕ)

Tactic:
simp_rw [degree_le_iff_coeff_zero, Nat.cast_lt]

Premises used: Polynomial.degree_le_iff_coeff_zero, Nat.cast_lt
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n m : ℕ
hnm : n < m
⊢ (hermite n).coeff m = 0

Tactic:
coeff_hermite_of_lt hnm

Premises used: Polynomial.coeff_hermite_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n m : ℕ
hnm : n < m
⊢ (hermite n).coeff m = 0

Tactic:
exact coeff_hermite_of_lt hnm

Premises used: Polynomial.coeff_hermite_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
⊢ (hermite n).coeff n ≠ 0

Tactic:
simp [coeff_hermite_self n]

Premises used: Polynomial.coeff_hermite_self
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
⊢ (hermite n).natDegree = n

Tactic:
natDegree_eq_of_degree_eq_some (degree_hermite n)

Premises used: Polynomial.degree_hermite, Polynomial.natDegree_eq_of_degree_eq_some
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
rw : (hermite n).coeff (hermite n).natDegree = 1
rw₁ : (hermite n).coeff n = 1
rw₂ rw₃ : Eq (α := ℤ) 1 1
⊢ (hermite n).leadingCoeff = 1

Tactic:
rw [← coeff_natDegree, natDegree_hermite, coeff_hermite_self]

Premises used: Polynomial.natDegree_hermite, Polynomial.coeff_natDegree, Polynomial.coeff_hermite_self
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
⊢ (hermite n).Monic

Tactic:
leadingCoeff_hermite n

Premises used: Polynomial.leadingCoeff_hermite, Polynomial.Monic
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
k : ℕ
hnk : Odd (0 + k)
⊢ Odd k

Tactic:
rw [zero_add k] at hnk

Premises used: zero_add
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
k : ℕ
hnk : Odd k
⊢ (hermite 0).coeff k = 0

Tactic:
coeff_hermite_of_lt hnk.pos

Premises used: Odd.pos, Polynomial.coeff_hermite_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
k : ℕ
hnk : Odd k
⊢ (hermite 0).coeff k = 0

Tactic:
exact coeff_hermite_of_lt hnk.pos

Premises used: Odd.pos, Polynomial.coeff_hermite_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0
hnk : Odd (n + 1 + 0)
⊢ Odd (n + Nat.succ 0)

Tactic:
rw [Nat.succ_add_eq_add_succ] at hnk

Premises used: Nat.succ_add_eq_add_succ
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
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
succ₂ succ₃ : Eq (α := ℤ) 0 0
⊢ (hermite (n + 1)).coeff 0 = 0

Tactic:
rw [coeff_hermite_succ_zero, ih hnk, neg_zero]

Premises used: Polynomial.coeff_hermite_succ_zero, neg_zero
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
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))
succ₁ : Odd (n + k)
⊢ (hermite (n + 1)).coeff (k + 1) = 0

Tactic:
rw [coeff_hermite_succ_succ, ih, ih, mul_zero, sub_zero]

Premises used: Polynomial.coeff_hermite_succ_succ, sub_zero, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
succ succ₁ succ₂ succ₃ : ∀ (hnk : Odd (n + (k + 1).succ)), Odd (n + (k + 2))
⊢ Odd (n + (k + 2))

Tactic:
rwa [Nat.succ_add_eq_add_succ] at hnk

Premises used: Nat.succ_add_eq_add_succ
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
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
rw₁ rw₂ : (n + k).succ.succ = n + k + 2
⊢ n.succ + k.succ = n + k + 2

Tactic:
rw [Nat.succ_add, Nat.add_succ]

Premises used: Nat.add_succ, Nat.succ_add
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ Odd (n + k + 2)

Tactic:
rw [(by rw [Nat.succ_add, Nat.add_succ] : n.succ + k.succ = n + k + 2)] at hnk
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + k + 2)
⊢ Odd (n + k)

Tactic:
(Nat.odd_add.mp hnk).mpr even_two

Premises used: Iff.mpr, even_two, Iff.mp, Nat.odd_add
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
ih : ∀ {k : ℕ} (hnk : Odd (n + k)), (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + k + 2)
⊢ Odd (n + k)

Tactic:
exact (Nat.odd_add.mp hnk).mpr even_two

Premises used: Iff.mpr, even_two, Iff.mp, Nat.odd_add
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
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
succ₁ : ∀ (k : ℕ) (hnk : Odd (n + 1 + (k + 1))), (hermite (n + 1)).coeff (k + 1) = 0
⊢ (hermite (n + 1)).coeff k = 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

Premises used: Iff.mpr, Polynomial.coeff_hermite_succ_zero, Polynomial.coeff_hermite_succ_succ, sub_zero, MulZeroClass.mul_zero, Iff.mp, neg_zero, Nat.succ_add_eq_add_succ, Nat.odd_add
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
hnk : Odd (n + k)
zero : ∀ {k : ℕ} (hnk : Odd (0 + k)), (hermite 0).coeff k = 0
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
⊢ (hermite n).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

Premises used: Iff.mpr, Polynomial.coeff_hermite_succ_zero, Polynomial.coeff_hermite_succ_succ, sub_zero, Odd.pos, zero_add, MulZeroClass.mul_zero, Iff.mp, Polynomial.coeff_hermite_of_lt, neg_zero, Nat.succ_add_eq_add_succ, Nat.odd_add
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
x : ℕ
⊢ (hermite (HMul.hMul (α := ℕ) 2 0 + x)).coeff x =
    HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(HMul.hMul (α := ℕ) 2 0 - 1)‼ : ℤ) *
      (↑((HMul.hMul (α := ℕ) 2 0 + x).choose x) : ℤ)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
⊢ (hermite (2 * n + 1 + 1)).coeff 0 = -(hermite (2 * n + 1)).coeff 1

Tactic:
coeff_hermite_succ_zero (2 * n + 1)

Premises used: HMul.hMul, Polynomial.coeff_hermite_succ_zero, HAdd.hAdd, OfNat.ofNat