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
m : σ →₀ ℕ
i : σ
h :
  Ne.{u_3 + 1} (α := R)
    (∑ᶠ (d : σ →₀ ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff m : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
          R))
    0
d : σ →₀ ℕ
hd : Ne.{u_3 + 1} (α := R) (if m = p • d then 1 else 0) 0
this :
  Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
    ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)
meq : m = p • d
⊢ p ∣ (m : (a : σ) → ℕ) i

Tactic:
simp [meq]
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hd :
  Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
⊢ ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i

Tactic:
have : ∀ i, p ∣ d i := fun _ => by_contra fun hc => hd (coeff_expand_of_not_dvd p hp φ hc)
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hd :
  Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
this : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ := Finsupp.mapRange (fun (n : ℕ) ↦ n / p) ⋯ d
⊢ p • m = d

Tactic:
have eq_aux : p • m = d := (Finsupp.ext fun a => Nat.eq_mul_of_div_eq_right (this a) rfl).symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hd :
  Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
this : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ := Finsupp.mapRange (fun (n : ℕ) ↦ n / p) ⋯ d
eq_aux : p • m = d
⊢ ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i

Tactic:
rw [Function.mem_support, ← eq_aux, ← coeff_apply (expand p hp φ), coeff_expand_smul,
    coeff_apply] at hd

Premises used: MvPowerSeries.expand, MvPowerSeries.coeff_expand_smul, MvPowerSeries.coeff_apply, Function.mem_support, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hd :
  Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
this : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ := Finsupp.mapRange (fun (n : ℕ) ↦ n / p) ⋯ d
eq_aux : p • m = d
this₁ : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
⊢ let m : σ →₀ ℕ := Finsupp.mapRange (fun (n : ℕ) ↦ n / p) ⋯ d;
  φ m ≠ 0

Tactic:
rw [Function.mem_support, ← eq_aux, ← coeff_apply (expand p hp φ), coeff_expand_smul,
    coeff_apply] at hd

Premises used: MvPowerSeries.expand, MvPowerSeries.coeff_expand_smul, MvPowerSeries.coeff_apply, Function.mem_support, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hd :
  Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d
this : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ := Finsupp.mapRange (fun (n : ℕ) ↦ n / p) ⋯ d
eq_aux : p • m = d
this₁ : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
hd₁ :
  let m : σ →₀ ℕ := Finsupp.mapRange (fun (n : ℕ) ↦ n / p) ⋯ d;
  φ m ≠ 0
⊢ let m : σ →₀ ℕ := Finsupp.mapRange (fun (n : ℕ) ↦ n / p) ⋯ d;
  p • m = d

Tactic:
rw [Function.mem_support, ← eq_aux, ← coeff_apply (expand p hp φ), coeff_expand_smul,
    coeff_apply] at hd

Premises used: MvPowerSeries.expand, MvPowerSeries.coeff_expand_smul, MvPowerSeries.coeff_apply, Function.mem_support, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
this : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ := Finsupp.mapRange (fun (n : ℕ) ↦ n / p) ⋯ d
hd : φ m ≠ 0
eq_aux : p • m = d
⊢ Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ) d

Tactic:
⟨m, hd, eq_aux⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
this : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ := Finsupp.mapRange (fun (n : ℕ) ↦ n / p) ⋯ d
hd : φ m ≠ 0
eq_aux : p • m = d
⊢ Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ) d

Tactic:
exact ⟨m, hd, eq_aux⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
⊢ Eq (α := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ))
    ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ)

Tactic:
(support_expand_subset p hp φ).antisymm ?_

Premises used: HasSubset.Subset.antisymm, MvPowerSeries.support_expand_subset
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
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) φ))
⊢ Eq (α := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ))
    ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ)

Tactic:
refine (support_expand_subset p hp φ).antisymm ?_

Premises used: HasSubset.Subset.antisymm, MvPowerSeries.support_expand_subset
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : Membership.mem (γ := Set (σ →₀ ℕ)) ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ) d
obtain :
  ∀ (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
⊢ Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := hd
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d n : σ →₀ ℕ
hn₁ : n ∈ Function.support φ
hn₂ : (fun (x : σ →₀ ℕ) ↦ p • x) n = d
simp : Ne.{u_3 + 1} (α := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ (p • n) : R) (0 : R)
⊢ Membership.mem (γ := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)) d

Tactic:
simp only [← hn₂, Function.mem_support]

Premises used: Function.mem_support
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d n : σ →₀ ℕ
hn₁ : n ∈ Function.support φ
hn₂ : (fun (x : σ →₀ ℕ) ↦ p • x) n = d
by_contra :
  ∀ (hc : Eq.{u_3 + 1} (α := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ (p • n) : R) (0 : R)),
    False
⊢ Ne.{u_3 + 1} (α := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ (p • n) : R) (0 : R)

Tactic:
by_contra hc
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
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)
⊢ Ne.{u_3 + 1} (α := R) 0 0

Tactic:
rw [Function.mem_support, ← coeff_apply φ, ← coeff_expand_smul p hp, coeff_apply, hc] at hn₁

