awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
a :
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
      R)
    (if n = 0 then (constantCoeff : (a : MvPowerSeries σ R) → R) x else 0 : R)
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale 0 : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((RingHom.comp C constantCoeff : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)

Tactic:
simp only [rescale, Pi.zero_apply, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    RingHom.coe_comp, Function.comp_apply, coeff_C]

Premises used: MvPowerSeries.rescale, OneHom.coe_mk, Pi.zero_apply, MonoidHom.coe_mk, MvPowerSeries.coeff_C, RingHom.coe_mk, RingHom.coe_comp, Function.comp_apply
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
pos :
  ∀ (h : n = 0),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
            ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
        R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) x : R)
neg :
  ∀ (h : ¬n = 0),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
            ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
        R)
      (0 : R)
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
      R)
    (if n = 0 then (constantCoeff : (a : MvPowerSeries σ R) → R) x else 0 : R)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
h : n = 0
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
      R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) x : R)

Tactic:
simp [h, coeff_apply, ← @coeff_zero_eq_constantCoeff_apply, coeff_apply]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff_apply, MvPowerSeries.coeff_apply
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
h : ¬n = 0
neg : (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m) * x n = 0
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
      R)
    (0 : R)

Tactic:
simp only [coeff_apply]

Premises used: MvPowerSeries.coeff_apply
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
h : ¬n = 0
⊢ 0 * x n = 0

Tactic:
zero_mul _

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
h : ¬n = 0
h₁ : Eq.{u_9 + 1} (α := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m) 0
⊢ (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m) * x n = 0

