-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
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
⊢ ⨅ (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)
have 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)
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 ..)