awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
⊢ (rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f =
    subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X) f
have 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)
Tactic: classical
  ext n
  rw [coeff_rescale]
  rw [coeff_subst (HasSubst.smul_X a),
    finsum_eq_sum _ (coeff_subst_finite (HasSubst.smul_X a) f n)]
  simp only [Pi.smul_apply', smul_eq_mul]
  rw [Finset.sum_eq_single n _ _]
  · simp [mul_comm, ← monomial_eq]
  · intro b hb hbn
    rw [← monomial_eq, coeff_monomial, if_neg (Ne.symm hbn), mul_zero]
  · intro hn
    simpa using hn
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
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
have h₁ : ∀ (n : σ →₀ ℕ),
  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: classical
  ext n
  rw [coeff_rescale]
  rw [coeff_subst (HasSubst.smul_X a),
    finsum_eq_sum _ (coeff_subst_finite (HasSubst.smul_X a) f n)]
  simp only [Pi.smul_apply', smul_eq_mul]
  rw [Finset.sum_eq_single n _ _]
  · simp [mul_comm, ← monomial_eq]
  · intro b hb hbn
    rw [← monomial_eq, coeff_monomial, if_neg (Ne.symm hbn), mul_zero]
  · intro hn
    simpa using hn
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
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)
h₁ :
  ∀ (n : σ →₀ ℕ),
    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)
⊢ (rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f =
    subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X) f
have h₂ : ∀ (n : σ →₀ ℕ),
  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))
          sorry,
      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: classical
  ext n
  rw [coeff_rescale]
  rw [coeff_subst (HasSubst.smul_X a),
    finsum_eq_sum _ (coeff_subst_finite (HasSubst.smul_X a) f n)]
  simp only [Pi.smul_apply', smul_eq_mul]
  rw [Finset.sum_eq_single n _ _]
  · simp [mul_comm, ← monomial_eq]
  · intro b hb hbn
    rw [← monomial_eq, coeff_monomial, if_neg (Ne.symm hbn), mul_zero]
  · intro hn
    simpa using hn
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
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)
h₁ :
  ∀ (n : σ →₀ ℕ),
    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)
h₂ :
  ∀ (n : σ →₀ ℕ),
    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)
⊢ (rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f =
    subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X) f
have h₃ : ∀ (n : σ →₀ ℕ),
  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))
          sorry,
      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: classical
  ext n
  rw [coeff_rescale]
  rw [coeff_subst (HasSubst.smul_X a),
    finsum_eq_sum _ (coeff_subst_finite (HasSubst.smul_X a) f n)]
  simp only [Pi.smul_apply', smul_eq_mul]
  rw [Finset.sum_eq_single n _ _]
  · simp [mul_comm, ← monomial_eq]
  · intro b hb hbn
    rw [← monomial_eq, coeff_monomial, if_neg (Ne.symm hbn), mul_zero]
  · intro hn
    simpa using hn
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a b : σ → R
⊢ Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) (rescaleAlgHom (a * b))
    (AlgHom.comp (rescaleAlgHom b) (rescaleAlgHom a))
have 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)
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
⊢ Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) (rescaleAlgHom 1) (AlgHom.id R (MvPowerSeries σ R))
have 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)
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
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
⊢ ∑ 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))
have 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)))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
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
⊢ ∑ 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))
have 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)))
Tactic: classical
    ext; simp [MvPolynomial.coeff_sum]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∈ s
⊢ 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)
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∈ s
⊢ 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)
have 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))
Tactic: classical
  ext
  grind [coeff_monomial, MvPolynomial.coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∉ s
⊢ Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) ((monomial x : (a : R) → MvPowerSeries σ R) r) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
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 0)
have a : m ∈ s → m = x → r = 0
Tactic: simp [truncFinset, MvPolynomial.coeff_sum, coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∉ s
⊢ Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) ((monomial x : (a : R) → MvPowerSeries σ R) r) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have 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)
Tactic: classical
  ext; simp [truncFinset, MvPolynomial.coeff_sum, coeff_monomial]
  grind
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
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)
⊢ Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) ((monomial x : (a : R) → MvPowerSeries σ R) r) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have a₂ : ∀ m ∈ s, m = x → r = 0
Tactic: classical
  ext; simp [truncFinset, MvPolynomial.coeff_sum, coeff_monomial]
  grind
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s t : Finset (σ →₀ ℕ)
h : s ⊆ t
p : MvPowerSeries σ R
⊢ 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)
have 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))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s t : Finset (σ →₀ ℕ)
h : s ⊆ t
p : MvPowerSeries σ R
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))
have 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))
Tactic: by_cases x ∈ s
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
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))
⊢ 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))
have 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))
Tactic: by_cases x ∈ s
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
inst_1 : CommSemiring S
f : R →+* S
p : MvPowerSeries σ R
⊢ Eq (α := MvPolynomial σ S)
    ((truncFinset S s : (a : MvPowerSeries σ S) → MvPolynomial σ S)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) p) :
      MvPolynomial σ S)
    ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) :
      MvPolynomial σ S)
