-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
h h₁ :
  ∀ (d : τ →₀ ℕ)
    (hd :
      LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
        (⨅ (d : σ →₀ ℕ),
          ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
            ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d)),
    Eq.{u_5 + 1} (α := S) ((coeff d : (a : MvPowerSeries τ S) → S) (subst a f) : S) (0 : S)
h₂ h₃ :
  ∀ (d : τ →₀ ℕ)
    (hd :
      LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
        (⨅ (d : σ →₀ ℕ),
          ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
            ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d))
    (x : σ →₀ ℕ),
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff x : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff d : (a : MvPowerSeries τ S) → S) (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
      0
pos :
  ∀ (d : τ →₀ ℕ)
    (hd :
      LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
        (⨅ (d : σ →₀ ℕ),
          ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
            ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d))
    (x : σ →₀ ℕ) (hfx : Eq.{u_3 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff x : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff d : (a : MvPowerSeries τ S) → S) (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
      0
neg neg₁ :
  ∀ (d : τ →₀ ℕ)
    (hd :
      LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
        (⨅ (d : σ →₀ ℕ),
          ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
            ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d))
    (x : σ →₀ ℕ) (hfx : ¬Eq.{u_3 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff x : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff d : (a : MvPowerSeries τ S) → S) (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
      0
neg₂ :
  ∀ (d : τ →₀ ℕ)
    (hd :
      LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
        (⨅ (d : σ →₀ ℕ),
          ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
            ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d))
    (x : σ →₀ ℕ) (hfx : ¬Eq.{u_3 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
    (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞) <
      weightedOrder.{u_4, u_5} (R := S) w (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e)
neg₃ :
  ∀ (d : τ →₀ ℕ)
    (hd :
      LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
        (⨅ (d : σ →₀ ℕ),
          ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
            ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d))
    (x : σ →₀ ℕ) (hfx : ¬Eq.{u_3 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
    LE.le (α := ℕ∞) (((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) x : ℕ∞)
      (∑ i ∈ x.support, weightedOrder.{u_4, u_5} (R := S) w ((fun (s : σ) (e : ℕ) ↦ a s ^ e) i ((x : (a : σ) → ℕ) i)) :
        ℕ∞)
neg₄ :
  ∀ (d : τ →₀ ℕ)
    (hd :
      LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
        (⨅ (d : σ →₀ ℕ),
          ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
            ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d))
    (x : σ →₀ ℕ) (hfx : ¬Eq.{u_3 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
    LE.le (α := ℕ∞) (∑ x_1 ∈ x.support, HSMul.hSMul (α := ℕ) ((x : (a : σ) → ℕ) x_1 : ℕ) (weightedOrder w (a x_1)))
      (∑ x_1 ∈ x.support, weightedOrder w (HPow.hPow (β := ℕ) (a x_1) ((x : (a : σ) → ℕ) x_1 : ℕ)))
⊢ ⨅ (d : σ →₀ ℕ),
      ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
        ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d ≤
    weightedOrder w (subst a f)

Tactic:
classical
  apply MvPowerSeries.le_weightedOrder
  intro d hd
  rw [coeff_subst ha, finsum_eq_zero_of_forall_eq_zero]
  intro x
  by_cases hfx : f.coeff x = 0
  · simp [hfx]
  rw [coeff_eq_zero_of_lt_weightedOrder w, smul_zero]
  refine hd.trans_le (((biInf_le _ hfx).trans ?_).trans (le_weightedOrder_prod ..))
  simp only [Finsupp.weight_apply, Finsupp.sum, Function.comp_apply]
  exact Finset.sum_le_sum fun i hi ↦ .trans (by simp) (le_weightedOrder_pow ..)

Premises used: Finsupp.sum, MvPowerSeries.le_weightedOrder_pow, smul_zero, MvPowerSeries.coeff_subst, MvPowerSeries.le_weightedOrder, Finset.sum_le_sum, Function.comp_apply, LE.le.trans, finsum_eq_zero_of_forall_eq_zero, MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder, Finsupp.weight_apply