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
φ : MvPowerSeries σ R
refine :
  Subset (α := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ)
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ))
refine₁ :
  ∀ ⦃d : σ →₀ ℕ⦄ (hd : Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ) d),
    Membership.mem (γ := Set (σ →₀ ℕ))
      (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
refine₂ :
  ∀ ⦃d : σ →₀ ℕ⦄ (n : σ →₀ ℕ) (hn₁ : n ∈ Function.support φ) (hn₂ : (fun (x : σ →₀ ℕ) ↦ p • x) n = d),
    Membership.mem (γ := Set (σ →₀ ℕ))
      (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
⊢ Eq (α := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ))
    ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ)
have refine₃ : ∀ ⦃d : σ →₀ ℕ⦄ (n : σ →₀ ℕ) (hn₁ : n ∈ Function.support φ) (hn₂ : (fun (x : σ →₀ ℕ) ↦ p • x) n = d),
  Ne.{u_3 + 1} (α := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ (p • n) : R) (0 : R)
Tactic: classical
  refine (support_expand_subset p hp φ).antisymm ?_
  intro d hd
  obtain ⟨n, hn₁, hn₂⟩ := hd
  simp only [← hn₂, Function.mem_support]
  by_contra hc
  rw [Function.mem_support, ← coeff_apply φ, ← coeff_expand_smul p hp, coeff_apply, hc] at hn₁
  contradiction
-- 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
φ : MvPowerSeries σ R
refine :
  Subset (α := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ)
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ))
refine₁ :
  ∀ ⦃d : σ →₀ ℕ⦄ (hd : Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ) d),
    Membership.mem (γ := Set (σ →₀ ℕ))
      (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
refine₂ :
  ∀ ⦃d : σ →₀ ℕ⦄ (n : σ →₀ ℕ) (hn₁ : n ∈ Function.support φ) (hn₂ : (fun (x : σ →₀ ℕ) ↦ p • x) n = d),
    Membership.mem (γ := Set (σ →₀ ℕ))
      (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
refine₃ :
  ∀ ⦃d : σ →₀ ℕ⦄ (n : σ →₀ ℕ) (hn₁ : n ∈ Function.support φ) (hn₂ : (fun (x : σ →₀ ℕ) ↦ p • x) n = d),
    Ne.{u_3 + 1} (α := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ (p • n) : R) (0 : R)
refine₄ :
  ∀ ⦃d : σ →₀ ℕ⦄ (n : σ →₀ ℕ) (hn₁ : n ∈ Function.support φ) (hn₂ : (fun (x : σ →₀ ℕ) ↦ p • x) n = d)
    (hc : Eq.{u_3 + 1} (α := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ (p • n) : R) (0 : R)),
    False
⊢ Eq (α := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ))
    ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ)
have refine₅ : ∀ ⦃d : σ →₀ ℕ⦄ (n : σ →₀ ℕ) (hn₁ : Ne.{u_3 + 1} (α := R) 0 0) (hn₂ : (fun (x : σ →₀ ℕ) ↦ p • x) n = d)
  (hc : Eq.{u_3 + 1} (α := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ (p • n) : R) (0 : R)),
  False
Tactic: classical
  refine (support_expand_subset p hp φ).antisymm ?_
  intro d hd
  obtain ⟨n, hn₁, hn₂⟩ := hd
  simp only [← hn₂, Function.mem_support]
  by_contra hc
  rw [Function.mem_support, ← coeff_apply φ, ← coeff_expand_smul p hp, coeff_apply, hc] at hn₁
  contradiction
-- 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
φ : MvPowerSeries σ R
⊢ order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) = p • φ.order
have pos : ∀ (hφ : φ = 0),
  order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) = p • φ.order
Tactic: by_cases! hφ : φ = 0
-- 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
φ : MvPowerSeries σ R
pos :
  ∀ (hφ : φ = 0),
    order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) = p • φ.order
⊢ order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) = p • φ.order
have neg : ∀ (hφ : φ ≠ 0),
  order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) = p • φ.order
Tactic: by_cases! hφ : φ = 0
-- 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
φ : MvPowerSeries σ R
hφ : φ = 0
⊢ Ne (α := ℕ∞) (↑p : ℕ∞) 0
have norm_cast : ¬p = 0
Tactic: norm_cast
-- 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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) = p • φ.order
have neg : order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) ≤ p • φ.order
Tactic: apply eq_of_le_of_ge
-- 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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
neg : order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) ≤ p • φ.order
⊢ order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) = p • φ.order
have neg₁ : p • φ.order ≤ order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)
Tactic: apply eq_of_le_of_ge
-- 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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) ≤ p • φ.order
have neg : ∀ (d : σ →₀ ℕ) (hd₁ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R))
  (hd₂ : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = φ.order),
  order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) ≤ p • φ.order
