awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
mp :
  w ≤ φ.lexOrder →
    ∀ (d : σ →₀ ℕ),
      (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
        Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
⊢ w ≤ φ.lexOrder ↔
    ∀ (d : σ →₀ ℕ),
      (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
        Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have mpr : (∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)) →
  w ≤ φ.lexOrder
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : w ≤ φ.lexOrder
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have mp : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
Tactic: apply coeff_eq_zero_of_lt_lexOrder
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h :
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
⊢ w ≤ φ.lexOrder
have mpr : ¬φ.lexOrder < w
Tactic: rw [← not_lt]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h :
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
h' : φ.lexOrder < w
⊢ φ ≠ 0
have rw : ¬φ.lexOrder = ⊤
Tactic: rw [ne_eq, ← lexOrder_eq_top_iff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h :
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
h' : φ.lexOrder < w
⊢ False
have hφ : φ ≠ 0
Tactic: have hφ : φ ≠ 0 := by
      rw [ne_eq, ← lexOrder_eq_top_iff_eq_zero]
      exact ne_top_of_lt h'
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h :
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
h' : φ.lexOrder < w
hφ : φ ≠ 0
⊢ False
have mpr : ∀ (d : σ →₀ ℕ) (hd : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))), False
Tactic: obtain ⟨d, hd⟩ := exists_finsupp_eq_lexOrder_of_ne_zero hφ
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h :
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
h' : φ.lexOrder < w
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))
⊢ False
have mpr : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w
Tactic: refine coeff_ne_zero_of_lexOrder hd.symm (h d ?_)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
⊢ min φ.lexOrder ψ.lexOrder ≤ (φ + ψ).lexOrder
have rw : ∀ (d : σ →₀ ℕ),
  (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < min φ.lexOrder ψ.lexOrder →
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (φ + ψ) : R) (0 : R)
Tactic: rw [le_lexOrder_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (hypothesis)
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 (σ →₀ ℕ))) < min φ.lexOrder ψ.lexOrder
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (φ + ψ) : R) (0 : R)
have hd₁ : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder ∧
  (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < ψ.lexOrder
Tactic: simp only [lt_min_iff] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (φ + ψ) : R) (0 : R)
have rw : HAdd.hAdd (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) ψ : R) =
  0
Tactic: rw [map_add, coeff_eq_zero_of_lt_lexOrder hd.1, coeff_eq_zero_of_lt_lexOrder hd.2, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (φ + ψ) : R) (0 : R)
have rw₁ : HAdd.hAdd (α := R) (β := R) (0 : R) ((coeff d : (a : MvPowerSeries σ R) → R) ψ : R) = 0
Tactic: rw [map_add, coeff_eq_zero_of_lt_lexOrder hd.1, coeff_eq_zero_of_lt_lexOrder hd.2, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (φ + ψ) : R) (0 : R)
have rw₂ : HAdd.hAdd (α := R) 0 0 = 0
Tactic: rw [map_add, coeff_eq_zero_of_lt_lexOrder hd.1, coeff_eq_zero_of_lt_lexOrder hd.2, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (φ + ψ) : R) (0 : R)
have rw₃ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [map_add, coeff_eq_zero_of_lt_lexOrder hd.1, coeff_eq_zero_of_lt_lexOrder hd.2, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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 (σ →₀ ℕ)))
⊢ (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)
have 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
Tactic: rw [coeff_mul, Finset.sum_eq_single_of_mem ⟨p, q⟩ (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (hypothesis)
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)
⊢ HMul.hMul (α := R) (β := R) ((coeff (u, v).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (u, v).2 : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
have h₁ : u + v = p + q
Tactic: simp only [Finset.mem_antidiagonal] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ HMul.hMul (α := R) (β := R) ((coeff (u, v).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (u, v).2 : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
have 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
Tactic: rcases trichotomy_of_add_eq_add (congrArg toLex h) with h'' | h'' | h''
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ HMul.hMul (α := R) (β := R) ((coeff (u, v).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (u, v).2 : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
have 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
Tactic: rcases trichotomy_of_add_eq_add (congrArg toLex h) with h'' | h'' | h''
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ HMul.hMul (α := R) (β := R) ((coeff (u, v).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (u, v).2 : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
have 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
Tactic: rcases trichotomy_of_add_eq_add (congrArg toLex h) with h'' | h'' | h''
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ HMul.hMul (α := R) (β := R) ((coeff (u, v).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (u, v).2 : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
have inr : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
Tactic: rw [coeff_eq_zero_of_lt_lexOrder (d := u), zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
have inr : LT.lt (α := WithTop (Lex (σ →₀ ℕ)))
  ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
  ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
Tactic: rw [hp]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ LT.lt (α := WithTop (Lex (σ →₀ ℕ)))
    ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
    ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
have inr : LT.lt (α := Lex (σ →₀ ℕ)) ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u : Lex (σ →₀ ℕ))
  ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p : Lex (σ →₀ ℕ))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ HMul.hMul (α := R) (β := R) ((coeff (u, v).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (u, v).2 : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
have inr : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) < ψ.lexOrder
Tactic: rw [coeff_eq_zero_of_lt_lexOrder (d := v), mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) < ψ.lexOrder
have inr : LT.lt (α := WithTop (Lex (σ →₀ ℕ)))
  ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
  ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
Tactic: rw [hq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ LT.lt (α := WithTop (Lex (σ →₀ ℕ)))
    ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
    ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
have inr : LT.lt (α := Lex (σ →₀ ℕ)) ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v : Lex (σ →₀ ℕ))
  ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q : Lex (σ →₀ ℕ))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
⊢ φ.lexOrder + ψ.lexOrder ≤ (φ * ψ).lexOrder
have rw : ∀ (d : σ →₀ ℕ),
  (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder →
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (φ * ψ) : R) (0 : R)
Tactic: rw [le_lexOrder_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (φ * ψ) : 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) φ : R)
      ((coeff p.2 : (a : MvPowerSeries σ R) → R) ψ : R))
  0
Tactic: rw [coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ 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
have 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
Tactic: apply Finset.sum_eq_zero
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (hypothesis)
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
⊢ HMul.hMul (α := R) (β := R) ((coeff (u, v).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (u, v).2 : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
have h₁ : u + v = d
Tactic: simp only [Finset.mem_antidiagonal] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ HMul.hMul (α := R) (β := R) ((coeff (u, v).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (u, v).2 : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
have h₁ : HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) =
  0
Tactic: simp only
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
have 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
Tactic: rcases this with (hu | hv)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
have 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
Tactic: rcases this with (hu | hv)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
have inl : HMul.hMul (α := R) (β := R) (0 : R) ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) = 0
Tactic: rw [coeff_eq_zero_of_lt_lexOrder hu, zero_mul]