awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) =
    ∑
      d ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
            HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
              ((coeff n : (a : MvPowerSeries σ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
                R))
          ⋯,
      HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff n : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (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) =
    ∑
      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)

Tactic:
simp only [Pi.smul_apply', smul_eq_mul]

Premises used: Pi.smul_apply', smul_eq_mul
-- 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) =
    HMul.hMul (α := R) (β := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          (n.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
        R)
rw :
  ∀
    b ∈
      Set.Finite.toFinset (s :=
        Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
            ((coeff n : (a : MvPowerSeries σ R) → R)
                (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
              R))
        ⋯,
    b ≠ n →
      HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff n : (a : MvPowerSeries σ R) → R)
              (b.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
            R) =
        0
rw₁ :
  n ∉
      Set.Finite.toFinset (s :=
        Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
            ((coeff n : (a : MvPowerSeries σ R) → R)
                (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
              R))
        ⋯ →
    HMul.hMul (α := R) (β := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff n : (a : MvPowerSeries σ R) → R)
            (n.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
          R) =
      0
⊢ HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
    ∑
      d ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
            HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
              ((coeff n : (a : MvPowerSeries σ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
                R))
          ⋯,
      HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff n : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
          R)

Tactic:
rw [Finset.sum_eq_single n _ _]

Premises used: Finset.sum_eq_single
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (α := R) (β := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          (n.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
        R)

Tactic:
simp [mul_comm, ← monomial_eq]

Premises used: mul_comm, MvPowerSeries.monomial_eq
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
n b : σ →₀ ℕ
hb :
  b ∈
    Set.Finite.toFinset (s :=
      Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff n : (a : MvPowerSeries σ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
            R))
      ⋯
hbn : b ≠ n
rw :
  HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((monomial b : (a : R) → MvPowerSeries σ R) (b.prod fun (s : σ) (n : ℕ) ↦ a s ^ n)) :
        R) =
    0
rw₁ :
  HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
      (if n = b then b.prod fun (s : σ) (n : ℕ) ↦ a s ^ n else 0 : R) =
    0
rw₂ : HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R) (0 : R) = 0
rw₃ rw₄ : Eq.{u_3 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          (b.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
        R) =
    0

Tactic:
rw [← monomial_eq, coeff_monomial, if_neg (Ne.symm hbn), mul_zero]

Premises used: Ne.symm, MulZeroClass.mul_zero, MvPowerSeries.coeff_monomial, MvPowerSeries.monomial_eq, if_neg
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
hn :
  n ∉
    Set.Finite.toFinset (s :=
      Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff n : (a : MvPowerSeries σ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
            R))
      ⋯
⊢ HMul.hMul (α := R) (β := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          (n.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
        R) =
    0

Tactic:
simpa using hn
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries σ R) ((rescaleAlgHom a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    ((rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)

Tactic:
simp [rescaleAlgHom, rescale_eq_subst]

Premises used: MvPowerSeries.rescale_eq_subst, MvPowerSeries.rescaleAlgHom
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a b : σ → R
H :
  ∀ (f : MvPowerSeries σ R),
    Eq (α := MvPowerSeries σ R)
      ((rescaleAlgHom (a * b) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
      ((AlgHom.comp (rescaleAlgHom b) (rescaleAlgHom a) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f :
        MvPowerSeries σ R)
⊢ Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) (rescaleAlgHom (a * b))
    (AlgHom.comp (rescaleAlgHom b) (rescaleAlgHom a))

Tactic:
ext1 f
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a b : σ → R
f : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries σ R)
    ((rescaleAlgHom (a * b) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    ((AlgHom.comp (rescaleAlgHom b) (rescaleAlgHom a) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f :
      MvPowerSeries σ R)

Tactic:
simp [rescaleAlgHom_apply, rescale_rescale]

Premises used: MvPowerSeries.rescale_rescale, MvPowerSeries.rescaleAlgHom_apply
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
H :
  ∀ (f : MvPowerSeries σ R),
    Eq (α := MvPowerSeries σ R) ((rescaleAlgHom 1 : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
      ((AlgHom.id R (MvPowerSeries σ R) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
⊢ Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) (rescaleAlgHom 1) (AlgHom.id R (MvPowerSeries σ R))

Tactic:
ext1 f
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
f : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries σ R) ((rescaleAlgHom 1 : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    ((AlgHom.id R (MvPowerSeries σ R) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)

Tactic:
simp [rescaleAlgHom, subst_self]

Premises used: MvPowerSeries.rescaleAlgHom, MvPowerSeries.subst_self
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R_1 : Type u_2
S : Type u_3
inst : CommSemiring R_1
s_1 : Finset (σ →₀ ℕ)
R : Type u_4
inst_1 : CommSemiring R
s : Finset (σ →₀ ℕ)
x x_1 : MvPowerSeries σ R
⊢ ∑ x_2 ∈ s,
      (MvPolynomial.monomial x_2 : (a : R) → MvPolynomial σ R) ((coeff x_2 : (a : MvPowerSeries σ R) → R) (x + x_1)) =
    HAdd.hAdd (α := MvPolynomial σ R)
      (∑ x_2 ∈ s,
        (MvPolynomial.monomial x_2 : (a : R) → MvPolynomial σ R) ((coeff x_2 : (a : MvPowerSeries σ R) → R) x))
      (∑ x ∈ s, (MvPolynomial.monomial x : (a : R) → MvPolynomial σ R) ((coeff x : (a : MvPowerSeries σ R) → R) x_1))

Tactic:
simp [sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R_1 : Type u_2
S : Type u_3
inst : CommSemiring R_1
s_1 : Finset (σ →₀ ℕ)
R : Type u_4
inst_1 : CommSemiring R
s : Finset (σ →₀ ℕ)
x : R
x_1 : MvPowerSeries σ R
a :
  ∀ (m : σ →₀ ℕ),
    MvPolynomial.coeff m
        (∑ x_2 ∈ s,
          (MvPolynomial.monomial x_2 : (a : R) → MvPolynomial σ R)
            ((coeff x_2 : (a : MvPowerSeries σ R) → R) (x • x_1))) =
      MvPolynomial.coeff m
        (HSMul.hSMul (α := R) (β := MvPolynomial σ R) ((RingHom.id R : (a : R) → R) x : R)
          (∑ x ∈ s,
            (MvPolynomial.monomial x : (a : R) → MvPolynomial σ R) ((coeff x : (a : MvPowerSeries σ R) → R) x_1)))
⊢ ∑ x_2 ∈ s,
      (MvPolynomial.monomial x_2 : (a : R) → MvPolynomial σ R) ((coeff x_2 : (a : MvPowerSeries σ R) → R) (x • x_1)) =
    HSMul.hSMul (α := R) (β := MvPolynomial σ R) ((RingHom.id R : (a : R) → R) x : R)
      (∑ x ∈ s, (MvPolynomial.monomial x : (a : R) → MvPolynomial σ R) ((coeff x : (a : MvPowerSeries σ R) → R) x_1))

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R_1 : Type u_2
S : Type u_3
inst : CommSemiring R_1
s_1 : Finset (σ →₀ ℕ)
R : Type u_4
inst_1 : CommSemiring R
s : Finset (σ →₀ ℕ)
x : R
x_1 : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m
      (∑ x_2 ∈ s,
        (MvPolynomial.monomial x_2 : (a : R) → MvPolynomial σ R)
          ((coeff x_2 : (a : MvPowerSeries σ R) → R) (x • x_1))) =
    MvPolynomial.coeff m
      (HSMul.hSMul (α := R) (β := MvPolynomial σ R) ((RingHom.id R : (a : R) → R) x : R)
        (∑ x ∈ s, (MvPolynomial.monomial x : (a : R) → MvPolynomial σ R) ((coeff x : (a : MvPowerSeries σ R) → R) x_1)))

Tactic:
simp [MvPolynomial.coeff_sum]

Premises used: MvPolynomial.coeff_sum
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R_1 : Type u_2
S : Type u_3
inst : CommSemiring R_1
s_1 : Finset (σ →₀ ℕ)
R : Type u_4
inst_1 : CommSemiring R
s : Finset (σ →₀ ℕ)
x : R
x_1 : MvPowerSeries σ R
a a₁ :
  ∀ (m : σ →₀ ℕ),
    MvPolynomial.coeff m
        (∑ x_2 ∈ s,
          (MvPolynomial.monomial x_2 : (a : R) → MvPolynomial σ R)
            ((coeff x_2 : (a : MvPowerSeries σ R) → R) (x • x_1))) =
      MvPolynomial.coeff m
        (HSMul.hSMul (α := R) (β := MvPolynomial σ R) ((RingHom.id R : (a : R) → R) x : R)
          (∑ x ∈ s,
            (MvPolynomial.monomial x : (a : R) → MvPolynomial σ R) ((coeff x : (a : MvPowerSeries σ R) → R) x_1)))
⊢ ∑ x_2 ∈ s,
      (MvPolynomial.monomial x_2 : (a : R) → MvPolynomial σ R) ((coeff x_2 : (a : MvPowerSeries σ R) → R) (x • x_1)) =
    HSMul.hSMul (α := R) (β := MvPolynomial σ R) ((RingHom.id R : (a : R) → R) x : R)
      (∑ x ∈ s, (MvPolynomial.monomial x : (a : R) → MvPolynomial σ R) ((coeff x : (a : MvPowerSeries σ R) → R) x_1))

Tactic:
classical
    ext; simp [MvPolynomial.coeff_sum]

Premises used: MvPolynomial.coeff_sum
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPowerSeries σ R
⊢ Eq (α := MvPolynomial σ R) ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
    (∑ x ∈ s, (MvPolynomial.monomial x : (a : R) → MvPolynomial σ R) ((coeff x : (a : MvPowerSeries σ R) → R) p) :
      MvPolynomial σ R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
p : MvPowerSeries σ R
h : x ∈ s
⊢ Eq.{u_2 + 1} (α := R) (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : R)
    ((coeff x : (a : MvPowerSeries σ R) → R) p : R)

Tactic:
simp [truncFinset_apply, MvPolynomial.coeff_sum, h]

Premises used: MvPowerSeries.truncFinset_apply, MvPolynomial.coeff_sum
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
p : MvPowerSeries σ R
h : x ∈ s
⊢ Eq.{u_2 + 1} (α := R) (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : R)
    ((coeff x : (a : MvPowerSeries σ R) → R) p : R)

Tactic:
classical
  simp [truncFinset_apply, MvPolynomial.coeff_sum, h]

Premises used: MvPowerSeries.truncFinset_apply, MvPolynomial.coeff_sum
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
p : MvPowerSeries σ R
h : x ∉ s
⊢ Eq.{u_2 + 1} (α := R) (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p)) 0

Tactic:
simp [truncFinset_apply, MvPolynomial.coeff_sum, h]

Premises used: MvPowerSeries.truncFinset_apply, MvPolynomial.coeff_sum
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
p : MvPowerSeries σ R
h : x ∉ s
⊢ Eq.{u_2 + 1} (α := R) (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p)) 0

Tactic:
classical
  simp [truncFinset_apply, MvPolynomial.coeff_sum, h]

Premises used: MvPowerSeries.truncFinset_apply, MvPolynomial.coeff_sum
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
inst_1 : DecidableEq σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
⊢ Eq.{u_2 + 1} (α := R) (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : R)
    (if x ∈ s then (coeff x : (a : MvPowerSeries σ R) → R) p else 0 : R)

Tactic:
simp [truncFinset_apply, MvPolynomial.coeff_sum]

Premises used: MvPowerSeries.truncFinset_apply, MvPolynomial.coeff_sum
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∈ s
a :
  ∀ (m : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      (MvPolynomial.coeff m
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) ((monomial x : (a : R) → MvPowerSeries σ R) r)))
      (MvPolynomial.coeff m ((MvPolynomial.monomial x : (a : R) → MvPolynomial σ R) r))
⊢ Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) ((monomial x : (a : R) → MvPowerSeries σ R) r) :
      MvPolynomial σ R)
    ((MvPolynomial.monomial x : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∈ s
m : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff m
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) ((monomial x : (a : R) → MvPowerSeries σ R) r)))
    (MvPolynomial.coeff m ((MvPolynomial.monomial x : (a : R) → MvPolynomial σ R) r))

Tactic:
grind [coeff_monomial, MvPolynomial.coeff_monomial]

Premises used: MvPowerSeries.coeff_monomial, MvPolynomial.coeff_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∈ s
a :
  ∀ (m : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      (MvPolynomial.coeff m
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) ((monomial x : (a : R) → MvPowerSeries σ R) r)))
      (MvPolynomial.coeff m ((MvPolynomial.monomial x : (a : R) → MvPolynomial σ R) r))
⊢ Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) ((monomial x : (a : R) → MvPowerSeries σ R) r) :
      MvPolynomial σ R)
    ((MvPolynomial.monomial x : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)

Tactic:
classical
  ext
  grind [coeff_monomial, MvPolynomial.coeff_monomial]

Premises used: MvPowerSeries.coeff_monomial, MvPolynomial.coeff_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∉ s
a :
  ∀ (m : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      (MvPolynomial.coeff m
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) ((monomial x : (a : R) → MvPowerSeries σ R) r)))
      (MvPolynomial.coeff m 0)
⊢ Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) ((monomial x : (a : R) → MvPowerSeries σ R) r) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∉ s
m : σ →₀ ℕ
a : m ∈ s → m = x → r = 0
⊢ Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff m
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) ((monomial x : (a : R) → MvPowerSeries σ R) r)))
    (MvPolynomial.coeff m 0)

Tactic:
simp [truncFinset, MvPolynomial.coeff_sum, coeff_monomial]

Premises used: MvPowerSeries.truncFinset, MvPowerSeries.coeff_monomial, MvPolynomial.coeff_sum
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∉ s
m : σ →₀ ℕ
⊢ m ∈ s → m = x → r = 0

Tactic:
grind
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∉ s
a a₁ :
  ∀ (m : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      (MvPolynomial.coeff m
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) ((monomial x : (a : R) → MvPowerSeries σ R) r)))
      (MvPolynomial.coeff m 0)
a₂ : ∀ m ∈ s, m = x → r = 0
⊢ Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) ((monomial x : (a : R) → MvPowerSeries σ R) r) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)

