awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
pos :
  ∀ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d,
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
      HMul.hMul (α := R) (β := R)
        ((coeff x.1 : (a : MvPowerSeries σ R) → R)
            ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
          R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R)
            ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R) :
          R)
⊢ 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)

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- 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 : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d
⊢ x.1 + x.2 = d

Tactic:
rw [Finset.mem_antidiagonal] at hx

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- 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 : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = d
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q

Tactic:
rw [← hx, map_add] at hd

Premises used: map_add
-- 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 : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = d
hd₁ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q
⊢ x.1 + x.2 = d

Tactic:
rw [← hx, map_add] at hd

Premises used: map_add
-- 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 : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q
hx : x.1 + x.2 = d
pos :
  HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    HMul.hMul (α := R) (β := R)
      (if (weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p then (coeff x.1 : (a : MvPowerSeries σ R) → R) f else 0 : R)
      (if (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q then (coeff x.2 : (a : MvPowerSeries σ R) → R) g else 0 : R)
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    HMul.hMul (α := R) (β := R)
      ((coeff x.1 : (a : MvPowerSeries σ R) → R)
          ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
        R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R)
          ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R) :
        R)

Tactic:
simp only [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 : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q
hx : x.1 + x.2 = d
pos :
  ∀ (h : (weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p ∧ (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q),
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
      HMul.hMul (α := R) (β := R)
        (if (weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p then (coeff x.1 : (a : MvPowerSeries σ R) → R) f else 0 : R)
        (if (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q then (coeff x.2 : (a : MvPowerSeries σ R) → R) g else 0 : R)
pos₁ :
  ∀ (h : (weight w : (a : σ →₀ ℕ) → ℕ) x.1 < p),
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
      HMul.hMul (α := R) (β := R)
        (if (weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p then (coeff x.1 : (a : MvPowerSeries σ R) → R) f else 0 : R)
        (if (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q then (coeff x.2 : (a : MvPowerSeries σ R) → R) g else 0 : R)
pos₂ :
  ∀ (h : (weight w : (a : σ →₀ ℕ) → ℕ) x.2 < q),
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
      HMul.hMul (α := R) (β := R)
        (if (weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p then (coeff x.1 : (a : MvPowerSeries σ R) → R) f else 0 : R)
        (if (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q then (coeff x.2 : (a : MvPowerSeries σ R) → R) g else 0 : R)
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    HMul.hMul (α := R) (β := R)
      (if (weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p then (coeff x.1 : (a : MvPowerSeries σ R) → R) f else 0 : R)
      (if (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q then (coeff x.2 : (a : MvPowerSeries σ R) → R) g else 0 : R)

Tactic:
rcases trichotomy_of_add_eq_add hd with h | h | h

Premises used: trichotomy_of_add_eq_add
-- 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 : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q
hx : x.1 + x.2 = d
h : (weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p ∧ (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q
pos :
  HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      (if (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q then (coeff x.2 : (a : MvPowerSeries σ R) → R) g else 0 : R)
pos₁ pos₂ :
  HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R)
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    HMul.hMul (α := R) (β := R)
      (if (weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p then (coeff x.1 : (a : MvPowerSeries σ R) → R) f else 0 : R)
      (if (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q then (coeff x.2 : (a : MvPowerSeries σ R) → R) g else 0 : R)

Tactic:
rw [if_pos h.1, if_pos h.2]

Premises used: if_pos, And.right, And.left
-- 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 : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q
hx : x.1 + x.2 = d
h : (weight w : (a : σ →₀ ℕ) → ℕ) x.1 < p
pos :
  HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    HMul.hMul (α := R) (β := R)
      (if (weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p then (coeff x.1 : (a : MvPowerSeries σ R) → R) f else 0 : R)
      (if (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q then (coeff x.2 : (a : MvPowerSeries σ R) → R) g else 0 : R)

Tactic:
rw [if_neg (ne_of_lt h), zero_mul]

Premises used: MulZeroClass.zero_mul, ne_of_lt, if_neg
-- 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 : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q
hx : x.1 + x.2 = d
h : (weight w : (a : σ →₀ ℕ) → ℕ) x.1 < p
⊢ LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) x.1) : ℕ∞) (↑p : ℕ∞)

Tactic:
rw [← ENat.coe_lt_coe] at h

Premises used: ENat.coe_lt_coe
-- 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 : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q
hx : x.1 + x.2 = d
h : LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) x.1) : ℕ∞) (↑p : ℕ∞)
pos : HMul.hMul (α := R) (β := R) (0 : R) ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) = 0
pos₁ pos₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    0

Tactic:
rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hf), zero_mul]

Premises used: MulZeroClass.zero_mul, MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder, lt_of_lt_of_le
-- 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 : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q
hx : x.1 + x.2 = d
h : (weight w : (a : σ →₀ ℕ) → ℕ) x.2 < q
pos :
  HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    HMul.hMul (α := R) (β := R)
      (if (weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p then (coeff x.1 : (a : MvPowerSeries σ R) → R) f else 0 : R)
      (if (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q then (coeff x.2 : (a : MvPowerSeries σ R) → R) g else 0 : R)

Tactic:
rw [if_neg (ne_of_lt h), mul_zero]

Premises used: MulZeroClass.mul_zero, ne_of_lt, if_neg
-- 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 : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q
hx : x.1 + x.2 = d
h : (weight w : (a : σ →₀ ℕ) → ℕ) x.2 < q
⊢ LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) x.2) : ℕ∞) (↑q : ℕ∞)

Tactic:
rw [← ENat.coe_lt_coe] at h

Premises used: ENat.coe_lt_coe
-- 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 : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q
hx : x.1 + x.2 = d
h : LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) x.2) : ℕ∞) (↑q : ℕ∞)
pos : HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R) (0 : R) = 0
pos₁ pos₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    0

Tactic:
rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hg), mul_zero]

Premises used: MulZeroClass.mul_zero, MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder, lt_of_lt_of_le
-- 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 : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
neg :
  Eq.{u_2 + 1} (α := 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)
    (0 : R)
⊢ 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)

