awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
p : ℕ
a : R
f : MvPowerSeries σ R
h :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      ((coeff d : (a : MvPowerSeries σ R) → R) fun (d : σ →₀ ℕ) ↦
          if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) (a • f) else 0 :
        R)
      ((coeff d : (a : MvPowerSeries σ R) → R)
          (HSMul.hSMul (α := R) (β := MvPowerSeries σ R) ((RingHom.id R : (a : R) → R) a : R) fun (d : σ →₀ ℕ) ↦
            if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) f else 0) :
        R)
⊢ (fun (d : σ →₀ ℕ) ↦
      if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) (a • f) else 0) =
    HSMul.hSMul (α := R) (β := MvPowerSeries σ R) ((RingHom.id R : (a : R) → R) a : R) fun (d : σ →₀ ℕ) ↦
      if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) f else 0

Tactic:
ext d
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
p : ℕ
a : R
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R) fun (d : σ →₀ ℕ) ↦
        if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) (a • f) else 0 :
      R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        (HSMul.hSMul (α := R) (β := MvPowerSeries σ R) ((RingHom.id R : (a : R) → R) a : R) fun (d : σ →₀ ℕ) ↦
          if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) f else 0) :
      R)

Tactic:
simp only [map_smul,
      smul_eq_mul, RingHom.id_apply, coeff_apply, mul_ite, mul_zero]

Premises used: RingHom.id_apply, mul_ite, MvPowerSeries.coeff_apply, MulZeroClass.mul_zero, smul_eq_mul, map_smul
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
p : ℕ
d : σ →₀ ℕ
f : MvPowerSeries σ R
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    (if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) f else 0 : R)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) < weightedOrder w f
h :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      ((coeff d : (a : MvPowerSeries σ R) → R)
          ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
        R)
      ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)

Tactic:
ext d
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) < weightedOrder w f
d : σ →₀ ℕ
h :
  Eq.{u_2 + 1} (α := R)
    (if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) f else 0 : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
rw [coeff_weightedHomogeneousComponent]

Premises used: MvPowerSeries.coeff_weightedHomogeneousComponent
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) < weightedOrder w f
d : σ →₀ ℕ
pos :
  ∀ (hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
neg :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p),
    Eq.{u_2 + 1} (α := R) (0 : R) ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ Eq.{u_2 + 1} (α := R)
    (if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) f else 0 : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
split_ifs with hd
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) < weightedOrder w f
d : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p
pos : Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
rw [coeff_zero]

Premises used: MvPowerSeries.coeff_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) < weightedOrder w f
d : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p
pos : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
apply coeff_eq_zero_of_lt_weightedOrder w

Premises used: MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) < weightedOrder w f
d : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p
pos : (↑p : ℕ∞) < weightedOrder w f
⊢ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f

Tactic:
rw [hd]
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) < weightedOrder w f
d : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p
⊢ (↑p : ℕ∞) < weightedOrder w f

Tactic:
hf
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) < weightedOrder w f
d : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p
⊢ (↑p : ℕ∞) < weightedOrder w f

Tactic:
exact hf
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) < weightedOrder w f
d : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p
neg neg₁ : Eq.{u_2 + 1} (α := R) 0 0
⊢ Eq.{u_2 + 1} (α := R) (0 : R) ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) = weightedOrder w f
hf' :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
rw : Eq (α := ℕ∞) (↑(toNat (↑p : ℕ∞)) : ℕ∞) (↑p : ℕ∞)
rw₁ rw₂ : Eq (α := ℕ∞) (↑p : ℕ∞) (↑p : ℕ∞)
⊢ (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f

Tactic:
rw [← hf, toNat_coe]

Premises used: ENat.toNat_coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) = weightedOrder w f
hf' :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
obtain :
  ∀ (d : σ →₀ ℕ)
    (hd :
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f),
    False
⊢ False

Tactic:
obtain ⟨d, hd⟩ := f.exists_coeff_ne_zero_and_weightedOrder w (by rw [← hf, toNat_coe])

Premises used: MvPowerSeries.exists_coeff_ne_zero_and_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) = weightedOrder w f
hf' :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
d : σ →₀ ℕ
hd :
  Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f
⊢ ¬Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧ (weight w : (a : σ →₀ ℕ) → ℕ) d = p

Tactic:
simp only [ne_eq, ← hf, Nat.cast_inj] at hd

Premises used: Nat.cast_inj, ne_eq
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) = weightedOrder w f
hf' :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
d : σ →₀ ℕ
hd :
  ¬Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧ (weight w : (a : σ →₀ ℕ) → ℕ) d = p
apply : Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ False

Tactic:
apply hd.1

Premises used: And.left
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) = weightedOrder w f
hf' :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
d : σ →₀ ℕ
hd :
  ¬Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧ (weight w : (a : σ →₀ ℕ) → ℕ) d = p
rw :
  ∀
    (hf' :
      ∀ (n : σ →₀ ℕ),
        Eq.{u_2 + 1} (α := R)
          ((coeff n : (a : MvPowerSeries σ R) → R)
              ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
            R)
          ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R))
    (d : σ →₀ ℕ)
    (hd :
      ¬Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (weight w : (a : σ →₀ ℕ) → ℕ) d = p),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
rw [MvPowerSeries.ext_iff] at hf'

Premises used: MvPowerSeries.ext_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) = weightedOrder w f
hf' :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)
d : σ →₀ ℕ
hd :
  ¬Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧ (weight w : (a : σ →₀ ℕ) → ℕ) d = p
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
specialize hf' d
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
hd :
  ¬Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧ (weight w : (a : σ →₀ ℕ) → ℕ) d = p
