awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vNonneg : ∀ (a : R), v a ≥ 0
pos :
  ∀ (h : HasGaussNorm v c f),
    LE.le (α := ℝ) 0
      (⨆ (t : σ →₀ ℕ), v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2)
neg :
  ∀ (h : ¬HasGaussNorm v c f),
    LE.le (α := ℝ) 0
      (⨆ (t : σ →₀ ℕ), v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2)
⊢ LE.le (α := ℝ) 0
    (⨆ (t : σ →₀ ℕ), v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2)

Tactic:
by_cases h : HasGaussNorm v c f

Premises used: MvPowerSeries.HasGaussNorm
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vNonneg : ∀ (a : R), v a ≥ 0
h : HasGaussNorm v c f
trans : 0 ≤ v ((constantCoeff : (a : MvPowerSeries σ R) → R) f)
trans₁ :
  v ((constantCoeff : (a : MvPowerSeries σ R) → R) f) ≤
    ⨆ (t : σ →₀ ℕ), v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2
⊢ LE.le (α := ℝ) 0
    (⨆ (t : σ →₀ ℕ), v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2)

Tactic:
trans v (constantCoeff f)

Premises used: MvPowerSeries.constantCoeff, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vNonneg : ∀ (a : R), v a ≥ 0
h : HasGaussNorm v c f
⊢ 0 ≤ v ((constantCoeff : (a : MvPowerSeries σ R) → R) f)

Tactic:
simp [vNonneg]
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vNonneg : ∀ (a : R), v a ≥ 0
h : HasGaussNorm v c f
⊢ (v ((coeff 0 : (a : MvPowerSeries σ R) → R) f) * Finsupp.prod 0 fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2) ≤ gaussNorm v c f

Tactic:
(le_gaussNorm v c f h 0)

Premises used: OfNat.ofNat, MvPowerSeries.le_gaussNorm
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vNonneg : ∀ (a : R), v a ≥ 0
h : HasGaussNorm v c f
h₁ :
  v ((constantCoeff : (a : MvPowerSeries σ R) → R) f) =
    v ((coeff 0 : (a : MvPowerSeries σ R) → R) f) * Finsupp.prod 0 fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2
⊢ v ((constantCoeff : (a : MvPowerSeries σ R) → R) f) ≤
    ⨆ (t : σ →₀ ℕ), v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2

Tactic:
convert! (le_gaussNorm v c f h 0)

Premises used: OfNat.ofNat, MvPowerSeries.le_gaussNorm
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vNonneg : ∀ (a : R), v a ≥ 0
h : HasGaussNorm v c f
⊢ v ((constantCoeff : (a : MvPowerSeries σ R) → R) f) =
    v ((coeff 0 : (a : MvPowerSeries σ R) → R) f) * Finsupp.prod 0 fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vNonneg : ∀ (a : R), v a ≥ 0
