awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : (degree : (a : σ →₀ ℕ) → ℕ) x < n
⊢ 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)
have 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
Tactic: rw [← coeff_truncTotal _ hx, ← sub_eq_zero, ← MvPolynomial.coeff_sub]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : (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
have 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
Tactic: apply (MvPolynomial.mem_pow_idealOfVars_iff' n _).mp
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : (degree : (a : σ →₀ ℕ) → ℕ) x < 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
have 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
Tactic: rw [toAdicCompletion_apply_eq_mk_truncTotal, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : (degree : (a : σ →₀ ℕ) → ℕ) x < 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
have 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 * ⊤
Tactic: nth_rw 1 [← Ideal.mul_top (MvPolynomial.idealOfVars σ R ^ n), ← Ideal.Quotient.eq,
      Ideal.Quotient.mk_out]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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 :=
          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
have 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 * ⊤)
Tactic: nth_rw 1 [← Ideal.mul_top (MvPolynomial.idealOfVars σ R ^ n), ← Ideal.Quotient.eq,
      Ideal.Quotient.mk_out]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
p : 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))
have 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))
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
p : MvPolynomial σ R
⊢ 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))
have 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)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
p : MvPolynomial σ 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)
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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)
⊢ (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
have 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) ⊤
Tactic: rw [← Ideal.Quotient.mk_out (f.val n), Ideal.Quotient.mk_eq_mk_iff_sub_mem]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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)
⊢ 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) ⊤
have 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
Tactic: simp only [smul_eq_mul, Ideal.mul_top, MvPolynomial.mem_pow_idealOfVars_iff',
    MvPolynomial.coeff_sub]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ 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
have 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
Tactic: rw [coeff_truncTotal _ h, coeff_toAdicCompletionInv, ← MvPolynomial.coeff_sub]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ 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
have 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 : ℕ))
Tactic: apply (MvPolynomial.mem_pow_idealOfVars_iff' (degree x + 1) _).mp
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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 : ℕ))
⊢ 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
have a₁ : (degree : (a : σ →₀ ℕ) → ℕ) x < HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)
Tactic: apply (MvPolynomial.mem_pow_idealOfVars_iff' (degree x + 1) _).mp
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ 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 : ℕ))
have 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 : ℕ)))
        ⊤)
Tactic: nth_rw 1 [← Ideal.mul_top (MvPolynomial.idealOfVars σ R ^ (degree x + 1)),
      ← smul_eq_mul, ← Ideal.Quotient.eq]