awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ_1 : Type u_1
R_1 : Type u_2
n_1 : ℕ
inst : CommRing R_1
inst_1 : Finite σ_1
σ : Type u_3
R : Type u_4
inst_2 : Finite σ
inst_3 : CommRing R
n : ℕ
p : MvPolynomial σ R
x : σ →₀ ℕ
h : (degree : (a : σ →₀ ℕ) → ℕ) x < n
rw :
  MvPolynomial.coeff x ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) -
      MvPolynomial.coeff x p =
    0
rw₁ :
  MvPolynomial.coeff x ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) =
    MvPolynomial.coeff x p
rw₂ : (coeff x : (a : MvPowerSeries σ R) → R) (↑p : MvPowerSeries σ R) = MvPolynomial.coeff x p
rw₃ rw₄ : MvPolynomial.coeff x p = MvPolynomial.coeff x p
⊢ MvPolynomial.coeff x
      (HSub.hSub (α := MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) : MvPolynomial σ R) p) =
    0

Tactic:
rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ h, MvPolynomial.coeff_coe]

Premises used: sub_eq_zero, MvPowerSeries.coeff_truncTotal, MvPolynomial.coeff_coe, MvPolynomial.coeff_sub
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ_1 : Type u_1
R_1 : Type u_2
n : ℕ
inst : CommRing R_1
inst_1 : Finite σ_1
σ : Type u_3
R : Type u_4
inst_2 : Finite σ
inst_3 : CommRing R
m n_1 : ℕ
h : m ≤ n_1
x : MvPowerSeries σ R
⊢ Eq (α := MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) m)
    ((AlgHom.comp (Ideal.Quotient.factorₐ (MvPolynomial σ R) ⋯) (truncTotalAlgHom σ R n_1) :
          (a : MvPowerSeries σ R) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ m)
        x :
      MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) m)
    ((truncTotalAlgHom σ R m : (a : MvPowerSeries σ R) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ m) x :
      MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) m)

Tactic:
simpa [Ideal.Quotient.mk_eq_mk_iff_sub_mem] using
        truncTotal_sub_truncTotal_mem_pow_idealOfVars h (le_refl _) _

