awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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)
⊢ 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)
have 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)
Tactic: rcases trichotomy_of_add_eq_add hd with h | h | h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ 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)
have 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)
Tactic: rw [if_pos h.1, if_pos h.2]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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)
⊢ 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)
have 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)
Tactic: rw [if_pos h.1, if_pos h.2]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ 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)
have pos : 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 [if_neg (ne_of_lt h), zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (hypothesis)
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
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have h₁ : LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) x.1) : ℕ∞) (↑p : ℕ∞)
Tactic: rw [← ENat.coe_lt_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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 : ℕ∞)
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have pos : HMul.hMul (α := R) (β := R) (0 : 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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have pos₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hf), zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ 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)
have pos : 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 [if_neg (ne_of_lt h), mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (hypothesis)
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
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have h₁ : LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) x.2) : ℕ∞) (↑q : ℕ∞)
Tactic: rw [← ENat.coe_lt_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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 : ℕ∞)
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have pos : HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R) (0 : R) = 0
Tactic: rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hg), mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have pos₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hg), mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ 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)
have 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)
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ 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)
have 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)
Tactic: apply IsWeightedHomogeneous.coeff_eq_zero _ hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ (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)
have 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)
Tactic: classical
  ext d
  rw [coeff_weightedHomogeneousComponent]
  split_ifs with hd
  · apply Finset.sum_congr rfl
    intro x hx
    rw [Finset.mem_antidiagonal] at hx
    rw [← hx, map_add] at hd
    simp only [coeff_weightedHomogeneousComponent]
    rcases trichotomy_of_add_eq_add hd with h | h | h
    · rw [if_pos h.1, if_pos h.2]
    · rw [if_neg (ne_of_lt h), zero_mul]
      rw [← ENat.coe_lt_coe] at h
      rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hf), zero_mul]
    · rw [if_neg (ne_of_lt h), mul_zero]
      rw [← ENat.coe_lt_coe] at h
      rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hg), mul_zero]
  · symm
    apply IsWeightedHomogeneous.coeff_eq_zero _ hd
    exact IsWeightedHomogeneous.mul
      (isWeightedHomogeneous_weightedHomogeneousComponent w f p)
      (isWeightedHomogeneous_weightedHomogeneousComponent w g q)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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)
have h₁ : ∀ (d : σ →₀ ℕ),
  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: classical
  ext d
  rw [coeff_weightedHomogeneousComponent]
  split_ifs with hd
  · apply Finset.sum_congr rfl
    intro x hx
    rw [Finset.mem_antidiagonal] at hx
    rw [← hx, map_add] at hd
    simp only [coeff_weightedHomogeneousComponent]
    rcases trichotomy_of_add_eq_add hd with h | h | h
    · rw [if_pos h.1, if_pos h.2]
    · rw [if_neg (ne_of_lt h), zero_mul]
      rw [← ENat.coe_lt_coe] at h
      rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hf), zero_mul]
    · rw [if_neg (ne_of_lt h), mul_zero]
      rw [← ENat.coe_lt_coe] at h
      rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hg), mul_zero]
  · symm
    apply IsWeightedHomogeneous.coeff_eq_zero _ hd
    exact IsWeightedHomogeneous.mul
      (isWeightedHomogeneous_weightedHomogeneousComponent w f p)
      (isWeightedHomogeneous_weightedHomogeneousComponent w g q)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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)
h₁ :
  ∀ (d : σ →₀ ℕ),
    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)
⊢ (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)
have pos : ∀ (d : σ →₀ ℕ) (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)
Tactic: classical
  ext d
  rw [coeff_weightedHomogeneousComponent]
  split_ifs with hd
  · apply Finset.sum_congr rfl
    intro x hx
    rw [Finset.mem_antidiagonal] at hx
    rw [← hx, map_add] at hd
    simp only [coeff_weightedHomogeneousComponent]
    rcases trichotomy_of_add_eq_add hd with h | h | h
    · rw [if_pos h.1, if_pos h.2]
    · rw [if_neg (ne_of_lt h), zero_mul]
      rw [← ENat.coe_lt_coe] at h
      rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hf), zero_mul]
    · rw [if_neg (ne_of_lt h), mul_zero]
      rw [← ENat.coe_lt_coe] at h
      rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hg), mul_zero]
  · symm
    apply IsWeightedHomogeneous.coeff_eq_zero _ hd
    exact IsWeightedHomogeneous.mul
      (isWeightedHomogeneous_weightedHomogeneousComponent w f p)
      (isWeightedHomogeneous_weightedHomogeneousComponent w g q)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
have apply : (weight 1 : (a : σ →₀ ℕ) → ℕ) d ≠ p
Tactic: apply IsWeightedHomogeneous.coeff_eq_zero hf
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) d ≠ p
have rwa : ∀ (hd : (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d ≠ p), (weight 1 : (a : σ →₀ ℕ) → ℕ) d ≠ p
Tactic: rwa [degree_eq_weight_one] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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 (degree : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) f else 0 : R)
have 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)
Tactic: rw [degree_eq_weight_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_3
R : Type u_4
t u : TopologicalSpace R
htu : t ≤ u
⊢ LE.le (α := TopologicalSpace (MvPowerSeries σ R)) (instTopologicalSpace R) (instTopologicalSpace R)
have 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))
Tactic: change ⨅ i, _ ≤ ⨅ i, _