awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < p • φ.order
h : ∃ (i : σ), ¬p ∣ (d : (a : σ) → ℕ) i
neg :
  ∀ (i : σ) (hi : ¬p ∣ (d : (a : σ) → ℕ) i),
    Eq.{u_3 + 1} (α := R)
      ((coeff d : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
        R)
      (0 : R)
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (0 : R)

Tactic:
obtain ⟨i, hi⟩ := h
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < p • φ.order
i : σ
hi : ¬p ∣ (d : (a : σ) → ℕ) i
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (0 : R)

Tactic:
coeff_expand_of_not_dvd p hp φ hi

Premises used: MvPowerSeries.coeff_expand_of_not_dvd
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < p • φ.order
i : σ
hi : ¬p ∣ (d : (a : σ) → ℕ) i
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (0 : R)

Tactic:
exact coeff_expand_of_not_dvd p hp φ hi

Premises used: MvPowerSeries.coeff_expand_of_not_dvd
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
h :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (↑φ : MvPowerSeries σ R) : MvPowerSeries σ R) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          (↑((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) : MvPowerSeries σ R) :
        R)
⊢ Eq (α := MvPowerSeries σ R)
    ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (↑φ : MvPowerSeries σ R) : MvPowerSeries σ R)
    ((↑((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) : MvPowerSeries σ R) : MvPowerSeries σ R)

Tactic:
ext n
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
h :
  Eq.{u_3 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (↑φ : MvPowerSeries σ R) : MvPowerSeries σ R) :
      R)
    (MvPolynomial.coeff n ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) : R)
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (↑φ : MvPowerSeries σ R) : MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        (↑((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) : MvPowerSeries σ R) :
      R)

Tactic:
simp only [MvPolynomial.coeff_coe]

Premises used: MvPolynomial.coeff_coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
pos :
  ∀ (h : ∀ (i : σ), p ∣ (n : (a : σ) → ℕ) i),
    Eq.{u_3 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (↑φ : MvPowerSeries σ R) : MvPowerSeries σ R) :
        R)
      (MvPolynomial.coeff n ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) : R)
neg :
  ∀ (h : ∃ (i : σ), ¬p ∣ (n : (a : σ) → ℕ) i),
    Eq.{u_3 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (↑φ : MvPowerSeries σ R) : MvPowerSeries σ R) :
        R)
      (MvPolynomial.coeff n ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) : R)
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (↑φ : MvPowerSeries σ R) : MvPowerSeries σ R) :
      R)
    (MvPolynomial.coeff n ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) : R)

Tactic:
by_cases! h : ∀ i, p ∣ n i
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (n : (a : σ) → ℕ) i
⊢ Eq (α := ℕ) ((fun (a : ℕ) ↦ a / p) 0) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (n : (a : σ) → ℕ) i
h₁ :
  ∀ (i : σ),
    Eq (α := ℕ) ((HSMul.hSMul (β := σ →₀ ℕ) p (Finsupp.mapRange (fun (a : ℕ) ↦ a / p) ⋯ n) : (a : σ) → ℕ) i : ℕ)
      ((n : (a : σ) → ℕ) i : ℕ)
⊢ HSMul.hSMul (β := σ →₀ ℕ) p (Finsupp.mapRange (fun (a : ℕ) ↦ a / p) ⋯ n) = n

Tactic:
ext i
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (n : (a : σ) → ℕ) i
i : σ
⊢ Eq (α := ℕ) ((HSMul.hSMul (β := σ →₀ ℕ) p (Finsupp.mapRange (fun (a : ℕ) ↦ a / p) ⋯ n) : (a : σ) → ℕ) i : ℕ)
    ((n : (a : σ) → ℕ) i : ℕ)

