awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ Eq.{u_2 + 1} (α := R) (MvPolynomial.coeff m ((trunc R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ) : R)
    (if m < n then (coeff m : (a : MvPowerSeries σ R) → R) φ else 0 : R)

Tactic:
simpa using coeff_truncFinset (s := Iio n) (x := m) φ

Premises used: MvPowerSeries.coeff_truncFinset
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
⊢ 0 ∈ Iio n

Tactic:
simpa using pos_of_ne_zero hnn

Premises used: pos_of_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
a : R
⊢ 0 ∈ Iio n

Tactic:
simpa using pos_of_ne_zero hnn

Premises used: pos_of_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
a₁ :
  ∀ (m : σ →₀ ℕ),
    MvPolynomial.coeff m
        ((trunc R n : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          (HMul.hMul (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) p)) =
      MvPolynomial.coeff m
        (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          ((trunc R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R))
⊢ (trunc R n : (a : MvPowerSeries σ R) → MvPolynomial σ R)
      (HMul.hMul (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) p) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((trunc R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)

Tactic:
ext m
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m
      ((trunc R n : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HMul.hMul (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) p)) =
    MvPolynomial.coeff m
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
        ((trunc R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R))

Tactic:
simp [coeff_trunc]

Premises used: MvPowerSeries.coeff_trunc
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : DecidableEq σ
inst_1 : CommSemiring R
inst_2 : CommSemiring S
n : σ →₀ ℕ
f : R →+* S
p : MvPowerSeries σ R
⊢ Eq (α := MvPolynomial σ S)
    ((trunc S n : (a : MvPowerSeries σ S) → MvPolynomial σ S)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) p) :
      MvPolynomial σ S)
    ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((trunc R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) :
      MvPolynomial σ S)

Tactic:
truncFinset_map f p

Premises used: MvPowerSeries.truncFinset_map
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ Eq.{u_2 + 1} (α := R) (MvPolynomial.coeff m ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ) : R)
    (if m ≤ n then (coeff m : (a : MvPowerSeries σ R) → R) φ else 0 : R)

Tactic:
simpa using coeff_truncFinset (s := Iic n) (x := m) φ

Premises used: MvPowerSeries.coeff_truncFinset
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
n m : σ →₀ ℕ
h : n ≤ m
φ : MvPowerSeries σ R
⊢ Eq (α := MvPolynomial σ R)
    ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (↑((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ) : MvPowerSeries σ R) :
      MvPolynomial σ R)
    ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)

Tactic:
truncFinset_truncFinset (Iic_subset_Iic.mpr h) φ

Premises used: Iff.mpr, Finset.Iic_subset_Iic, MvPowerSeries.truncFinset_truncFinset
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
n : σ →₀ ℕ
⊢ 0 ∈ Iic n

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
n : σ →₀ ℕ
a : R
⊢ 0 ∈ Iic n

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
a : σ →₀ ℕ
⊢ ∀ ⦃b : σ →₀ ℕ⦄, b ≤ a → a ∈ (↑(Iic n) : Set (σ →₀ ℕ)) → b ∈ (↑(Iic n) : Set (σ →₀ ℕ))

Tactic:
grind
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ m ∈ Iic n

Tactic:
simpa
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ (coeff m : (a : MvPowerSeries σ R) → R) (f * g) =
    MvPolynomial.coeff m
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R))

Tactic:
(coeff_trunc'_mul_trunc'_eq_coeff_mul n f g h).symm

Premises used: MvPowerSeries.coeff_trunc'_mul_trunc'_eq_coeff_mul, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
n : σ →₀ ℕ
k : ℕ
hk : 1 ≤ k
φ : MvPowerSeries σ R
a : σ →₀ ℕ
⊢ ∀ ⦃b : σ →₀ ℕ⦄, b ≤ a → a ∈ (↑(Iic n) : Set (σ →₀ ℕ)) → b ∈ (↑(Iic n) : Set (σ →₀ ℕ))

Tactic:
grind
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
a₁ :
  ∀ (m : σ →₀ ℕ),
    MvPolynomial.coeff m
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          (HMul.hMul (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) p)) =
      MvPolynomial.coeff m
        (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
          ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R))
⊢ (trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R)
      (HMul.hMul (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) p) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R)

Tactic:
ext m
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m
      ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HMul.hMul (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) p)) =
    MvPolynomial.coeff m
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p : MvPolynomial σ R))

Tactic:
simp [coeff_trunc']

Premises used: MvPowerSeries.coeff_trunc'
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : DecidableEq σ
inst_1 : CommSemiring R
inst_2 : CommSemiring S
n : σ →₀ ℕ
f : R →+* S
p : MvPowerSeries σ R
⊢ Eq (α := MvPolynomial σ S)
    ((trunc' S n : (a : MvPowerSeries σ S) → MvPolynomial σ S)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) p) :
      MvPolynomial σ S)
    ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) :
      MvPolynomial σ S)

