awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
r : R
rw :
  (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (HSMul.hSMul (β := R) r 1) =
    HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) e : MvPowerSeries σ R)
rw₁ :
  (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (HSMul.hSMul (β := R) r 1) =
    HSMul.hSMul (β := MvPowerSeries σ R) r
      (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) e)
rw₂ :
  HSMul.hSMul (β := MvPowerSeries σ R) r ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) 1) =
    HSMul.hSMul (β := MvPowerSeries σ R) r
      (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) e)
⊢ (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (r * 1) =
    HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) e : MvPowerSeries σ R)
have rw₃ : HSMul.hSMul (β := MvPowerSeries σ R) r
    (e.prod fun (s : σ) (n : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) n) =
  HSMul.hSMul (β := MvPowerSeries σ R) r
    (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) e)
Tactic: rw [← smul_eq_mul, ← MvPowerSeries.smul_eq_C_mul, LinearMap.CompatibleSMul.map_smul,
    MvPowerSeries.monomial_one_eq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
p : ℕ
r : R
⊢ (MvPowerSeries.monomial (p • e) : (a : R) → MvPowerSeries σ R) r =
    HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) p ^ e : MvPowerSeries σ R)
have rw : HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
    ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
    (∏ x ∈ e.support, HPow.hPow (α := MvPowerSeries σ R) (β := ℕ) (MvPowerSeries.X x) ((p • e : (a : σ) → ℕ) x : ℕ) :
      MvPowerSeries σ R) =
  HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
    ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
    (∏ a ∈ e.support,
        HPow.hPow (β := ℕ) (HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X a) p) ((e : (a : σ) → ℕ) a : ℕ) :
      MvPowerSeries σ R)
Tactic: rw [MvPowerSeries.monomial_eq', Finsupp.prod_of_support_subset _ Finsupp.support_smul _
    (by simp), Finsupp.prod]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ (e.prod fun (s : σ) (n : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (MvPowerSeries.X s) ^ n) =
    HSMul.hSMul (α := A) (β := MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n)
      ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) 1)
have rw : (e.prod fun (s : σ) (n : ℕ) ↦
    HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
        ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) (a s)) : MvPowerSeries σ R)
        (MvPowerSeries.X s) ^
      n) =
  HSMul.hSMul (α := A) (β := MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n)
    ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) 1)
Tactic: rw [Finsupp.prod_congr
    (g2 := fun s n ↦ ((MvPowerSeries.C (algebraMap A R (a s)) * (MvPowerSeries.X s)) ^ n))]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra A R
e : σ →₀ ℕ
a : σ → A
rw :
  (e.prod fun (s : σ) (n : ℕ) ↦
      HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
          ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) (a s)) : MvPowerSeries σ R)
          (MvPowerSeries.X s) ^
        n) =
    HSMul.hSMul (α := A) (β := MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n)
      ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) 1)
⊢ (e.prod fun (s : σ) (n : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (MvPowerSeries.X s) ^ n) =
    HSMul.hSMul (α := A) (β := MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n)
      ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) 1)
have rw₁ : ∀ x ∈ e.support,
  HPow.hPow (β := ℕ) (HSMul.hSMul (β := MvPowerSeries σ R) (a x) (MvPowerSeries.X x)) ((e : (a : σ) → ℕ) x : ℕ) =
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
        ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) (a x)) : MvPowerSeries σ R)
        (MvPowerSeries.X x))
      ((e : (a : σ) → ℕ) x : ℕ)
Tactic: rw [Finsupp.prod_congr
    (g2 := fun s n ↦ ((MvPowerSeries.C (algebraMap A R (a s)) * (MvPowerSeries.X s)) ^ n))]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra A R
e : σ →₀ ℕ
a_1 : σ → A
a : A
f : MvPowerSeries σ R
⊢ a • f =
    HMul.hMul (α := MvPowerSeries σ R)
      ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) a) : MvPowerSeries σ R) f
have rw : a • f = HSMul.hSMul (α := R) ((algebraMap A R : (a : A) → R) a : R) f
Tactic: rw [← MvPowerSeries.smul_eq_C_mul, IsScalarTower.algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra A R
e : σ →₀ ℕ
a_1 : σ → A
a : A
f : MvPowerSeries σ R
rw : a • f = HSMul.hSMul (α := R) ((algebraMap A R : (a : A) → R) a : R) f
⊢ a • f =
    HMul.hMul (α := MvPowerSeries σ R)
      ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) a) : MvPowerSeries σ R) f