h : ¬HasGaussNorm v c f
⊢ LE.le (α := ℝ) 0
    (⨆ (t : σ →₀ ℕ), v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f = 0
⊢ gaussNorm v c f = 0

Tactic:
simp [hf, vZero]
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
refine : gaussNorm v c f = 0 → f = 0
⊢ gaussNorm v c f = 0 ↔ f = 0

Tactic:
refine ⟨?_, fun hf ↦ by simp [hf, vZero]⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
contrapose! : f ≠ 0 → gaussNorm v c f ≠ 0
⊢ gaussNorm v c f = 0 → f = 0

Tactic:
contrapose!
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
h : 0 < gaussNorm v c f
⊢ gaussNorm v c f ≠ 0

Tactic:
apply ne_of_gt

Premises used: ne_of_gt
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
h :
  ∀ (n : σ →₀ ℕ) (hn : Ne.{u_1 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
    0 < gaussNorm v c f
⊢ 0 < gaussNorm v c f

Tactic:
obtain ⟨n, hn⟩ := (MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero f).mp hf

Premises used: Iff.mp, MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
n : σ →₀ ℕ
hn : Ne.{u_1 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ LT.lt (α := ℝ) 0 (∏ i ∈ n.support, HPow.hPow (β := ℕ) (c i) ((n : (a : σ) → ℕ) i : ℕ))

Tactic:
Finset.prod_pos fun i a ↦ (fun i ↦ pow_pos (hc i) (n i)) i

Premises used: pow_pos, Finset.prod_pos, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
n : σ →₀ ℕ
hn : Ne.{u_1 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ LT.lt (α := ℝ) 0 (∏ i ∈ n.support, HPow.hPow (β := ℕ) (c i) ((n : (a : σ) → ℕ) i : ℕ))

Tactic:
exact Finset.prod_pos fun i a ↦ (fun i ↦ pow_pos (hc i) (n i)) i

Premises used: pow_pos, Finset.prod_pos, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
n : σ →₀ ℕ
hn : Ne.{u_1 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
apply : 0 < v ((coeff n : (a : MvPowerSeries σ R) → R) f)
⊢ 0 <
    v ((coeff n : (a : MvPowerSeries σ R) → R) f) * ∏ i ∈ n.support, HPow.hPow (β := ℕ) (c i) ((n : (a : σ) → ℕ) i : ℕ)

Tactic:
apply mul_pos _ (by exact Finset.prod_pos fun i a ↦ (fun i ↦ pow_pos (hc i) (n i)) i)

Premises used: mul_pos
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
n : σ →₀ ℕ
hn : Ne.{u_1 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ v ((coeff n : (a : MvPowerSeries σ R) → R) f) = 0 →
    Eq.{u_1 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
specialize h_eq_zero (f.coeff n)

Premises used: MvPowerSeries.coeff, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
n : σ →₀ ℕ
hn : Ne.{u_1 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
h_eq_zero :
  v ((coeff n : (a : MvPowerSeries σ R) → R) f) = 0 →
    Eq.{u_1 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ 0 < v ((coeff n : (a : MvPowerSeries σ R) → R) f)

Tactic:
grind
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
n : σ →₀ ℕ
hn : Ne.{u_1 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ v ((coeff n : (a : MvPowerSeries σ R) → R) f) * ∏ i ∈ n.support, HPow.hPow (β := ℕ) (c i) ((n : (a : σ) → ℕ) i : ℕ) ≤
    gaussNorm v c f

Tactic:
le_gaussNorm v c f hbd n

Premises used: Finsupp.prod, MvPowerSeries.le_gaussNorm
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
n : σ →₀ ℕ
hn : Ne.{u_1 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
v₁ :
  0 <
    v ((coeff n : (a : MvPowerSeries σ R) → R) f) * ∏ i ∈ n.support, HPow.hPow (β := ℕ) (c i) ((n : (a : σ) → ℕ) i : ℕ)
⊢ 0 < gaussNorm v c f

Tactic:
calc
  0 < v (f.coeff n) * ∏ i ∈ n.support, (c i) ^ (n i) := by
    apply mul_pos _ (by exact Finset.prod_pos fun i a ↦ (fun i ↦ pow_pos (hc i) (n i)) i)
    specialize h_eq_zero (f.coeff n)
    grind
  _ ≤ _ := le_gaussNorm v c f hbd n

Premises used: Finsupp.support, MvPowerSeries.coeff, DFunLike.coe, MvPowerSeries.le_gaussNorm
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : ∀ (x y : R), v (x + y) ≤ max (v x) (v y)
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
⊢ ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))

Tactic:
have H (t : σ →₀ ℕ) : 0 ≤ ∏ i ∈ t.support, c i ^ t i :=
    Finset.prod_nonneg (fun i hi ↦ pow_nonneg (hc i) (t i))
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : ∀ (x y : R), v (x + y) ≤ max (v x) (v y)
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
⊢ v
      (HAdd.hAdd (α := R) (β := R) ((coeff t : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff t : (a : MvPowerSeries σ R) → R) g : R)) ≤
    max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g))

Tactic:
specialize hv (coeff t f) (coeff t g)

Premises used: MvPowerSeries.coeff, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
hv :
  v
      (HAdd.hAdd (α := R) (β := R) ((coeff t : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff t : (a : MvPowerSeries σ R) → R) g : R)) ≤
    max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g))
inl :
  ∀
    (h :
      max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g)) =
        v ((coeff t : (a : MvPowerSeries σ R) → R) f)),
    v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
      max
        (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
        (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
inr :
  ∀
    (h :
      max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g)) =
        v ((coeff t : (a : MvPowerSeries σ R) → R) g)),
    v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
      max
        (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
        (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
⊢ v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
      ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
    max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))

Tactic:
rcases max_choice (v ((coeff t) f)) (v ((coeff t) g)) with h | h

Premises used: max_choice, MvPowerSeries.coeff, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
hv :
  v
      (HAdd.hAdd (α := R) (β := R) ((coeff t : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff t : (a : MvPowerSeries σ R) → R) g : R)) ≤
    max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g))
h :
  max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) f)
