awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
p : MvPolynomial σ R
⊢ Eq (α := MvPowerSeries σ A)
    ((algebraMap (MvPolynomial σ R) (MvPowerSeries σ A) : (a : MvPolynomial σ R) → MvPowerSeries σ A) p :
      MvPowerSeries σ A)
    ((map (algebraMap R A) : (a : MvPowerSeries σ R) → MvPowerSeries σ A) (↑p : MvPowerSeries σ R) : MvPowerSeries σ A)

Tactic:
rfl

Premises used: MvPolynomial.toMvPowerSeries, MvPolynomial.coeff, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
f : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries σ A)
    ((algebraMap (MvPowerSeries σ R) (MvPowerSeries σ A) : (a : MvPowerSeries σ R) → MvPowerSeries σ A) f :
      MvPowerSeries σ A)
    ((map (algebraMap R A) : (a : MvPowerSeries σ R) → MvPowerSeries σ A) f : MvPowerSeries σ A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
l m n : ℕ
h : l ≤ m
h' : l ≤ n
p : MvPowerSeries σ R
⊢ HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((truncTotal m : (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) l

Tactic:
(MvPolynomial.mem_pow_idealOfVars_iff' ..).mpr (fun x 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
inst_1 : Finite σ
l m n : ℕ
h : l ≤ m
h' : l ≤ n
p : MvPowerSeries σ R
refine :
  ∀ (x : σ →₀ ℕ) (hx : (degree : (a : σ →₀ ℕ) → ℕ) x < l),
    MvPolynomial.coeff x
        (HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((truncTotal m : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
          ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
      0
⊢ HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((truncTotal m : (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) l

Tactic:
refine (MvPolynomial.mem_pow_idealOfVars_iff' ..).mpr (fun x 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
inst_1 : Finite σ
l m n : ℕ
h : l ≤ m
h' : l ≤ n
p : MvPowerSeries σ R
x : σ →₀ ℕ
hx : (degree : (a : σ →₀ ℕ) → ℕ) x < l
⊢ (degree : (a : σ →₀ ℕ) → ℕ) x < m

Tactic:
lia
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
l m n : ℕ
h : l ≤ m
h' : l ≤ n
p : MvPowerSeries σ R
x : σ →₀ ℕ
hx : (degree : (a : σ →₀ ℕ) → ℕ) x < l
⊢ (degree : (a : σ →₀ ℕ) → ℕ) x < n

Tactic:
lia
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
l m n : ℕ
h : l ≤ m
h' : l ≤ n
p : MvPowerSeries σ R
x : σ →₀ ℕ
hx : (degree : (a : σ →₀ ℕ) → ℕ) x < l
rw :
  HSub.hSub (α := R) (MvPolynomial.coeff x ((truncTotal m : (a : MvPowerSeries σ R) → MvPolynomial σ R) p))
      (MvPolynomial.coeff x ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p)) =
    0
rw₁ :
  Eq.{u_2 + 1} (α := R) (MvPolynomial.coeff x ((truncTotal m : (a : MvPowerSeries σ R) → MvPolynomial σ R) p))
    (MvPolynomial.coeff x ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p))
rw₂ :
  Eq.{u_2 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) p : R)
    (MvPolynomial.coeff x ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : R)
rw₃ rw₄ :
  Eq.{u_2 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) p : R) ((coeff x : (a : MvPowerSeries σ R) → R) p : R)
⊢ MvPolynomial.coeff x
      (HSub.hSub (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((truncTotal m : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    0

Tactic:
rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ (by lia),
    coeff_truncTotal _ (by lia)]

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

Tactic:
(MvPolynomial.mem_pow_idealOfVars_iff' ..).mpr (fun x hx ↦ ?_)

Premises used: Iff.mpr, MvPolynomial.mem_pow_idealOfVars_iff'
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : CommRing R
inst_1 : Finite σ
p q : MvPowerSeries σ R
refine :
  ∀ (x : σ →₀ ℕ) (hx : (degree : (a : σ →₀ ℕ) → ℕ) x < n),
    MvPolynomial.coeff x
        (HSub.hSub (α := MvPolynomial σ R)
          ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p * q) : MvPolynomial σ R)
          (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
            ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) q : MvPolynomial σ R))) =
      0
⊢ HSub.hSub (α := MvPolynomial σ R)
      ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p * q) : MvPolynomial σ R)
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) ∈
    HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n

Tactic:
refine (MvPolynomial.mem_pow_idealOfVars_iff' ..).mpr (fun x hx ↦ ?_)

Premises used: Iff.mpr, MvPolynomial.mem_pow_idealOfVars_iff'
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : CommRing R
inst_1 : Finite σ
p q : MvPowerSeries σ R
x : σ →₀ ℕ
hx : (degree : (a : σ →₀ ℕ) → ℕ) x < n
rw :
  MvPolynomial.coeff x ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p * q)) -
      MvPolynomial.coeff x
        (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
          ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
    0
rw₁ :
  MvPolynomial.coeff x ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p * q)) =
    MvPolynomial.coeff x
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) q : MvPolynomial σ R))
rw₂ :
  (coeff x : (a : MvPowerSeries σ R) → R) (p * q) =
    MvPolynomial.coeff x
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) q : MvPolynomial σ R))
rw₃ rw₄ :
  Eq.{u_2 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) (p * q) : R)
    ((coeff x : (a : MvPowerSeries σ R) → R) (p * q) : R)
