awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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) → ℝ) (∑ 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)
have ha : 0 ≤ c ^ i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (hypothesis)
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 * 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))
have this : c ^ j * c ^ (i - j) = c ^ i
Tactic: have : c ^ j * c ^ (i - j) = c ^ i := by simp_all [← pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (hypothesis)
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) *
      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))
have hp_le : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) ≤ gaussNorm v c p
Tactic: have hp_le := p.le_gaussNorm v hc j
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (hypothesis)
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) → ℝ) (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))
have hq_le : 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)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (hypothesis)
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
⊢ 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))
have this : 0 ≤ gaussNorm v c p
Tactic: have := p.gaussNorm_nonneg v hc
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (hypothesis)
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) *
      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))
have hp_le₁ : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) ≤
  p.support.sup' sorry fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
Tactic: simp_all only [gaussNorm, ↓reduceDIte]
Cleared hypotheses: hp_le, hq_le, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (hypothesis)
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) → ℝ) (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))
have hq_le₁ : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i - j)) : ℝ) (c ^ (i - j)) ≤
  q.support.sup' sorry fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i)
Tactic: simp_all only [gaussNorm, ↓reduceDIte]
Cleared hypotheses: hp_le, hq_le, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (hypothesis)
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)
⊢ 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))
have this₁ : LE.le (α := ℝ) 0 (p.support.sup' sorry fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
Tactic: simp_all only [gaussNorm, ↓reduceDIte]
Cleared hypotheses: hp_le, hq_le, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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))
⊢ 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))
have c0 : 0 ≤ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff (i - j)) : ℝ) (c ^ (i - j))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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) → ℝ) (∑ 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))
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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)
⊢ 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))
have 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))
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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))
⊢ 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))
have 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' sorry fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
    (q.support.sup' sorry 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (hypothesis)
Goal:
c : ℝ
R : Type u_3
inst : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑v : (a : R) → ℝ)
hc : 0 < c
p q : R[X]
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
have hc0 : 0 ≤ c
Tactic: have hc0 : 0 ≤ c := le_of_lt hc
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
have 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)
Tactic: obtain ⟨i, hi_p, hlt_p⟩ := p.exists_min_eq_gaussNorm v hc0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
have 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)
Tactic: obtain ⟨j, hj_q, hlt_q⟩ := q.exists_min_eq_gaussNorm v hc0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
have 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)
Tactic: wlog hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussNorm (goal)
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)
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
have 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)
Tactic: wlog hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
Cleared hypotheses: hna, hc, p, q, hc0, i, hi_p, hlt_p, j, hj_q, hlt_q