awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ ψ : MvPolynomial σ R
⊢ (↑(φ + ψ) : MvPowerSeries σ R) = (↑φ : MvPowerSeries σ R) + (↑ψ : MvPowerSeries σ R)

Tactic:
rfl

Premises used: MvPolynomial.toMvPowerSeries, MvPolynomial.coeff, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ ψ : MvPolynomial σ R
n : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (↑(φ * ψ) : MvPowerSeries σ R) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) ((↑φ : MvPowerSeries σ R) * (↑ψ : MvPowerSeries σ R)) : R)

Tactic:
simp only [coeff_coe, MvPowerSeries.coeff_mul, coeff_mul]

Premises used: MvPolynomial.coeff_coe, MvPolynomial.coeff_mul, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ ψ : MvPolynomial σ R
n : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (↑(φ * ψ) : MvPowerSeries σ R) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) ((↑φ : MvPowerSeries σ R) * (↑ψ : MvPowerSeries σ R)) : R)

Tactic:
classical
    simp only [coeff_coe, MvPowerSeries.coeff_mul, coeff_mul]

Premises used: MvPolynomial.coeff_coe, MvPolynomial.coeff_mul, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
r : R
⊢ (↑(r • φ) : MvPowerSeries σ R) = r • (↑φ : MvPowerSeries σ R)

Tactic:
rfl

Premises used: MvPolynomial.toMvPowerSeries, MvPolynomial.coeff, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
a : R
⊢ Eq (α := MvPowerSeries σ R) (↑((C : (a : R) → MvPolynomial σ R) a) : MvPowerSeries σ R)
    ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) a)

Tactic:
coe_monomial _ _

Premises used: Function.update, MvPolynomial.coe_monomial, Pi.single, dite, Finsupp.single
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : σ
⊢ Eq (α := MvPowerSeries σ R) (↑(X s) : MvPowerSeries σ R) (MvPowerSeries.X s)

Tactic:
coe_monomial _ _

Premises used: MvPolynomial.coe_monomial, MvPolynomial.X, MvPowerSeries.X
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x y : MvPolynomial σ R
h : (↑x : MvPowerSeries σ R) = (↑y : MvPowerSeries σ R)
a : ∀ (m : σ →₀ ℕ), coeff m x = coeff m y
⊢ x = y

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x y : MvPolynomial σ R
h : (↑x : MvPowerSeries σ R) = (↑y : MvPowerSeries σ R)
m : σ →₀ ℕ
a :
  Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R) (↑x : MvPowerSeries σ R) : R)
    ((MvPowerSeries.coeff m : (a : MvPowerSeries σ R) → R) (↑y : MvPowerSeries σ R) : R)
⊢ coeff m x = coeff m y

Tactic:
simp_rw [← coeff_coe, h]

Premises used: MvPolynomial.coeff_coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ ψ : MvPolynomial σ R
⊢ (↑φ : MvPowerSeries σ R) = (↑ψ : MvPowerSeries σ R) ↔ φ = ψ

Tactic:
(coe_injective σ R).eq_iff

Premises used: Function.Injective.eq_iff, MvPolynomial.coe_injective
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
rw : (↑φ : MvPowerSeries σ R) = (↑0 : MvPowerSeries σ R) ↔ φ = 0
rw₁ rw₂ : φ = 0 ↔ φ = 0
⊢ (↑φ : MvPowerSeries σ R) = 0 ↔ φ = 0

Tactic:
rw [← coe_zero, coe_inj]

Premises used: MvPolynomial.coe_zero, MvPolynomial.coe_inj
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
rw : (↑φ : MvPowerSeries σ R) = (↑1 : MvPowerSeries σ R) ↔ φ = 1
rw₁ rw₂ : φ = 1 ↔ φ = 1
⊢ (↑φ : MvPowerSeries σ R) = 1 ↔ φ = 1

Tactic:
rw [← coe_one, coe_inj]