have rw₁ : a • f = a • f
Tactic: rw [← MvPowerSeries.smul_eq_C_mul, IsScalarTower.algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ (e.prod fun (s : σ) (n : ℕ) ↦
      HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
          ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) (a s)) : MvPowerSeries σ R)
          (MvPowerSeries.X s) ^
        n) =
    HSMul.hSMul (α := A) (β := MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n)
      ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) 1)
have this : ∀ (a : A) (f : MvPowerSeries σ R),
  a • f =
    HMul.hMul (α := MvPowerSeries σ R)
      ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) a) : MvPowerSeries σ R) f
Tactic: have (a : A) (f : MvPowerSeries σ R) : a • f =
      MvPowerSeries.C ((algebraMap A R) a) * f := by
      rw [← MvPowerSeries.smul_eq_C_mul, IsScalarTower.algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra A R
e : σ →₀ ℕ
a : σ → A
this :
  ∀ (a : A) (f : MvPowerSeries σ R),
    a • f =
      HMul.hMul (α := MvPowerSeries σ R)
        ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) a) : MvPowerSeries σ R) f
⊢ (e.prod fun (s : σ) (n : ℕ) ↦
      HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
          ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) (a s)) : MvPowerSeries σ R)
          (MvPowerSeries.X s) ^
        n) =
    HSMul.hSMul (α := A) (β := MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n)
      ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) 1)
have simp : HMul.hMul (α := MvPowerSeries σ R)
    (e.prod fun (a_1 : σ) (b : ℕ) ↦
      (MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) (a a_1 ^ b)))
    ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) 1) =
  HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
    ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R)
        ((algebraMap A R : (a : A) → R) (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n)) :
      MvPowerSeries σ R)
    ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) 1 : MvPowerSeries σ R)
Tactic: simp only [mul_pow, Finsupp.prod_mul, ← map_pow, ← MvPowerSeries.monomial_one_eq, this]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra A R
e : σ →₀ ℕ
a : σ → A
x : σ
h : x ∈ e.support
⊢ HPow.hPow (β := ℕ) (HSMul.hSMul (β := MvPowerSeries σ R) (a x) (MvPowerSeries.X x)) ((e : (a : σ) → ℕ) x : ℕ) =
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
        ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) (a x)) : MvPowerSeries σ R)
        (MvPowerSeries.X x))
      ((e : (a : σ) → ℕ) x : ℕ)
have rw : HPow.hPow (β := ℕ)
    (HSMul.hSMul (α := R) (β := MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) (a x) : R) (MvPowerSeries.X x))
    ((e : (a : σ) → ℕ) x : ℕ) =
  HPow.hPow (β := ℕ)
    (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) (a x)) : MvPowerSeries σ R)
      (MvPowerSeries.X x))
    ((e : (a : σ) → ℕ) x : ℕ)
Tactic: rw [algebra_compatible_smul R, MvPowerSeries.smul_eq_C_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra A R
e : σ →₀ ℕ
a : σ → A
x : σ
h : x ∈ e.support
rw :
  HPow.hPow (β := ℕ)
      (HSMul.hSMul (α := R) (β := MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) (a x) : R) (MvPowerSeries.X x))
      ((e : (a : σ) → ℕ) x : ℕ) =
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
        ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) (a x)) : MvPowerSeries σ R)
        (MvPowerSeries.X x))
      ((e : (a : σ) → ℕ) x : ℕ)
⊢ HPow.hPow (β := ℕ) (HSMul.hSMul (β := MvPowerSeries σ R) (a x) (MvPowerSeries.X x)) ((e : (a : σ) → ℕ) x : ℕ) =
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
        ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) (a x)) : MvPowerSeries σ R)
        (MvPowerSeries.X x))
      ((e : (a : σ) → ℕ) x : ℕ)
have rw₁ : HPow.hPow (β := ℕ)
    (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) (a x)) : MvPowerSeries σ R)
      (MvPowerSeries.X x))
    ((e : (a : σ) → ℕ) x : ℕ) =
  HPow.hPow (β := ℕ)
    (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) (a x)) : MvPowerSeries σ R)
      (MvPowerSeries.X x))
    ((e : (a : σ) → ℕ) x : ℕ)
