awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
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
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)))
⊢ 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)

Tactic:
ext x
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
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)))
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)))
⊢ 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
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
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 : σ →₀ ℕ
h : 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:
grind [coeff_map, MvPolynomial.coeff_map]

Premises used: MvPolynomial.coeff_map, MvPowerSeries.coeff_map
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
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 : σ →₀ ℕ
h : 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:
grind [coeff_map, MvPolynomial.coeff_map]

Premises used: MvPolynomial.coeff_map, MvPowerSeries.coeff_map
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
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)

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

Premises used: MvPolynomial.coeff_mul, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
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
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)
⊢ 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:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
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
⊢ i + j = x

Tactic:
simp only [mem_antidiagonal] at hij

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
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
⊢ i ≤ x

Tactic:
simp [← hij]
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
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
⊢ j ≤ x

Tactic:
simp [← hij]
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
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)
rw₁ 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)
⊢ 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:
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)]

Premises used: MvPowerSeries.coeff_truncFinset_of_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
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)
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)
⊢ 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)

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)]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, Finset.sum_congr, rfl, MvPolynomial.coeff_mul, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
hs : IsLowerSet (↑s : Set (σ →₀ ℕ))
k : ℕ
p : MvPowerSeries σ 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) 1) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (HPow.hPow (β := ℕ) p 1) : MvPolynomial σ R)

Tactic:
simp [truncFinset_truncFinset]

Premises used: MvPowerSeries.truncFinset_truncFinset
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
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)
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))))
⊢ 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)

Tactic:
ext x
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
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))))
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))))
⊢ 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
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
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
⊢ s ⊆ s

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
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))))

Tactic:
simp [coeff_truncFinset_eq_zero _ hx]

Premises used: MvPowerSeries.coeff_truncFinset_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
hs : IsLowerSet (↑s : Set (σ →₀ ℕ))
k : ℕ
hk : 1 ≤ k
p : MvPowerSeries σ R
base :
  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) 1) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (HPow.hPow (β := ℕ) p 1) : MvPolynomial σ R)
succ :
  ∀ (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)
⊢ 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) k) :
      MvPolynomial σ R)
    ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (p ^ k) : MvPolynomial σ R)

Tactic:
induction k, hk using Nat.le_induction with
  | base => simp [truncFinset_truncFinset]
  | succ n hmn ih =>
    ext x; by_cases hx : x ∈ s
    · 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]
    simp [coeff_truncFinset_eq_zero _ hx]

Premises used: pow_succ, MvPowerSeries.truncFinset_truncFinset
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPowerSeries σ R
a : σ →₀ ℕ
contrapose :
  a ∉ s →
    a ∉ MvPolynomial.support.{u_2, u_1} (R := R) ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p)
⊢ Membership.mem (γ := Finset (σ →₀ ℕ))
      (MvPolynomial.support.{u_2, u_1} (R := R) ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p)) a →
    a ∈ s

Tactic:
contrapose
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPowerSeries σ R
a : σ →₀ ℕ
⊢ a ∉ s →
    a ∉ MvPolynomial.support.{u_2, u_1} (R := R) ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p)

Tactic:
simpa using coeff_truncFinset_eq_zero p

Premises used: MvPowerSeries.coeff_truncFinset_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPowerSeries σ R
⊢ MvPolynomial.totalDegree.{u_2, u_1} (R := R) (σ := σ)
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) ≤
    s.sup (⇑degree : (a : σ →₀ ℕ) → ℕ)

Tactic:
simpa [MvPolynomial.totalDegree] using sup_mono (support_truncFinset_subset p)

Premises used: MvPolynomial.totalDegree, Finset.sup_mono, MvPowerSeries.support_truncFinset_subset
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
⊢ (truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) = p ↔ p.support ⊆ s

Tactic:
⟨fun h ↦ ?_, fun h ↦ MvPolynomial.ext _ _ fun x ↦ ?_⟩

Premises used: MvPolynomial.ext, MvPowerSeries.truncFinset, MvPolynomial.toMvPowerSeries, Iff.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
refine_1 :
  ∀ (h : (truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) = p), p.support ⊆ s
refine_2 :
  ∀ (h : p.support ⊆ s) (x : σ →₀ ℕ),
    MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) =
      MvPolynomial.coeff x p
⊢ (truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) = p ↔ p.support ⊆ s

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ MvPolynomial.ext _ _ fun x ↦ ?_⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
h : (truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) = p
refine_1 :
  MvPolynomial.support.{u_2, u_1} (R := R)
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) ⊆
    s
⊢ p.support ⊆ s

Tactic:
rw [← h]
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
h : (truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) = p
⊢ MvPolynomial.support.{u_2, u_1} (R := R)
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) ⊆
    s

Tactic:
support_truncFinset_subset ..

Premises used: MvPowerSeries.support_truncFinset_subset
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
h : (truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R) = p
⊢ MvPolynomial.support.{u_2, u_1} (R := R)
      ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) ⊆
    s

Tactic:
exact support_truncFinset_subset ..

Premises used: MvPowerSeries.support_truncFinset_subset
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
h : p.support ⊆ s
x : σ →₀ ℕ
pos :
  x ∈ s →
    MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) =
      MvPolynomial.coeff x p
neg :
  x ∉ s →
    MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) =
      MvPolynomial.coeff x p
⊢ MvPolynomial.coeff x ((truncFinset R s : (a : MvPowerSeries σ R) → MvPolynomial σ R) (↑p : MvPowerSeries σ R)) =
    MvPolynomial.coeff x p

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

Tactic:
grind [MvPolynomial.coeff_coe]

Premises used: MvPolynomial.coeff_coe