Tactic:
simp [(Nat.mul_div_cancel' (h i))]

Premises used: Nat.mul_div_cancel'
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (n : (a : σ) → ℕ) i
pos :
  ∀ (m : σ →₀ ℕ) (hm : p • m = n),
    Eq.{u_3 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (↑φ : MvPowerSeries σ R) : MvPowerSeries σ R) :
        R)
      (MvPolynomial.coeff n ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) : R)
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (↑φ : MvPowerSeries σ R) : MvPowerSeries σ R) :
      R)
    (MvPolynomial.coeff n ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) : R)

Tactic:
obtain ⟨m, hm⟩ : ∃ m, p • m = n := ⟨n.mapRange (fun a ↦ a / p) (by simp),
      by ext i; simp [(Nat.mul_div_cancel' (h i))]⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (n : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = n
pos :
  Eq.{u_3 + 1} (α := R)
    ((coeff (p • m) : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (↑φ : MvPowerSeries σ R) : MvPowerSeries σ R) :
      R)
    (MvPolynomial.coeff (p • m) ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) : R)
pos₁ :
  Eq.{u_3 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) (↑φ : MvPowerSeries σ R) : R)
    (MvPolynomial.coeff (p • m) ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) : R)
pos₂ : (coeff m : (a : MvPowerSeries σ R) → R) (↑φ : MvPowerSeries σ R) = MvPolynomial.coeff m φ
pos₃ pos₄ : MvPolynomial.coeff m φ = MvPolynomial.coeff m φ
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (↑φ : MvPowerSeries σ R) : MvPowerSeries σ R) :
      R)
    (MvPolynomial.coeff n ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) : R)

Tactic:
rw [← hm, coeff_expand_smul p hp _ _, φ.coeff_expand_smul _ hp, φ.coeff_coe]

Premises used: MvPolynomial.coeff_expand_smul, MvPowerSeries.coeff_expand_smul, MvPolynomial.coeff_coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∃ (i : σ), ¬p ∣ (n : (a : σ) → ℕ) i
neg :
  ∀ (i : σ) (hi : ¬p ∣ (n : (a : σ) → ℕ) i),
    Eq.{u_3 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (↑φ : MvPowerSeries σ R) : MvPowerSeries σ R) :
        R)
      (MvPolynomial.coeff n ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) : R)
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (↑φ : MvPowerSeries σ R) : MvPowerSeries σ R) :
      R)
    (MvPolynomial.coeff n ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) : R)

Tactic:
obtain ⟨i, hi⟩ := h
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
i : σ
hi : ¬p ∣ (n : (a : σ) → ℕ) i
neg :
  Eq.{u_3 + 1} (α := R) 0 (MvPolynomial.coeff n ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
neg₁ neg₂ : Eq.{u_3 + 1} (α := R) 0 0
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (↑φ : MvPowerSeries σ R) : MvPowerSeries σ R) :
      R)
    (MvPolynomial.coeff n ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) : R)

Tactic:
rw [coeff_expand_of_not_dvd p hp _ hi, MvPolynomial.coeff_expand_of_not_dvd _ hi]

Premises used: MvPowerSeries.coeff_expand_of_not_dvd, MvPolynomial.coeff_expand_of_not_dvd
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
a :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R)
      (MvPolynomial.coeff d
        ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
      (MvPolynomial.coeff d
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))
⊢ Eq (α := MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) :
      MvPolynomial σ R)
    ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ) :
      MvPolynomial σ R)

Tactic:
ext d
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
pos :
  ∀ (h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i),
    Eq.{u_3 + 1} (α := R)
      (MvPolynomial.coeff d
        ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
      (MvPolynomial.coeff d
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))
neg :
  ∀ (h : ∃ (i : σ), ¬p ∣ (d : (a : σ) → ℕ) i),
    Eq.{u_3 + 1} (α := R)
      (MvPolynomial.coeff d
        ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
      (MvPolynomial.coeff d
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))
⊢ Eq.{u_3 + 1} (α := R)
    (MvPolynomial.coeff d
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
    (MvPolynomial.coeff d
      ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))