have a : ∀ (x : σ →₀ ℕ),
  Eq.{u_3 + 1} (α := S)
    (MvPolynomial.coeff x
      ((truncFinset S s : (a : MvPowerSeries σ S) → MvPolynomial σ S)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) p)))
    (MvPolynomial.coeff x
      ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p)))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
inst_1 : CommSemiring S
f : R →+* S
p : MvPowerSeries σ R
x : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := S)
    (MvPolynomial.coeff x
      ((truncFinset S s : (a : MvPowerSeries σ S) → MvPolynomial σ S)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) p)))
    (MvPolynomial.coeff x
      ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p)))
have pos : x ∈ s →
  Eq.{u_3 + 1} (α := S)
    (MvPolynomial.coeff x
      ((truncFinset S s : (a : MvPowerSeries σ S) → MvPolynomial σ S)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) p)))
    (MvPolynomial.coeff x
      ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p)))
Tactic: by_cases x ∈ s
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
inst_1 : CommSemiring S
f : R →+* S
p : MvPowerSeries σ R
x : σ →₀ ℕ
pos :
  x ∈ s →
    Eq.{u_3 + 1} (α := S)
      (MvPolynomial.coeff x
        ((truncFinset S s : (a : MvPowerSeries σ S) → MvPolynomial σ S)
          ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) p)))
      (MvPolynomial.coeff x
        ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S)
          ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p)))
⊢ Eq.{u_3 + 1} (α := S)
    (MvPolynomial.coeff x
      ((truncFinset S s : (a : MvPowerSeries σ S) → MvPolynomial σ S)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) p)))
    (MvPolynomial.coeff x
      ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p)))
have neg : x ∉ s →
  Eq.{u_3 + 1} (α := S)
    (MvPolynomial.coeff x
      ((truncFinset S s : (a : MvPowerSeries σ S) → MvPolynomial σ S)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) p)))
    (MvPolynomial.coeff x
      ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p)))
Tactic: by_cases x ∈ s
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
hs : IsLowerSet (↑s : Set (σ →₀ ℕ))
x : σ →₀ ℕ
f g : MvPowerSeries σ R
hx : x ∈ s
⊢ MvPolynomial.coeff x
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)) =
    (coeff x : (a : MvPowerSeries σ R) → R) (f * g)
have simp : Eq.{u_2 + 1} (α := R)
  (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ x,
    HMul.hMul (α := R) (MvPolynomial.coeff x.1 ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) f))
      (MvPolynomial.coeff x.2 ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) g)))
  (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ x,
    HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff p.2 : (a : MvPowerSeries σ R) → R) g : R))
Tactic: simp only [MvPowerSeries.coeff_mul, MvPolynomial.coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
hs : IsLowerSet (↑s : Set (σ →₀ ℕ))
x : σ →₀ ℕ
f g : MvPowerSeries σ R
hx : x ∈ s
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ x,
      HMul.hMul (α := R) (MvPolynomial.coeff x.1 ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) f))
        (MvPolynomial.coeff x.2 ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) g)))
    (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ x,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) g : R))
have apply : ∀ x_1 ∈ @antidiagonal _ Finsupp.instAddMonoid _ x,
  HMul.hMul (α := R) (MvPolynomial.coeff x_1.1 ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) f))
      (MvPolynomial.coeff x_1.2 ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) g)) =
    HMul.hMul (α := R) (β := R) ((coeff x_1.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x_1.2 : (a : MvPowerSeries σ R) → R) g : R)
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Trunc (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
hs : IsLowerSet (↑s : Set (σ →₀ ℕ))
x : σ →₀ ℕ
f g : MvPowerSeries σ R
hx : x ∈ s
i j : σ →₀ ℕ
hij : (i, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ x
⊢ HMul.hMul (α := R) (MvPolynomial.coeff (i, j).1 ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) f))
      (MvPolynomial.coeff (i, j).2 ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) g)) =
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R)
have hij₁ : i + j = x
Tactic: simp only [mem_antidiagonal] at hij
Cleared hypotheses: hij