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
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
⊢ ∃ (i : σ), GT.gt (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) ((n : (a : σ) → ℕ) i : ℕ)
have by_contra! : ∀ (hc : ∀ (i : σ), LE.le (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) ((n : (a : σ) → ℕ) i : ℕ)), False
Tactic: by_contra! hc
-- 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
⊢ ¬p • m ≤ p • n
have obtain : ∀ (i : σ) (hi : GT.gt (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) ((n : (a : σ) → ℕ) i : ℕ)), ¬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)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (hypothesis)
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 : ℕ)
⊢ ¬p • m ≤ p • n
have this : ¬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)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (hypothesis)
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 not_le : ¬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)
-- 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
not_le : ¬p • m ≤ p • 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 neg : Eq.{u_3 + 1} (α := R)
  (if d ≤ p • n then
      (coeff d : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
    else 0 :
    R)
  (MvPolynomial.coeff d
      ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)) :
    R)
Tactic: rw [coeff_trunc', ← hm, if_neg not_le, MvPolynomial.coeff_expand_smul _ hp, coeff_trunc',
        if_neg 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
not_le : ¬p • m ≤ p • n
neg :
  Eq.{u_3 + 1} (α := R)
    (if d ≤ p • n then
        (coeff d : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
      else 0 :
      R)
    (MvPolynomial.coeff d
        ((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 neg₁ : 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 [coeff_trunc', ← hm, if_neg not_le, MvPolynomial.coeff_expand_smul _ hp, coeff_trunc',
        if_neg 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
not_le : ¬p • m ≤ p • n
neg :
  Eq.{u_3 + 1} (α := R)
    (if d ≤ p • n then
        (coeff d : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
      else 0 :
      R)
    (MvPolynomial.coeff d
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)) :
      R)
neg₁ :
  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 neg₂ : Eq.{u_3 + 1} (α := R) 0
  (MvPolynomial.coeff (p • m)
    ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))
Tactic: rw [coeff_trunc', ← hm, if_neg not_le, MvPolynomial.coeff_expand_smul _ hp, coeff_trunc',
        if_neg 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
not_le : ¬p • m ≤ p • n
neg :
  Eq.{u_3 + 1} (α := R)
    (if d ≤ p • n then
        (coeff d : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
      else 0 :
      R)
    (MvPolynomial.coeff d
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)) :
      R)
neg₁ :
  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)
neg₂ :
  Eq.{u_3 + 1} (α := R) 0
    (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 neg₃ : Eq.{u_3 + 1} (α := R) 0 (MvPolynomial.coeff m ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ))
Tactic: rw [coeff_trunc', ← hm, if_neg not_le, MvPolynomial.coeff_expand_smul _ hp, coeff_trunc',
        if_neg 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
not_le : ¬p • m ≤ p • n
neg :
  Eq.{u_3 + 1} (α := R)
    (if d ≤ p • n then
        (coeff d : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
      else 0 :
      R)
    (MvPolynomial.coeff d
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)) :
      R)
neg₁ :
  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)
neg₂ :
  Eq.{u_3 + 1} (α := R) 0
    (MvPolynomial.coeff (p • m)
      ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))
neg₃ : Eq.{u_3 + 1} (α := R) 0 (MvPolynomial.coeff m ((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₄ : Eq.{u_3 + 1} (α := R) (0 : R) (if m ≤ n then (coeff m : (a : MvPowerSeries σ R) → R) φ else 0 : R)
Tactic: rw [coeff_trunc', ← hm, if_neg not_le, MvPolynomial.coeff_expand_smul _ hp, coeff_trunc',
        if_neg 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
not_le : ¬p • m ≤ p • n
neg :
  Eq.{u_3 + 1} (α := R)
    (if d ≤ p • n then
        (coeff d : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
      else 0 :
      R)
    (MvPolynomial.coeff d
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)) :
      R)
neg₁ :
  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)
neg₂ :
  Eq.{u_3 + 1} (α := R) 0
    (MvPolynomial.coeff (p • m)
      ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))
neg₃ : Eq.{u_3 + 1} (α := R) 0 (MvPolynomial.coeff m ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ))
neg₄ : Eq.{u_3 + 1} (α := R) (0 : 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 neg₅ : Eq.{u_3 + 1} (α := R) 0 0
Tactic: rw [coeff_trunc', ← hm, if_neg not_le, MvPolynomial.coeff_expand_smul _ hp, coeff_trunc',
        if_neg 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
⊢ 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 : ∀ (i : σ) (hi : ¬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: obtain ⟨i, hi⟩ := h
Cleared hypotheses: h
-- 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 : σ →₀ ℕ
i : σ
hi : ¬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 neg : 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) φ)))
  0
