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
f : MvPowerSeries σ R
n : ℕ
⊢ f.order = (↑n : ℕ∞) ↔
    (∃ (d : σ →₀ ℕ),
        Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
          (degree : (a : σ →₀ ℕ) → ℕ) d = n) ∧
      ∀ (d : σ →₀ ℕ),
        (degree : (a : σ →₀ ℕ) → ℕ) d < n →
          Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
have simp_rw : f.order = (↑n : ℕ∞) ↔
  (∃ (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n) ∧
    ∀ (d : σ →₀ ℕ),
      (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d < n →
        Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
Tactic: simp_rw [degree_eq_weight_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
d : σ →₀ ℕ
a : R
inst_1 : Decidable (a = 0)
⊢ order.{u_1, u_2} (σ := σ) (R := R) ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    if a = 0 then ⊤ else (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
have rw : order.{u_1, u_2} (σ := σ) (R := R) ((monomial d : (a : R) → MvPowerSeries σ R) a) =
  if a = 0 then ⊤ else (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
Tactic: rw [degree_eq_weight_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
d : σ →₀ ℕ
a : R
h : a ≠ 0
⊢ order.{u_1, u_2} (σ := σ) (R := R) ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
have rw : order.{u_1, u_2} (σ := σ) (R := R) ((monomial d : (a : R) → MvPowerSeries σ R) a) =
  (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
Tactic: rw [degree_eq_weight_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
⊢ 1 ≤ f.order ↔ Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
have mp : 1 ≤ f.order → Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
mp : 1 ≤ f.order → Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ 1 ≤ f.order ↔ Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
have mpr : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R) → 1 ≤ f.order
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
h : 1 ≤ f.order
⊢ Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
have mp : (↑((degree : (a : σ →₀ ℕ) → ℕ) 0) : ℕ∞) < f.order
Tactic: apply coeff_of_lt_order
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
h : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ 1 ≤ f.order
have mpr : ∀ (d : σ →₀ ℕ) (hd : LT.lt (α := ℕ∞) (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) 1),
  Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
Tactic: refine MvPowerSeries.le_order fun d hd ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
h : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
hd : LT.lt (α := ℕ∞) (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) 1
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
have hd₁ : Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (0 : ℕ)
Tactic: rw [Nat.cast_lt_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
f : MvPowerSeries σ R
⊢ f.order ≠ 0 ↔ Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
have rw : 1 ≤ f.order ↔ Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
Tactic: rw [← ENat.one_le_iff_ne_zero, one_le_order_iff_constCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
rw : 1 ≤ f.order ↔ Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ f.order ≠ 0 ↔ Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
have rw₁ : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ↔
  Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
Tactic: rw [← ENat.one_le_iff_ne_zero, one_le_order_iff_constCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
n : ℕ
hf : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ (↑n : ℕ∞) ≤ (f ^ n).order
have refine : (↑n : ℕ∞) ≤ n • f.order
Tactic: refine .trans ?_ (le_order_pow n)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < g.order
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * (1 - g)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
have h₁ : (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < g.order
Tactic: rw [degree_eq_weight_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < g.order
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) ((1 - g) * f) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
have h₁ : (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < g.order
Tactic: rw [degree_eq_weight_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_4
ι : Type u_5
inst : CommRing R
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
⊢ (∀ i ∈ s, (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < (g i).order) →
    Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
have rw : (∀ i ∈ s, (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < (g i).order) →
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
Tactic: rw [degree_eq_weight_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), Membership.mem (α := R) T ((coeff n : (a : MvPowerSeries σ R) → R) p : R)
⊢ (p.toSubring T hp).order = p.order
have refine_1 : (p.toSubring T hp).order ≤ p.order
Tactic: refine eq_of_le_of_ge ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), Membership.mem (α := R) T ((coeff n : (a : MvPowerSeries σ R) → R) p : R)
refine_1 : (p.toSubring T hp).order ≤ p.order
⊢ (p.toSubring T hp).order = p.order
have refine_2 : p.order ≤ (p.toSubring T hp).order
Tactic: refine eq_of_le_of_ge ?_ ?_
-- 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 : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g p
d : σ →₀ ℕ
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : 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) (f + g) : 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 g : MvPowerSeries σ R
p : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g p
d : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
have rw : HAdd.hAdd (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) g : R) =
  0
Tactic: rw [map_add, hf.coeff_eq_zero hd, hg.coeff_eq_zero hd, add_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 : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g p
d : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p
rw :
  HAdd.hAdd (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) g : R) =
    0
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
have rw₁ : HAdd.hAdd (α := R) (β := R) (0 : R) ((coeff d : (a : MvPowerSeries σ R) → R) g : R) = 0
Tactic: rw [map_add, hf.coeff_eq_zero hd, hg.coeff_eq_zero hd, add_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 : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g p
d : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p
rw :
  HAdd.hAdd (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) g : R) =
    0
rw₁ : HAdd.hAdd (α := R) (β := R) (0 : R) ((coeff d : (a : MvPowerSeries σ R) → R) g : R) = 0
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
have rw₂ : HAdd.hAdd (α := R) 0 0 = 0
Tactic: rw [map_add, hf.coeff_eq_zero hd, hg.coeff_eq_zero hd, add_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 : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g p
d : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p
rw :
  HAdd.hAdd (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) g : R) =
    0
rw₁ : HAdd.hAdd (α := R) (β := R) (0 : R) ((coeff d : (a : MvPowerSeries σ R) → R) g : R) = 0
rw₂ : HAdd.hAdd (α := R) 0 0 = 0
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
have rw₃ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [map_add, hf.coeff_eq_zero hd, hg.coeff_eq_zero hd, add_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 : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R) →
    (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
have rw : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q →
  Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : 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 g : MvPowerSeries σ R
p q : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)
have rw : 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: rw [coeff_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 : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
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
have h : ∀ 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: apply Finset.sum_eq_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 : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
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) =
    0
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 (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 : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = d
this : (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) =
    0
have inl : ∀ (hp : (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
Tactic: rcases this with hp | hq
Cleared hypotheses: this
-- 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 : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = d
this : (weight w : (a : σ →₀ ℕ) → ℕ) x.1 ≠ p ∨ (weight w : (a : σ →₀ ℕ) → ℕ) x.2 ≠ q
inl :
  ∀ (hp : (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
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have inr : ∀ (hq : (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
Tactic: rcases this with hp | hq
Cleared hypotheses: this
-- 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 : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = d
hp : (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 inl : HMul.hMul (α := R) (β := R) (0 : R) ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) = 0
Tactic: rw [hf.coeff_eq_zero hp, 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 : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = d
hp : (weight w : (a : σ →₀ ℕ) → ℕ) x.1 ≠ p
inl : 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 inl₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [hf.coeff_eq_zero hp, 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 : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = d
hq : (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 inr : HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R) (0 : R) = 0
Tactic: rw [hg.coeff_eq_zero hq, 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 : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = d
hq : (weight w : (a : σ →₀ ℕ) → ℕ) x.2 ≠ q
inr : 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 inr₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [hg.coeff_eq_zero hq, 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 : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
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) =
    0
have h : (weight w : (a : σ →₀ ℕ) → ℕ) x.1 ≠ p ∨ (weight w : (a : σ →₀ ℕ) → ℕ) x.2 ≠ q
Tactic: 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]
-- 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 : σ →₀ ℕ
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
have h : ¬((weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p ∧ (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q)
Tactic: rw [← not_and_or]
-- 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 : σ →₀ ℕ
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
have h : (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
Tactic: apply 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 : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
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
have h : (weight w : (a : σ →₀ ℕ) → ℕ) (x.1 + x.2) = p + q
Tactic: 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 : σ →₀ ℕ
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
h : (weight w : (a : σ →₀ ℕ) → ℕ) (x.1 + x.2) = p + q
⊢ (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
have h₁ : HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q
Tactic: 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 : σ →₀ ℕ
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
h : (weight w : (a : σ →₀ ℕ) → ℕ) (x.1 + x.2) = p + q
h₁ : HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q
⊢ (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
have h₂ : HAdd.hAdd (β := ℕ) p ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q
Tactic: 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 : σ →₀ ℕ
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
h : (weight w : (a : σ →₀ ℕ) → ℕ) (x.1 + x.2) = p + q
h₁ : HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q
h₂ : HAdd.hAdd (β := ℕ) p ((weight w : (a : σ →₀ ℕ) → ℕ) x.2 : ℕ) = p + q
⊢ (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
have h₃ : p + q = p + q
Tactic: 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 : σ →₀ ℕ
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R) →
    (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
have rw : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q →
  Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)
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]