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 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 : ℕ)
⊢ 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)
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 : ℕ)
⊢ 0 ≤ v ((coeff t : (a : MvPowerSeries σ R) → R) (f + 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)
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)) *
      ∏ 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) g)
simp :
  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 : ℕ)
⊢ 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) g) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)

Tactic:
simp only [sup_eq_right]

Premises used: sup_eq_right
-- 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) g)
⊢ v ((coeff t : (a : MvPowerSeries σ R) → R) f) ≤ 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) g)
⊢ 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) g)
⊢ 0 ≤ 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) g)
⊢ 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:
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) g)
⊢ 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) g) * ∏ 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) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) := by
        simp only [sup_eq_right]
        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) g)
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) g) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)
inr :
  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) 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:
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) g)
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) g) * ∏ 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) 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) g)
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) g) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)
⊢ 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) g)
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) g) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)
⊢ 0 ≤ v ((coeff t : (a : MvPowerSeries σ R) → R) (f + 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) g)
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) 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 : ℕ) ≤
    v ((coeff t : (a : MvPowerSeries σ R) → R) g) * ∏ 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
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 ((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:
have Final (t : σ →₀ ℕ) : v ((coeff t) (f + g)) * ∏ i ∈ t.support, c ↑i ^ t ↑i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i)
      (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) := by
    specialize hv (coeff t f) (coeff t g)
    rcases max_choice (v ((coeff t) f)) (v ((coeff t) g)) with h | h
    · 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)
      simp_rw [this]
      exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)
    · 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) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) := by
        simp only [sup_eq_right]
        exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)
      simp_rw [this]
      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
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 : ℕ))
Final :
  ∀ (t : σ →₀ ℕ),
    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 : ℕ))
⊢ gaussNorm v c (f + g) ≤ max (gaussNorm v c f) (gaussNorm v c g)

Tactic:
Real.iSup_le ?_ ?_

Premises used: Real.iSup_le, MvPowerSeries.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
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
Final :
  ∀ (t : σ →₀ ℕ),
    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 : ℕ))
refine_1 :
  ∀ (i : σ →₀ ℕ),
    (v ((coeff i : (a : MvPowerSeries σ R) → R) (f + g)) * i.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2) ≤
      max (gaussNorm v c f) (gaussNorm v c g)
refine_2 : 0 ≤ max (gaussNorm v c f) (gaussNorm v c g)
⊢ gaussNorm v c (f + g) ≤ max (gaussNorm v c f) (gaussNorm v c g)

Tactic:
refine Real.iSup_le ?_ ?_

Premises used: Real.iSup_le
-- 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 : ℕ))
Final :
  ∀ (t : σ →₀ ℕ),
    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 : ℕ))
t : σ →₀ ℕ
simp :
  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 : ℕ)) ≤
      gaussNorm v c 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 : ℕ)) ≤
      gaussNorm v c g
⊢ 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 : ℕ)) ≤
    max (gaussNorm v c f) (gaussNorm v c g)

Tactic:
simp only [le_sup_iff]

Premises used: le_sup_iff