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 ℝ
p : R[X]
hc : 0 ≤ c
h_nonempty :
  Set.Nonempty (α := ℕ) {i : ℕ | gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)}
j : ℕ
hj_lt : ∀ m ≤ j, ¬gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff m) : ℝ) (c ^ m)
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p

Tactic:
exact lt_of_le_of_ne (le_gaussNorm v _ hc j) fun a ↦ hj_lt j (Nat.le_refl j) a.symm

Premises used: Nat.le_refl, Polynomial.le_gaussNorm, Eq.symm, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
inl : ∀ (hp : p = 0), gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
inr : p ≠ 0 → gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)

Tactic:
rcases eq_or_ne p 0 with hp | _

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
hp : p = 0
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)

Tactic:
simp [hp]
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
inr : ∀ (hq : q = 0), gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
inr₁ : q ≠ 0 → gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)

Tactic:
rcases eq_or_ne q 0 with hq | _

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
hq : q = 0
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)

Tactic:
simp [hq]
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
h_1 : q ≠ 0
inr : ∀ (hpq : p + q = 0), gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
inr₁ : ∀ (hpq : p + q ≠ 0), gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)

Tactic:
rcases eq_or_ne (p + q) 0 with hpq | hpq

Premises used: HAdd.hAdd, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
h_1 : q ≠ 0
hpq : p + q = 0
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)

Tactic:
simp [hpq, hc, gaussNorm_nonneg]

Premises used: 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
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
h_1 : q ≠ 0
hpq : p + q ≠ 0
inr :
  ∀ b ∈ (p + q).support,
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) ((p + q).coeff b) : ℝ) (c ^ b) ≤
      max
        (if h : p.support.Nonempty then
          p.support.sup' h fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
        else 0)
        (if h : q.support.Nonempty then
          q.support.sup' h fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i)
        else 0)
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)

Tactic:
simp only [gaussNorm, support_nonempty, ne_eq, hpq, not_false_eq_true, ↓reduceDIte,
    Finset.sup'_le_iff]

Premises used: reduceDIte, ne_eq, Finset.sup'_le_iff, not_false_eq_true, Polynomial.support_nonempty, 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
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
h_1 : q ≠ 0
hpq : p + q ≠ 0
i : ℕ
inr :
  i ∈ (p + q).support →
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) ((p + q).coeff i) : ℝ) (c ^ i) ≤
      max
        (if h : p.support.Nonempty then
          p.support.sup' h fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
        else 0)
        (if h : q.support.Nonempty then
          q.support.sup' h fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i)
        else 0)
⊢ i ∈ (p + q).support →
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) ((p + q).coeff i) : ℝ) (c ^ i) ≤
      max
        (if h : p.support.Nonempty then
          p.support.sup' h fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
        else 0)
        (if h : q.support.Nonempty then
          q.support.sup' h fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i)
        else 0)

Tactic:
_
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
h_1 : q ≠ 0
hpq : p + q ≠ 0
i : ℕ
h_2 : i ∈ (p + q).support
rw :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i + q.coeff i) : ℝ) (c ^ i) ≤
    HMul.hMul (α := ℝ) (max ((v : (a : R) → ℝ) (p.coeff i)) ((v : (a : R) → ℝ) (q.coeff i)) : ℝ) (c ^ i)
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) ((p + q).coeff i) : ℝ) (c ^ i) ≤
    HMul.hMul (α := ℝ) (max ((v : (a : R) → ℝ) (p.coeff i)) ((v : (a : R) → ℝ) (q.coeff i)) : ℝ) (c ^ i)

Tactic:
rw [coeff_add]