Premises used: MvPowerSeries.coeff_expand_smul, MvPowerSeries.coeff_apply, Function.mem_support
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
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)
hn₃ : Ne.{u_3 + 1} (α := R) 0 0
⊢ (fun (x : σ →₀ ℕ) ↦ p • x) n = d

Tactic:
rw [Function.mem_support, ← coeff_apply φ, ← coeff_expand_smul p hp, coeff_apply, hc] at hn₁

Premises used: MvPowerSeries.coeff_expand_smul, MvPowerSeries.coeff_apply, Function.mem_support
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
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)
hn₃ : Ne.{u_3 + 1} (α := R) 0 0
hn₄ : (fun (x : σ →₀ ℕ) ↦ p • x) n = d
⊢ Eq.{u_3 + 1} (α := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ (p • n) : R) (0 : R)

Tactic:
rw [Function.mem_support, ← coeff_apply φ, ← coeff_expand_smul p hp, coeff_apply, hc] at hn₁

Premises used: MvPowerSeries.coeff_expand_smul, MvPowerSeries.coeff_apply, Function.mem_support
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
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:
contradiction
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
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
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
⊢ Eq (α := Set (σ →₀ ℕ))
    (Function.support.{u_1, u_3} (M := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ))
    ((fun (x : σ →₀ ℕ) ↦ p • x) '' Function.support φ)

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

Premises used: MvPowerSeries.coeff_expand_smul, MvPowerSeries.coeff_apply, HasSubset.Subset.antisymm, Function.mem_support, MvPowerSeries.support_expand_subset
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
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
neg :
  ∀ (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

Tactic:
by_cases! hφ : φ = 0
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ = 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬p = 0
⊢ Ne (α := ℕ∞) (↑p : ℕ∞) 0

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
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

Tactic:
simpa [hφ] using (ENat.mul_top (by norm_cast)).symm

Premises used: ENat.mul_top, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
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
neg₁ : p • φ.order ≤ order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)
⊢ order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) = p • φ.order

Tactic:
apply eq_of_le_of_ge

Premises used: eq_of_le_of_ge
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
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
⊢ 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φ)

Premises used: MvPowerSeries.exists_coeff_ne_zero_and_order, Iff.mp, MvPowerSeries.ne_zero_iff_order_finite
-- 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₁ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
hd₂ : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = φ.order
⊢ p • φ.order = (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (p • d)) : ℕ∞)

Tactic:
simp [← hd₂]
-- 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₁ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
hd₂ : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = φ.order
⊢ p • φ.order = (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (p • d)) : ℕ∞)

Tactic:
have : p • φ.order = (p • d).degree := by simp [← hd₂]
-- 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₁ : 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)) : ℕ∞)
neg :
  order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) ≤
    (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (p • d)) : ℕ∞)
⊢ order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ) ≤ p • φ.order

Tactic:
rw [this]
-- 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₁ : 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) φ) ≤
    (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (p • d)) : ℕ∞)

Tactic:
order_le <| (coeff_expand_smul p hp φ _) ▸ hd₁

Premises used: Eq.rec, MvPowerSeries.coeff_expand_smul, MvPowerSeries.order_le, Eq.symm
-- 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₁ : 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) φ) ≤
    (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (p • d)) : ℕ∞)

Tactic:
exact order_le <| (coeff_expand_smul p hp φ _) ▸ hd₁

Premises used: MvPowerSeries.order_le
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
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) φ)

Tactic:
MvPowerSeries.le_order fun d hd => ?_

Premises used: MvPowerSeries.le_order
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
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)
⊢ p • φ.order ≤ order.{u_1, u_3} (σ := σ) (R := R) ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)

Tactic:
refine MvPowerSeries.le_order fun d hd => ?_

Premises used: MvPowerSeries.le_order
-- 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
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)
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)
⊢ 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
-- 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
⊢ 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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < p • φ.order
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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < p • φ.order
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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < p • φ.order
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
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)
⊢ 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))]⟩
-- 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
m : σ →₀ ℕ
hm : p • m = d
pos : (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) m) : ℕ∞) < φ.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:
rw [← hm, coeff_expand_smul, coeff_of_lt_order]

Premises used: MvPowerSeries.coeff_of_lt_order, MvPowerSeries.coeff_expand_smul
-- 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
m : σ →₀ ℕ
hm : p • m = d
⊢ 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

Premises used: Nat.cast_mul, nsmul_eq_mul, smul_eq_mul, map_nsmul
-- 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 : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
hd : HMul.hMul (α := ℕ∞) (↑p : ℕ∞) (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) m) : ℕ∞) < (↑p : ℕ∞) * φ.order
⊢ (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) m) : ℕ∞) < φ.order

Tactic:
lt_of_mul_lt_mul_left' hd

Premises used: lt_of_mul_lt_mul_left'
-- 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 : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
hd : HMul.hMul (α := ℕ∞) (↑p : ℕ∞) (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) m) : ℕ∞) < (↑p : ℕ∞) * φ.order
⊢ (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) m) : ℕ∞) < φ.order

Tactic:
exact lt_of_mul_lt_mul_left' hd

Premises used: lt_of_mul_lt_mul_left'