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 : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
rw rw₁ rw₂ rw₃ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R) →
    (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
have rw₄ : ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
  Eq.{u_2 + 1} (α := R)
    (∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) g : R))
    0
Tactic: classical
  rw [not_imp_comm]
  intro hd
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  intro x hx
  rw [Finset.mem_antidiagonal] at hx
  suffices weight w x.1 ≠ p ∨ weight w x.2 ≠ q by
    rcases this with hp | hq
    · rw [hf.coeff_eq_zero hp, zero_mul]
    · rw [hg.coeff_eq_zero hq, mul_zero]
  rw [← not_and_or]
  rintro ⟨hp, hq⟩
  apply hd
  rw [← hx, map_add, hp, hq]
-- 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 : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
rw rw₁ rw₂ rw₃ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)
rw₄ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R)
      (∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d,
        HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R) g : R))
      0
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R) →
    (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
have h : ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
  ∀ 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) =
      0
Tactic: classical
  rw [not_imp_comm]
  intro hd
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  intro x hx
  rw [Finset.mem_antidiagonal] at hx
  suffices weight w x.1 ≠ p ∨ weight w x.2 ≠ q by
    rcases this with hp | hq
    · rw [hf.coeff_eq_zero hp, zero_mul]
    · rw [hg.coeff_eq_zero hq, mul_zero]
  rw [← not_and_or]
  rintro ⟨hp, hq⟩
  apply hd
  rw [← hx, map_add, hp, hq]
-- 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 : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
rw rw₁ rw₂ rw₃ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)
rw₄ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R)
      (∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d,
        HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R) g : R))
      0
h h₁ :
  ∀ (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) =
      0
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R) →
    (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
have h₂ : ∀ (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) =
    0
Tactic: classical
  rw [not_imp_comm]
  intro hd
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  intro x hx
  rw [Finset.mem_antidiagonal] at hx
  suffices weight w x.1 ≠ p ∨ weight w x.2 ≠ q by
    rcases this with hp | hq
    · rw [hf.coeff_eq_zero hp, zero_mul]
    · rw [hg.coeff_eq_zero hq, mul_zero]
  rw [← not_and_or]
  rintro ⟨hp, hq⟩
  apply hd
  rw [← hx, map_add, hp, hq]
-- 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 : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
rw rw₁ rw₂ rw₃ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)
rw₄ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R)
      (∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d,
        HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R) g : R))
      0
h h₁ :
  ∀ (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) =
      0
h₂ :
  ∀ (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) =
      0
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R) →
    (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
have h₃ : ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q) (x : (σ →₀ ℕ) × (σ →₀ ℕ)) (hx : x.1 + x.2 = d),
  (weight w : (a : σ →₀ ℕ) → ℕ) x.1 ≠ p ∨ (weight w : (a : σ →₀ ℕ) → ℕ) x.2 ≠ q
Tactic: classical
  rw [not_imp_comm]
  intro hd
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  intro x hx
  rw [Finset.mem_antidiagonal] at hx
  suffices weight w x.1 ≠ p ∨ weight w x.2 ≠ q by
    rcases this with hp | hq
    · rw [hf.coeff_eq_zero hp, zero_mul]
    · rw [hg.coeff_eq_zero hq, mul_zero]
  rw [← not_and_or]
  rintro ⟨hp, hq⟩
  apply hd
  rw [← hx, map_add, hp, hq]
-- 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 : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
rw rw₁ rw₂ rw₃ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)
rw₄ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R)
      (∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d,
        HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R) g : R))
      0
h h₁ :
  ∀ (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) =
      0
h₂ :
  ∀ (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) =
      0
h₃ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q) (x : (σ →₀ ℕ) × (σ →₀ ℕ)) (hx : x.1 + x.2 = d),
    (weight w : (a : σ →₀ ℕ) → ℕ) x.1 ≠ p ∨ (weight w : (a : σ →₀ ℕ) → ℕ) x.2 ≠ q
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R) →
    (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
have h₄ : ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q) (x : (σ →₀ ℕ) × (σ →₀ ℕ)) (hx : x.1 + x.2 = d),
  ¬((weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p ∧ (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q)
Tactic: classical
  rw [not_imp_comm]
  intro hd
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  intro x hx
  rw [Finset.mem_antidiagonal] at hx
  suffices weight w x.1 ≠ p ∨ weight w x.2 ≠ q by
    rcases this with hp | hq
    · rw [hf.coeff_eq_zero hp, zero_mul]
    · rw [hg.coeff_eq_zero hq, mul_zero]
  rw [← not_and_or]
  rintro ⟨hp, hq⟩
  apply hd
  rw [← hx, map_add, hp, hq]
-- 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 : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
rw rw₁ rw₂ rw₃ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)
rw₄ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R)
      (∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d,
        HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R) g : R))
      0
h h₁ :
  ∀ (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) =
      0
h₂ :
  ∀ (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) =
      0
h₃ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q) (x : (σ →₀ ℕ) × (σ →₀ ℕ)) (hx : x.1 + x.2 = d),
    (weight w : (a : σ →₀ ℕ) → ℕ) x.1 ≠ p ∨ (weight w : (a : σ →₀ ℕ) → ℕ) x.2 ≠ q
h₄ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q) (x : (σ →₀ ℕ) × (σ →₀ ℕ)) (hx : x.1 + x.2 = d),
    ¬((weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p ∧ (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q)
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R) →
    (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
have h₅ : ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q) (x : (σ →₀ ℕ) × (σ →₀ ℕ)) (hx : x.1 + x.2 = d)
  (hp : (weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p) (hq : (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q), False
Tactic: classical
  rw [not_imp_comm]
  intro hd
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  intro x hx
  rw [Finset.mem_antidiagonal] at hx
  suffices weight w x.1 ≠ p ∨ weight w x.2 ≠ q by
    rcases this with hp | hq
    · rw [hf.coeff_eq_zero hp, zero_mul]
    · rw [hg.coeff_eq_zero hq, mul_zero]
  rw [← not_and_or]
  rintro ⟨hp, hq⟩
  apply hd
  rw [← hx, map_add, hp, hq]
-- 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 : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
rw rw₁ rw₂ rw₃ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)
rw₄ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q),
    Eq.{u_2 + 1} (α := R)
      (∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d,
        HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R) g : R))
      0
