awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
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)
have neg : Eq.{u_3 + 1} (α := R) 0 (MvPolynomial.coeff n ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) φ))
Tactic: rw [coeff_expand_of_not_dvd p hp _ hi, MvPolynomial.coeff_expand_of_not_dvd _ hi]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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) φ))
⊢ 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)
have neg₁ : Eq.{u_3 + 1} (α := R) 0 0
Tactic: rw [coeff_expand_of_not_dvd p hp _ hi, MvPolynomial.coeff_expand_of_not_dvd _ hi]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ 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)
have 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) φ)))
Tactic: ext d
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
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) φ)))
have 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) φ)))
Tactic: by_cases! h : ∀ i, p ∣ d i
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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) φ)))
⊢ 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) φ)))
have 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) φ)))
Tactic: by_cases! h : ∀ i, p ∣ d i
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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
⊢ HSMul.hSMul (β := σ →₀ ℕ) p (Finsupp.mapRange (fun (a : ℕ) ↦ a / p) ⋯ d) = d
have h₁ : ∀ (i : σ),
  Eq (α := ℕ) ((HSMul.hSMul (β := σ →₀ ℕ) p (Finsupp.mapRange (fun (a : ℕ) ↦ a / p) sorry d) : (a : σ) → ℕ) i : ℕ)
    ((d : (a : σ) → ℕ) i : ℕ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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.{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) φ)))
have 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) φ)))
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))]⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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
⊢ 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) φ)))
have 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) φ)))
Tactic: by_cases h_le : m ≤ n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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) φ)))
⊢ 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) φ)))
have 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) φ)))
Tactic: by_cases h_le : m ≤ n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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
⊢ 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) φ)))
have 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) φ)))
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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) φ)))
⊢ 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) φ)))
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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)
⊢ 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) φ)))
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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)
⊢ 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) φ)))
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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)
⊢ 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) φ)))
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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)
⊢ 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) φ)))
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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)
⊢ 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) φ)))
have pos₆ : Eq.{u_3 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : 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]