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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : p = 0
⊢ PowerSeries.gaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R) = gaussNorm v c p

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
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
neg :
  Eq (α := ℝ) (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
    (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
⊢ PowerSeries.gaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R) = gaussNorm v c p

Tactic:
simp only [PowerSeries.gaussNorm_eq, coeff_coe, gaussNorm, support_nonempty, ne_eq, hp,
      not_false_eq_true, ↓reduceDIte]

Premises used: PowerSeries.gaussNorm_eq, reduceDIte, ne_eq, not_false_eq_true, Polynomial.coeff_coe, 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
neg :
  LE.le (α := ℝ) (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
    (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
neg₁ :
  LE.le (α := ℝ) (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
    (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
⊢ Eq (α := ℝ) (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
    (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
neg :
  ∀ (x : ℕ),
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff x) : ℝ) (c ^ x) ≤
      p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
⊢ LE.le (α := ℝ) (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
    (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))

Tactic:
apply ciSup_le

Premises used: ciSup_le
-- 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
n : ℕ
pos :
  ∀ (h : n ∈ p.support),
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff n) : ℝ) (c ^ n) ≤
      p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
neg :
  ∀ (h : n ∉ p.support),
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff n) : ℝ) (c ^ n) ≤
      p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff n) : ℝ) (c ^ n) ≤
    p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)

Tactic:
by_cases h : n ∈ p.support

Premises used: Polynomial.support
-- 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
n : ℕ
h : n ∈ p.support
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff n) : ℝ) (c ^ n) ≤
    p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)

Tactic:
Finset.le_sup' (fun j ↦ v (p.coeff j) * c ^ j) h

Premises used: HMul.hMul, Polynomial.coeff, HPow.hPow, Finset.le_sup', DFunLike.coe
-- 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
n : ℕ
h : n ∈ p.support
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff n) : ℝ) (c ^ n) ≤
    p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)

Tactic:
exact Finset.le_sup' (fun j ↦ v (p.coeff j) * c ^ j) h

Premises used: HMul.hMul, Polynomial.coeff, HPow.hPow, Finset.le_sup', DFunLike.coe
-- 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
n : ℕ
h : n ∉ p.support
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff n) : ℝ) (c ^ n) ≤
    p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)

Tactic:
simp_all [sup'_nonneg_of_ne_zero v (support_nonempty.mpr hp) hc]

Premises used: Iff.mpr, _private.0.Polynomial.sup'_nonneg_of_ne_zero, Polynomial.support_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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
neg :
  ∀ (i : ℕ) (hi : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)),
    LE.le (α := ℝ) (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
      (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
⊢ LE.le (α := ℝ) (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
    (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))

Tactic:
obtain ⟨i, hi⟩ := exists_eq_gaussNorm v c p

Premises used: Polynomial.exists_eq_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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
i : ℕ
hi : gaussNorm v c p = HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
⊢ (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)

Tactic:
simp only [gaussNorm, support_nonempty.mpr hp, ↓reduceDIte] at hi

Premises used: Iff.mpr, reduceDIte, 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
i : ℕ
hi :
  (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
neg :
  HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) ≤
    ⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
⊢ LE.le (α := ℝ) (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))
    (⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i))

Tactic:
rw [hi]
-- 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
i : ℕ
hi :
  (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) ≤
    ⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)

Tactic:
le_ciSup (aux_bdd v p) i

Premises used: le_ciSup, _private.0.Polynomial.aux_bdd
-- 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
i : ℕ
hi :
  (p.support.sup' ⋯ fun (i : ℕ) ↦ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)) =
    HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) ≤
    ⨆ (i : ℕ), HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i)

Tactic:
exact le_ciSup (aux_bdd v p) i

Premises used: le_ciSup, _private.0.Polynomial.aux_bdd
-- 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
h_eq_zero : ∀ (x : R), Eq (α := ℝ) ((v : (a : R) → ℝ) x : ℝ) (0 : ℝ) → x = 0
hc : 0 < c
rw : PowerSeries.gaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R) = 0 ↔ p = 0
⊢ gaussNorm v c p = 0 ↔ p = 0