h h₁ :
  ∀ (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) =
      0
h₂ :
  ∀ (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) =
      0
h₃ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q) (x : (σ →₀ ℕ) × (σ →₀ ℕ)) (hx : x.1 + x.2 = d),
    (weight w : (a : σ →₀ ℕ) → ℕ) x.1 ≠ p ∨ (weight w : (a : σ →₀ ℕ) → ℕ) x.2 ≠ q
h₄ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q) (x : (σ →₀ ℕ) × (σ →₀ ℕ)) (hx : x.1 + x.2 = d),
    ¬((weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p ∧ (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q)
h₅ :
  ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q) (x : (σ →₀ ℕ) × (σ →₀ ℕ)) (hx : x.1 + x.2 = d)
    (hp : (weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p) (hq : (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q), False
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R) →
    (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
have h₆ : ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q) (x : (σ →₀ ℕ) × (σ →₀ ℕ)) (hx : x.1 + x.2 = d)
  (hp : (weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p) (hq : (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q),
  (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
Tactic: classical
  rw [not_imp_comm]
  intro hd
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  intro x hx
  rw [Finset.mem_antidiagonal] at hx
  suffices weight w x.1 ≠ p ∨ weight w x.2 ≠ q by
    rcases this with hp | hq
    · rw [hf.coeff_eq_zero hp, zero_mul]
    · rw [hg.coeff_eq_zero hq, mul_zero]
  rw [← not_and_or]
  rintro ⟨hp, hq⟩
  apply hd
  rw [← hx, map_add, hp, hq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
⊢ (fun (d : σ →₀ ℕ) ↦
      if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) (f + g) else 0) =
    HAdd.hAdd (α := MvPowerSeries σ R)
      (fun (d : σ →₀ ℕ) ↦ if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) f else 0)
      fun (d : σ →₀ ℕ) ↦ if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) g else 0
have 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) (f + g) else 0 :
      R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        (HAdd.hAdd (α := MvPowerSeries σ R)
          (fun (d : σ →₀ ℕ) ↦
            if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) f else 0)
          fun (d : σ →₀ ℕ) ↦
          if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) g else 0) :
      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 : σ → ℕ
p : ℕ
f g : 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) (f + g) else 0 :
      R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        (HAdd.hAdd (α := MvPowerSeries σ R)
          (fun (d : σ →₀ ℕ) ↦
            if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) f else 0)
          fun (d : σ →₀ ℕ) ↦
          if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then (coeff d : (a : MvPowerSeries σ R) → R) g else 0) :
      R)
have h : (if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then f d + g d else 0) =
  (if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then f d else 0) + if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then g d else 0
Tactic: simp only [map_add, coeff_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ (if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then f d + g d else 0) =
    (if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then f d else 0) + if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then g d else 0
have pos : ∀ (h : (weight w : (a : σ →₀ ℕ) → ℕ) d = p), f d + g d = f d + g d
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
pos : ∀ (h : (weight w : (a : σ →₀ ℕ) → ℕ) d = p), f d + g d = f d + g d
⊢ (if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then f d + g d else 0) =
    (if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then f d else 0) + if (weight w : (a : σ →₀ ℕ) → ℕ) d = p then g d else 0
have neg : ∀ (h : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p), 0 = HAdd.hAdd (α := R) 0 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p
⊢ 0 = HAdd.hAdd (α := R) 0 0
have neg : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
p : ℕ
a : R
f : MvPowerSeries σ 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
have 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)
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 : (↑p : ℕ∞) < weightedOrder w f
⊢ Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
have 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)
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 : (↑p : ℕ∞) < weightedOrder w f
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)
have 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)
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 : (↑p : ℕ∞) < weightedOrder w f
d : σ →₀ ℕ
⊢ 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)
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) 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 : (↑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)
⊢ 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)
have neg : ∀ (hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p),
  Eq.{u_2 + 1} (α := R) (0 : R) ((coeff d : (a : MvPowerSeries σ R) → 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 : (↑p : ℕ∞) < weightedOrder w f
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) 0 : R)
have pos : Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
Tactic: rw [coeff_zero]
-- 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
d : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = p
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
have pos : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f
Tactic: apply coeff_eq_zero_of_lt_weightedOrder w
-- 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
d : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p
⊢ Eq.{u_2 + 1} (α := R) (0 : R) ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
have neg : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [map_zero]
-- 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)
⊢ (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
have rw : Eq (α := ℕ∞) (↑(toNat (↑p : ℕ∞)) : ℕ∞) (↑p : ℕ∞)
Tactic: rw [← hf, toNat_coe]
-- 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)
rw : Eq (α := ℕ∞) (↑(toNat (↑p : ℕ∞)) : ℕ∞) (↑p : ℕ∞)
⊢ (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
have rw₁ : Eq (α := ℕ∞) (↑p : ℕ∞) (↑p : ℕ∞)
Tactic: rw [← hf, toNat_coe]
-- 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)
⊢ False
have 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
Tactic: obtain ⟨d, hd⟩ := f.exists_coeff_ne_zero_and_weightedOrder w (by rw [← hf, toNat_coe])
-- 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' :
  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
⊢ False
have hd₁ : ¬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
Cleared hypotheses: hd