Premises used: MvPolynomial.coe_one, MvPolynomial.coe_inj
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
⊢ (↑(φ ^ n) : MvPowerSeries σ R) = (↑φ : MvPowerSeries σ R) ^ n

Tactic:
coeToMvPowerSeries.ringHom.map_pow _ _

Premises used: MvPolynomial.toMvPowerSeries, MvPolynomial.coeff, MvPolynomial.coeToMvPowerSeries.ringHom, RingHom.map_pow
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
⊢ (ringHom : (a : MvPolynomial σ R) → MvPowerSeries σ R) φ = (↑φ : MvPowerSeries σ R)

Tactic:
rfl

Premises used: MvPolynomial.toMvPowerSeries, MvPolynomial.coeff, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
simp :
  Eq (α := MvPowerSeries σ R)
    (↑(e.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (X n) e) : MvPowerSeries σ R)
    (e.prod fun (s : σ) (n : ℕ) ↦ (↑(HPow.hPow (α := MvPolynomial σ R) (X s) n) : MvPowerSeries σ R))
⊢ Eq (α := MvPowerSeries σ R) ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) 1)
    (e.prod fun (s : σ) (n : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) n)

Tactic:
simp only [← coe_X, ← coe_pow, ← coe_monomial, monomial_eq, map_one, one_mul]

Premises used: MvPolynomial.coe_monomial, MvPolynomial.coe_X, MvPolynomial.coe_pow, map_one, MvPolynomial.monomial_eq, one_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
⊢ Eq (α := MvPowerSeries σ R)
    (↑(e.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ R) (X n) e) : MvPowerSeries σ R)
    (e.prod fun (s : σ) (n : ℕ) ↦ (↑(HPow.hPow (α := MvPolynomial σ R) (X s) n) : MvPowerSeries σ R))

Tactic:
simp only [← coeToMvPowerSeries.ringHom_apply, ← map_finsuppProd]

Premises used: map_finsuppProd, MvPolynomial.coeToMvPowerSeries.ringHom_apply
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
r : R
rw : ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (r * 1) : MvPowerSeries σ R)
| ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)

Tactic:
rw [← mul_one r]

Premises used: mul_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
r : R
conv_lhs :
  (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)
⊢ (MvPowerSeries.monomial 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) e : MvPowerSeries σ R)

Tactic:
conv_lhs => rw [← mul_one r]

Premises used: mul_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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)
rw₃ 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)
⊢ (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)

Tactic:
rw [← smul_eq_mul, ← MvPowerSeries.smul_eq_C_mul, LinearMap.CompatibleSMul.map_smul,
    MvPowerSeries.monomial_one_eq]

Premises used: MvPowerSeries.smul_eq_C_mul, MvPowerSeries.monomial_one_eq, smul_eq_mul, LinearMap.CompatibleSMul.map_smul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
p : ℕ
r : R
⊢ ∀ i ∈ e.support, HPow.hPow (α := MvPowerSeries σ R) (β := ℕ) (MvPowerSeries.X i) 0 = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
p : ℕ
r : R
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)
⊢ (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)

Tactic:
rw [MvPowerSeries.monomial_eq', Finsupp.prod_of_support_subset _ Finsupp.support_smul _
    (by simp), Finsupp.prod]

Premises used: Finsupp.prod_of_support_subset, Finsupp.support_smul, Finsupp.prod, MvPowerSeries.monomial_eq'
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
e : σ →₀ ℕ
p : ℕ
r : R
⊢ 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:
simp [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
τ : Type u_3
d : σ →₀ ℕ
f : σ → τ
⊢ Eq (α := MvPowerSeries τ R) ((MvPowerSeries.monomial (mapDomain f d) : (a : R) → MvPowerSeries τ R) 1)
    (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) (MvPowerSeries.X (f s)) e)

Tactic:
simp [pow_add, prod_sum_index, MvPowerSeries.monomial_one_eq, mapDomain]

