awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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

Tactic:
.trans ?_ (le_order_pow n)

Premises used: LE.le.trans, MvPowerSeries.le_order_pow
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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)
refine : (↑n : ℕ∞) ≤ n • f.order
⊢ (↑n : ℕ∞) ≤ (f ^ n).order

Tactic:
refine .trans ?_ (le_order_pow n)
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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 : ℕ∞) ≤ n • f.order

Tactic:
simpa using le_mul_of_one_le_right' (one_le_order_iff_constCoeff_eq_zero.mpr hf)

Premises used: Iff.mpr, MvPowerSeries.one_le_order_iff_constCoeff_eq_zero, le_mul_of_one_le_right'
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
a : R
⊢ f.order ≤ (a • f).order

Tactic:
le_weightedOrder_smul _

Premises used: MvPowerSeries.le_weightedOrder_smul, MvPowerSeries.order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
S : Type u_3
inst_1 : Semiring S
f : R →+* S
φ : MvPowerSeries σ R
⊢ φ.order ≤ order.{u_1, u_3} (σ := σ) (R := S) ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ)

Tactic:
le_weightedOrder_map _ _

Premises used: MvPowerSeries.le_weightedOrder_map, MvPowerSeries.order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < g.order
⊢ (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < g.order

Tactic:
rw [degree_eq_weight_one] at h

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight fun (x : σ) ↦ 1 : (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)

Tactic:
coeff_mul_left_one_sub_of_lt_weightedOrder _ h

Premises used: MvPowerSeries.coeff_mul_left_one_sub_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight fun (x : σ) ↦ 1 : (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)

Tactic:
exact coeff_mul_left_one_sub_of_lt_weightedOrder _ h

Premises used: MvPowerSeries.coeff_mul_left_one_sub_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight fun (x : σ) ↦ 1 : (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)

Tactic:
coeff_mul_right_one_sub_of_lt_weightedOrder _ h

Premises used: MvPowerSeries.coeff_mul_right_one_sub_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight fun (x : σ) ↦ 1 : (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)

Tactic:
exact coeff_mul_right_one_sub_of_lt_weightedOrder _ h

Premises used: MvPowerSeries.coeff_mul_right_one_sub_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_4
ι : Type u_5
inst : CommRing R
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
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)
⊢ (∀ 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)

Tactic:
rw [degree_eq_weight_one]

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_4
ι : Type u_5
inst : CommRing R
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
⊢ (∀ 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:
coeff_mul_prod_one_sub_of_lt_weightedOrder _ d s f g

Premises used: MvPowerSeries.order, MvPowerSeries.coeff_mul_prod_one_sub_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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, (↑((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:
exact coeff_mul_prod_one_sub_of_lt_weightedOrder _ d s f g

Premises used: MvPowerSeries.coeff_mul_prod_one_sub_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_3
inst : Ring R
f : MvPowerSeries σ R
⊢ (-f).order = f.order

Tactic:
weightedOrder_neg _ f

Premises used: MvPowerSeries.weightedOrder_neg, MvPowerSeries.order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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

Tactic:
eq_of_le_of_ge ?_ ?_

Premises used: eq_of_le_of_ge
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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
refine_2 : p.order ≤ (p.toSubring T hp).order
⊢ (p.toSubring T hp).order = p.order

Tactic:
refine eq_of_le_of_ge ?_ ?_

Premises used: eq_of_le_of_ge
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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)
d : σ →₀ ℕ
hd : (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < (p.toSubring T hp).order
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R) (0 : R)

Tactic:
simp [coeff_of_lt_order hd, ← p.coeff_toSubring T hp]

Premises used: MvPowerSeries.coeff_of_lt_order, MvPowerSeries.coeff_toSubring
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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

Tactic:
exact le_order fun d hd => by simp [coeff_of_lt_order hd, ← p.coeff_toSubring T hp]

Premises used: MvPowerSeries.le_order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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)
d : σ →₀ ℕ
hd : (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < p.order
⊢ Eq.{u_3 + 1} (α := ↥T) ((coeff d : (a : MvPowerSeries σ ↥T) → ↥T) (p.toSubring T hp) : ↥T) (0 : ↥T)

Tactic:
exact_mod_cast (coeff_toSubring p T hp) ▸ (coeff_of_lt_order hd)
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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.order ≤ (p.toSubring T hp).order

Tactic:
exact le_order fun d hd => by exact_mod_cast (coeff_toSubring p T hp) ▸ (coeff_of_lt_order hd)

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

Tactic:
simpa [Classical.not_not] using mt (@hf d) hd

Premises used: Classical.not_not, mt
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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 : σ →₀ ℕ
rw :
  ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p →
    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

Tactic:
rw [not_imp_comm]

Premises used: not_imp_comm
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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
rw₃ rw₄ : Eq.{u_2 + 1} (α := R) 0 0
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)

Tactic:
rw [map_add, hf.coeff_eq_zero hd, hg.coeff_eq_zero hd, add_zero]

Premises used: map_add, MvPowerSeries.IsWeightedHomogeneous.coeff_eq_zero, add_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
rw :
  ¬(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

Tactic:
rw [not_imp_comm]

Premises used: not_imp_comm
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)

Tactic:
rw [coeff_mul]

Premises used: MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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
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
⊢ 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:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : 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
⊢ x.1 + x.2 = d

Tactic:
rw [Finset.mem_antidiagonal] at hx

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : 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
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
⊢ 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
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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
inl₁ inl₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    0

Tactic:
rw [hf.coeff_eq_zero hp, zero_mul]

Premises used: MulZeroClass.zero_mul, MvPowerSeries.IsWeightedHomogeneous.coeff_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : 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
inr₁ inr₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    0

Tactic:
rw [hg.coeff_eq_zero hq, mul_zero]

Premises used: MulZeroClass.mul_zero, MvPowerSeries.IsWeightedHomogeneous.coeff_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
hd : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
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) =
    0

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]
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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
h : ¬((weight w : (a : σ →₀ ℕ) → ℕ) x.1 = p ∧ (weight w : (a : σ →₀ ℕ) → ℕ) x.2 = q)
⊢ (weight w : (a : σ →₀ ℕ) → ℕ) x.1 ≠ p ∨ (weight w : (a : σ →₀ ℕ) → ℕ) x.2 ≠ q

Tactic:
rw [← not_and_or]

Premises used: not_and_or
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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 : σ →₀ ℕ) → ℕ) d = p + q
⊢ False

Tactic:
apply hd
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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
h₃ h₄ : p + q = p + q
⊢ (weight w : (a : σ →₀ ℕ) → ℕ) d = p + q

Tactic:
rw [← hx, map_add, hp, hq]

Premises used: map_add
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : 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
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
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R) →
    (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]

Premises used: not_imp_comm, Finset.sum_eq_zero, map_add, Finset.HasAntidiagonal.mem_antidiagonal, not_and_or, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
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)
⊢ (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

Tactic:
ext d
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
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
⊢ 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:
simp only [map_add, coeff_apply]

Premises used: map_add, MvPowerSeries.coeff_apply
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
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
neg : ∀ (h : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p), 0 = HAdd.hAdd (α := R) 0 0
⊢ (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:
split_ifs with h
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (weight w : (a : σ →₀ ℕ) → ℕ) d = p
⊢ f d + g d = f d + g d

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
p : ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ¬(weight w : (a : σ →₀ ℕ) → ℕ) d = p
neg neg₁ : Eq.{u_2 + 1} (α := R) 0 0
⊢ 0 = HAdd.hAdd (α := R) 0 0

Tactic:
rw [add_zero]

Premises used: add_zero