awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i j : σ →₀ ℕ
hij : i + j = 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 rw : HMul.hMul (α := R) (β := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R)
    (MvPolynomial.coeff (i, j).2 ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) g) : R) =
  HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
    ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R)
Tactic: rw [coeff_truncFinset_of_mem _ (hs (show i ≤ x by simp [← hij]) hx),
    coeff_truncFinset_of_mem _ (hs (show j ≤ x by simp [← hij]) hx)]
-- 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
i j : σ →₀ ℕ
hij : i + j = x
rw :
  HMul.hMul (α := R) (β := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R)
      (MvPolynomial.coeff (i, j).2 ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) g) : R) =
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R)
⊢ 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 rw₁ : HMul.hMul (α := R) (β := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R)
    ((coeff j : (a : MvPowerSeries σ R) → R) g : R) =
  HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
    ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R)
Tactic: rw [coeff_truncFinset_of_mem _ (hs (show i ≤ x by simp [← hij]) hx),
    coeff_truncFinset_of_mem _ (hs (show j ≤ x by simp [← hij]) hx)]
-- 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: classical
  simp only [MvPowerSeries.coeff_mul, MvPolynomial.coeff_mul]
  apply sum_congr rfl
  rintro ⟨i, j⟩ hij
  simp only [mem_antidiagonal] at hij
  rw [coeff_truncFinset_of_mem _ (hs (show i ≤ x by simp [← hij]) hx),
    coeff_truncFinset_of_mem _ (hs (show j ≤ x by simp [← hij]) hx)]
-- 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
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))
⊢ 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₁ : ∀ 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: classical
  simp only [MvPowerSeries.coeff_mul, MvPolynomial.coeff_mul]
  apply sum_congr rfl
  rintro ⟨i, j⟩ hij
  simp only [mem_antidiagonal] at hij
  rw [coeff_truncFinset_of_mem _ (hs (show i ≤ x by simp [← hij]) hx),
    coeff_truncFinset_of_mem _ (hs (show j ≤ x by simp [← hij]) hx)]
-- 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
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))
simp₁ :
  ∀ 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)
⊢ 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₂ : ∀ (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)
Tactic: classical
  simp only [MvPowerSeries.coeff_mul, MvPolynomial.coeff_mul]
  apply sum_congr rfl
  rintro ⟨i, j⟩ hij
  simp only [mem_antidiagonal] at hij
  rw [coeff_truncFinset_of_mem _ (hs (show i ≤ x by simp [← hij]) hx),
    coeff_truncFinset_of_mem _ (hs (show j ≤ x by simp [← hij]) hx)]
-- 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
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))
simp₁ :
  ∀ 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)
simp₂ :
  ∀ (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)
⊢ 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₃ : ∀ (i j : σ →₀ ℕ) (hij : i + j = 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)
Tactic: classical
  simp only [MvPowerSeries.coeff_mul, MvPolynomial.coeff_mul]
  apply sum_congr rfl
  rintro ⟨i, j⟩ hij
  simp only [mem_antidiagonal] at hij
  rw [coeff_truncFinset_of_mem _ (hs (show i ≤ x by simp [← hij]) hx),
    coeff_truncFinset_of_mem _ (hs (show j ≤ x by simp [← hij]) hx)]
-- 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 (σ →₀ ℕ))
k : ℕ
p : MvPowerSeries σ R
n : ℕ
hmn : 1 ≤ n
ih :
  Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) n) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ n) : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1)) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1)) : MvPolynomial σ R)
have succ : ∀ (x : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff x
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1))))
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1))))
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 : Finset (σ →₀ ℕ)
hs : IsLowerSet (↑s : Set (σ →₀ ℕ))
k : ℕ
p : MvPowerSeries σ R
n : ℕ
hmn : 1 ≤ n
ih :
  Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) n) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ n) : MvPolynomial σ R)
x : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff x
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1))))
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1))))
have pos : ∀ (hx : x ∈ s),
  Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff x
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1))))
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1))))
Tactic: by_cases hx : 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 (σ →₀ ℕ))
k : ℕ
p : MvPowerSeries σ R
n : ℕ
hmn : 1 ≤ n
ih :
  Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) n) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ n) : MvPolynomial σ R)
x : σ →₀ ℕ
pos :
  ∀ (hx : x ∈ s),
    Eq.{u_2 + 1} (α := R)
      (MvPolynomial.coeff x
        ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          (HPow.hPow (α := MvPowerSeries σ R)
            (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1))))
      (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1))))
⊢ Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff x
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1))))
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1))))
have neg : ∀ (hx : x ∉ s),
  Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff x
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1))))
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1))))
Tactic: by_cases hx : 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 (σ →₀ ℕ))
k : ℕ
p : MvPowerSeries σ R
n : ℕ
hmn : 1 ≤ n
ih :
  Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) n) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ n) : MvPolynomial σ R)