Tactic:
classical
  ext; simp [truncFinset, MvPolynomial.coeff_sum, coeff_monomial]
  grind

Premises used: MvPowerSeries.truncFinset, MvPowerSeries.coeff_monomial, MvPolynomial.coeff_sum
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
h : 0 ∈ s
r : R
⊢ Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) ((C : (a : R) → MvPowerSeries σ R) r) :
      MvPolynomial σ R)
    ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)

Tactic:
truncFinset_monomial r h

Premises used: Function.update, Pi.single, dite, MvPowerSeries.truncFinset_monomial, Finsupp.single
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
h : 0 ∈ s
⊢ Eq (α := MvPolynomial σ R) ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) 1) 1

Tactic:
truncFinset_C h 1

Premises used: Function.update, MvPowerSeries.truncFinset_C, Pi.single, dite, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s t : Finset (σ →₀ ℕ)
h : s ⊆ t
p : MvPowerSeries σ R
a :
  ∀ (x : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      (MvPolynomial.coeff x
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          (↑((truncFinset R t : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R)))
      (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p))
⊢ Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (↑((truncFinset R t : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)

Tactic:
ext x
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s t : Finset (σ →₀ ℕ)
h : s ⊆ t
p : MvPowerSeries σ R
x : σ →₀ ℕ
pos :
  x ∈ s →
    Eq.{u_2 + 1} (α := R)
      (MvPolynomial.coeff x
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          (↑((truncFinset R t : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R)))
      (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p))
neg :
  x ∉ s →
    Eq.{u_2 + 1} (α := R)
      (MvPolynomial.coeff x
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          (↑((truncFinset R t : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R)))
      (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p))
⊢ Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff x
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (↑((truncFinset R t : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R)))
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p))

Tactic:
by_cases x ∈ s
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s t : Finset (σ →₀ ℕ)
h : s ⊆ t
p : MvPowerSeries σ R
x : σ →₀ ℕ
h_1 : x ∈ s
⊢ Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff x
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (↑((truncFinset R t : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R)))
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p))

Tactic:
grind [MvPolynomial.coeff_coe]

Premises used: MvPolynomial.coeff_coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s t : Finset (σ →₀ ℕ)
h : s ⊆ t
p : MvPowerSeries σ R
x : σ →₀ ℕ
h_1 : x ∉ s
⊢ Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff x
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (↑((truncFinset R t : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R)))
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p))

Tactic:
grind [MvPolynomial.coeff_coe]

Premises used: MvPolynomial.coeff_coe