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
n : ℕ
inst : CommRing R
inst_1 : Finite σ
p q : MvPowerSeries σ R
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
have 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
Tactic: rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ hx,
    coeff_truncTotal_mul_truncTotal_eq_coeff_mul _ _ hx]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ 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
have 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))
Tactic: rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ hx,
    coeff_truncTotal_mul_truncTotal_eq_coeff_mul _ _ hx]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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))
⊢ 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
have 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))
Tactic: rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ hx,
    coeff_truncTotal_mul_truncTotal_eq_coeff_mul _ _ hx]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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))
⊢ 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
have rw₃ : Eq.{u_2 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) (p * q) : R)
  ((coeff x : (a : MvPowerSeries σ R) → R) (p * q) : R)
Tactic: rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ hx,
    coeff_truncTotal_mul_truncTotal_eq_coeff_mul _ _ hx]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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 : ℕ
⊢ 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
have 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
Tactic: by_cases! h : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ 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
have 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
Tactic: by_cases! h : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (hypothesis)
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
⊢ 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
have this : 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])
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ 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
have 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
Tactic: rw [truncTotal_one h, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ 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
have neg₁ : Eq (α := MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) 1 1
Tactic: rw [truncTotal_one h, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ (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)
have 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
Tactic: rw [← map_mul, Ideal.Quotient.mk_eq_mk_iff_sub_mem]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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 : ℕ
⊢ 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
have 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
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ 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
have rw₁ : Eq (α := MvPolynomial σ R ⧸ HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) 0 0
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ 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)
have 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)
Tactic: change (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) (truncTotal n p) =
      (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) p
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ 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)
have 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
Tactic: rw [Ideal.Quotient.eq, MvPolynomial.mem_pow_idealOfVars_iff']
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ MvPolynomial.coeff x
      (HSub.hSub (α := MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) : MvPolynomial σ R) p) =
    0
have rw : MvPolynomial.coeff x ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) -
    MvPolynomial.coeff x p =
  0
Tactic: rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ h, MvPolynomial.coeff_coe]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ MvPolynomial.coeff x
      (HSub.hSub (α := MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) : MvPolynomial σ R) p) =
    0
have rw₁ : MvPolynomial.coeff x ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) =
  MvPolynomial.coeff x p
Tactic: rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ h, MvPolynomial.coeff_coe]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ MvPolynomial.coeff x
      (HSub.hSub (α := MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) : MvPolynomial σ R) p) =
    0
have rw₂ : (coeff x : (a : MvPowerSeries σ R) → R) (↑p : MvPowerSeries σ R) = MvPolynomial.coeff x p
Tactic: rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ h, MvPolynomial.coeff_coe]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ MvPolynomial.coeff x
      (HSub.hSub (α := MvPolynomial σ R)
        ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) : MvPolynomial σ R) p) =
    0
have rw₃ : MvPolynomial.coeff x p = MvPolynomial.coeff x p
Tactic: rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ h, MvPolynomial.coeff_coe]