Tactic:
truncFinset_map f p

Premises used: MvPowerSeries.truncFinset_map
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
n : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ MvPolynomial.totalDegree.{u_2, u_1} (R := R) (σ := σ) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ) ≤
    (degree : (a : σ →₀ ℕ) → ℕ) n

Tactic:
simpa [← sup_Iic_of_monotone degree_mono] using totalDegree_truncFinset φ

Premises used: MvPowerSeries.totalDegree_truncFinset, Finsupp.degree_mono, Finset.sup_Iic_of_monotone
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
h : f = g
⊢ ∀ (n : σ →₀ ℕ),
    Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
refine :
  ∀
    (h :
      ∀ (n : σ →₀ ℕ),
        Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)),
    f = g
⊢ f = g ↔
    ∀ (n : σ →₀ ℕ),
      Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)

Tactic:
refine ⟨fun h => by simp [h], fun h => ?_⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
h :
  ∀ (n : σ →₀ ℕ),
    Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
h₁ :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) g : R)
⊢ f = g

Tactic:
ext n
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
h :
  ∀ (n : σ →₀ ℕ),
    Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
n : σ →₀ ℕ
⊢ Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)

Tactic:
specialize h n
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h :
  Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
f' : MvPowerSeries σ R
rw :
  Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
    (if n ≤ n then (coeff n : (a : MvPowerSeries σ R) → R) f' else 0 : R)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
    (MvPolynomial.coeff n ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f') : R)

Tactic:
rw [coeff_trunc', if_pos le_rfl]

Premises used: le_rfl, if_pos, MvPowerSeries.coeff_trunc'
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h :
  Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
⊢ ∀ {f' : MvPowerSeries σ R},
    Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
      (MvPolynomial.coeff n ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f') : R)

Tactic:
have {f' : MvPowerSeries σ R} : f'.coeff n = (trunc' R n f').coeff n := by
    rw [coeff_trunc', if_pos le_rfl]
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h :
  Eq (α := MvPolynomial σ R) ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
this :
  ∀ {f' : MvPowerSeries σ R},
    Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
      (MvPolynomial.coeff n ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f') : R)
h₁ :
  Eq.{u_2 + 1} (α := R) (MvPolynomial.coeff n ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f))
    (MvPolynomial.coeff n ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) g))
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) ((coeff n : (a : MvPowerSeries σ R) → R) g : R)

Tactic:
simp_rw [this, h]
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
h : f = g
⊢ ∃ᶠ (m : σ →₀ ℕ) in atTop,
    Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)

Tactic:
simp [h, atTop_neBot]

Premises used: Filter.atTop_neBot
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
refine :
  ∀
    (h :
      ∃ᶠ (m : σ →₀ ℕ) in atTop,
        Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
          ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)),
    f = g
⊢ f = g ↔
    ∃ᶠ (m : σ →₀ ℕ) in atTop,
      Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
        ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)

Tactic:
refine ⟨fun h => by simp [h, atTop_neBot], fun h => ?_⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
h :
  ∃ᶠ (m : σ →₀ ℕ) in atTop,
    Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
h₁ :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) g : R)
⊢ f = g

Tactic:
ext n
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
h :
  ∃ᶠ (m : σ →₀ ℕ) in atTop,
    Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
n : σ →₀ ℕ
h₁ :
  ∀ (m : σ →₀ ℕ) (hm₁ : n ≤ m)
    (hm₂ :
      Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
        ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)),
    Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) g : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) ((coeff n : (a : MvPowerSeries σ R) → R) g : R)

Tactic:
obtain ⟨m, hm₁, hm₂⟩ := h.forall_exists_of_atTop n

Premises used: Filter.Frequently.forall_exists_of_atTop
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
h :
  ∃ᶠ (m : σ →₀ ℕ) in atTop,
    Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
n m : σ →₀ ℕ
hm₁ : n ≤ m
hm₂ :
  Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
