awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
inst_4 : MulHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
h_supp_p : p.support.Nonempty
h_supp_q : q.support.Nonempty
i : ℕ
h : i ∈ (p * q).support
j : ℕ
left : j ∈ range (i + 1)
right :
  LE.le (α := ℝ) ((v : (a : R) → ℝ) (∑ j ∈ range (i + 1), p.coeff j * q.coeff (i - j)) : ℝ)
    ((v : (a : R) → ℝ) (p.coeff j * q.coeff (i - j)) : ℝ)
hp_le : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) ≤ gaussNorm v c p
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i - j)) : ℝ) (c ^ (i - j)) ≤ gaussNorm v c q

Tactic:
have hq_le := q.le_gaussNorm v hc (i - j)
-- 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 : ℝ
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
inst_4 : MulHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
h_supp_p : p.support.Nonempty
h_supp_q : q.support.Nonempty
i : ℕ
h : i ∈ (p * q).support
j : ℕ
left : j ∈ range (i + 1)
right :
  LE.le (α := ℝ) ((v : (a : R) → ℝ) (∑ j ∈ range (i + 1), p.coeff j * q.coeff (i - j)) : ℝ)
    ((v : (a : R) → ℝ) (p.coeff j * q.coeff (i - j)) : ℝ)
hp_le : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) ≤ gaussNorm v c p
hq_le : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i - j)) : ℝ) (c ^ (i - j)) ≤ gaussNorm v c q
⊢ 0 ≤ gaussNorm v c p

Tactic:
have := p.gaussNorm_nonneg v hc
-- 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 : ℝ
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
inst_4 : MulHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
h_supp_p : p.support.Nonempty
h_supp_q : q.support.Nonempty
i : ℕ
h : i ∈ (p * q).support
j : ℕ
left : j ∈ range (i + 1)
right :
  LE.le (α := ℝ) ((v : (a : R) → ℝ) (∑ j ∈ range (i + 1), p.coeff j * q.coeff (i - j)) : ℝ)
    ((v : (a : R) → ℝ) (p.coeff j * q.coeff (i - j)) : ℝ)
hp_le : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) ≤ gaussNorm v c p
hq_le : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i - j)) : ℝ) (c ^ (i - j)) ≤ gaussNorm v c q
this : 0 ≤ gaussNorm v c p
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) ≤
    p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)

Tactic:
simp_all only [gaussNorm, ↓reduceDIte]

Premises used: reduceDIte, Polynomial.gaussNorm
-- 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 : ℝ
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
inst_4 : MulHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
h_supp_p : p.support.Nonempty
h_supp_q : q.support.Nonempty
i : ℕ
h : i ∈ (p * q).support
j : ℕ
left : j ∈ range (i + 1)
right :
  LE.le (α := ℝ) ((v : (a : R) → ℝ) (∑ j ∈ range (i + 1), p.coeff j * q.coeff (i - j)) : ℝ)
    ((v : (a : R) → ℝ) (p.coeff j * q.coeff (i - j)) : ℝ)
hp_le : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) ≤ gaussNorm v c p
hq_le : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i - j)) : ℝ) (c ^ (i - j)) ≤ gaussNorm v c q
this : 0 ≤ gaussNorm v c p
hp_le₁ :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) ≤
    p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i - j)) : ℝ) (c ^ (i - j)) ≤
    q.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i)

Tactic:
simp_all only [gaussNorm, ↓reduceDIte]

Premises used: reduceDIte, Polynomial.gaussNorm
-- 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 : ℝ
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
inst_4 : MulHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
h_supp_p : p.support.Nonempty
h_supp_q : q.support.Nonempty
i : ℕ
h : i ∈ (p * q).support
j : ℕ
left : j ∈ range (i + 1)
right :
  LE.le (α := ℝ) ((v : (a : R) → ℝ) (∑ j ∈ range (i + 1), p.coeff j * q.coeff (i - j)) : ℝ)
    ((v : (a : R) → ℝ) (p.coeff j * q.coeff (i - j)) : ℝ)
hp_le : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) ≤ gaussNorm v c p
hq_le : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i - j)) : ℝ) (c ^ (i - j)) ≤ gaussNorm v c q
this : 0 ≤ gaussNorm v c p
hp_le₁ :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) ≤
    p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hq_le₁ :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i - j)) : ℝ) (c ^ (i - j)) ≤
    q.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i)
⊢ LE.le (α := ℝ) 0 (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))

Tactic:
simp_all only [gaussNorm, ↓reduceDIte]

Premises used: reduceDIte, Polynomial.gaussNorm
-- 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 : ℝ
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
inst_4 : MulHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
h_supp_p : p.support.Nonempty
h_supp_q : q.support.Nonempty
i : ℕ
h : i ∈ (p * q).support
j : ℕ
left : j ∈ range (i + 1)
right :
  LE.le (α := ℝ) ((v : (a : R) → ℝ) (∑ j ∈ range (i + 1), p.coeff j * q.coeff (i - j)) : ℝ)
    ((v : (a : R) → ℝ) (p.coeff j * q.coeff (i - j)) : ℝ)
hp_le :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) ≤
    p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
hq_le :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i - j)) : ℝ) (c ^ (i - j)) ≤
    q.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i)
this : LE.le (α := ℝ) 0 (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
c0 : 0 ≤ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i - j)) : ℝ) (c ^ (i - j))
b0 : LE.le (α := ℝ) 0 (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i - j)) : ℝ) (c ^ (i - j)) ≤
    HMul.hMul (α := ℝ) (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
      (q.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i))

