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 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ x
⊢ LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
have mpr : ∀ (h : LE.le (α := Lex R⟦Γ⟧) 0 0),
  LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0))
Tactic: obtain rfl | hlt := h.eq_or_lt
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ x
mpr :
  ∀ (h : LE.le (α := Lex R⟦Γ⟧) 0 0),
    LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0))
⊢ LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
have mpr₁ : ∀ (hlt : 0 < x), LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
Tactic: obtain rfl | hlt := h.eq_or_lt
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
inst_2 : AddCommMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
⊢ a + c ≤ b + c
have inl : ∀ (hab : a ≤ a), a + c ≤ a + c
Tactic: obtain rfl | hlt := hab.eq_or_lt
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
inst_2 : AddCommMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
inl : ∀ (hab : a ≤ a), a + c ≤ a + c
⊢ a + c ≤ b + c
have inr : ∀ (hlt : a < b), a + c ≤ b + c
Tactic: obtain rfl | hlt := hab.eq_or_lt
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
inst_2 : AddCommMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
hlt : a < b
⊢ a + c ≤ b + c
have inr : a + c < b + c
Tactic: apply le_of_lt
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
inst_2 : AddCommMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
hlt : a < b
⊢ a + c < b + c
have inr : ∀
  (hlt :
    ∃ (i : Γ),
      (∀ j < i,
          Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j)
            (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)) ∧
        LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)),
  ∃ (i : Γ),
    (∀ j < i,
        Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (a + c)) j)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (b + c)) j)) ∧
      LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (a + c)) i)
        (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (b + c)) i)
Tactic: rw [lt_iff] at hlt ⊢
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
inst_2 : AddCommMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
hlt :
  ∃ (i : Γ),
    (∀ j < i,
        Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)) ∧
      LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
⊢ ∃ (i : Γ),
    (∀ j < i,
        Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (a + c)) j)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (b + c)) j)) ∧
      LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (a + c)) i)
        (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (b + c)) i)
have inr : ∀ (i : Γ)
  (hj :
    ∀ j < i,
      Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j))
  (hi :
    LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)),
  ∃ (i : Γ),
    (∀ j < i,
        Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (a + c)) j)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (b + c)) j)) ∧
      LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (a + c)) i)
        (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (b + c)) i)
Tactic: obtain ⟨i, hj, hi⟩ := hlt
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
inst_2 : AddCommMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
⊢ ∃ (i : Γ),
    (∀ j < i,
        Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (a + c)) j)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (b + c)) j)) ∧
      LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (a + c)) i)
        (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (b + c)) i)
have inr : ∀ (j : Γ) (hji : j < i),
  Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (a + c)) j)
    (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (b + c)) j)
Tactic: refine ⟨i, fun j hji ↦ ?_, add_left_strictMono hi⟩
-- 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⟦Γ⟧
⊢ Eq.{u_1 + 1} (α := Set Γ) (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
have inl : ∀ (hle : x ≤ 0),
  Eq.{u_1 + 1} (α := Set Γ) (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
Tactic: obtain hle | hge := le_total x 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 : Lex R⟦Γ⟧
inl :
  ∀ (hle : x ≤ 0),
    Eq.{u_1 + 1} (α := Set Γ) (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
      (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
⊢ Eq.{u_1 + 1} (α := Set Γ) (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
have inr : ∀ (hge : 0 ≤ x),
  Eq.{u_1 + 1} (α := Set Γ) (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
Tactic: obtain hle | hge := le_total x 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 : Lex R⟦Γ⟧
hle : x ≤ 0
⊢ Eq.{u_1 + 1} (α := Set Γ) (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
have inl : Eq.{u_1 + 1} (α := Set Γ) (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (-x)))
  (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
Tactic: rw [abs_eq_neg_self.mpr hle]
-- 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⟦Γ⟧
hge : 0 ≤ x
⊢ Eq.{u_1 + 1} (α := Set Γ) (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
have inr : Eq.{u_1 + 1} (α := Set Γ) (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
  (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
Tactic: rw [abs_eq_self.mpr hge]
-- 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⟦Γ⟧
⊢ 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⟦Γ⟧) x))
have inl : ∀ (hle : 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⟦Γ⟧) x))
Tactic: obtain hle | hge := le_total x 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 : Lex R⟦Γ⟧
inl :
  ∀ (hle : 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⟦Γ⟧) x))
⊢ 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⟦Γ⟧) x))
have inr : ∀ (hge : 0 ≤ x),
  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⟦Γ⟧) x))
Tactic: obtain hle | hge := le_total x 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 : Lex R⟦Γ⟧
hle : 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⟦Γ⟧) x))
have inl : 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⟦Γ⟧) x))
Tactic: rw [abs_eq_neg_self.mpr hle, ofLex_neg, orderTop_neg]
-- 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⟦Γ⟧
hle : x ≤ 0
inl :
  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⟦Γ⟧) x))
