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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
i : ℕ
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) ((PowerSeries.coeff i : (a : PowerSeries R) → R) (↑p : PowerSeries R) : R) : ℝ)
      (c ^ i) ≤
    PowerSeries.gaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R)
have hbd : PowerSeries.HasGaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R)
Tactic: apply PowerSeries.le_gaussNorm
-- 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
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
⊢ gaussNorm v 0 p = (v : (a : R) → ℝ) (p.coeff 0)
have this : Eq (α := (i : ℕ) → ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (HPow.hPow (α := ℝ) 0 i))
  fun (i : ℕ) ↦ if i = 0 then (v : (a : R) → ℝ) (p.coeff 0) else 0
Tactic: have : (fun i ↦ v (p.coeff i) * 0 ^ i) = fun i ↦ if i = 0 then v (p.coeff 0) else 0 := by
    aesop
-- 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
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
this :
  Eq (α := (i : ℕ) → ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (HPow.hPow (α := ℝ) 0 i))
    fun (i : ℕ) ↦ if i = 0 then (v : (a : R) → ℝ) (p.coeff 0) else 0
⊢ gaussNorm v 0 p = (v : (a : R) → ℝ) (p.coeff 0)
have inl : p.coeff 0 = 0 → gaussNorm v 0 p = (v : (a : R) → ℝ) (p.coeff 0)
Tactic: rcases eq_or_ne (p.coeff 0) 0 with _ | hcoeff0
-- 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
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
this :
  Eq (α := (i : ℕ) → ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (HPow.hPow (α := ℝ) 0 i))
    fun (i : ℕ) ↦ if i = 0 then (v : (a : R) → ℝ) (p.coeff 0) else 0
inl : p.coeff 0 = 0 → gaussNorm v 0 p = (v : (a : R) → ℝ) (p.coeff 0)
⊢ gaussNorm v 0 p = (v : (a : R) → ℝ) (p.coeff 0)
have inr : ∀ (hcoeff0 : p.coeff 0 ≠ 0), gaussNorm v 0 p = (v : (a : R) → ℝ) (p.coeff 0)
Tactic: rcases eq_or_ne (p.coeff 0) 0 with _ | hcoeff0
-- 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
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
this :
  Eq (α := (i : ℕ) → ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (HPow.hPow (α := ℝ) 0 i))
    fun (i : ℕ) ↦ if i = 0 then (v : (a : R) → ℝ) (p.coeff 0) else 0
hcoeff0 : p.coeff 0 ≠ 0
⊢ gaussNorm v 0 p = (v : (a : R) → ℝ) (p.coeff 0)
have inr : gaussNorm v 0 p ≤ (v : (a : R) → ℝ) (p.coeff 0)
Tactic: apply le_antisymm
-- 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
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
this :
  Eq (α := (i : ℕ) → ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (HPow.hPow (α := ℝ) 0 i))
    fun (i : ℕ) ↦ if i = 0 then (v : (a : R) → ℝ) (p.coeff 0) else 0
hcoeff0 : p.coeff 0 ≠ 0
inr : gaussNorm v 0 p ≤ (v : (a : R) → ℝ) (p.coeff 0)
⊢ gaussNorm v 0 p = (v : (a : R) → ℝ) (p.coeff 0)
have inr₁ : (v : (a : R) → ℝ) (p.coeff 0) ≤ gaussNorm v 0 p
Tactic: apply le_antisymm
-- 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 ℝ
p : R[X]
hc : 0 ≤ c
⊢ Set.Nonempty (α := ℕ) {i : ℕ | gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)}
have obtain : ∀ (i : ℕ) (hi : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)),
  Set.Nonempty (α := ℕ) {i : ℕ | gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)}
Tactic: obtain ⟨i, hi⟩ := exists_eq_gaussNorm v c p
-- 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 ℝ
p : R[X]
hc : 0 ≤ c
⊢ ∃ (i : ℕ),
    gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) ∧
      ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
have h_nonempty : Set.Nonempty (α := ℕ) {i : ℕ | gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)}
Tactic: have h_nonempty : {i | gaussNorm v c p = v (p.coeff i) * c ^ i}.Nonempty := by
    obtain ⟨i, hi⟩ := exists_eq_gaussNorm v c p
    exact ⟨i, Set.mem_setOf.mpr hi⟩
