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 : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
⊢ x + (i + j - x) = i + j

Tactic:
simp_all
-- 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 : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
⊢ x + (i + j - x) = i + j

Tactic:
have : x + (i + j - x) = i + j := by simp_all
-- 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 :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) : ℝ) (c ^ (i + 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))
h₁ :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ) (c ^ (i + j)) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (c ^ j)
convert_to :
  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)
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) : ℝ) (c ^ (i + j)) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ) (c ^ (i + j))

Tactic:
convert_to v (p.coeff x) * c ^ x * (v (q.coeff (i + j - x)) * c ^ (i + j - x)) <
    v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j)

Premises used: HMul.hMul, HSub.hSub, Polynomial.coeff, HPow.hPow, HAdd.hAdd, DFunLike.coe
-- 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
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) : ℝ) (c ^ (i + 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))

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
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ) (c ^ (i + j)) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) *
      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
inl :
  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)
inr :
  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)
⊢ 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:
rcases lt_or_gt_of_ne hneq

Premises used: lt_or_gt_of_ne
-- 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 : x < i
hbc : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - 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 x) : ℝ) (c ^ x) * gaussNorm v c q

Tactic:
gcongr
-- 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 : x < i
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) ≤ gaussNorm v c q

Tactic:
q.le_gaussNorm v hc0 (i + j - x)

Premises used: Polynomial.le_gaussNorm, HSub.hSub, HAdd.hAdd
-- 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 : x < i
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i + j - x)) : ℝ) (c ^ (i + j - x)) ≤ gaussNorm v c q

Tactic:
exact q.le_gaussNorm v hc0 (i + j - x)

Premises used: Polynomial.le_gaussNorm, HSub.hSub, HAdd.hAdd
-- 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 : x < i
rw rw₁ :
  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 j) : ℝ) (c ^ j)
⊢ 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:
rw [hj_q]
-- 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 : x < i
hbc :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
⊢ 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:
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 : x < i
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) <
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)

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 : 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)
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)
⊢ 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))
    _ ≤ 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

Premises used: HMul.hMul, HSub.hSub, Polynomial.coeff, HPow.hPow, HAdd.hAdd, DFunLike.coe, Polynomial.gaussNorm
-- 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) → ℝ) (p.coeff x) : ℝ) (c ^ x) ≤ gaussNorm v c p
⊢ 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:
gcongr
-- 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) → ℝ) (p.coeff x) : ℝ) (c ^ x) ≤ gaussNorm v c p

Tactic:
p.le_gaussNorm v hc0 x

Premises used: Polynomial.le_gaussNorm
-- 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) → ℝ) (p.coeff x) : ℝ) (c ^ x) ≤ gaussNorm v c p

Tactic:
exact p.le_gaussNorm v hc0 x

Premises used: Polynomial.le_gaussNorm