awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd :
  (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder ∧
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < ψ.lexOrder
rw :
  HAdd.hAdd (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
rw₁ : HAdd.hAdd (α := R) (β := R) (0 : R) ((coeff d : (a : MvPowerSeries σ R) → R) ψ : 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) (φ + ψ) : R) (0 : R)

Tactic:
rw [map_add, coeff_eq_zero_of_lt_lexOrder hd.1, coeff_eq_zero_of_lt_lexOrder hd.2, add_zero]

Premises used: map_add, And.right, And.left, add_zero, MvPowerSeries.coeff_eq_zero_of_lt_lexOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
⊢ (p, q) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (p + q)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
rw :
  ∀ b ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (p + q),
    b ≠ (p, q) →
      HMul.hMul (α := R) (β := R) ((coeff b.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff b.2 : (a : MvPowerSeries σ R) → R) ψ : R) =
        0
⊢ (coeff (p + q) : (a : MvPowerSeries σ R) → R) (φ * ψ) =
    HMul.hMul (α := R) (β := R) ((coeff p : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff q : (a : MvPowerSeries σ R) → R) ψ : R)

Tactic:
rw [coeff_mul, Finset.sum_eq_single_of_mem ⟨p, q⟩ (by simp)]

Premises used: Finset.sum_eq_single_of_mem, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
u v : σ →₀ ℕ
h : (u, v) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ (p + q)
h' : (u, v) ≠ (p, q)
⊢ u + v = p + q

Tactic:
simp only [Finset.mem_antidiagonal] at h

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
inl :
  ∀ (h'' : u = p ∧ v = q),
    HMul.hMul (α := R) (β := R) ((coeff (u, v).1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff (u, v).2 : (a : MvPowerSeries σ R) → R) ψ : R) =
      0
inr :
  ∀ (h'' : u < p),
    HMul.hMul (α := R) (β := R) ((coeff (u, v).1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff (u, v).2 : (a : MvPowerSeries σ R) → R) ψ : R) =
      0
inr₁ :
  ∀ (h'' : v < q),
    HMul.hMul (α := R) (β := R) ((coeff (u, v).1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff (u, v).2 : (a : MvPowerSeries σ R) → R) ψ : R) =
      0
⊢ HMul.hMul (α := R) (β := R) ((coeff (u, v).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (u, v).2 : (a : MvPowerSeries σ R) → R) ψ : R) =
    0

Tactic:
rcases trichotomy_of_add_eq_add (congrArg toLex h) with h'' | h'' | h''

Premises used: congrArg, trichotomy_of_add_eq_add, DFunLike.coe, toLex
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
h'' : u = p ∧ v = q
⊢ (u, v) = (p, q)

Tactic:
simp [h''.1, h''.2]

Premises used: And.right, And.left
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
h'' : u = p ∧ v = q
⊢ HMul.hMul (α := R) (β := R) ((coeff (u, v).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (u, v).2 : (a : MvPowerSeries σ R) → R) ψ : R) =
    0

Tactic:
exact False.elim (h' (by simp [h''.1, h''.2]))

Premises used: False.elim
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
h'' : u < p
inr : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
⊢ HMul.hMul (α := R) (β := R) ((coeff (u, v).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (u, v).2 : (a : MvPowerSeries σ R) → R) ψ : R) =
    0

Tactic:
rw [coeff_eq_zero_of_lt_lexOrder (d := u), zero_mul]

Premises used: MulZeroClass.zero_mul, MvPowerSeries.coeff_eq_zero_of_lt_lexOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
h'' : u < p
inr :
  LT.lt (α := WithTop (Lex (σ →₀ ℕ)))
    ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
    ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
⊢ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder

Tactic:
rw [hp]
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
h'' : u < p
inr inr₁ inr₂ inr₃ :
  LT.lt (α := Lex (σ →₀ ℕ)) ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u : Lex (σ →₀ ℕ))
    ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p : Lex (σ →₀ ℕ))
⊢ LT.lt (α := WithTop (Lex (σ →₀ ℕ)))
    ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
    ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
h'' : v < q
inr : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) < ψ.lexOrder
⊢ HMul.hMul (α := R) (β := R) ((coeff (u, v).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (u, v).2 : (a : MvPowerSeries σ R) → R) ψ : R) =
    0

Tactic:
rw [coeff_eq_zero_of_lt_lexOrder (d := v), mul_zero]

Premises used: MulZeroClass.mul_zero, MvPowerSeries.coeff_eq_zero_of_lt_lexOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
h'' : v < q
inr :
  LT.lt (α := WithTop (Lex (σ →₀ ℕ)))
    ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
    ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
⊢ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) < ψ.lexOrder

Tactic:
rw [hq]
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
h'' : v < q
inr inr₁ inr₂ inr₃ :
  LT.lt (α := Lex (σ →₀ ℕ)) ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v : Lex (σ →₀ ℕ))
    ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q : Lex (σ →₀ ℕ))
⊢ LT.lt (α := WithTop (Lex (σ →₀ ℕ)))
    ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
    ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
rw :
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (φ * ψ) : R) (0 : R)
⊢ φ.lexOrder + ψ.lexOrder ≤ (φ * ψ).lexOrder

Tactic:
rw [le_lexOrder_iff]

Premises used: MvPowerSeries.le_lexOrder_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder
rw :
  Eq.{u_2 + 1} (α := R)
    (∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) ψ : R))
    0
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (φ * ψ) : R) (0 : R)

Tactic:
rw [coeff_mul]

Premises used: MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder
h :
  ∀ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d,
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) ψ : R) =
      0