hf' :
  Eq.{u_2 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ (weight w : (a : σ →₀ ℕ) → ℕ) d = p → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
simp only [coeff_weightedHomogeneousComponent, coeff_zero, ite_eq_right_iff] at hf'

Premises used: MvPowerSeries.coeff_zero, MvPowerSeries.coeff_weightedHomogeneousComponent, ite_eq_right_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
hd :
  ¬Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧ (weight w : (a : σ →₀ ℕ) → ℕ) d = p
hf' :
  (weight w : (a : σ →₀ ℕ) → ℕ) d = p → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
hf' hd.2

Premises used: And.right
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
hd :
  ¬Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧ (weight w : (a : σ →₀ ℕ) → ℕ) d = p
hf' :
  (weight w : (a : σ →₀ ℕ) → ℕ) d = p → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
exact hf' hd.2

Premises used: And.right
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
d : σ →₀ ℕ
rw :
  ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p →
    Eq.{u_2 + 1} (α := R)
      ((coeff d : (a : MvPowerSeries σ R) → R)
          ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
        R)
      (0 : R)
⊢ Ne.{u_2 + 1} (α := R)
      ((coeff d : (a : MvPowerSeries σ R) → R)
          ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
        R)
      (0 : R) →
    (weight w : (a : σ →₀ ℕ) → ℕ) d = p

Tactic:
rw [not_imp_comm]

Premises used: not_imp_comm
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
d : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p
rw :
  Eq.{u_2 + 1} (α := R)
    (if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) f else 0 : R) (0 : R)
rw₁ rw₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    (0 : R)

Tactic:
rw [coeff_weightedHomogeneousComponent, if_neg hd]

Premises used: MvPowerSeries.coeff_weightedHomogeneousComponent, if_neg
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
mp :
  IsWeightedHomogeneous w f p → f = (weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f
mpr :
  f = (weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f → IsWeightedHomogeneous w f p
⊢ IsWeightedHomogeneous w f p ↔ f = (weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f

Tactic:
constructor
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
mp :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff d : (a : MvPowerSeries σ R) → R)
          ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
        R)
⊢ f = (weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f

Tactic:
ext d
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
d : σ →₀ ℕ
mp :
  Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
    (if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) f else 0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)

Tactic:
rw [coeff_weightedHomogeneousComponent]

Premises used: MvPowerSeries.coeff_weightedHomogeneousComponent
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
d : σ →₀ ℕ
pos :
  ∀ (hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
neg :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
    (if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) f else 0 : R)

Tactic:
split_ifs with hd
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
d : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
d : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
hf.coeff_eq_zero hd

Premises used: MvPowerSeries.IsWeightedHomogeneous.coeff_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
d : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
exact hf.coeff_eq_zero hd

Premises used: MvPowerSeries.IsWeightedHomogeneous.coeff_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : f = (weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f
mpr :
  IsWeightedHomogeneous.{u_1, u_2} (R := R) w
    ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) p
⊢ IsWeightedHomogeneous w f p

Tactic:
rw [hf]
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : f = (weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f
d : σ →₀ ℕ
⊢ Ne.{u_2 + 1} (α := R)
      ((coeff d : (a : MvPowerSeries σ R) → R)
          ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
        R)
      (0 : R) →
    (weight w : (a : σ →₀ ℕ) → ℕ) d = p

Tactic:
isWeightedHomogeneous_weightedHomogeneousComponent w f p

Premises used: MvPowerSeries.isWeightedHomogeneous_weightedHomogeneousComponent
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : f = (weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f
⊢ IsWeightedHomogeneous.{u_1, u_2} (R := R) w
    ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) p

Tactic:
exact isWeightedHomogeneous_weightedHomogeneousComponent w f p

Premises used: MvPowerSeries.isWeightedHomogeneous_weightedHomogeneousComponent
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : (↑p : ℕ∞) ≤ weightedOrder w f
hg : (↑q : ℕ∞) ≤ weightedOrder w g
h :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      ((coeff d : (a : MvPowerSeries σ R) → R)
          ((weightedHomogeneousComponent w (p + q) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (f * g) :
            MvPowerSeries σ R) :
        R)
      ((coeff d : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
            ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
            ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)) :
        R)
⊢ (weightedHomogeneousComponent w (p + q) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (f * g) =
    HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
      ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)

Tactic:
ext d
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : (↑p : ℕ∞) ≤ weightedOrder w f
hg : (↑q : ℕ∞) ≤ weightedOrder w g
d : σ →₀ ℕ
h :
  Eq.{u_2 + 1} (α := R)
    (if (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q then (coeff d : (a : MvPowerSeries σ R) → R) (f * g) else 0 : R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
          ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
          ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)) :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        ((weightedHomogeneousComponent w (p + q) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (f * g) :
          MvPowerSeries σ R) :
      R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
          ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
          ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)) :
      R)

Tactic:
rw [coeff_weightedHomogeneousComponent]

Premises used: MvPowerSeries.coeff_weightedHomogeneousComponent
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : (↑p : ℕ∞) ≤ weightedOrder w f
hg : (↑q : ℕ∞) ≤ weightedOrder w g
d : σ →₀ ℕ
pos :
  ∀ (hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
            ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
            ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)) :
        R)
neg :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R) (0 : R)
      ((coeff d : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
            ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
            ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)) :
        R)
⊢ Eq.{u_2 + 1} (α := R)
    (if (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q then (coeff d : (a : MvPowerSeries σ R) → R) (f * g) else 0 : R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
          ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
          ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)) :
      R)

Tactic:
split_ifs with hd