⊢ 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⟦Γ⟧) x))
have inl₁ : 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⟦Γ⟧) x))
Tactic: rw [abs_eq_neg_self.mpr hle, ofLex_neg, orderTop_neg]
-- 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⟦Γ⟧
hle : x ≤ 0
inl :
  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⟦Γ⟧) x))
inl₁ :
  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⟦Γ⟧) x))
⊢ 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⟦Γ⟧) x))
have inl₂ : 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⟦Γ⟧) x))
Tactic: rw [abs_eq_neg_self.mpr hle, ofLex_neg, orderTop_neg]
-- 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⟦Γ⟧
hge : 0 ≤ x
⊢ 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⟦Γ⟧) x))
have inr : 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⟦Γ⟧) x))
Tactic: rw [abs_eq_self.mpr hge]
-- 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
inst_4 : Zero Γ
x : Lex R⟦Γ⟧
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
have inl : Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |0|))
  (order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0))
Tactic: obtain rfl | hne := eq_or_ne x 0
Cleared hypotheses: x
-- 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
inst_4 : Zero Γ
x : Lex R⟦Γ⟧
inl :
  Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |0|))
    (order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0))
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
have inr : ∀ (hne : x ≠ 0),
  Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
Tactic: obtain rfl | hne := eq_or_ne x 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
inst_4 : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
have hne' : Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)
Tactic: have hne' : ofLex x ≠ 0 := hne
-- 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
inst_4 : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
hne' : Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
have habs : Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x| : R⟦Γ⟧) (0 : R⟦Γ⟧)
Tactic: have habs : ofLex |x| ≠ 0 := by simpa using hne
-- 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
inst_4 : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
hne' : Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)
habs : Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x| : R⟦Γ⟧) (0 : R⟦Γ⟧)
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|))
    (order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
have inr : Eq.{u_1 + 1} (α := WithTop Γ) (↑(order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)) : WithTop Γ)
  (↑(order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) : WithTop Γ)
Tactic: apply WithTop.coe_injective
-- 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
inst_4 : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
hne' : Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)
habs : Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x| : R⟦Γ⟧) (0 : R⟦Γ⟧)
⊢ Eq.{u_1 + 1} (α := WithTop Γ) (↑(order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |x|)) : WithTop Γ)
    (↑(order.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) : WithTop Γ)
have inr : 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⟦Γ⟧) x))
Tactic: rw [order_eq_orderTop_of_ne_zero habs, order_eq_orderTop_of_ne_zero hne']
-- 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⟦Γ⟧
⊢ 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 inl : ∀ (hlt : x < 0),
  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: obtain hlt | rfl | hgt := lt_trichotomy x 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 : Lex R⟦Γ⟧
inl :
  ∀ (hlt : x < 0),
    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⟦Γ⟧) |0|))
  |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0)|
Tactic: obtain hlt | rfl | hgt := lt_trichotomy x 0
Cleared hypotheses: x
-- 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⟦Γ⟧
inl :
  ∀ (hlt : x < 0),
    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)|
inr :
  Eq.{u_2 + 1} (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) |0|))
    |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0)|
⊢ 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₁ : ∀ (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)|
Tactic: obtain hlt | rfl | hgt := lt_trichotomy x 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 : Lex R⟦Γ⟧
hlt : x < 0
⊢ 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 hlt' : LT.lt.{u_2} (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) 0
Tactic: obtain hlt' := leadingCoeff_neg_iff.mpr hlt
-- 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⟦Γ⟧
hlt : x < 0
hlt' : LT.lt.{u_2} (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) 0
⊢ 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 inl : 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_neg_self.mpr hlt.le, abs_eq_neg_self.mpr hlt'.le, ofLex_neg, leadingCoeff_neg]
-- 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⟦Γ⟧
hlt : x < 0
hlt' : LT.lt.{u_2} (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) 0
inl :
  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 inl₁ : 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_neg_self.mpr hlt.le, abs_eq_neg_self.mpr hlt'.le, ofLex_neg, leadingCoeff_neg]
-- 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⟦Γ⟧
hlt : x < 0
hlt' : LT.lt.{u_2} (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) 0
inl :
  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)|
inl₁ :
  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 inl₂ : 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_neg_self.mpr hlt.le, abs_eq_neg_self.mpr hlt'.le, ofLex_neg, leadingCoeff_neg]
-- 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⟦Γ⟧
hlt : x < 0
hlt' : LT.lt.{u_2} (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) 0
inl :
  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)|
inl₁ :
  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))
inl₂ :
  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 inl₃ : 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_neg_self.mpr hlt.le, abs_eq_neg_self.mpr hlt'.le, ofLex_neg, leadingCoeff_neg]