Tactic:
gcongr
-- 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 : ℝ
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
inst_4 : MulHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
h_supp_p : p.support.Nonempty
h_supp_q : q.support.Nonempty
i : ℕ
h : i ∈ (p * q).support
j : ℕ
left : j ∈ range (i + 1)
right :
  LE.le (α := ℝ) ((v : (a : R) → ℝ) (∑ j ∈ range (i + 1), p.coeff j * q.coeff (i - j)) : ℝ)
    ((v : (a : R) → ℝ) (p.coeff j * q.coeff (i - j)) : ℝ)
v₁ :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (∑ j ∈ range (i + 1), p.coeff j * q.coeff (i - j)) : ℝ) (c ^ i) ≤
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j * q.coeff (i - j)) : ℝ) (c ^ i)
v₂ :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j * q.coeff (i - j)) : ℝ) (c ^ i) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i - j)) : ℝ) (c ^ (i - j))
v₃ :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) *
      HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i - j)) : ℝ) (c ^ (i - j)) ≤
    HMul.hMul (α := ℝ) (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
      (q.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i))
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (∑ x ∈ range i.succ, p.coeff x * q.coeff (i - x)) : ℝ) (c ^ i) ≤
    HMul.hMul (α := ℝ) (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
      (q.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i))

Tactic:
calc
  v (∑ j ∈ range (i + 1), p.coeff j * q.coeff (i - j)) * c ^ i
  _ ≤ v (p.coeff j * q.coeff (i - j)) * c ^ i := by gcongr
  _ = (v (p.coeff j) * c ^ j) * (v (q.coeff (i - j)) * c ^ (i - j)) := by
      have : c ^ j * c ^ (i - j) = c ^ i := by simp_all [← pow_add]
      grind
  _ ≤ (p.support.sup' _ fun i ↦ v (p.coeff i) * c ^ i)
    * q.support.sup' _ fun i ↦ v (q.coeff i) * c ^ i := by
      have hp_le := p.le_gaussNorm v hc j
      have hq_le := q.le_gaussNorm v hc (i - j)
      have := p.gaussNorm_nonneg v hc
      simp_all only [gaussNorm, ↓reduceDIte]
      gcongr

Premises used: HMul.hMul, HSub.hSub, Polynomial.coeff, Finset.range, HPow.hPow, HAdd.hAdd, Finset.sup', OfNat.ofNat, DFunLike.coe, Polynomial.support, Finset.sum
-- 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]
⊢ 0 ≤ c

Tactic:
have hc0 : 0 ≤ c := le_of_lt hc
-- 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]
hc0 : 0 ≤ c
obtain :
  ∀ (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),
    gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)

Tactic:
obtain ⟨i, hi_p, hlt_p⟩ := p.exists_min_eq_gaussNorm v hc0

Premises used: Polynomial.exists_min_eq_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]
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
obtain :
  ∀ (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),
    gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)

Tactic:
obtain ⟨j, hj_q, hlt_q⟩ := q.exists_min_eq_gaussNorm v hc0

Premises used: Polynomial.exists_min_eq_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]
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
inr :
  ∀
    (this :
      ∀ {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]) (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 : ℝ)),
        gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q))
    (hvpq :
      ¬(Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧
          Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ))),
    gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
wlog :
  ∀ {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]) (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 : ℝ)),
    gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)

Tactic:
wlog hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0

Premises used: Polynomial.coeff, DFunLike.coe
-- 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]
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
this :
  ∀ {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]) (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 : ℝ)),
    gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
hvpq :
  ¬(Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ) ∧ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ))
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)

Tactic:
grind [mul_mul_mul_comm, gaussNorm_nonneg]

Premises used: mul_mul_mul_comm, Polynomial.gaussNorm_nonneg
-- 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 : ℝ)
⊢ Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)

Tactic:
have := hvpq.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 : Ne (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (0 : ℝ)
⊢ Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)

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

Tactic:
apply le_of_eq_of_le _ <| (p * q).le_gaussNorm v hc0 (i + j)

Premises used: HMul.hMul, Polynomial.le_gaussNorm, HAdd.hAdd, le_of_eq_of_le
-- 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 : ℝ)
⊢ i ∈ range (i + j).succ

Tactic:
simp
-- 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 : ℝ)
rw :
  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 (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ) (c ^ (i + j))
rw₁ :
  ∀ j_1 ∈ range (i + j).succ,
    j_1 ≠ i →
      LT.lt (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (j_1, i + j - j_1).1 * q.coeff (j_1, i + j - j_1).2) : ℝ)
        ((v : (a : R) → ℝ) (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ)
⊢ gaussNorm v c p * gaussNorm v c q = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) ((p * q).coeff (i + j)) : ℝ) (c ^ (i + j))

Tactic:
rw [hi_p, hj_q, coeff_mul, Nat.sum_antidiagonal_eq_sum_range_succ_mk,
    IsNonarchimedean.apply_sum_eq_of_lt hna (k := i) (by simp)]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, Polynomial.coeff_mul, IsNonarchimedean.apply_sum_eq_of_lt
-- 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 : ℝ)
⊢ 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 (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ) (c ^ (i + 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 : Ne (α := ℝ) ((v : (a : R) → ℝ) (q.coeff j) : ℝ) (0 : ℝ)
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
apply :
  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))
⊢ LT.lt (α := ℝ) ((v : (a : R) → ℝ) (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) : ℝ)
    ((v : (a : R) → ℝ) (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) : ℝ)

Tactic:
apply lt_of_mul_lt_mul_right _ <| pow_nonneg hc0 (i + j)

Premises used: pow_nonneg, HAdd.hAdd, lt_of_mul_lt_mul_right