Tactic:
by_cases! h : ∀ i, p ∣ d i
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
⊢ Eq (α := ℕ) ((fun (a : ℕ) ↦ a / p) 0) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
h₁ :
  ∀ (i : σ),
    Eq (α := ℕ) ((HSMul.hSMul (β := σ →₀ ℕ) p (Finsupp.mapRange (fun (a : ℕ) ↦ a / p) ⋯ d) : (a : σ) → ℕ) i : ℕ)
      ((d : (a : σ) → ℕ) i : ℕ)
⊢ HSMul.hSMul (β := σ →₀ ℕ) p (Finsupp.mapRange (fun (a : ℕ) ↦ a / p) ⋯ d) = d

Tactic:
ext i
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
i : σ
⊢ Eq (α := ℕ) ((HSMul.hSMul (β := σ →₀ ℕ) p (Finsupp.mapRange (fun (a : ℕ) ↦ a / p) ⋯ d) : (a : σ) → ℕ) i : ℕ)
    ((d : (a : σ) → ℕ) i : ℕ)

Tactic:
simp [(Nat.mul_div_cancel' (h i))]

Premises used: Nat.mul_div_cancel'
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
pos :
  ∀ (m : σ →₀ ℕ) (hm : p • m = d),
    Eq.{u_3 + 1} (α := R)
      (MvPolynomial.coeff d
        ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
      (MvPolynomial.coeff d
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))
⊢ Eq.{u_3 + 1} (α := R)
    (MvPolynomial.coeff d
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
    (MvPolynomial.coeff d
      ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))

Tactic:
obtain ⟨m, hm⟩ : ∃ m, p • m = d := ⟨d.mapRange (fun a ↦ a / p) (by simp),
      by ext i; simp [(Nat.mul_div_cancel' (h i))]⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
pos :
  ∀ (h_le : m ≤ n),
    Eq.{u_3 + 1} (α := R)
      (MvPolynomial.coeff d
        ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
      (MvPolynomial.coeff d
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))
neg :
  ∀ (h_le : ¬m ≤ n),
    Eq.{u_3 + 1} (α := R)
      (MvPolynomial.coeff d
        ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
      (MvPolynomial.coeff d
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))
⊢ Eq.{u_3 + 1} (α := R)
    (MvPolynomial.coeff d
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
    (MvPolynomial.coeff d
      ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))

Tactic:
by_cases h_le : m ≤ n
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
h_le : m ≤ n
pos :
  Eq.{u_3 + 1} (α := R)
    (MvPolynomial.coeff (p • m)
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
    (MvPolynomial.coeff (p • m)
      ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))
pos₁ :
  Eq.{u_3 + 1} (α := R)
    (if p • m ≤ p • n then
        (coeff (p • m) : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
      else 0 :
      R)
    (MvPolynomial.coeff (p • m)
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)) :
      R)
pos₂ :
  Eq.{u_3 + 1} (α := R)
    ((coeff (p • m) : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (MvPolynomial.coeff (p • m)
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)) :
      R)
pos₃ :
  Eq.{u_3 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    (MvPolynomial.coeff (p • m)
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)) :
      R)
pos₄ :
  Eq.{u_3 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    (MvPolynomial.coeff m ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ) : R)
pos₅ :
  Eq.{u_3 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    (if m ≤ n then (coeff m : (a : MvPowerSeries σ R) → R) φ else 0 : R)
pos₆ pos₇ :
  Eq.{u_3 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
⊢ Eq.{u_3 + 1} (α := R)
    (MvPolynomial.coeff d
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
    (MvPolynomial.coeff d
      ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))

Tactic:
rw [← hm, coeff_trunc', if_pos (nsmul_le_nsmul_right h_le p), coeff_expand_smul,
        MvPolynomial.coeff_expand_smul _ hp, coeff_trunc', if_pos h_le]

Premises used: MvPolynomial.coeff_expand_smul, nsmul_le_nsmul_right, MvPowerSeries.coeff_expand_smul, if_pos, MvPowerSeries.coeff_trunc'
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
by_contra! : ∀ (hc : ∀ (i : σ), LE.le (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) ((n : (a : σ) → ℕ) i : ℕ)), False
⊢ ∃ (i : σ), GT.gt (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) ((n : (a : σ) → ℕ) i : ℕ)

Tactic:
by_contra! hc
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
hc : ∀ (i : σ), LE.le (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) ((n : (a : σ) → ℕ) i : ℕ)
⊢ False

Tactic:
h_le (Finsupp.coe_le_coe.mp hc)

Premises used: Finsupp.coe_le_coe, Iff.mp
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
hc : ∀ (i : σ), LE.le (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) ((n : (a : σ) → ℕ) i : ℕ)
⊢ False

Tactic:
exact h_le (Finsupp.coe_le_coe.mp hc)

Premises used: Finsupp.coe_le_coe, Iff.mp
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
obtain : ∀ (i : σ) (hi : GT.gt (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) ((n : (a : σ) → ℕ) i : ℕ)), ¬p • m ≤ p • n
⊢ ¬p • m ≤ p • n

Tactic:
obtain ⟨i, hi⟩ : ∃ i, m i > n i := by
          by_contra! hc
          exact h_le (Finsupp.coe_le_coe.mp hc)
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
i : σ
hi : GT.gt (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) ((n : (a : σ) → ℕ) i : ℕ)
⊢ ¬HSMul.hSMul (β := ℕ) p ((m : (a : σ) → ℕ) i : ℕ) ≤ HSMul.hSMul (β := ℕ) p ((n : (a : σ) → ℕ) i : ℕ)

Tactic:
simp [Nat.mul_lt_mul_of_pos_left hi (p.ne_zero_iff_zero_lt.mp hp)]

Premises used: Nat.ne_zero_iff_zero_lt, Nat.mul_lt_mul_of_pos_left, Iff.mp
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
i : σ
hi : GT.gt (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) ((n : (a : σ) → ℕ) i : ℕ)
⊢ ¬HSMul.hSMul (β := ℕ) p ((m : (a : σ) → ℕ) i : ℕ) ≤ HSMul.hSMul (β := ℕ) p ((n : (a : σ) → ℕ) i : ℕ)

Tactic:
have : ¬ p • m i ≤ p • n i := by
          simp [Nat.mul_lt_mul_of_pos_left hi (p.ne_zero_iff_zero_lt.mp hp)]
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
i : σ
hi : GT.gt (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) ((n : (a : σ) → ℕ) i : ℕ)
this : ¬HSMul.hSMul (β := ℕ) p ((m : (a : σ) → ℕ) i : ℕ) ≤ HSMul.hSMul (β := ℕ) p ((n : (a : σ) → ℕ) i : ℕ)
⊢ ¬p • m ≤ p • n

Tactic:
Not.intro fun a ↦ this (a i)

Premises used: Not.intro
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
i : σ
hi : GT.gt (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) ((n : (a : σ) → ℕ) i : ℕ)
this : ¬HSMul.hSMul (β := ℕ) p ((m : (a : σ) → ℕ) i : ℕ) ≤ HSMul.hSMul (β := ℕ) p ((n : (a : σ) → ℕ) i : ℕ)
⊢ ¬p • m ≤ p • n

Tactic:
exact Not.intro fun a ↦ this (a i)

Premises used: Not.intro
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
⊢ ¬p • m ≤ p • n

Tactic:
have not_le : ¬ p • m ≤ p • n := by
        obtain ⟨i, hi⟩ : ∃ i, m i > n i := by
          by_contra! hc
          exact h_le (Finsupp.coe_le_coe.mp hc)
        have : ¬ p • m i ≤ p • n i := by
          simp [Nat.mul_lt_mul_of_pos_left hi (p.ne_zero_iff_zero_lt.mp hp)]
        exact Not.intro fun a ↦ this (a i)