simp :
  v ((coeff t : (a : MvPowerSeries σ R) → R) g) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
    v ((coeff t : (a : MvPowerSeries σ R) → R) f) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)
⊢ max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) f) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)

Tactic:
simp only [sup_eq_left]

Premises used: sup_eq_left
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
hv :
  v
      (HAdd.hAdd (α := R) (β := R) ((coeff t : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff t : (a : MvPowerSeries σ R) → R) g : R)) ≤
    max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g))
h :
  max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) f)
⊢ v ((coeff t : (a : MvPowerSeries σ R) → R) g) ≤ v ((coeff t : (a : MvPowerSeries σ R) → R) f)

Tactic:
aesop
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
hv :
  v
      (HAdd.hAdd (α := R) (β := R) ((coeff t : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff t : (a : MvPowerSeries σ R) → R) g : R)) ≤
    max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g))
h :
  max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) f)
⊢ LE.le (α := ℝ) (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
    (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))

Tactic:
aesop
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
hv :
  v
      (HAdd.hAdd (α := R) (β := R) ((coeff t : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff t : (a : MvPowerSeries σ R) → R) g : R)) ≤
    max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g))
h :
  max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) f)
⊢ 0 ≤ v ((coeff t : (a : MvPowerSeries σ R) → R) g)

Tactic:
aesop
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
hv :
  v
      (HAdd.hAdd (α := R) (β := R) ((coeff t : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff t : (a : MvPowerSeries σ R) → R) g : R)) ≤
    max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g))
h :
  max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) f)
⊢ v ((coeff t : (a : MvPowerSeries σ R) → R) g) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
    v ((coeff t : (a : MvPowerSeries σ R) → R) f) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)

Tactic:
exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)

Premises used: mul_le_mul_of_nonneg
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
hv :
  v
      (HAdd.hAdd (α := R) (β := R) ((coeff t : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff t : (a : MvPowerSeries σ R) → R) g : R)) ≤
    max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g))
h :
  max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) f)
⊢ max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) f) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)

Tactic:
have : max (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i)
          (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) =
          (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i) := by
        simp only [sup_eq_left]
        exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
hv :
  v
      (HAdd.hAdd (α := R) (β := R) ((coeff t : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff t : (a : MvPowerSeries σ R) → R) g : R)) ≤
    max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g))
h :
  max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) f)
this :
  max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) f) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)
inl :
  v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
      ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
    v ((coeff t : (a : MvPowerSeries σ R) → R) f) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)
⊢ v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
      ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
    max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))

Tactic:
simp_rw [this]
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
hv :
  v
      (HAdd.hAdd (α := R) (β := R) ((coeff t : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff t : (a : MvPowerSeries σ R) → R) g : R)) ≤
    max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g))
h :
  max (v ((coeff t : (a : MvPowerSeries σ R) → R) f)) (v ((coeff t : (a : MvPowerSeries σ R) → R) g)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) f)
this :
  max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) f) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)
⊢ v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) ≤ v ((coeff t : (a : MvPowerSeries σ R) → R) f)

Tactic:
aesop