⊢ MvPolynomial.coeff x
      (HSub.hSub (α := MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p * q) : MvPolynomial σ R)
        (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
          ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) q : MvPolynomial σ R))) =
    0

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

Premises used: sub_eq_zero, MvPowerSeries.coeff_truncTotal, MvPolynomial.coeff_sub, MvPowerSeries.coeff_truncTotal_mul_truncTotal_eq_coeff_mul
-- 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 : ℕ
pos :
  ∀ (h : n = 0),
    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) 1))
      1
neg :
  ∀ (h : n ≠ 0),
    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) 1))
      1
⊢ 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) 1))
    1

Tactic:
by_cases! h : n = 0
-- 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 : ℕ
h : n = 0
⊢ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n = ⊤

Tactic:
simp [h]
-- 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 : ℕ
h : n = 0
⊢ Subsingleton (MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n)

Tactic:
have := Ideal.Quotient.subsingleton_iff.mpr
        (show MvPolynomial.idealOfVars σ R ^ n = ⊤ by simp [h])
-- 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 : ℕ
h : n = 0
this : Subsingleton (MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n)
⊢ 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) 1))
    1

Tactic:
Subsingleton.allEq ..

Premises used: Subsingleton.allEq
-- 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 : ℕ
h : n = 0
this : Subsingleton (MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n)
⊢ 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) 1))
    1

Tactic:
exact Subsingleton.allEq ..

Premises used: Subsingleton.allEq
-- 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 : ℕ
h : n ≠ 0
neg :
  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)
      1)
    1
neg₁ neg₂ : Eq (α := MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) 1 1
⊢ 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) 1))
    1

Tactic:
rw [truncTotal_one h, map_one]

Premises used: MvPowerSeries.truncTotal_one, map_one
-- 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 q : MvPowerSeries σ R
rw :
  HSub.hSub (α := MvPolynomial σ R)
      ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p * q) : MvPolynomial σ R)
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) q : 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 * q)) =
    HMul.hMul (α := MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) (β :=
      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) q) :
        MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n)

Tactic:
rw [← map_mul, Ideal.Quotient.mk_eq_mk_iff_sub_mem]

Premises used: map_mul, Ideal.Quotient.mk_eq_mk_iff_sub_mem
-- 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 q : MvPowerSeries σ R
⊢ HSub.hSub (α := MvPolynomial σ R)
      ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p * q) : MvPolynomial σ R)
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) ∈
    HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n

Tactic:
truncTotal_mul_sub_mul_truncTotal_mem_pow_idealOfVars p q

Premises used: Set.Mem, MvPowerSeries.truncTotal_mul_sub_mul_truncTotal_mem_pow_idealOfVars
-- 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 q : MvPowerSeries σ R
⊢ HSub.hSub (α := MvPolynomial σ R)
      ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p * q) : MvPolynomial σ R)
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) ∈
    HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n

Tactic:
exact truncTotal_mul_sub_mul_truncTotal_mem_pow_idealOfVars p q

Premises used: MvPowerSeries.truncTotal_mul_sub_mul_truncTotal_mem_pow_idealOfVars
-- 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 : ℕ
rw :
  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)
      0)
    0
rw₁ rw₂ : Eq (α := MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) 0 0
⊢ 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) 0))
    0

Tactic:
rw [map_zero, map_zero]

Premises used: map_zero
-- 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 : ℕ
x x_1 : MvPowerSeries σ R
⊢ (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) (x + x_1)) =
    HAdd.hAdd (α := MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) (β :=
      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) x) :
        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) x_1) :
        MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n)

Tactic:
simp
-- 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
change :
  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 : MvPowerSeries σ R)) :
      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)
        p :
      MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n)
⊢ 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)
          ((algebraMap (MvPolynomial σ R) (MvPowerSeries σ R) : (a : MvPolynomial σ R) → MvPowerSeries σ R) p)) :
      MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n)
    ((algebraMap (MvPolynomial σ R)
            (MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n)
        p :
      MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n)

Tactic:
change (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) (truncTotal n p) =
      (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) p

Premises used: MvPowerSeries.truncTotal, Ideal.Quotient.mk, MvPolynomial.toMvPowerSeries, HPow.hPow, MvPolynomial.idealOfVars, DFunLike.coe
-- 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
rw :
  ∀ (x : σ →₀ ℕ),
    (degree : (a : σ →₀ ℕ) → ℕ) x < n →
      MvPolynomial.coeff x
          (HSub.hSub (α := MvPolynomial σ R)
            ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) : MvPolynomial σ R)
            p) =
        0
⊢ 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 : MvPowerSeries σ R)) :
      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)
        p :
      MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n)

Tactic:
rw [Ideal.Quotient.eq, MvPolynomial.mem_pow_idealOfVars_iff']

Premises used: MvPolynomial.mem_pow_idealOfVars_iff', Ideal.Quotient.eq