Premises used: le_refl, MvPowerSeries.truncTotal_sub_truncTotal_mem_pow_idealOfVars, Ideal.Quotient.mk_eq_mk_iff_sub_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
n : ℕ
p : MvPowerSeries σ R
⊢ Eq (α :=
    MvPolynomial σ R ⧸
      HSMul.hSMul (β := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
        (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤)
    ((↑((toAdicCompletion σ R :
                (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
              p) :
          (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
        n :
      MvPolynomial σ R ⧸
        HSMul.hSMul (β := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
          (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤)
    ((Ideal.Quotient.mk
            (HSMul.hSMul (β := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
              (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 ⧸
        HSMul.hSMul (β := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
          (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤)

Tactic:
rfl
-- 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
rw :
  MvPolynomial.coeff x
      (HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        (Quotient.out (s :=
            (HSMul.hSMul (β := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
                (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤).quotientRel)
            ((↑((toAdicCompletion σ R :
                      (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
                    p) :
                (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
              n) :
          MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    0
⊢ Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff x
        (Quotient.out (s :=
          (HSMul.hSMul (β := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
              (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤).quotientRel)
          ((↑((toAdicCompletion σ R :
                    (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
                  p) :
              (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
            n)) :
      R)
    ((coeff x : (a : MvPowerSeries σ R) → R) p : R)

Tactic:
rw [← coeff_truncTotal _ hx, ← sub_eq_zero, ← MvPolynomial.coeff_sub]

Premises used: sub_eq_zero, MvPowerSeries.coeff_truncTotal, MvPolynomial.coeff_sub
-- 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 :=
          (HSMul.hSMul (β := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
              (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤).quotientRel)
          ((↑((toAdicCompletion σ R :
                    (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
                  p) :
              (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
            n) :
        MvPolynomial σ R)
      ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R) ∈
    HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n
a₁ : (degree : (a : σ →₀ ℕ) → ℕ) x < n
⊢ MvPolynomial.coeff x
      (HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        (Quotient.out (s :=
            (HSMul.hSMul (β := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
                (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤).quotientRel)
            ((↑((toAdicCompletion σ R :
                      (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
                    p) :
                (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
              n) :
          MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    0

Tactic:
apply (MvPolynomial.mem_pow_idealOfVars_iff' n _).mp

Premises used: MvPolynomial.mem_pow_idealOfVars_iff', Iff.mp
-- 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
⊢ HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      (Quotient.out (s :=
          (HSMul.hSMul (β := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
              (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤).quotientRel)
          ((↑((toAdicCompletion σ R :
                    (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
                  p) :
              (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
            n) :
        MvPolynomial σ R)
      ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R) ∈
    HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n

Tactic:
rw [toAdicCompletion_apply_eq_mk_truncTotal, smul_eq_mul]

Premises used: MvPowerSeries.toAdicCompletion_apply_eq_mk_truncTotal, smul_eq_mul
-- 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
⊢ (degree : (a : σ →₀ ℕ) → ℕ) x < n

Tactic:
hx
-- 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
⊢ (degree : (a : σ →₀ ℕ) → ℕ) x < n

Tactic:
exact hx
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
p : MvPolynomial σ R
symm :
  Eq (α := AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    ((AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R) :
          (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
        p :
      AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    ((toAdicCompletion σ R : (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
        (↑p : MvPowerSeries σ R) :
      AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
⊢ Eq (α := AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    ((toAdicCompletion σ R : (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
        (↑p : MvPowerSeries σ R) :
      AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    ((AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R) :
          (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
        p :
      AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))

Tactic:
symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
p : MvPolynomial σ R
h :
  ∀ (n : ℕ),
    Eq (α :=
      MvPolynomial σ R ⧸
        HSMul.hSMul (β := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
          (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤)
      ((↑((AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R) :
                (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
              p) :
          (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
        n)
      ((↑((toAdicCompletion σ R :
                (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
              (↑p : MvPowerSeries σ R)) :
          (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
        n)
⊢ Eq (α := AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    ((AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R) :
          (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
        p :
      AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    ((toAdicCompletion σ R : (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
        (↑p : MvPowerSeries σ R) :
      AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))

Tactic:
ext n
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
p : MvPolynomial σ R
n : ℕ
this :
  HSub.hSub (β := MvPolynomial σ R) p
      ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) : MvPolynomial σ R) ∈
    HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n
⊢ Eq (α :=
    MvPolynomial σ R ⧸
      HSMul.hSMul (β := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
        (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤)
    ((↑((AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R) :
              (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
            p) :
        (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
      n)
    ((↑((toAdicCompletion σ R :
              (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
            (↑p : MvPowerSeries σ R)) :
        (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
      n)

Tactic:
simpa [toAdicCompletion, AdicCompletion.liftAlgHom, AdicCompletion.liftRingHom,
      Ideal.Quotient.mk_eq_mk_iff_sub_mem]

Premises used: AdicCompletion.liftRingHom, AdicCompletion.liftAlgHom, MvPowerSeries.toAdicCompletion, Ideal.Quotient.mk_eq_mk_iff_sub_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
p : MvPolynomial σ R
n : ℕ
h :
  HSub.hSub (β := MvPolynomial σ R) p
      ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) : MvPolynomial σ R) ∈
    HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n
⊢ Eq (α :=
    MvPolynomial σ R ⧸
      HSMul.hSMul (β := Submodule (MvPolynomial σ R) (MvPolynomial σ R))
        (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤)
    ((↑((AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R) :
              (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
            p) :
        (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
      n)
    ((↑((toAdicCompletion σ R :
              (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
            (↑p : MvPowerSeries σ R)) :
        (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
      n)

Tactic:
suffices p - (truncTotal n) p ∈ MvPolynomial.idealOfVars σ R ^ n by
    simpa [toAdicCompletion, AdicCompletion.liftAlgHom, AdicCompletion.liftRingHom,
      Ideal.Quotient.mk_eq_mk_iff_sub_mem]
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
p : MvPolynomial σ R
n : ℕ
x : σ →₀ ℕ
hx : (degree : (a : σ →₀ ℕ) → ℕ) x < n
⊢ MvPolynomial.coeff x
      (HSub.hSub (β := MvPolynomial σ R) p
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) : MvPolynomial σ R)) =
    0

Tactic:
simp [coeff_truncTotal _ hx]

Premises used: MvPowerSeries.coeff_truncTotal
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
p : MvPolynomial σ R
n : ℕ
⊢ HSub.hSub (β := MvPolynomial σ R) p
      ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) : MvPolynomial σ R) ∈
    HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n

Tactic:
exact (MvPolynomial.mem_pow_idealOfVars_iff' ..).mpr fun x hx ↦ by simp [coeff_truncTotal _ hx]

Premises used: Iff.mpr, MvPolynomial.mem_pow_idealOfVars_iff'
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
x : σ →₀ ℕ
f : AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
⊢ (coeff x : (a : MvPowerSeries σ R) → R) (toAdicCompletionInv σ R f) =
    MvPolynomial.coeff x
      (Quotient.out
        ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
          (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ))))

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
n : ℕ
f : AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
rw :
  HSub.hSub (α := MvPolynomial σ R)
      ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (toAdicCompletionInv σ R f) : MvPolynomial σ R)
      (Quotient.out ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤) n)) ∈
    HSMul.hSMul (β := Ideal (MvPolynomial σ R))
      (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤
⊢ (Ideal.Quotient.mk
          (HSMul.hSMul (β := Ideal (MvPolynomial σ R))
            (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) (toAdicCompletionInv σ R f)) =
    (↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤) n

Tactic:
rw [← Ideal.Quotient.mk_out (f.val n), Ideal.Quotient.mk_eq_mk_iff_sub_mem]

Premises used: Ideal.Quotient.mk_out, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Subtype.val
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
n : ℕ
f : AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
simp :
  ∀ (x : σ →₀ ℕ),
    (degree : (a : σ →₀ ℕ) → ℕ) x < n →
      MvPolynomial.coeff x ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (toAdicCompletionInv σ R f)) -
          MvPolynomial.coeff x
            (Quotient.out ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤) n)) =
        0
⊢ HSub.hSub (α := MvPolynomial σ R)
      ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (toAdicCompletionInv σ R f) : MvPolynomial σ R)
      (Quotient.out ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤) n)) ∈
    HSMul.hSMul (β := Ideal (MvPolynomial σ R))
      (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤

Tactic:
simp only [smul_eq_mul, Ideal.mul_top, MvPolynomial.mem_pow_idealOfVars_iff',
    MvPolynomial.coeff_sub]

Premises used: MvPolynomial.mem_pow_idealOfVars_iff', MvPolynomial.coeff_sub, smul_eq_mul, Ideal.mul_top
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
n : ℕ
f : AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : (degree : (a : σ →₀ ℕ) → ℕ) x < n
rw :
  MvPolynomial.coeff x
      (Quotient.out
          ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
            (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ))) -
        Quotient.out ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤) n)) =
    0
⊢ MvPolynomial.coeff x ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (toAdicCompletionInv σ R f)) -
      MvPolynomial.coeff x (Quotient.out ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤) n)) =
    0

Tactic:
rw [coeff_truncTotal _ h, coeff_toAdicCompletionInv, ← MvPolynomial.coeff_sub]

Premises used: MvPowerSeries.coeff_toAdicCompletionInv, MvPowerSeries.coeff_truncTotal, MvPolynomial.coeff_sub
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
n : ℕ
f : AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : (degree : (a : σ →₀ ℕ) → ℕ) x < n
a :
  Quotient.out
        ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
          (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ))) -
      Quotient.out ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤) n) ∈
    HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R)
      (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ))
a₁ : (degree : (a : σ →₀ ℕ) → ℕ) x < HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)
⊢ MvPolynomial.coeff x
      (Quotient.out
          ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
            (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ))) -
        Quotient.out ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤) n)) =
    0

Tactic:
apply (MvPolynomial.mem_pow_idealOfVars_iff' (degree x + 1) _).mp

Premises used: Finsupp.degree, MvPolynomial.mem_pow_idealOfVars_iff', HAdd.hAdd, Iff.mp, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
n : ℕ
f : AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : (degree : (a : σ →₀ ℕ) → ℕ) x < n
a :
  Eq (α :=
    MvPolynomial σ R ⧸
      HSMul.hSMul (β := Ideal (MvPolynomial σ R))
        (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R)
          (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)))
        ⊤)
    ((Ideal.Quotient.mk
            (HSMul.hSMul (β := Ideal (MvPolynomial σ R))
              (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R)
                (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)))
              ⊤) :
          (a : MvPolynomial σ R) →
            MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ ((degree : (a : σ →₀ ℕ) → ℕ) x + 1) • ⊤)
        (Quotient.out
          ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
            (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)))) :
      MvPolynomial σ R ⧸
        HSMul.hSMul (β := Ideal (MvPolynomial σ R))
          (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R)
            (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)))
          ⊤)
    ((Ideal.Quotient.mk
            (HSMul.hSMul (β := Ideal (MvPolynomial σ R))
              (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R)
                (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)))
              ⊤) :
          (a : MvPolynomial σ R) →
            MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ ((degree : (a : σ →₀ ℕ) → ℕ) x + 1) • ⊤)
        (Quotient.out ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤) n)) :
      MvPolynomial σ R ⧸
        HSMul.hSMul (β := Ideal (MvPolynomial σ R))
          (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R)
            (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)))
          ⊤)
⊢ Quotient.out
        ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
          (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ))) -
      Quotient.out ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤) n) ∈
    HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R)
      (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ))

Tactic:
nth_rw 1 [← Ideal.mul_top (MvPolynomial.idealOfVars σ R ^ (degree x + 1)),
      ← smul_eq_mul, ← Ideal.Quotient.eq]

Premises used: Finsupp.degree, Ideal.Quotient.eq, HPow.hPow, HAdd.hAdd, smul_eq_mul, Ideal.mul_top, OfNat.ofNat, MvPolynomial.idealOfVars, DFunLike.coe