-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
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))
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))
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 * p)
pos₇ pos₈ :
  Eq.{u_2 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) (p ^ n * p) : R)
    ((coeff x : (a : MvPowerSeries σ R) → R) (p ^ n * p) : R)
⊢ 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))))

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]

Premises used: pow_succ, MvPowerSeries.coeff_truncFinset_of_mem, MvPowerSeries.coeff_truncFinset_mul_truncFinset_eq_coeff_mul, MvPowerSeries.truncFinset_truncFinset