-- 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 ℝ
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)}
⊢ ∃ (i : ℕ),
    gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) ∧
      ∀ j < i, HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
have refine : ∀
  j <
    Nat.find (p :=
      Membership.mem (γ := Set ℕ)
        {i : ℕ | gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)})
      h_nonempty,
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
Tactic: refine ⟨Nat.find h_nonempty, Nat.find_spec h_nonempty, ?_⟩
-- 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 ℝ
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 :
  j <
    Nat.find (p :=
      Membership.mem (γ := Set ℕ)
        {i : ℕ | gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)})
      h_nonempty
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff j) : ℝ) (c ^ j) < gaussNorm v c p
have hj_lt₁ : ∀ m ≤ j, ¬gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff m) : ℝ) (c ^ m)
Tactic: simp only [Nat.lt_find_iff, Set.mem_setOf_eq] at hj_lt
Cleared hypotheses: hj_lt
-- 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
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]
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
have inl : ∀ (hp : p = 0), gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
Tactic: rcases eq_or_ne p 0 with hp | _
-- 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
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)
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
have inr : p ≠ 0 → gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
Tactic: rcases eq_or_ne p 0 with hp | _
-- 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
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
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
have inr : ∀ (hq : q = 0), gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
Tactic: rcases eq_or_ne q 0 with hq | _
-- 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
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)
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
have inr₁ : q ≠ 0 → gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
Tactic: rcases eq_or_ne q 0 with hq | _
-- 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
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
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
have inr : ∀ (hpq : p + q = 0), 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
-- 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
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)
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
have inr₁ : ∀ (hpq : p + q ≠ 0), 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
-- 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
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)
have 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)
Tactic: simp only [gaussNorm, support_nonempty, ne_eq, hpq, not_false_eq_true, ↓reduceDIte,
    Finset.sup'_le_iff]
-- 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
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 + q).coeff i) : ℝ) (c ^ i) ≤
    HMul.hMul (α := ℝ) (max ((v : (a : R) → ℝ) (p.coeff i)) ((v : (a : R) → ℝ) (q.coeff i)) : ℝ) (c ^ i)
have 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)
Tactic: rw [coeff_add]
-- 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
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 + q.coeff i) : ℝ) (c ^ i) ≤
    HMul.hMul (α := ℝ) (max ((v : (a : R) → ℝ) (p.coeff i)) ((v : (a : R) → ℝ) (q.coeff i)) : ℝ) (c ^ i)
have 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)) : ℝ)
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
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 (α := ℝ) (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))
have 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))
Tactic: rw [max_mul_of_nonneg _ _ (pow_nonneg hc _)]
-- 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
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
⊢ 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)
have a : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) ≤ gaussNorm v c p
Tactic: apply max_le_max
-- 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
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
⊢ 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)
have a₁ : HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (q.coeff i) : ℝ) (c ^ i) ≤ gaussNorm v c q
Tactic: apply max_le_max
-- 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
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 + 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)
have 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)
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
-- 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
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)
⊢ 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)
have 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))
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
-- 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
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))
⊢ 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)
have 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)
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
-- 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
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q
have inl : ∀ (hpq : p * q = 0), gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q
Tactic: rcases eq_or_ne (p * q) 0 with hpq | hpq
-- 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
inl : ∀ (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
have inr : ∀ (hpq : p * q ≠ 0), gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q
Tactic: rcases eq_or_ne (p * q) 0 with hpq | hpq
-- 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
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q
have h_supp_p : p.support.Nonempty
Tactic: have h_supp_p : p.support.Nonempty := support_nonempty.mpr <| left_ne_zero_of_mul hpq
-- 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
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q
have h_supp_q : q.support.Nonempty
Tactic: have h_supp_q : q.support.Nonempty := support_nonempty.mpr <| right_ne_zero_of_mul hpq
-- 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
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q
have 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' 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: 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]
-- 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
⊢ 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 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' 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: obtain ⟨j, _, _⟩ := IsNonarchimedean.finset_image_add_of_nonempty hna _ nonempty_range_add_one