Premises used: Polynomial.coeff_add
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
h_1 : q ≠ 0
hpq : p + q ≠ 0
i : ℕ
h_2 : i ∈ (p + q).support
hbc :
  LE.le (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i + q.coeff i) : ℝ)
    (max ((v : (a : R) → ℝ) (p.coeff i)) ((v : (a : R) → ℝ) (q.coeff i)) : ℝ)
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i + q.coeff i) : ℝ) (c ^ i) ≤
    HMul.hMul (α := ℝ) (max ((v : (a : R) → ℝ) (p.coeff i)) ((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
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
h_1 : q ≠ 0
hpq : p + q ≠ 0
i : ℕ
h_2 : i ∈ (p + q).support
⊢ LE.le (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i + q.coeff i) : ℝ)
    (max ((v : (a : R) → ℝ) (p.coeff i)) ((v : (a : R) → ℝ) (q.coeff i)) : ℝ)

Tactic:
hna (p.coeff i) (q.coeff i)

Premises used: Polynomial.coeff
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
h_1 : q ≠ 0
hpq : p + q ≠ 0
i : ℕ
h_2 : i ∈ (p + q).support
⊢ LE.le (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i + q.coeff i) : ℝ)
    (max ((v : (a : R) → ℝ) (p.coeff i)) ((v : (a : R) → ℝ) (q.coeff i)) : ℝ)

Tactic:
exact hna (p.coeff i) (q.coeff i)

Premises used: Polynomial.coeff
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
h_1 : q ≠ 0
hpq : p + q ≠ 0
i : ℕ
h_2 : i ∈ (p + q).support
rw rw₁ :
  max (HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
      (HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i)) =
    max (HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
      (HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i))
⊢ HMul.hMul (α := ℝ) (max ((v : (a : R) → ℝ) (p.coeff i)) ((v : (a : R) → ℝ) (q.coeff i)) : ℝ) (c ^ i) =
    max (HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
      (HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i))

Tactic:
rw [max_mul_of_nonneg _ _ (pow_nonneg hc _)]

Premises used: pow_nonneg, max_mul_of_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
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
h_1 : q ≠ 0
hpq : p + q ≠ 0
i : ℕ
h_2 : i ∈ (p + q).support
a : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) ≤ gaussNorm v c p
a₁ : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i) ≤ gaussNorm v c q
⊢ max (HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
      (HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i)) ≤
    max (gaussNorm v c p) (gaussNorm v c q)

Tactic:
apply max_le_max

Premises used: max_le_max
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
Goal:
R : Type u_1
F : Type u_2
inst : Semiring R
inst_1 : FunLike F R ℝ
v : F
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
h_1 : q ≠ 0
hpq : p + q ≠ 0
i : ℕ
h_2 : i ∈ (p + q).support
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) ≤ gaussNorm v c p

Tactic:
le_gaussNorm v _ hc i

Premises used: Polynomial.le_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
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
h_1 : q ≠ 0
hpq : p + q ≠ 0
i : ℕ
h_2 : i ∈ (p + q).support
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) ≤ gaussNorm v c p

Tactic:
exact le_gaussNorm v _ hc i

Premises used: Polynomial.le_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
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
h_1 : q ≠ 0
hpq : p + q ≠ 0
i : ℕ
h_2 : i ∈ (p + q).support
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i) ≤ gaussNorm v c q

Tactic:
le_gaussNorm v _ hc i

Premises used: Polynomial.le_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
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
h_1 : q ≠ 0
hpq : p + q ≠ 0
i : ℕ
h_2 : i ∈ (p + q).support
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i) ≤ gaussNorm v c q

Tactic:
exact le_gaussNorm v _ hc i

Premises used: Polynomial.le_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
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hna : IsNonarchimedean.{0, u_1} (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
c : ℝ
hc : 0 ≤ c
p q : R[X]
h : p ≠ 0
h_1 : q ≠ 0
hpq : p + q ≠ 0
i : ℕ
h_2 : i ∈ (p + q).support
v₁ :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) ((p + q).coeff i) : ℝ) (c ^ i) ≤
    HMul.hMul (α := ℝ) (max ((v : (a : R) → ℝ) (p.coeff i)) ((v : (a : R) → ℝ) (q.coeff i)) : ℝ) (c ^ i)
