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))
simp_rw :
  (∃ (n : ℕ), |y| ≤ n • |x|) ↔
    ∃ (n : ℕ),
      |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)|
⊢ LE.le (α := ArchimedeanClass (Lex R⟦Γ⟧)) (ArchimedeanClass.mk x) (ArchimedeanClass.mk y) ↔
    LE.le.{u_2} (α := ArchimedeanClass R)
      (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))
      (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))

Tactic:
simp_rw [ArchimedeanClass.mk_le_mk]

Premises used: ArchimedeanClass.mk_le_mk
-- 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))
inl :
  ∀
    (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⟦Γ⟧) 0))),
    (∃ (n : ℕ), |0| ≤ n • |x|) ↔
      ∃ (n : ℕ),
        |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0)| ≤
          HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
inr :
  ∀ (hy : y ≠ 0),
    (∃ (n : ℕ), |y| ≤ n • |x|) ↔
      ∃ (n : ℕ),
        |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|) ↔
    ∃ (n : ℕ),
      |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)|

Tactic:
obtain rfl | hy := eq_or_ne y 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- 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 : 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⟦Γ⟧) 0))
⊢ (∃ (n : ℕ), |0| ≤ n • |x|) ↔
    ∃ (n : ℕ),
      |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0)| ≤
        HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|

Tactic:
simp_all
-- 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
⊢ Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y : R⟦Γ⟧) (0 : R⟦Γ⟧)

Tactic:
simpa using hy
-- 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
⊢ x ≠ 0

Tactic:
simpa using orderTop_ne_top.1 <| h ▸ orderTop_ne_top.2 (by simpa using hy)

Premises used: HahnSeries.orderTop_ne_top, Iff.mp
-- 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
⊢ x ≠ 0

Tactic:
have hx : x ≠ 0 := by simpa using orderTop_ne_top.1 <| h ▸ orderTop_ne_top.2 (by simpa using hy)
-- 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
⊢ 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|))

Tactic:
simpa using h
-- 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
⊢ 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|))

Tactic:
have h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop := by simpa using h
-- 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|))
inr :
  (∃ (n : ℕ), |y| ≤ n • |x|) →
    ∃ (n : ℕ),
      |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₁ :
  (∃ (n : ℕ),
      |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|
⊢ (∃ (n : ℕ), |y| ≤ n • |x|) ↔
    ∃ (n : ℕ),
      |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)|

Tactic:
constructor
-- 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|
⊢ ∃ (n : ℕ),
    |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)|

Tactic:
⟨n + 1, ?_⟩

Premises used: HAdd.hAdd, Exists.intro, 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 : |y| ≤ n • |x|
inr :
  |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)|
⊢ ∃ (n : ℕ),
    |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)|

Tactic:
refine ⟨n + 1, ?_⟩
-- 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|
⊢ 0 < |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 : |y| ≤ n • |x|
⊢ n < n + 1

Tactic:
simp
-- 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|
⊢ |y| < (n + 1) • |x|

Tactic:
have hn' : |y| < (n + 1) • |x| :=
      lt_of_le_of_lt hn <| nsmul_lt_nsmul_left (by simpa using hx) (by simp)
-- 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|
inr :
  ∀ (j : Γ)
    (hj :
      ∀ j_1 < j,
        Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j_1)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|)) j_1))
    (hi :
      LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j)
        (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|)) j)),
    |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:
obtain ⟨j, hj, hi⟩ := (lt_iff _ _).mp hn'

Premises used: Iff.mp, HahnSeries.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)
inr :
  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]

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 : |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)
⊢ Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y| : R⟦Γ⟧) (0 : R⟦Γ⟧)

Tactic:
simpa using hy
-- 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)
⊢ Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x| : R⟦Γ⟧) (0 : R⟦Γ⟧)

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 : |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)
inr :
  coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)
      (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)) ⋯) ≤
    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|)) ⋯))
⊢ 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:
rw [leadingCoeff_of_ne_zero (by simpa using hy), leadingCoeff_of_ne_zero (by simpa using hx)]

Premises used: HahnSeries.leadingCoeff_of_ne_zero
-- 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)
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|)) ⋯))
⊢ coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)
      (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)) ⋯) ≤
    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:
simp_rw [← h']
-- 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)
inr :
  ∀ (hjlt : (↑j : WithTop Γ) < orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)),
    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|)) ⋯))
inr₁ :
  ∀ (hjeq : (↑j : WithTop Γ) = orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)),
    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|)) ⋯))
inr₂ :
  ∀ (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|)) ⋯))
⊢ 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:
obtain hjlt | hjeq | hjgt := lt_trichotomy (WithTop.some j) (ofLex |x|).orderTop

Premises used: abs, HahnSeries.orderTop, WithTop.some, ofLex, DFunLike.coe, lt_trichotomy
-- 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)
hjlt : (↑j : WithTop Γ) < 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:
have hjlt' : j < (ofLex |y|).orderTop := h'.symm ▸ hjlt
-- 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)
hjlt : (↑j : WithTop Γ) < orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)
hjlt' : (↑j : WithTop Γ) < orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)
⊢ 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:
simp [coeff_eq_zero_of_lt_orderTop hjlt, coeff_eq_zero_of_lt_orderTop hjlt'] at hi

Premises used: HahnSeries.coeff_eq_zero_of_lt_orderTop