awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
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|)) ⋯))
⊢ 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|)) ⋯))
have 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|)) sorry) ≤
    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|)) sorry))
Tactic: obtain hjlt | hjeq | hjgt := lt_trichotomy (WithTop.some j) (ofLex |x|).orderTop
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (hypothesis)
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|)
⊢ 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|)) ⋯))
have hjlt' : (↑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
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
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|)
      (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|)) ⋯))
have h₁ : WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)) sorry = j
Tactic: convert! hi.le
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
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|
have 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)
Tactic: refine ⟨n + 1, ((lt_iff _ _).mpr ?_).le⟩
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
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)|
⊢ ∃ (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)
have inr : ∀ j < WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) sorry,
  Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j)
    (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|)) j)
Tactic: refine ⟨(ofLex x).orderTop.untop (by simpa using hx), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
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)
⊢ ∃ (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)
have 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)) sorry))
  (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|))
    (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) sorry))
Tactic: refine ⟨(ofLex x).orderTop.untop (by simpa using hx), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
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)) ⋯
⊢ Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j)
    (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|)) j)
have trans : Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j) 0
Tactic: trans 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
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
⊢ Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j)
    (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|)) j)
have trans₁ : Eq.{u_2 + 1} (α := R) 0 (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|)) j)
Tactic: trans 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
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)) ⋯
⊢ Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j) 0
have hi : (↑j : WithTop Γ) < orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)
Tactic: apply coeff_eq_zero_of_lt_orderTop
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
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)) ⋯
⊢ Eq.{u_2 + 1} (α := R) 0 (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((n + 1) • |x|)) j)
have suffices : Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j) 0
Tactic: suffices (ofLex |x|).coeff j = 0 by simp [this]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
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)) ⋯
⊢ Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j) 0
have hi : (↑j : WithTop Γ) < orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)
Tactic: apply coeff_eq_zero_of_lt_orderTop
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
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)|
⊢ 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)) ⋯))
have inr : coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)
    (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) sorry) <
  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)) sorry))
Tactic: rw [ofLex_smul, coeff_smul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (hypothesis)
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)|
⊢ 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)) ⋯))
have 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|))
Tactic: simp_rw [← leadingCoeff_abs] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (hypothesis)
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|))
⊢ 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)) ⋯))
have this₁ : coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)
    (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)) sorry) <
  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|)) sorry))
Tactic: rw [leadingCoeff_of_ne_zero (by simpa using hy), leadingCoeff_of_ne_zero (by simpa using hx)]
        at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
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 :
  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|)) ⋯))
⊢ 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)) ⋯))
have 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|))
Tactic: convert! this using 3
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
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 :
  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|)) ⋯))
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|))
⊢ 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)) ⋯))
have h₂ : WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) sorry =
  WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)) sorry
Tactic: convert! this using 3