Tactic:
rw [← gaussNorm_coe_powerSeries _ _ (le_of_lt hc)]

Premises used: le_of_lt, Polynomial.gaussNorm_coe_powerSeries
-- 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
h_eq_zero : ∀ (x : R), Eq (α := ℝ) ((v : (a : R) → ℝ) x : ℝ) (0 : ℝ) → x = 0
hc : 0 < c
⊢ Eq (α := ℝ) ((v : (a : R) → ℝ) 0 : ℝ) (0 : ℝ)

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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
h_eq_zero : ∀ (x : R), Eq (α := ℝ) ((v : (a : R) → ℝ) x : ℝ) (0 : ℝ) → x = 0
hc : 0 < c
⊢ ∀ (a : R), GE.ge (α := ℝ) ((v : (a : R) → ℝ) a : ℝ) (0 : ℝ)

Tactic:
simp
-- 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
h_eq_zero : ∀ (x : R), Eq (α := ℝ) ((v : (a : R) → ℝ) x : ℝ) (0 : ℝ) → x = 0
hc : 0 < c
⊢ PowerSeries.HasGaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R)

Tactic:
simpa [PowerSeries.HasGaussNorm] using aux_bdd v p

Premises used: PowerSeries.HasGaussNorm, _private.0.Polynomial.aux_bdd
-- 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
h_eq_zero : ∀ (x : R), Eq (α := ℝ) ((v : (a : R) → ℝ) x : ℝ) (0 : ℝ) → x = 0
hc : 0 < c
h : p = 0 ↔ (↑p : PowerSeries R) = 0
⊢ PowerSeries.gaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R) = 0 ↔ p = 0

Tactic:
convert!
    PowerSeries.gaussNorm_eq_zero_iff v c p (by grind) (by simp) h_eq_zero hc
      (by simpa [PowerSeries.HasGaussNorm] using aux_bdd v p)

Premises used: PowerSeries.gaussNorm_eq_zero_iff, Polynomial.toPowerSeries, DFunLike.coe
-- 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
h_eq_zero : ∀ (x : R), Eq (α := ℝ) ((v : (a : R) → ℝ) x : ℝ) (0 : ℝ) → x = 0
hc : 0 < c
⊢ p = 0 ↔ (↑p : PowerSeries R) = 0

Tactic:
Iff.symm coe_eq_zero_iff

Premises used: Polynomial.coe_eq_zero_iff, Iff.symm
-- 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
h_eq_zero : ∀ (x : R), Eq (α := ℝ) ((v : (a : R) → ℝ) x : ℝ) (0 : ℝ) → x = 0
hc : 0 < c
⊢ p = 0 ↔ (↑p : PowerSeries R) = 0

Tactic:
exact Iff.symm coe_eq_zero_iff

Premises used: Polynomial.coe_eq_zero_iff, Iff.symm
-- 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 : ℝ
p : R[X]
inst_2 : NonnegHomClass F R ℝ
hc : 0 ≤ c
pos : ∀ (hp : p.support.Nonempty), 0 ≤ gaussNorm v c p
neg : ∀ (hp : ¬p.support.Nonempty), 0 ≤ gaussNorm v c p
⊢ 0 ≤ gaussNorm v c p

Tactic:
by_cases hp : p.support.Nonempty

Premises used: Finset.Nonempty, Polynomial.support
-- 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 : ℝ
p : R[X]
inst_2 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : p.support.Nonempty
⊢ 0 ≤ gaussNorm v c p

Tactic:
simp_all [gaussNorm, sup'_nonneg_of_ne_zero, -Finset.le_sup'_iff]

Premises used: Finset.le_sup'_iff, _private.0.Polynomial.sup'_nonneg_of_ne_zero, 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 : ℝ
p : R[X]
inst_2 : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p.support.Nonempty
⊢ 0 ≤ gaussNorm v c p

