-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
hs : IsLowerSet (↑s : Set (σ →₀ ℕ))
k : ℕ
p : MvPowerSeries σ R
n : ℕ
hmn : 1 ≤ n
ih :
  Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) n) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ n) : MvPolynomial σ R)
x : σ →₀ ℕ
hx : x ∈ s
pos :
  Eq.{u_2 + 1} (α := R)
    ((coeff x : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1)) :
      R)
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1))) : R)
pos₁ :
  Eq.{u_2 + 1} (α := R)
    ((coeff x : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1)) :
      R)
    ((coeff x : (a : MvPowerSeries σ R) → R) (p ^ (n + 1)) : R)
pos₂ :
  Eq.{u_2 + 1} (α := R)
    ((coeff x : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R)
            (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) n *
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R)) :
      R)
    ((coeff x : (a : MvPowerSeries σ R) → R) (p ^ (n + 1)) : R)
pos₃ :
  MvPolynomial.coeff x
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
            (HPow.hPow (α := MvPowerSeries σ R)
              (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) n) :
          MvPolynomial σ R)
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
            (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) :
          MvPolynomial σ R)) =
    (coeff x : (a : MvPowerSeries σ R) → R) (p ^ (n + 1))
pos₄ :
  MvPolynomial.coeff x
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ n) : MvPolynomial σ R)
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
            (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) :
          MvPolynomial σ R)) =
    (coeff x : (a : MvPowerSeries σ R) → R) (p ^ (n + 1))
⊢ Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff x
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1))))
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1))))
have pos₅ : MvPolynomial.coeff x
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ n) : MvPolynomial σ R)
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
  (coeff x : (a : MvPowerSeries σ R) → R) (p ^ (n + 1))
Tactic: rw [coeff_truncFinset_of_mem _ hx, coeff_truncFinset_of_mem _ hx, pow_succ,
        ← coeff_truncFinset_mul_truncFinset_eq_coeff_mul hs _ _ hx, ih, truncFinset_truncFinset
        (by rfl), pow_succ, coeff_truncFinset_mul_truncFinset_eq_coeff_mul hs _ _ hx]