Tactic:
symm
-- 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 : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
apply :
  IsWeightedHomogeneous w
    (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))
    (p + q)
⊢ Eq.{u_2 + 1} (α := 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)
    (0 : R)

Tactic:
apply IsWeightedHomogeneous.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 g : MvPowerSeries σ R
p q : ℕ
hf : (↑p : ℕ∞) ≤ weightedOrder w f
hg : (↑q : ℕ∞) ≤ weightedOrder w g
d : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
d_1 : σ →₀ ℕ
⊢ Ne.{u_2 + 1} (α := R)
      ((coeff d_1 : (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)
      (0 : R) →
    (weight w : (a : σ →₀ ℕ) → ℕ) d_1 = p + q

Tactic:
IsWeightedHomogeneous.mul
      (isWeightedHomogeneous_weightedHomogeneousComponent w f p)
      (isWeightedHomogeneous_weightedHomogeneousComponent w g q)

Premises used: MvPowerSeries.IsWeightedHomogeneous.mul, 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
d : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
⊢ IsWeightedHomogeneous w
    (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))
    (p + q)

Tactic:
exact IsWeightedHomogeneous.mul
      (isWeightedHomogeneous_weightedHomogeneousComponent w f p)
      (isWeightedHomogeneous_weightedHomogeneousComponent w g q)

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

Tactic:
apply IsWeightedHomogeneous.coeff_eq_zero hf

Premises used: MvPowerSeries.IsWeightedHomogeneous.coeff_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
p : ℕ
hf : f.IsHomogeneous p
d : σ →₀ ℕ
hd : (degree : (a : σ →₀ ℕ) → ℕ) d ≠ p
rwa rwa₁ rwa₂ rwa₃ : ∀ (hd : (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d ≠ p), (weight 1 : (a : σ →₀ ℕ) → ℕ) d ≠ p
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) d ≠ p

Tactic:
rwa [degree_eq_weight_one] at hd

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f g : MvPowerSeries σ R
p : ℕ
hf : f.IsHomogeneous p
hg : g.IsHomogeneous p
d : σ →₀ ℕ
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R) →
    (weight 1 : (a : σ →₀ ℕ) → ℕ) d = p