f' : MvPowerSeries σ R
rw :
  Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
    (if n ≤ m then (coeff n : (a : MvPowerSeries σ R) → R) f' else 0 : R)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
    (MvPolynomial.coeff n ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f') : R)

Tactic:
rw [coeff_trunc', if_pos hm₁]

Premises used: if_pos, MvPowerSeries.coeff_trunc'
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
h :
  ∃ᶠ (m : σ →₀ ℕ) in atTop,
    Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
n m : σ →₀ ℕ
hm₁ : n ≤ m
hm₂ :
  Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
⊢ ∀ {f' : MvPowerSeries σ R},
    Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
      (MvPolynomial.coeff n ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f') : R)

Tactic:
have {f' : MvPowerSeries σ R} : f'.coeff n = (trunc' R m f').coeff n := by
    rw [coeff_trunc', if_pos hm₁]
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
inst : DecidableEq σ
inst_1 : CommSemiring R
f g : MvPowerSeries σ R
h :
  ∃ᶠ (m : σ →₀ ℕ) in atTop,
    Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
n m : σ →₀ ℕ
hm₁ : n ≤ m
hm₂ :
  Eq (α := MvPolynomial σ R) ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R)
    ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) g : MvPolynomial σ R)
this :
  ∀ {f' : MvPowerSeries σ R},
    Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f' : R)
      (MvPolynomial.coeff n ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f') : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) ((coeff n : (a : MvPowerSeries σ R) → R) g : R)

Tactic:
simp [this, hm₂]
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
p : MvPowerSeries σ R
x : σ →₀ ℕ
h : (degree : (a : σ →₀ ℕ) → ℕ) x < n
⊢ Membership.mem (γ := Finset (σ →₀ ℕ)) (Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) ⋯)
    x

Tactic:
simpa
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
p : MvPowerSeries σ R
x : σ →₀ ℕ
h : n ≤ (degree : (a : σ →₀ ℕ) → ℕ) x
⊢ x ∉ Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) ⋯

Tactic:
simpa
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
h : n ≠ 0
revert :
  ∀ (h : n ≠ 0),
    Membership.mem (γ := Finset (σ →₀ ℕ))
      (Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) ⋯) 0
⊢ Membership.mem (γ := Finset (σ →₀ ℕ)) (Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) ⋯)
    0

Tactic:
revert h
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
contrapose : 0 ∉ Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) ⋯ → n = 0
⊢ ∀ (h : n ≠ 0),
    Membership.mem (γ := Finset (σ →₀ ℕ))
      (Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) ⋯) 0

Tactic:
contrapose
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
⊢ 0 ∉ Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) ⋯ → n = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
x : σ →₀ ℕ
p q : MvPowerSeries σ R
hx : (degree : (a : σ →₀ ℕ) → ℕ) x < n
x_1 x_2 : σ →₀ ℕ
h : x_2 ≤ x_1
simp : (degree : (a : σ →₀ ℕ) → ℕ) x_1 < n → (degree : (a : σ →₀ ℕ) → ℕ) x_2 < n
⊢ x_1 ∈ (↑(Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) ⋯) : Set (σ →₀ ℕ)) →
    x_2 ∈ (↑(Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) ⋯) : Set (σ →₀ ℕ))

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
x : σ →₀ ℕ
p q : MvPowerSeries σ R
hx : (degree : (a : σ →₀ ℕ) → ℕ) x < n
x_1 x_2 : σ →₀ ℕ
h : x_2 ≤ x_1
⊢ (degree : (a : σ →₀ ℕ) → ℕ) x_1 < n → (degree : (a : σ →₀ ℕ) → ℕ) x_2 < n

Tactic:
grind [degree_mono h]

Premises used: Finsupp.degree_mono
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
x : σ →₀ ℕ
p q : MvPowerSeries σ R
hx : (degree : (a : σ →₀ ℕ) → ℕ) x < n
⊢ Membership.mem (γ := Finset (σ →₀ ℕ)) (Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) ⋯)
    x

Tactic:
simpa
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
p : MvPowerSeries σ R
h : n ≠ 0
apply :
  sup.{0, u_1} (β := σ →₀ ℕ) (Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) ⋯)
      (⇑degree : (a : σ →₀ ℕ) → ℕ) <
    n
⊢ MvPolynomial.totalDegree.{u_2, u_1} (R := R) (σ := σ)
      ((truncTotal n : (a : MvPowerSeries σ R) → MvPolynomial σ R) p) <
    n

Tactic:
apply (totalDegree_truncFinset p).trans_lt

Premises used: MvPowerSeries.totalDegree_truncFinset, LE.le.trans_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.Trunc
Goal:
σ : Type u_1
R : Type u_2
n : ℕ
inst : Finite σ
inst_1 : CommSemiring R
p : MvPowerSeries σ R
h : n ≠ 0
⊢ sup.{0, u_1} (β := σ →₀ ℕ) (Set.Finite.toFinset (s := {f : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) f < n}) ⋯)
      (⇑degree : (a : σ →₀ ℕ) → ℕ) <
    n

Tactic:
simp [Finset.sup_lt_iff (Nat.lt_of_sub_ne_zero h)]

Premises used: Finset.sup_lt_iff, Nat.lt_of_sub_ne_zero