x : σ →₀ ℕ
hx : x ∈ s
⊢ Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff x
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1))))
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1))))
have pos : Eq.{u_2 + 1} (α := R)
  ((coeff x : (a : MvPowerSeries σ R) → R)
      (HPow.hPow (α := MvPowerSeries σ R)
        (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1)) :
    R)
  (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1))) : R)
Tactic: rw [coeff_truncFinset_of_mem _ hx, coeff_truncFinset_of_mem _ hx, pow_succ,
        ← coeff_truncFinset_mul_truncFinset_eq_coeff_mul hs _ _ hx, ih, truncFinset_truncFinset
        (by rfl), pow_succ, coeff_truncFinset_mul_truncFinset_eq_coeff_mul hs _ _ hx]
-- 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 (σ →₀ ℕ))
k : ℕ
p : MvPowerSeries σ R
n : ℕ
hmn : 1 ≤ n
ih :
  Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) n) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ n) : MvPolynomial σ R)
x : σ →₀ ℕ
hx : x ∈ s
pos :
  Eq.{u_2 + 1} (α := R)
    ((coeff x : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1)) :
      R)
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1))) : R)
⊢ Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff x
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1))))
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1))))
have pos₁ : Eq.{u_2 + 1} (α := R)
  ((coeff x : (a : MvPowerSeries σ R) → R)
      (HPow.hPow (α := MvPowerSeries σ R)
        (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1)) :
    R)
  ((coeff x : (a : MvPowerSeries σ R) → R) (p ^ (n + 1)) : R)
Tactic: rw [coeff_truncFinset_of_mem _ hx, coeff_truncFinset_of_mem _ hx, pow_succ,
        ← coeff_truncFinset_mul_truncFinset_eq_coeff_mul hs _ _ hx, ih, truncFinset_truncFinset
        (by rfl), pow_succ, coeff_truncFinset_mul_truncFinset_eq_coeff_mul hs _ _ hx]
-- 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 (σ →₀ ℕ))
k : ℕ
p : MvPowerSeries σ R
n : ℕ
hmn : 1 ≤ n
ih :
  Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) n) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ n) : MvPolynomial σ R)
x : σ →₀ ℕ
hx : x ∈ s
pos :
  Eq.{u_2 + 1} (α := R)
    ((coeff x : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1)) :
      R)
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1))) : R)
pos₁ :
  Eq.{u_2 + 1} (α := R)
    ((coeff x : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1)) :
      R)
    ((coeff x : (a : MvPowerSeries σ R) → R) (p ^ (n + 1)) : R)
⊢ Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff x
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1))))
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1))))
have pos₂ : Eq.{u_2 + 1} (α := R)
  ((coeff x : (a : MvPowerSeries σ R) → R)
      (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) n *
        (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R)) :
    R)
  ((coeff x : (a : MvPowerSeries σ R) → R) (p ^ (n + 1)) : R)
Tactic: rw [coeff_truncFinset_of_mem _ hx, coeff_truncFinset_of_mem _ hx, pow_succ,
        ← coeff_truncFinset_mul_truncFinset_eq_coeff_mul hs _ _ hx, ih, truncFinset_truncFinset
        (by rfl), pow_succ, coeff_truncFinset_mul_truncFinset_eq_coeff_mul hs _ _ hx]
-- 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 (σ →₀ ℕ))
k : ℕ
p : MvPowerSeries σ R
n : ℕ
hmn : 1 ≤ n
ih :
  Eq (α := MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) n) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ n) : MvPolynomial σ R)
x : σ →₀ ℕ
hx : x ∈ s
pos :
  Eq.{u_2 + 1} (α := R)
    ((coeff x : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1)) :
      R)
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1))) : R)
pos₁ :
  Eq.{u_2 + 1} (α := R)
    ((coeff x : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1)) :
      R)
    ((coeff x : (a : MvPowerSeries σ R) → R) (p ^ (n + 1)) : R)
pos₂ :
  Eq.{u_2 + 1} (α := R)
    ((coeff x : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R)
            (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) n *
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R)) :
      R)
    ((coeff x : (a : MvPowerSeries σ R) → R) (p ^ (n + 1)) : R)
⊢ Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff x
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) (n + 1))))
    (MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ (n + 1))))
have pos₃ : MvPolynomial.coeff x
    (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          (HPow.hPow (α := MvPowerSeries σ R)
            (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) n) :
        MvPolynomial σ R)
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          (↑((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) : MvPowerSeries σ R) :
        MvPolynomial σ R)) =
  (coeff x : (a : MvPowerSeries σ R) → R) (p ^ (n + 1))
Tactic: rw [coeff_truncFinset_of_mem _ hx, coeff_truncFinset_of_mem _ hx, pow_succ,
        ← coeff_truncFinset_mul_truncFinset_eq_coeff_mul hs _ _ hx, ih, truncFinset_truncFinset
        (by rfl), pow_succ, coeff_truncFinset_mul_truncFinset_eq_coeff_mul hs _ _ hx]