Tactic:
IsWeightedHomogeneous.add hf hg

Premises used: MvPowerSeries.IsWeightedHomogeneous.add
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f g : MvPowerSeries σ R
p q : ℕ
hf : f.IsHomogeneous p
hg : g.IsHomogeneous q
d : σ →₀ ℕ
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R) →
    (weight 1 : (a : σ →₀ ℕ) → ℕ) d = p + q

Tactic:
IsWeightedHomogeneous.mul hf hg

Premises used: MvPowerSeries.IsWeightedHomogeneous.mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
p : ℕ
d : σ →₀ ℕ
f : MvPowerSeries σ R
rw :
  Eq.{u_2 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        ((homogeneousComponent p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    (if (weight fun (x : σ) ↦ 1 : (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)
        ((homogeneousComponent p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    (if (degree : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) f else 0 : R)

Tactic:
rw [degree_eq_weight_one]

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
p : ℕ
d : σ →₀ ℕ
f : MvPowerSeries σ R
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        ((homogeneousComponent p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    (if (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) f else 0 : R)

Tactic:
coeff_weightedHomogeneousComponent 1 p d f

Premises used: MvPowerSeries.coeff_weightedHomogeneousComponent, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
p : ℕ
d : σ →₀ ℕ
f : MvPowerSeries σ R
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        ((homogeneousComponent p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    (if (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) f else 0 : R)

Tactic:
exact coeff_weightedHomogeneousComponent 1 p d f

Premises used: MvPowerSeries.coeff_weightedHomogeneousComponent, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) < f.order
⊢ Eq (α := MvPowerSeries σ R)
    ((homogeneousComponent p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)

Tactic:
weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero hf

Premises used: MvPowerSeries.weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
p : ℕ
hf : (↑p : ℕ∞) = f.order
⊢ Ne (α := MvPowerSeries σ R)
    ((homogeneousComponent p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)

Tactic:
weightedHomogeneousComponent_of_weightedOrder hf

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

Tactic:
isWeightedHomogeneous_weightedHomogeneousComponent 1 f p

Premises used: MvPowerSeries.isWeightedHomogeneous_weightedHomogeneousComponent, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
p : ℕ
⊢ f.IsHomogeneous p ↔ f = (homogeneousComponent p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f

Tactic:
isWeightedHomogeneous_iff_eq_weightedHomogeneousComponent

Premises used: MvPowerSeries.IsHomogeneous, MvPowerSeries.isWeightedHomogeneous_iff_eq_weightedHomogeneousComponent
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f g : MvPowerSeries σ R
p q : ℕ
hf : (↑p : ℕ∞) ≤ f.order
hg : (↑q : ℕ∞) ≤ g.order
⊢ (homogeneousComponent (p + q) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (f * g) =
    HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((homogeneousComponent p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
      ((homogeneousComponent q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)

Tactic:
weightedHomogeneousComponent_mul_of_le_weightedOrder hf hg

Premises used: MvPowerSeries.weightedHomogeneousComponent_mul_of_le_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_3
R : Type u_4
t u : TopologicalSpace R
htu : t ≤ u
change :
  LE.le (α := TopologicalSpace (MvPowerSeries σ R))
    (⨅ (i : σ →₀ ℕ),
      TopologicalSpace.induced (Y := (fun (a : σ →₀ ℕ) ↦ R) i) (fun (f : (i : σ →₀ ℕ) → (fun (a : σ →₀ ℕ) ↦ R) i) ↦ f i)
        ((fun (i : σ →₀ ℕ) ↦ t) i))
    (⨅ (i : σ →₀ ℕ),
      TopologicalSpace.induced (Y := (fun (a : σ →₀ ℕ) ↦ R) i) (fun (f : (i : σ →₀ ℕ) → (fun (a : σ →₀ ℕ) ↦ R) i) ↦ f i)
        ((fun (i : σ →₀ ℕ) ↦ u) i))
⊢ LE.le (α := TopologicalSpace (MvPowerSeries σ R)) (instTopologicalSpace R) (instTopologicalSpace R)

Tactic:
change ⨅ i, _ ≤ ⨅ i, _