Premises used: Finsupp.mapDomain, pow_add, Finsupp.prod_sum_index, MvPowerSeries.monomial_one_eq
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ ψ : MvPolynomial σ R
A : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
r : R
⊢ Eq (α := MvPowerSeries σ A)
    (OneHom.toFun (M := MvPolynomial σ R)
      (↑(↑(RingHom.comp (MvPowerSeries.map (algebraMap R A)) ringHom) : MvPolynomial σ R →* MvPowerSeries σ A) :
        OneHom (MvPolynomial σ R) (MvPowerSeries σ A))
      ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) r))
    ((algebraMap R (MvPowerSeries σ A) : (a : R) → MvPowerSeries σ A) r)

Tactic:
simp [MvPowerSeries.algebraMap_apply]

Premises used: MvPowerSeries.algebraMap_apply
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
A : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
⊢ Eq (α := MvPowerSeries σ A) ((algHom A : (a : MvPolynomial σ R) → MvPowerSeries σ A) φ : MvPowerSeries σ A)
    ((MvPowerSeries.map (algebraMap R A) : (a : MvPowerSeries σ R) → MvPowerSeries σ A) (↑φ : 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
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)
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 : ℕ)
⊢ (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)

Tactic:
rw [Finsupp.prod_congr
    (g2 := fun s n ↦ ((MvPowerSeries.C (algebraMap A R (a s)) * (MvPowerSeries.X s)) ^ n))]

Premises used: Finsupp.prod_congr
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
rw₁ rw₂ : a • f = a • f
⊢ a • f =
    HMul.hMul (α := MvPowerSeries σ R)
      ((MvPowerSeries.C : (a : R) → MvPowerSeries σ R) ((algebraMap A R : (a : A) → R) a) : MvPowerSeries σ R) f

Tactic:
rw [← MvPowerSeries.smul_eq_C_mul, IsScalarTower.algebraMap_smul]

Premises used: MvPowerSeries.smul_eq_C_mul, IsScalarTower.algebraMap_smul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
⊢ ∀ (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]
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
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)
⊢ (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:
simp only [mul_pow, Finsupp.prod_mul, ← map_pow, ← MvPowerSeries.monomial_one_eq, this]

Premises used: Finsupp.prod_mul, map_pow, MvPowerSeries.monomial_one_eq, mul_pow
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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
⊢ 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 [map_finsuppProd, map_pow]

Premises used: map_finsuppProd, map_pow
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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 : σ
_ :
  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 : ℕ)
⊢ 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:
_
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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 : ℕ)
rw₁ 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 : ℕ)
⊢ 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 [algebra_compatible_smul R, MvPowerSeries.smul_eq_C_mul]

Premises used: MvPowerSeries.smul_eq_C_mul, algebra_compatible_smul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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)
rw₃ 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))
⊢ 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)

Tactic:
rw [MvPowerSeries.prod_smul_X_eq_smul_monomial_one, ← map_smul, smul_eq_mul, mul_one]

Premises used: smul_eq_mul, mul_one, map_smul, MvPowerSeries.prod_smul_X_eq_smul_monomial_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_4
R : Type u_5
inst : CommSemiring R
e : σ →₀ ℕ
r : R
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)
⊢ 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)

Tactic:
rw [MvPowerSeries.prod_smul_X_eq_smul_monomial_one, ← map_smul, smul_eq_mul, mul_one]

Premises used: smul_eq_mul, mul_one, map_smul, MvPowerSeries.prod_smul_X_eq_smul_monomial_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
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)
    ((MvPowerSeries.monomial e : (a : R) → MvPowerSeries σ R) (e.prod fun (s : σ) (n : ℕ) ↦ r ^ n) : MvPowerSeries σ R)

Tactic:
simp only [Finsupp.sum, Finsupp.prod, Finset.prod_pow_eq_pow_sum]

Premises used: Finsupp.sum, Finset.prod_pow_eq_pow_sum, Finsupp.prod