Tactic:
simp_all [gaussNorm, sup'_nonneg_of_ne_zero, -Finset.le_sup'_iff]

Premises used: Finset.le_sup'_iff, _private.0.Polynomial.sup'_nonneg_of_ne_zero, 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
i : ℕ
rw :
  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)
⊢ HMul.hMul (α := ℝ) ((v : (a : R) → ℝ) (p.coeff i) : ℝ) (c ^ i) ≤ gaussNorm v c p

Tactic:
rw [← gaussNorm_coe_powerSeries _ _ hc, ← coeff_coe]

Premises used: Polynomial.gaussNorm_coe_powerSeries, Polynomial.coeff_coe
-- 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 : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
i : ℕ
hbd : PowerSeries.HasGaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R)
⊢ 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)

Tactic:
apply PowerSeries.le_gaussNorm

Premises used: PowerSeries.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
c : ℝ
p : R[X]
inst_2 : ZeroHomClass F R ℝ
inst_3 : NonnegHomClass F R ℝ
hc : 0 ≤ c
i : ℕ
⊢ PowerSeries.HasGaussNorm (⇑v : (a : R) → ℝ) c (↑p : PowerSeries R)

Tactic:
simpa [PowerSeries.HasGaussNorm] using aux_bdd v p

Premises used: PowerSeries.HasGaussNorm, _private.0.Polynomial.aux_bdd
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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 ℝ
⊢ 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:
aesop
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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 ℝ
⊢ 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
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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)
inr : ∀ (hcoeff0 : p.coeff 0 ≠ 0), gaussNorm v 0 p = (v : (a : R) → ℝ) (p.coeff 0)
⊢ gaussNorm v 0 p = (v : (a : R) → ℝ) (p.coeff 0)

Tactic:
rcases eq_or_ne (p.coeff 0) 0 with _ | hcoeff0

Premises used: Polynomial.coeff, 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
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
h : p.coeff 0 = 0
⊢ gaussNorm v 0 p = (v : (a : R) → ℝ) (p.coeff 0)

Tactic:
simp_all [gaussNorm]

Premises used: 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
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)
inr₁ : (v : (a : R) → ℝ) (p.coeff 0) ≤ gaussNorm v 0 p
⊢ gaussNorm v 0 p = (v : (a : R) → ℝ) (p.coeff 0)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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)

Tactic:
aesop (add norm (by simp [gaussNorm, Finset.sup'_le_iff]))

Premises used: Norm.norm
-- Module: Mathlib.RingTheory.Polynomial.GaussNorm
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
⊢ (v : (a : R) → ℝ) (p.coeff 0) ≤ gaussNorm v 0 p

Tactic:
grind [p.le_gaussNorm v (le_refl 0) 0]

Premises used: le_refl, Polynomial.le_gaussNorm, 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 ℝ
p : R[X]
hc : 0 ≤ c
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)}
⊢ 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

Premises used: Polynomial.exists_eq_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 ℝ
p : R[X]
hc : 0 ≤ c
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:
⟨i, Set.mem_setOf.mpr hi⟩

Premises used: Iff.mpr, Set.mem_setOf, Set.Nonempty, Exists.intro
-- 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
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:
exact ⟨i, Set.mem_setOf.mpr hi⟩
-- 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
⊢ 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⟩
-- 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)}
⊢ ∃ (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

Tactic:
⟨Nat.find h_nonempty, Nat.find_spec h_nonempty, ?_⟩

Premises used: And.intro, Nat.find, Exists.intro, Nat.find_spec
-- 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)}
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
⊢ ∃ (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

Tactic:
refine ⟨Nat.find h_nonempty, Nat.find_spec h_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 ℝ
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
⊢ ∀ 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

Premises used: Set.mem_setOf_eq, Nat.lt_find_iff
-- 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:
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