Tactic: rw [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
d : σ →₀ ℕ
i : σ
hi : ¬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) φ)))
    0
have pos : ∀ (hd : d ≤ p • 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) φ)))
    0
Tactic: by_cases hd : d ≤ p • 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 : σ →₀ ℕ
i : σ
hi : ¬p ∣ (d : (a : σ) → ℕ) i
pos :
  ∀ (hd : d ≤ p • 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) φ)))
      0
⊢ 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) φ)))
    0
have neg : ∀ (hd : ¬d ≤ p • 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) φ)))
    0
Tactic: by_cases hd : d ≤ p • 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 : σ →₀ ℕ
i : σ
hi : ¬p ∣ (d : (a : σ) → ℕ) i
hd : d ≤ p • 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) φ)))
    0
have pos : Eq.{u_3 + 1} (α := R)
  (if d ≤ p • n then
      (coeff d : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
    else 0 :
    R)
  (0 : R)
Tactic: rw [coeff_trunc', if_pos hd, coeff_expand_of_not_dvd _ hp _ 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
d : σ →₀ ℕ
i : σ
hi : ¬p ∣ (d : (a : σ) → ℕ) i
hd : d ≤ p • n
pos :
  Eq.{u_3 + 1} (α := R)
    (if d ≤ p • n then
        (coeff d : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
      else 0 :
      R)
    (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) φ)))
    0
have pos₁ : 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: rw [coeff_trunc', if_pos hd, coeff_expand_of_not_dvd _ hp _ 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
d : σ →₀ ℕ
i : σ
hi : ¬p ∣ (d : (a : σ) → ℕ) i
hd : d ≤ p • n
pos :
  Eq.{u_3 + 1} (α := R)
    (if d ≤ p • n then
        (coeff d : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
      else 0 :
      R)
    (0 : R)
pos₁ :
  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)
    (MvPolynomial.coeff d
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
    0
have pos₂ : Eq.{u_3 + 1} (α := R) 0 0
Tactic: rw [coeff_trunc', if_pos hd, coeff_expand_of_not_dvd _ hp _ 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
d : σ →₀ ℕ
i : σ
hi : ¬p ∣ (d : (a : σ) → ℕ) i
hd : ¬d ≤ p • 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) φ)))
    0
have neg : Eq.{u_3 + 1} (α := R)
  (if d ≤ p • n then
      (coeff d : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
    else 0 :
    R)
  (0 : R)
Tactic: rw [coeff_trunc', if_neg hd]
-- 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 : σ →₀ ℕ
i : σ
hi : ¬p ∣ (d : (a : σ) → ℕ) i
hd : ¬d ≤ p • n
neg :
  Eq.{u_3 + 1} (α := R)
    (if d ≤ p • n then
        (coeff d : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
      else 0 :
      R)
    (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) φ)))
    0
have neg₁ : Eq.{u_3 + 1} (α := R) 0 0
Tactic: rw [coeff_trunc', if_neg hd]
-- 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
n m : σ →₀ ℕ
h : n ≤ m
inst_1 : DecidableEq σ
f : MvPowerSeries σ R
⊢ Eq (α := MvPolynomial σ R)
    ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (↑((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
              ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f)) :
          MvPowerSeries σ R) :
      MvPolynomial σ R)
have rw : Eq (α := MvPolynomial σ R)
  ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) :
    MvPolynomial σ R)
  ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
      ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        (↑((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R)) :
    MvPolynomial σ R)
Tactic: rw [← expand_eq_expand p hp, trunc'_expand, ← trunc'_trunc' h]
-- 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
n m : σ →₀ ℕ
h : n ≤ m
inst_1 : DecidableEq σ
f : MvPowerSeries σ R
rw :
  Eq (α := MvPolynomial σ R)
    ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          (↑((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R)) :
      MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (↑((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
              ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f)) :
          MvPowerSeries σ R) :
      MvPolynomial σ R)
have rw₁ : Eq (α := MvPolynomial σ R)
  ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) :
    MvPolynomial σ R)
  ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (↑((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R)) :
    MvPolynomial σ R)
Tactic: rw [← expand_eq_expand p hp, trunc'_expand, ← trunc'_trunc' h]