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 : 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
⊢ False
have apply : Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
Tactic: apply hd.1
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
have 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)
Tactic: rw [MvPowerSeries.ext_iff] at hf'
Cleared hypotheses: hf', d, hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (hypothesis)
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) f : R) (0 : R)
have 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)
Tactic: specialize hf' d
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (hypothesis)
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)
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
have hf'₁ : (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'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
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
have 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)
Tactic: rw [not_imp_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
d : σ →₀ ℕ
hd : ¬(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)
have 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)
Tactic: rw [coeff_weightedHomogeneousComponent, if_neg hd]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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)
⊢ 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)
have rw₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [coeff_weightedHomogeneousComponent, if_neg hd]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
⊢ IsWeightedHomogeneous w f p ↔ f = (weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f
have mp : IsWeightedHomogeneous w f p → f = (weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ IsWeightedHomogeneous w f p ↔ f = (weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f
have mpr : f = (weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f → IsWeightedHomogeneous w f p
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
⊢ f = (weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f
have 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)
Tactic: ext d
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
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)
have 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)
Tactic: rw [coeff_weightedHomogeneousComponent]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
d : σ →₀ ℕ
⊢ 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)
have 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)
Tactic: split_ifs with hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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)
⊢ 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)
have neg : ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p),
  Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
Tactic: split_ifs with hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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 w f p
have mpr : IsWeightedHomogeneous.{u_1, u_2} (R := R) w
  ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) p
Tactic: rw [hf]
-- 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: ext d
-- 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 : σ →₀ ℕ
⊢ 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)
have 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)
Tactic: rw [coeff_weightedHomogeneousComponent]
-- 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 : σ →₀ ℕ
⊢ 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)
have 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)
Tactic: split_ifs with 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
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)
⊢ 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)
have 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)
Tactic: split_ifs with 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
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)
have 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)
Tactic: apply Finset.sum_congr rfl
-- 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 : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : 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)
have hx₁ : x.1 + x.2 = d
Tactic: rw [Finset.mem_antidiagonal] at hx
Cleared hypotheses: hx
-- 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 : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = 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)
have hd₁ : HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q
Tactic: rw [← hx, map_add] at hd
Cleared hypotheses: hd, hx
-- 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
⊢ 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)
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)
    (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: simp only [coeff_weightedHomogeneousComponent]
-- 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
⊢ 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.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)
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
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)
⊢ 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.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)
Tactic: rcases trichotomy_of_add_eq_add hd with h | h | h