awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj :
  ∀ j_1 < j,
    coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j_1 =
      HSMul.hSMul (β := R) (n + 1) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j_1)
hi :
  coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j <
    HSMul.hSMul (β := R) (n + 1) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j)
hjeq : (↑j : WithTop Γ) = orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)
⊢ coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j ≤
    HSMul.hSMul (β := R) (n + 1) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j)

Tactic:
hi.le

Premises used: LT.lt.le
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj :
  ∀ j_1 < j,
    coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j_1 =
      HSMul.hSMul (β := R) (n + 1) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j_1)
hi :
  coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j <
    HSMul.hSMul (β := R) (n + 1) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j)
hjeq : (↑j : WithTop Γ) = orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)
h₁ : WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)) ⋯ = j
h₂ : WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)) ⋯ = j
⊢ coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)
      (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)) ⋯) ≤
    HSMul.hSMul (β := R) (n + 1)
      (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)
        (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)) ⋯))

Tactic:
convert! hi.le

Premises used: LT.lt.le
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj :
  ∀ j_1 < j,
    coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j_1 =
      HSMul.hSMul (β := R) (n + 1) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j_1)
hi :
  coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j <
    HSMul.hSMul (β := R) (n + 1) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j)
hjeq : (↑j : WithTop Γ) = orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)
⊢ WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)) ⋯ = j

Tactic:
(WithTop.untop_eq_iff _).mpr hjeq.symm

Premises used: Iff.mpr, WithTop.untop_eq_iff, Eq.symm
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj :
  ∀ j_1 < j,
    coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j_1 =
      HSMul.hSMul (β := R) (n + 1) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j_1)
hi :
  coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j <
    HSMul.hSMul (β := R) (n + 1) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j)
hjeq : (↑j : WithTop Γ) = orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)
⊢ WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)) ⋯ = j

Tactic:
exact (WithTop.untop_eq_iff _).mpr hjeq.symm

Premises used: Iff.mpr, WithTop.untop_eq_iff, Eq.symm
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj :
  ∀ j_1 < j,
    coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j_1 =
      HSMul.hSMul (β := R) (n + 1) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j_1)
hi :
  coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j <
    HSMul.hSMul (β := R) (n + 1) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j)
hjgt : orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) < (↑j : WithTop Γ)
⊢ coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)
      (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)) ⋯) ≤
    HSMul.hSMul (β := R) (n + 1)
      (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)
        (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)) ⋯))

Tactic:
(hj _ ((WithTop.untop_lt_iff _).mpr hjgt)).le

Premises used: Iff.mpr, Lex, Eq.le, WithTop.untop_lt_iff
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj :
  ∀ j_1 < j,
    coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j_1 =
      HSMul.hSMul (β := R) (n + 1) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j_1)
hi :
  coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j <
    HSMul.hSMul (β := R) (n + 1) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j)
hjgt : orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) < (↑j : WithTop Γ)
⊢ coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)
      (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)) ⋯) ≤
    HSMul.hSMul (β := R) (n + 1)
      (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)
        (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)) ⋯))

Tactic:
exact (hj _ ((WithTop.untop_lt_iff _).mpr hjgt)).le

Premises used: Iff.mpr, Eq.le, WithTop.untop_lt_iff
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn :
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)| ≤
    HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
⊢ ∃ (n : ℕ), |y| ≤ n • |x|

Tactic:
⟨n + 1, ((lt_iff _ _).mpr ?_).le⟩

Premises used: Iff.mpr, LT.lt.le, HAdd.hAdd, Exists.intro, HahnSeries.lt_iff, OfNat.ofNat
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn :
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)| ≤
    HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
inr :
  ∃ (i : Γ),
    (∀ j < i,
        Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|)) j)) ∧
      LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) i)
        (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|)) i)
⊢ ∃ (n : ℕ), |y| ≤ n • |x|

Tactic:
refine ⟨n + 1, ((lt_iff _ _).mpr ?_).le⟩
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn :
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)| ≤
    HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
⊢ Ne.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⊤

Tactic:
simpa using hx
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn :
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)| ≤
    HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
inr :
  ∀ j < WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j)
      (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|)) j)
inr₁ :
  LT.lt.{u_2} (α := R)
    (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)
      (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯))
    (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|))
      (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯))
⊢ ∃ (i : Γ),
    (∀ j < i,
        Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|)) j)) ∧
      LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) i)
        (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|)) i)

Tactic:
refine ⟨(ofLex x).orderTop.untop (by simpa using hx), ?_, ?_⟩
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn :
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)| ≤
    HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
j : Γ
hj : j < WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯
trans : Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j) 0
trans₁ : Eq.{u_2 + 1} (α := R) 0 (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|)) j)
⊢ Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j)
    (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|)) j)

Tactic:
trans 0
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn :
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)| ≤
    HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
j : Γ
hj : j < WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯
hi : (↑j : WithTop Γ) < orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)
⊢ Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j) 0

Tactic:
apply coeff_eq_zero_of_lt_orderTop

Premises used: HahnSeries.coeff_eq_zero_of_lt_orderTop
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn :
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)| ≤
    HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
j : Γ
hj : j < WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯
⊢ (↑j : WithTop Γ) < orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)

Tactic:
simpa [← h] using hj
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn :
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)| ≤
    HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
j : Γ
hj : j < WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯
this : Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j) 0
⊢ Eq.{u_2 + 1} (α := R) 0 (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|)) j)

Tactic:
simp [this]
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn :
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)| ≤
    HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
j : Γ
hj : j < WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯
suffices : Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j) 0
⊢ Eq.{u_2 + 1} (α := R) 0 (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|)) j)

Tactic:
suffices (ofLex |x|).coeff j = 0 by simp [this]
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn :
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)| ≤
    HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
j : Γ
hj : j < WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯
hi : (↑j : WithTop Γ) < orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)
⊢ Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j) 0

Tactic:
apply coeff_eq_zero_of_lt_orderTop

Premises used: HahnSeries.coeff_eq_zero_of_lt_orderTop
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn :
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)| ≤
    HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
j : Γ
hj : j < WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯
⊢ (↑j : WithTop Γ) < orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)

Tactic:
simpa using hj
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn :
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)| ≤
    HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
inr :
  coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)
      (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯) <
    HSMul.hSMul (β := R) (n + 1)
      (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)
        (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯))
⊢ LT.lt.{u_2} (α := R)
    (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)
      (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯))
    (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|))
      (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯))

Tactic:
rw [ofLex_smul, coeff_smul]

Premises used: HahnSeries.coeff_smul, ofLex_smul
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn :
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)| ≤
    HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
this :
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)| <
    HSMul.hSMul (β := R) (n + 1) |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
⊢ leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) <
    HSMul.hSMul (β := R) (n + 1) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))

Tactic:
simp_rw [← leadingCoeff_abs] at this

Premises used: HahnSeries.leadingCoeff_abs
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hy : y ≠ 0
hx : x ≠ 0
h' :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
n : ℕ
hn :
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)| ≤
    HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
this :
  leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) <
    HSMul.hSMul (β := R) (n + 1) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
⊢ Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y| : R⟦Γ⟧) (0 : R⟦Γ⟧)

Tactic:
simpa using hy