Tactic: obtain ⟨d, hd₁, hd₂⟩ := exists_coeff_ne_zero_and_order (ne_zero_iff_order_finite.mp hφ)
-- 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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd₁ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
hd₂ : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = φ.order
⊢ order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) ≤ p • φ.order
have this : p • φ.order = (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (p • d)) : ℕ∞)
Tactic: have : p • φ.order = (p • d).degree := by simp [← 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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd₁ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
hd₂ : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = φ.order
this : p • φ.order = (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (p • d)) : ℕ∞)
⊢ order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) ≤ p • φ.order
have neg : order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) ≤
  (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (p • d)) : ℕ∞)
Tactic: rw [this]
-- 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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ p • φ.order ≤ order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)
have neg : ∀ (d : σ →₀ ℕ) (hd : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < p • φ.order),
  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: refine MvPowerSeries.le_order fun d 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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < p • φ.order
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (0 : R)
have pos : ∀ (h : ∀ (i : σ), 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: 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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < p • φ.order
pos :
  ∀ (h : ∀ (i : σ), 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)
have neg : ∀ (h : ∃ (i : σ), ¬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: 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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < p • φ.order
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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < p • φ.order
h : ∀ (i : σ), 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)
have pos : ∀ (m : σ →₀ ℕ) (hm : p • m = d),
  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 ⟨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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < p • φ.order
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (0 : R)
have pos : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) m) : ℕ∞) < φ.order
Tactic: rw [← hm, coeff_expand_smul, coeff_of_lt_order]
-- 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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < p • φ.order
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
⊢ (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) m) : ℕ∞) < φ.order
have hd₁ : HMul.hMul (α := ℕ∞) (↑p : ℕ∞) (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) m) : ℕ∞) < (↑p : ℕ∞) * φ.order
Tactic: simp only [← hm, map_nsmul, smul_eq_mul, Nat.cast_mul, nsmul_eq_mul] at hd
Cleared hypotheses: 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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < p • φ.order
h : ∃ (i : σ), ¬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)
have 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)
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
φ : MvPolynomial σ 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)
have 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)
Tactic: ext 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
φ : MvPolynomial σ R
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)
have 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)
Tactic: simp only [MvPolynomial.coeff_coe]
-- 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 : σ →₀ ℕ
⊢ 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 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)
Tactic: by_cases! h : ∀ i, p ∣ n 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
φ : 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)
⊢ 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 : ∀ (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)
Tactic: by_cases! h : ∀ i, p ∣ n 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
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (n : (a : σ) → ℕ) i
⊢ HSMul.hSMul (β := σ →₀ ℕ) p (Finsupp.mapRange (fun (a : ℕ) ↦ a / p) ⋯ n) = n
have h₁ : ∀ (i : σ),
  Eq (α := ℕ) ((HSMul.hSMul (β := σ →₀ ℕ) p (Finsupp.mapRange (fun (a : ℕ) ↦ a / p) sorry n) : (a : σ) → ℕ) i : ℕ)
    ((n : (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
φ : MvPolynomial σ R
n : σ →₀ ℕ
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)
have 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)
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))]⟩
-- 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 : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (n : (a : σ) → ℕ) i
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)
have 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)
Tactic: rw [← hm, coeff_expand_smul p hp _ _, φ.coeff_expand_smul _ hp, φ.coeff_coe]
-- 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 : σ →₀ ℕ
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)
⊢ 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 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)
Tactic: rw [← hm, coeff_expand_smul p hp _ _, φ.coeff_expand_smul _ hp, φ.coeff_coe]
-- 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 : σ →₀ ℕ
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)
⊢ 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 pos₂ : (coeff m : (a : MvPowerSeries σ R) → R) (↑φ : MvPowerSeries σ R) = MvPolynomial.coeff m φ
Tactic: rw [← hm, coeff_expand_smul p hp _ _, φ.coeff_expand_smul _ hp, φ.coeff_coe]
-- 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 : σ →₀ ℕ
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 φ
⊢ 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 pos₃ : MvPolynomial.coeff m φ = MvPolynomial.coeff m φ
Tactic: rw [← hm, coeff_expand_smul p hp _ _, φ.coeff_expand_smul _ hp, φ.coeff_coe]
-- 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 : σ →₀ ℕ
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)
have 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)
Tactic: obtain ⟨i, hi⟩ := h
Cleared hypotheses: h