Tactic: rw [algebra_compatible_smul R, MvPowerSeries.smul_eq_C_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
r : σ → R
⊢ Eq (α := MvPowerSeries σ R)
    ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n))
    (e.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (r s) (MvPowerSeries.X s) ^ e)
have rw : (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n) =
  HSMul.hSMul (α := R) (β := MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n)
    ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) 1)
Tactic: rw [MvPowerSeries.prod_smul_X_eq_smul_monomial_one, ← map_smul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
r : σ → R
rw :
  (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n) =
    HSMul.hSMul (α := R) (β := MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n)
      ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) 1)
⊢ Eq (α := MvPowerSeries σ R)
    ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n))
    (e.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (r s) (MvPowerSeries.X s) ^ e)
have rw₁ : Eq (α := MvPowerSeries σ R)
  ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n) : MvPowerSeries σ R)
  ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R)
      (HSMul.hSMul (α := R) (β := R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n) 1) :
    MvPowerSeries σ R)
Tactic: rw [MvPowerSeries.prod_smul_X_eq_smul_monomial_one, ← map_smul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
r : σ → R
rw :
  (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n) =
    HSMul.hSMul (α := R) (β := MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n)
      ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) 1)
rw₁ :
  Eq (α := MvPowerSeries σ R)
    ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n) :
      MvPowerSeries σ R)
    ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R)
        (HSMul.hSMul (α := R) (β := R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n) 1) :
      MvPowerSeries σ R)
⊢ Eq (α := MvPowerSeries σ R)
    ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n))
    (e.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (r s) (MvPowerSeries.X s) ^ e)
have rw₂ : Eq (α := MvPowerSeries σ R)
  ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n) : MvPowerSeries σ R)
  ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R)
      (HMul.hMul (α := R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n) 1) :
    MvPowerSeries σ R)
Tactic: rw [MvPowerSeries.prod_smul_X_eq_smul_monomial_one, ← map_smul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
r : σ → R
rw :
  (MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n) =
    HSMul.hSMul (α := R) (β := MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n)
      ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) 1)
rw₁ :
  Eq (α := MvPowerSeries σ R)
    ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n) :
      MvPowerSeries σ R)
    ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R)
        (HSMul.hSMul (α := R) (β := R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n) 1) :
      MvPowerSeries σ R)
rw₂ :
  Eq (α := MvPowerSeries σ R)
    ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n) :
      MvPowerSeries σ R)
    ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R)
        (HMul.hMul (α := R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n) 1) :
      MvPowerSeries σ R)
⊢ Eq (α := MvPowerSeries σ R)
    ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n))
    (e.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (r s) (MvPowerSeries.X s) ^ e)
have rw₃ : Eq (α := MvPowerSeries σ R)
  ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n))
  ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r s ^ n))
Tactic: rw [MvPowerSeries.prod_smul_X_eq_smul_monomial_one, ← map_smul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_4
R : Type u_5
inst : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ Eq (α := MvPowerSeries σ R)
    ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (HPow.hPow (β := ℕ) r (e.sum fun (x : σ) (n : ℕ) ↦ n)) :
      MvPowerSeries σ R)
    (e.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) r (MvPowerSeries.X s) ^ e : MvPowerSeries σ R)
have rw : Eq (α := MvPowerSeries σ R)
  ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (HPow.hPow (β := ℕ) r (e.sum fun (x : σ) (n : ℕ) ↦ n)) :
    MvPowerSeries σ R)
  ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r ^ n) : MvPowerSeries σ R)
Tactic: rw [MvPowerSeries.prod_smul_X_eq_smul_monomial_one, ← map_smul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
have 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
Tactic: refine (MvPolynomial.mem_pow_idealOfVars_iff' ..).mpr (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ 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
have 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
Tactic: rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ (by lia),
    coeff_truncTotal _ (by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ 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
have 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))
Tactic: rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ (by lia),
    coeff_truncTotal _ (by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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))
⊢ 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
have 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)
Tactic: rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ (by lia),
    coeff_truncTotal _ (by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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)
⊢ 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
have rw₃ : Eq.{u_2 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) p : R) ((coeff x : (a : MvPowerSeries σ R) → R) p : R)
Tactic: rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ (by lia),
    coeff_truncTotal _ (by lia)]
-- 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
⊢ 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
have 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
Tactic: refine (MvPolynomial.mem_pow_idealOfVars_iff' ..).mpr (fun x hx ↦ ?_)