awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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 : x < i
⊢ 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)
have 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)) ≤
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) * gaussNorm v c q
Tactic: calc
    v (p.coeff x) * c ^ x * (v (q.coeff (i + j - x)) * c ^ (i + j - x))
    _ ≤ v (p.coeff x) * c ^ x * gaussNorm v c q := by
        gcongr
        exact q.le_gaussNorm v hc0 (i + j - x)
    _ = v (p.coeff x) * c ^ x * (v (q.coeff j) * c ^ j) := by
        rw [hj_q]
    _ < v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j) := by
        gcongr 1
        grind
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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 : x < i
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)) ≤
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) * gaussNorm v c q
⊢ 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)
have v₂ : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) * gaussNorm v c q =
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
    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))
    _ ≤ v (p.coeff x) * c ^ x * gaussNorm v c q := by
        gcongr
        exact q.le_gaussNorm v hc0 (i + j - x)
    _ = v (p.coeff x) * c ^ x * (v (q.coeff j) * c ^ j) := by
        rw [hj_q]
    _ < v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j) := by
        gcongr 1
        grind
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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 : x < i
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)) ≤
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) * gaussNorm v c q
v₂ :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) * gaussNorm v c q =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) *
      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)
have v₃ : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ 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 j) : ℝ) (c ^ j)
Tactic: calc
    v (p.coeff x) * c ^ x * (v (q.coeff (i + j - x)) * c ^ (i + j - x))
    _ ≤ v (p.coeff x) * c ^ x * gaussNorm v c q := by
        gcongr
        exact q.le_gaussNorm v hc0 (i + j - x)
    _ = v (p.coeff x) * c ^ x * (v (q.coeff j) * c ^ j) := by
        rw [hj_q]
    _ < v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j) := by
        gcongr 1
        grind
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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) → ℝ) (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))
have hbc : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) ≤ gaussNorm v c p
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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
⊢ 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))
have 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))
Tactic: rw [hi_p]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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) → ℝ) (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)
have 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)
Tactic: gcongr 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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) → ℝ) (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)
have 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))
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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))
⊢ 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)
have 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))
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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))
⊢ 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)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
⊢ hermite (n + 1) = HSub.hSub (β := ℤ[X]) (X * hermite n) ((derivative : (a : ℤ[X]) → ℤ[X]) (hermite n) : ℤ[X])
have 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])
Tactic: rw [hermite]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
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
have 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)
Tactic: rw [Function.iterate_succ_apply', ← ih, hermite_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
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)
⊢ hermite (n + 1) =
    (fun (p : ℤ[X]) ↦ HSub.hSub (β := ℤ[X]) (X * p) ((derivative : (a : ℤ[X]) → ℤ[X]) p : ℤ[X]))^[n + 1] 1
have succ₁ : hermite (n + 1) = HSub.hSub (β := ℤ[X]) (X * hermite n) ((derivative : (a : ℤ[X]) → ℤ[X]) (hermite n) : ℤ[X])
Tactic: rw [Function.iterate_succ_apply', ← ih, hermite_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
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])
⊢ hermite (n + 1) =
    (fun (p : ℤ[X]) ↦ HSub.hSub (β := ℤ[X]) (X * p) ((derivative : (a : ℤ[X]) → ℤ[X]) p : ℤ[X]))^[n + 1] 1
have 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])
Tactic: rw [Function.iterate_succ_apply', ← ih, hermite_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
⊢ hermite n = (fun (p : ℤ[X]) ↦ HSub.hSub (β := ℤ[X]) (X * p) ((derivative : (a : ℤ[X]) → ℤ[X]) p : ℤ[X]))^[n] 1
have zero : hermite 0 = (fun (p : ℤ[X]) ↦ HSub.hSub (β := ℤ[X]) (X * p) ((derivative : (a : ℤ[X]) → ℤ[X]) p : ℤ[X]))^[0] 1
Tactic: induction n with
  | zero => rfl
  | succ n ih => rw [Function.iterate_succ_apply', ← ih, hermite_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n : ℕ
zero : hermite 0 = (fun (p : ℤ[X]) ↦ HSub.hSub (β := ℤ[X]) (X * p) ((derivative : (a : ℤ[X]) → ℤ[X]) p : ℤ[X]))^[0] 1
⊢ hermite n = (fun (p : ℤ[X]) ↦ HSub.hSub (β := ℤ[X]) (X * p) ((derivative : (a : ℤ[X]) → ℤ[X]) p : ℤ[X]))^[n] 1
have 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
Tactic: induction n with
  | zero => rfl
  | succ n ih => rw [Function.iterate_succ_apply', ← ih, hermite_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n k : ℕ
⊢ (hermite (n + 1)).coeff (k + 1) = (hermite n).coeff k - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 * (hermite n).coeff (k + 2)
have 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)
Tactic: rw [hermite_succ, coeff_sub, coeff_X_mul, coeff_derivative, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n k : ℕ
⊢ (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)
have 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)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n k : ℕ
hnk : n < k
⊢ (hermite n).coeff k = 0
have obtain : ∀ (k : ℕ) (hnk : n < n + k + 1), (hermite n).coeff (n + k + 1) = 0
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt hnk
Cleared hypotheses: k, hnk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (hypothesis)
Goal:
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
⊢ (hermite (n + 1)).coeff (n + 1 + k + 1) = 0
have this : n + k + 1 + 2 = n + (k + 2) + 1
Tactic: have : n + k + 1 + 2 = n + (k + 2) + 1 := by ring
-- 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
⊢ (hermite (n + 1)).coeff (n + 1 + k + 1) = 0
have succ : (hermite n).coeff (n + 1 + k) - HAdd.hAdd (α := ℤ) (↑(n + 1 + k) : ℤ) 2 * (hermite n).coeff (n + 1 + k + 2) = 0
Tactic: rw [coeff_hermite_succ_succ, add_right_comm, this, ih k, ih (k + 2), mul_zero, sub_zero]