Tactic:
convert! zero_mul _

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
h : ¬n = 0
⊢ ∃ (x : σ), ¬Eq (α := ℕ) ((n : (a : σ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
simp only [DFunLike.ext_iff, not_forall, Finsupp.coe_zero, Pi.zero_apply] at h

Premises used: Pi.zero_apply, DFunLike.ext_iff, Classical.not_forall, Finsupp.coe_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
h : ∃ (x : σ), ¬Eq (α := ℕ) ((n : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
h₁ :
  ∀ (s : σ) (h : ¬Eq (α := ℕ) ((n : (a : σ) → ℕ) s : ℕ) (0 : ℕ)),
    Eq.{u_9 + 1} (α := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m) 0
⊢ Eq.{u_9 + 1} (α := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m) 0

Tactic:
obtain ⟨s, h⟩ := h
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
s : σ
h : ¬Eq (α := ℕ) ((n : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
apply : s ∈ n.support
⊢ Eq.{u_9 + 1} (α := R) (∏ x ∈ n.support, HPow.hPow (α := R) (β := ℕ) 0 ((n : (a : σ) → ℕ) x : ℕ)) 0

Tactic:
apply Finset.prod_eq_zero (i := s) _ (zero_pow h)

Premises used: Finset.prod_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
s : σ
h : ¬Eq (α := ℕ) ((n : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
⊢ s ∈ n.support

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
a :
  ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((rescale 0 : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((RingHom.comp C constantCoeff : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
        R)
a₁ :
  ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
            ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
        R)
      (if n = 0 then (constantCoeff : (a : MvPowerSeries σ R) → R) x else 0 : R)
pos :
  ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ) (h : n = 0),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
            ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
        R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) x : R)
neg neg₁ :
  ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ) (h : ¬n = 0),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
            ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
        R)
      (0 : R)
⊢ Eq (α := MvPowerSeries σ R →+* MvPowerSeries σ R) (rescale 0) (RingHom.comp C constantCoeff)

Tactic:
classical
  ext x n
  simp only [rescale, Pi.zero_apply, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    RingHom.coe_comp, Function.comp_apply, coeff_C]
  split_ifs with h
  · simp [h, coeff_apply, ← @coeff_zero_eq_constantCoeff_apply, coeff_apply]
  · simp only [coeff_apply]
    convert! zero_mul _
    simp only [DFunLike.ext_iff, not_forall, Finsupp.coe_zero, Pi.zero_apply] at h
    obtain ⟨s, h⟩ := h
    simp only [Finsupp.prod]
    apply Finset.prod_eq_zero (i := s) _ (zero_pow h)
    simpa using h

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff_apply, MvPowerSeries.rescale, MulZeroClass.zero_mul, OneHom.coe_mk, Pi.zero_apply, DFunLike.ext_iff, MvPowerSeries.coeff_apply, MonoidHom.coe_mk, MvPowerSeries.coeff_C, RingHom.coe_mk, RingHom.coe_comp, Function.comp_apply, Classical.not_forall, Finsupp.prod, Finsupp.coe_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
f : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries σ R) ((rescale 0 : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    ((C : (a : R) → MvPowerSeries σ R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f) : MvPowerSeries σ R)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
a :
  ∀ (f : MvPowerSeries σ R) (n : σ →₀ ℕ),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((rescale 1 : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((RingHom.id (MvPowerSeries σ R) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
        R)
⊢ Eq (α := MvPowerSeries σ R →+* MvPowerSeries σ R) (rescale 1) (RingHom.id (MvPowerSeries σ R))

Tactic:
ext f n
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale 1 : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((RingHom.id (MvPowerSeries σ R) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)

Tactic:
simp [coeff_rescale, Finsupp.prod]

Premises used: MvPowerSeries.coeff_rescale, Finsupp.prod
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
f : MvPowerSeries σ R
a b : σ → R
h :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((rescale b : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
              ((rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
            MvPowerSeries σ R) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((rescale (a * b) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
        R)
⊢ Eq (α := MvPowerSeries σ R)
    ((rescale b : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
      MvPowerSeries σ R)
    ((rescale (a * b) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)

Tactic:
ext n
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
f : MvPowerSeries σ R
a b : σ → R
n : σ →₀ ℕ
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale b : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
          MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale (a * b) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)

Tactic:
simp [← mul_assoc, mul_pow, mul_comm]

Premises used: mul_assoc, mul_comm, mul_pow
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
a b : σ → R
a₁ :
  ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((rescale (a * b) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((RingHom.comp (rescale b) (rescale a) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
        R)
⊢ Eq (α := MvPowerSeries σ R →+* MvPowerSeries σ R) (rescale (a * b)) (RingHom.comp (rescale b) (rescale a))

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
a b : σ → R
x : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale (a * b) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((RingHom.comp (rescale b) (rescale a) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)

Tactic:
simp [← rescale_rescale]

Premises used: MvPowerSeries.rescale_rescale
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d = n
h :
  ∀ (e : σ →₀ ℕ),
    Eq.{u_9 + 1} (α := R)
      ((coeff e : (a : MvPowerSeries σ R) → R)
          ((rescale (Function.const σ r) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
        R)
      ((coeff e : (a : MvPowerSeries σ R) → R) (r ^ n • f) : R)
⊢ (rescale (Function.const σ r) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f = r ^ n • f

Tactic:
ext e
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d = n
e : σ →₀ ℕ
h :
  HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (β := R) (r ^ n) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff e : (a : MvPowerSeries σ R) → R)
        ((rescale (Function.const σ r) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    ((coeff e : (a : MvPowerSeries σ R) → R) (r ^ n • f) : R)

Tactic:
simp only [MvPowerSeries.coeff_rescale, map_smul, Finsupp.prod, Function.const_apply,
    Finset.prod_pow_eq_pow_sum, smul_eq_mul]

Premises used: Function.const_apply, Finset.prod_pow_eq_pow_sum, MvPowerSeries.coeff_rescale, smul_eq_mul, Finsupp.prod, map_smul
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d = n
e : σ →₀ ℕ
pos :
  ∀ (he : e ∈ Function.support f),
    HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
        ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
      HMul.hMul (β := R) (r ^ n) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
neg :
  ∀ (he : e ∉ Function.support f),
    HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
        ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
      HMul.hMul (β := R) (r ^ n) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
⊢ HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (β := R) (r ^ n) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
by_cases he : e ∈ f.support

Premises used: Function.support
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d = n
e : σ →₀ ℕ
he : e ∈ Function.support f
pos :
  HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (β := R) (HPow.hPow (β := ℕ) r ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) e : ℕ))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
pos₁ pos₂ :
  HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
⊢ HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (β := R) (r ^ n) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
rw [← hf e he, Finsupp.degree_apply]

Premises used: Finsupp.degree_apply
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d = n
e : σ →₀ ℕ
he : e ∉ Function.support f
⊢ f e = 0

Tactic:
simp only [Function.mem_support, ne_eq, not_not] at he

Premises used: Classical.not_not, ne_eq, Function.mem_support
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d = n
e : σ →₀ ℕ
he : f e = 0
⊢ HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (β := R) (r ^ n) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
simp [he, mul_zero, coeff_apply]

Premises used: MvPowerSeries.coeff_apply, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b_1 : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a b : σ → R
a₁ :
  ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((rescale (a * b) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((HMul.hMul (α := MvPowerSeries σ R →+* MvPowerSeries σ R) (rescale a) (rescale b) :
                (a : MvPowerSeries σ R) → MvPowerSeries σ R)
              x :
            MvPowerSeries σ R) :
        R)
⊢ rescale (a * b) = HMul.hMul (α := MvPowerSeries σ R →+* MvPowerSeries σ R) (rescale a) (rescale b)

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b_1 : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a b : σ → R
x : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale (a * b) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((HMul.hMul (α := MvPowerSeries σ R →+* MvPowerSeries σ R) (rescale a) (rescale b) :
              (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            x :
          MvPowerSeries σ R) :
      R)

Tactic:
simp [mul_comm, rescale_rescale]

Premises used: MvPowerSeries.rescale_rescale, mul_comm
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
h :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R) (subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X) f) : R)
⊢ (rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f =
    subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X) f

Tactic:
ext n
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
h :
  HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
    (coeff n : (a : MvPowerSeries σ R) → R) (subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X) f)
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X) f) : R)

Tactic:
rw [coeff_rescale]

Premises used: MvPowerSeries.coeff_rescale
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
h :
  HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
    ∑
      i ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
            HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
              ((coeff n : (a : MvPowerSeries σ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X s ^ e) :
                R))
          ⋯,
      HSMul.hSMul (α := R) (β := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff n : (a : MvPowerSeries σ R) → R)
            (i.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X s ^ e) :
          R)
⊢ HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
    (coeff n : (a : MvPowerSeries σ R) → R) (subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X) f)

Tactic:
rw [coeff_subst (HasSubst.smul_X a),
    finsum_eq_sum _ (coeff_subst_finite (HasSubst.smul_X a) f n)]

Premises used: finsum_eq_sum, MvPowerSeries.coeff_subst, MvPowerSeries.HasSubst.smul_X, MvPowerSeries.coeff_subst_finite