v₂ :
  HMul.hMul (α := ℝ) (max ((v : (a : R) → ℝ) (p.coeff i)) ((v : (a : R) → ℝ) (q.coeff i)) : ℝ) (c ^ i) =
    max (HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
      (HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i))
v₃ :
  max (HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
      (HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i)) ≤
    max (gaussNorm v c p) (gaussNorm v c q)
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) ((p + q).coeff i) : ℝ) (c ^ i) ≤
    max
      (if h : p.support.Nonempty then
        p.support.sup' h fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
      else 0)
      (if h : q.support.Nonempty then
        q.support.sup' h fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i)
      else 0)

Tactic:
calc
  v ((p + q).coeff i) * c ^ i
    ≤ max (v (p.coeff i)) (v (q.coeff i)) * c ^ i := by
    rw [coeff_add]
    gcongr
    exact hna (p.coeff i) (q.coeff i)
  _ = max (v (p.coeff i) * c ^ i) (v (q.coeff i) * c ^ i) := by
    rw [max_mul_of_nonneg _ _ (pow_nonneg hc _)]
  _ ≤ max (gaussNorm v c p) (gaussNorm v c q) := by
    apply max_le_max <;>
    exact le_gaussNorm v _ hc i

Premises used: HMul.hMul, Polynomial.coeff, HPow.hPow, HAdd.hAdd, Max.max, DFunLike.coe, 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
inl : ∀ (hpq : p * q = 0), gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q
inr : ∀ (hpq : p * q ≠ 0), gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q

Tactic:
rcases eq_or_ne (p * q) 0 with hpq | hpq

Premises used: HMul.hMul, eq_or_ne, OfNat.ofNat
-- 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
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q

Tactic:
simp [hpq, hc, gaussNorm_nonneg, mul_nonneg]

Premises used: mul_nonneg, 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 : ℝ
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
⊢ p.support.Nonempty

Tactic:
have h_supp_p : p.support.Nonempty := support_nonempty.mpr <| left_ne_zero_of_mul hpq
-- 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
⊢ q.support.Nonempty

Tactic:
have h_supp_q : q.support.Nonempty := support_nonempty.mpr <| right_ne_zero_of_mul hpq
-- 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
inr :
  ∀ b ∈ (p * q).support,
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (∑ x ∈ range b.succ, p.coeff x * q.coeff (b - x)) : ℝ) (c ^ b) ≤
      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))
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q

Tactic:
simp only [gaussNorm, support_nonempty, ne_eq, hpq, not_false_eq_true, ↓reduceDIte, h_supp_p,
    h_supp_q, sup'_le_iff, coeff_mul, Nat.sum_antidiagonal_eq_sum_range_succ_mk]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, reduceDIte, Polynomial.coeff_mul, ne_eq, Finset.sup'_le_iff, not_false_eq_true, Polynomial.support_nonempty, 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 : ℕ
inr :
  i ∈ (p * q).support →
    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))
⊢ i ∈ (p * q).support →
    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:
_
-- 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
inr :
  ∀ j ∈ range (i + 1),
    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)) : ℝ) →
      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))
⊢ 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:
obtain ⟨j, _, _⟩ := IsNonarchimedean.finset_image_add_of_nonempty hna _ nonempty_range_add_one

Premises used: Finset.nonempty_range_add_one, IsNonarchimedean.finset_image_add_of_nonempty
-- 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)) : ℝ)
ha : 0 ≤ c ^ i
⊢ 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)

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)) : ℝ)
⊢ c ^ j * c ^ (i - j) = c ^ i

Tactic:
simp_all [← pow_add]

Premises used: pow_add
-- 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)) : ℝ)
⊢ c ^ j * c ^ (i - j) = c ^ i

Tactic:
have : c ^ j * c ^ (i - j) = c ^ i := by simp_all [← pow_add]
-- 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)) : ℝ)
this : c ^ j * c ^ (i - j) = c ^ i
⊢ 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))

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

Tactic:
have hp_le := p.le_gaussNorm v hc j