-- 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 : σ →₀ ℕ
inl :
  ∀
    (h :
      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 : ℕ)),
    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
inr :
  ∀
    (h :
      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 : ℕ)),
    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 : ℕ)) ≤
      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

Tactic:
rcases max_choice (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i)
        (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) with h | h

Premises used: max_choice, HMul.hMul, Finsupp.support, Finset.prod, HPow.hPow, MvPowerSeries.coeff, DFunLike.coe