-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : (degree : (a : σ →₀ ℕ) → ℕ) x < n
a :
  HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      (Quotient.out (s :=
          Submodule.quotientRel (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤))
          ((Ideal.Quotient.mk (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤) :
              (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤)
            ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p)) :
        MvPolynomial σ R)
      ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R) ∈
    HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤
a₁ :
  Eq (α := MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤)
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤)
        (Quotient.out (s :=
          Submodule.quotientRel (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤))
          ((Ideal.Quotient.mk (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤) :
              (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤)
            ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p))) :
      MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤)
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) :
      MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤)
a₂ a₃ :
  Eq (α := MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤)
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) :
      MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤)
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) :
      MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤)
⊢ HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      (Quotient.out (s :=
          Submodule.quotientRel (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤))
          ((Ideal.Quotient.mk (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n * ⊤) :
              (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤)
            ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p)) :
        MvPolynomial σ R)
      ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R) ∈
    HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n

Tactic:
nth_rw 1 [← Ideal.mul_top (MvPolynomial.idealOfVars σ R ^ n), ← Ideal.Quotient.eq,
      Ideal.Quotient.mk_out]

Premises used: Ideal.Quotient.eq, HPow.hPow, Ideal.Quotient.mk_out, Ideal.mul_top, MvPolynomial.idealOfVars