awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Lex R⟦Γ⟧
hgt : 0 < x
⊢ Eq.{u_2 + 1} (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
have hgt' : LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
Tactic: obtain hgt' := leadingCoeff_pos_iff.mpr hgt
-- 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 : Lex R⟦Γ⟧
hgt : 0 < x
hgt' : LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
⊢ Eq.{u_2 + 1} (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
have inr : Eq.{u_2 + 1} (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
Tactic: rw [abs_eq_self.mpr hgt.le, abs_eq_self.mpr hgt'.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 : Lex R⟦Γ⟧
hgt : 0 < x
hgt' : LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
inr :
  Eq.{u_2 + 1} (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
⊢ Eq.{u_2 + 1} (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)|
have inr₁ : Eq.{u_2 + 1} (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
  (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
Tactic: rw [abs_eq_self.mpr hgt.le, abs_eq_self.mpr hgt'.le]
-- 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 :
  LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
⊢ |x| < |y|
have h₁ : LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
  (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
Tactic: rw [← orderTop_abs x, ← orderTop_abs y] at h
Cleared hypotheses: h
-- 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 :
  LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
⊢ |x| < |y|
have refine_1 : ∀ j < WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)) sorry,
  Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j)
Tactic: refine (lt_iff _ _).mpr ⟨(ofLex |y|).orderTop.untop h.ne_top, ?_, ?_⟩
-- 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 :
  LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
refine_1 :
  ∀ j < WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)) ⋯,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|) j)
      (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|) j)
⊢ |x| < |y|
have refine_2 : LT.lt.{u_2} (α := R)
  (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)
    (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)) sorry))
  (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)
    (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |y|)) sorry))
Tactic: refine (lt_iff _ _).mpr ⟨(ofLex |y|).orderTop.untop h.ne_top, ?_, ?_⟩
-- 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))
⊢ 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)))
have 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)|
Tactic: simp_rw [ArchimedeanClass.mk_le_mk]
-- 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))
⊢ (∃ (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)|
have 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)|
Tactic: obtain rfl | hy := eq_or_ne y 0
Cleared hypotheses: y, h
-- 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))
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)|
⊢ (∃ (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)|
have 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)|
Tactic: obtain rfl | hy := eq_or_ne y 0
-- 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
⊢ (∃ (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)|
have hx : x ≠ 0
Tactic: have hx : x ≠ 0 := by simpa using orderTop_ne_top.1 <| h ▸ orderTop_ne_top.2 (by simpa using hy)
-- 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
⊢ (∃ (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)|
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: have h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop := by simpa using h
-- 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 : ℕ), |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)|
have 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)|
Tactic: constructor
-- 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|))
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)|
⊢ (∃ (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)|
have 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|
Tactic: constructor
-- 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|
⊢ ∃ (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)|
have 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)|
Tactic: refine ⟨n + 1, ?_⟩
-- 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|
⊢ |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)|
have hn' : |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)
-- 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|
⊢ |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)|
have 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)|
Tactic: obtain ⟨j, hj, hi⟩ := (lt_iff _ _).mp hn'
-- 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)
⊢ |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)|
have 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|))
Tactic: simp_rw [← leadingCoeff_abs]
-- 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)
⊢ 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|))
have inr : 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)]
-- 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)
⊢ 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|)) ⋯))
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: simp_rw [← h']
-- 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)
⊢ 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 : ∀ (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|)) 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 (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|)) ⋯))
⊢ 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₁ : ∀ (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|)) 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