⊢ Eq.{u_2 + 1} (α := R)
    (∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) ψ : R))
    0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : (u, v) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d
⊢ u + v = d

Tactic:
simp only [Finset.mem_antidiagonal] at h

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
h₁ :
  HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
⊢ HMul.hMul (α := R) (β := R) ((coeff (u, v).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (u, v).2 : (a : MvPowerSeries σ R) → R) ψ : R) =
    0

Tactic:
simp only
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
this :
  (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder ∨
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) < ψ.lexOrder
inl :
  ∀ (hu : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder),
    HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) =
      0
inr :
  ∀ (hv : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) < ψ.lexOrder),
    HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) =
      0
⊢ HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) =
    0

Tactic:
rcases this with (hu | hv)
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
hu : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
inl : HMul.hMul (α := R) (β := R) (0 : R) ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) = 0
inl₁ inl₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) =
    0

Tactic:
rw [coeff_eq_zero_of_lt_lexOrder hu, zero_mul]

Premises used: MulZeroClass.zero_mul, MvPowerSeries.coeff_eq_zero_of_lt_lexOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
hv : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) < ψ.lexOrder
inr : HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R) (0 : R) = 0
inr₁ inr₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) =
    0

Tactic:
rw [coeff_eq_zero_of_lt_lexOrder hv, mul_zero]

Premises used: MulZeroClass.mul_zero, MvPowerSeries.coeff_eq_zero_of_lt_lexOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
h₁ :
  (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder ∨
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) < ψ.lexOrder
⊢ HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) =
    0

Tactic:
suffices toLex u < lexOrder φ ∨ toLex v < lexOrder ψ by
    rcases this with (hu | hv)
    · rw [coeff_eq_zero_of_lt_lexOrder hu, zero_mul]
    · rw [coeff_eq_zero_of_lt_lexOrder hv, mul_zero]
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
h₁ :
  φ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) →
    ¬ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ)))
⊢ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder ∨
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) < ψ.lexOrder

Tactic:
rw [or_iff_not_imp_left, not_lt, ← not_le]

Premises used: not_le, not_lt, Classical.or_iff_not_imp_left
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
hu : φ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ)))
hv : ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ)))
h₁ :
  ∀ (hd : ¬φ.lexOrder + ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))))
    (u v : σ →₀ ℕ) (h : u + v = d)
    (hu : φ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))))
    (hv : ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ)))), False
⊢ False

Tactic:
rw [← not_le] at hd

Premises used: not_le
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ¬φ.lexOrder + ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))
u v : σ →₀ ℕ
h : u + v = d
hu : φ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ)))
hv : ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ)))
h₁ : φ.lexOrder + ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))
⊢ False

Tactic:
apply hd
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ¬φ.lexOrder + ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))
u v : σ →₀ ℕ
h : u + v = d
hu : φ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ)))
hv : ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ)))
⊢ φ.lexOrder + ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))

Tactic:
simp only [← h, toLex_add, WithTop.coe_add, add_le_add hu hv]

Premises used: add_le_add, toLex_add, WithTop.coe_add
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
inst_3 : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
inl : (0 * ψ).lexOrder = lexOrder.{u_1, u_2} (R := R) 0 + ψ.lexOrder
inr : ∀ (hφ : φ ≠ 0), (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Tactic:
obtain rfl | hφ := eq_or_ne φ 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
inst_3 : NoZeroDivisors R
ψ : MvPowerSeries σ R
⊢ (0 * ψ).lexOrder = lexOrder.{u_1, u_2} (R := R) 0 + ψ.lexOrder

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
inst_3 : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
inr : (φ * 0).lexOrder = φ.lexOrder + lexOrder.{u_1, u_2} (R := R) 0
inr₁ : ∀ (hψ : ψ ≠ 0), (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Tactic:
obtain rfl | hψ := eq_or_ne ψ 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
inst_3 : NoZeroDivisors R
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ (φ * 0).lexOrder = φ.lexOrder + lexOrder.{u_1, u_2} (R := R) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
inst_3 : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
hψ : ψ ≠ 0
inr :
  ∀ (p : σ →₀ ℕ) (hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))),
    (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Tactic:
rcases exists_finsupp_eq_lexOrder_of_ne_zero hφ with ⟨p, hp⟩

Premises used: MvPowerSeries.exists_finsupp_eq_lexOrder_of_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
inst_3 : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
hψ : ψ ≠ 0
p : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
inr :
  ∀ (q : σ →₀ ℕ) (hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))),
    (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Tactic:
rcases exists_finsupp_eq_lexOrder_of_ne_zero hψ with ⟨q, hq⟩

Premises used: MvPowerSeries.exists_finsupp_eq_lexOrder_of_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
inst_3 : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
hψ : ψ ≠ 0
p : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
q : σ →₀ ℕ
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
apply : (φ * ψ).lexOrder ≤ φ.lexOrder + ψ.lexOrder
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Tactic:
apply le_antisymm _ (lexOrder_mul_ge φ ψ)

Premises used: le_antisymm, MvPowerSeries.lexOrder_mul_ge
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
inst_3 : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
hψ : ψ ≠ 0
p : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
q : σ →₀ ℕ
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
rw :
  (φ * ψ).lexOrder ≤
    HAdd.hAdd (α := WithTop (Lex (σ →₀ ℕ))) (β := WithTop (Lex (σ →₀ ℕ)))
      ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
      ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
⊢ (φ * ψ).lexOrder ≤ φ.lexOrder + ψ.lexOrder

Tactic:
rw [hp, hq]