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
a_1 b_1 : Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))
x : Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)
ao : Γ
x_1 : Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)
bo : Γ
a : R
ha : a ≠ 0
b : R
hb : b ≠ 0
h_1 :
  LE.le (α := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
        (ao, FiniteArchimedeanClass.mk a ha) :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
        (bo, FiniteArchimedeanClass.mk b hb) :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
h :
  LT.lt.{u_1} (α := Γ)
    ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
        ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
          (ao, FiniteArchimedeanClass.mk a ha))).1
    ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
        ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
          (bo, FiniteArchimedeanClass.mk b hb))).1
⊢ LE.le (α := FiniteArchimedeanClass (Lex R⟦Γ⟧))
    (FiniteArchimedeanClass.mk ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧) ((single ao : (a : R) → R⟦Γ⟧) a)) ⋯ :
      FiniteArchimedeanClass (Lex R⟦Γ⟧))
    (FiniteArchimedeanClass.mk ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧) ((single bo : (a : R) → R⟦Γ⟧) b)) ⋯ :
      FiniteArchimedeanClass (Lex R⟦Γ⟧))
have inl : LT.lt.{u_1} (α := WithTop Γ)
    (orderTop.{u_1, u_2} (R := R)
      ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧) ((single ao : (a : R) → R⟦Γ⟧) a))))
    (orderTop.{u_1, u_2} (R := R)
      ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧) ((single bo : (a : R) → R⟦Γ⟧) b)))) ∨
  Eq.{u_1 + 1} (α := WithTop Γ)
      (orderTop.{u_1, u_2} (R := R)
        ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧) ((single ao : (a : R) → R⟦Γ⟧) a))))
      (orderTop.{u_1, u_2} (R := R)
        ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧) ((single bo : (a : R) → R⟦Γ⟧) b)))) ∧
    LE.le.{u_2} (α := ArchimedeanClass R)
      (ArchimedeanClass.mk
        (leadingCoeff.{u_1, u_2} (Γ := Γ)
          ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧) ((single ao : (a : R) → R⟦Γ⟧) a)))))
      (ArchimedeanClass.mk
        (leadingCoeff.{u_1, u_2} (Γ := Γ)
          ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧) ((single bo : (a : R) → R⟦Γ⟧) b)))))
Tactic: rw [FiniteArchimedeanClass.mk_le_mk, archimedeanClassMk_le_archimedeanClassMk_iff]
-- 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
⊢ FiniteArchimedeanClass (Lex R⟦Γ⟧) ≃o Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))
have h₁ : Eq (α := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)) →o Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
  (OrderHom.comp (finiteArchimedeanClassOrderHomLex Γ R) (finiteArchimedeanClassOrderHomInvLex Γ R)) OrderHom.id
Tactic: apply OrderIso.ofHomInv (finiteArchimedeanClassOrderHomLex Γ R)
    (finiteArchimedeanClassOrderHomInvLex Γ R)
-- 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
h₁ :
  Eq (α := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)) →o Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    (OrderHom.comp (finiteArchimedeanClassOrderHomLex Γ R) (finiteArchimedeanClassOrderHomInvLex Γ R)) OrderHom.id
⊢ FiniteArchimedeanClass (Lex R⟦Γ⟧) ≃o Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))
have h₂ : Eq (α := FiniteArchimedeanClass (Lex R⟦Γ⟧) →o FiniteArchimedeanClass (Lex R⟦Γ⟧))
  (OrderHom.comp (β := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))) (finiteArchimedeanClassOrderHomInvLex Γ R)
      (finiteArchimedeanClassOrderHomLex Γ R) :
    FiniteArchimedeanClass (Lex R⟦Γ⟧) →o FiniteArchimedeanClass (Lex R⟦Γ⟧))
  (OrderHom.id : FiniteArchimedeanClass (Lex R⟦Γ⟧) →o FiniteArchimedeanClass (Lex R⟦Γ⟧))
Tactic: apply OrderIso.ofHomInv (finiteArchimedeanClassOrderHomLex Γ R)
    (finiteArchimedeanClassOrderHomInvLex Γ R)
-- 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
⊢ Eq (α := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)) →o Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    (OrderHom.comp (finiteArchimedeanClassOrderHomLex Γ R) (finiteArchimedeanClassOrderHomInvLex Γ R)) OrderHom.id
have h₁ : ∀ (x : Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))),
  Eq (α := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((OrderHom.comp (finiteArchimedeanClassOrderHomLex Γ R) (finiteArchimedeanClassOrderHomInvLex Γ R) :
          (a : Lex (Γ × FiniteArchimedeanClass R)) → Lex (Γ × FiniteArchimedeanClass R))
        x :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((OrderHom.id : (a : Lex (Γ × FiniteArchimedeanClass R)) → Lex (Γ × FiniteArchimedeanClass R)) x :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
Tactic: ext 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 (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))
⊢ Eq (α := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((OrderHom.comp (finiteArchimedeanClassOrderHomLex Γ R) (finiteArchimedeanClassOrderHomInvLex Γ R) :
          (a : Lex (Γ × FiniteArchimedeanClass R)) → Lex (Γ × FiniteArchimedeanClass R))
        x :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((OrderHom.id : (a : Lex (Γ × FiniteArchimedeanClass R)) → Lex (Γ × FiniteArchimedeanClass R)) x :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
have h₁ : ∀ (x : Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)),
  Eq (α := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((OrderHom.comp (finiteArchimedeanClassOrderHomLex Γ R) (finiteArchimedeanClassOrderHomInvLex Γ R) :
          (a : Lex (Γ × FiniteArchimedeanClass R)) → Lex (Γ × FiniteArchimedeanClass R))
        ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) x) :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((OrderHom.id : (a : Lex (Γ × FiniteArchimedeanClass R)) → Lex (Γ × FiniteArchimedeanClass R))
        ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) x) :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
Tactic: cases x with | h x
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 : Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)
⊢ Eq (α := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((OrderHom.comp (finiteArchimedeanClassOrderHomLex Γ R) (finiteArchimedeanClassOrderHomInvLex Γ R) :
          (a : Lex (Γ × FiniteArchimedeanClass R)) → Lex (Γ × FiniteArchimedeanClass R))
        ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) x) :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((OrderHom.id : (a : Lex (Γ × FiniteArchimedeanClass R)) → Lex (Γ × FiniteArchimedeanClass R))
        ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) x) :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
have h₁ : ∀ (order : Γ) (coeff : FiniteArchimedeanClass R),
  Eq (α := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((OrderHom.comp (finiteArchimedeanClassOrderHomLex Γ R) (finiteArchimedeanClassOrderHomInvLex Γ R) :
          (a : Lex (Γ × FiniteArchimedeanClass R)) → Lex (Γ × FiniteArchimedeanClass R))
        ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (order, coeff)) :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((OrderHom.id : (a : Lex (Γ × FiniteArchimedeanClass R)) → Lex (Γ × FiniteArchimedeanClass R))
        ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (order, coeff)) :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
Tactic: obtain ⟨order, coeff⟩ := x
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
order : Γ
coeff : FiniteArchimedeanClass R
⊢ Eq (α := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((OrderHom.comp (finiteArchimedeanClassOrderHomLex Γ R) (finiteArchimedeanClassOrderHomInvLex Γ R) :
          (a : Lex (Γ × FiniteArchimedeanClass R)) → Lex (Γ × FiniteArchimedeanClass R))
        ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (order, coeff)) :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((OrderHom.id : (a : Lex (Γ × FiniteArchimedeanClass R)) → Lex (Γ × FiniteArchimedeanClass R))
        ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R)) (order, coeff)) :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
have h₁ : ∀ (a : R) (ha : a ≠ 0),
  Eq (α := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((OrderHom.comp (finiteArchimedeanClassOrderHomLex Γ R) (finiteArchimedeanClassOrderHomInvLex Γ R) :
          (a : Lex (Γ × FiniteArchimedeanClass R)) → Lex (Γ × FiniteArchimedeanClass R))
        ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
          (order, FiniteArchimedeanClass.mk a ha)) :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
    ((OrderHom.id : (a : Lex (Γ × FiniteArchimedeanClass R)) → Lex (Γ × FiniteArchimedeanClass R))
        ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
          (order, FiniteArchimedeanClass.mk a ha)) :
      Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
Tactic: induction coeff using FiniteArchimedeanClass.ind with | mk a ha
Cleared hypotheses: coeff
-- 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
⊢ Eq (α := FiniteArchimedeanClass (Lex R⟦Γ⟧) →o FiniteArchimedeanClass (Lex R⟦Γ⟧))
    (OrderHom.comp (β := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))) (finiteArchimedeanClassOrderHomInvLex Γ R)
        (finiteArchimedeanClassOrderHomLex Γ R) :
      FiniteArchimedeanClass (Lex R⟦Γ⟧) →o FiniteArchimedeanClass (Lex R⟦Γ⟧))
    (OrderHom.id : FiniteArchimedeanClass (Lex R⟦Γ⟧) →o FiniteArchimedeanClass (Lex R⟦Γ⟧))
have h₂ : ∀ (x : FiniteArchimedeanClass (Lex R⟦Γ⟧)),
  Eq (α := ArchimedeanClass (Lex R⟦Γ⟧))
    (↑(((OrderHom.comp (β := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
                (finiteArchimedeanClassOrderHomInvLex Γ R) (finiteArchimedeanClassOrderHomLex Γ R) :
              FiniteArchimedeanClass (Lex R⟦Γ⟧) →o FiniteArchimedeanClass (Lex R⟦Γ⟧)) :
            (a : FiniteArchimedeanClass (Lex R⟦Γ⟧)) → FiniteArchimedeanClass (Lex R⟦Γ⟧))
          x) :
      ArchimedeanClass (Lex R⟦Γ⟧))
    (↑((OrderHom.id : (a : FiniteArchimedeanClass (Lex R⟦Γ⟧)) → FiniteArchimedeanClass (Lex R⟦Γ⟧)) x) :
      ArchimedeanClass (Lex R⟦Γ⟧))
Tactic: ext 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 : FiniteArchimedeanClass (Lex R⟦Γ⟧)
⊢ Eq (α := ArchimedeanClass (Lex R⟦Γ⟧))
    (↑(((OrderHom.comp (β := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
                (finiteArchimedeanClassOrderHomInvLex Γ R) (finiteArchimedeanClassOrderHomLex Γ R) :
              FiniteArchimedeanClass (Lex R⟦Γ⟧) →o FiniteArchimedeanClass (Lex R⟦Γ⟧)) :
            (a : FiniteArchimedeanClass (Lex R⟦Γ⟧)) → FiniteArchimedeanClass (Lex R⟦Γ⟧))
          x) :
      ArchimedeanClass (Lex R⟦Γ⟧))
    (↑((OrderHom.id : (a : FiniteArchimedeanClass (Lex R⟦Γ⟧)) → FiniteArchimedeanClass (Lex R⟦Γ⟧)) x) :
      ArchimedeanClass (Lex R⟦Γ⟧))
have h₂ : ∀ (a : Lex R⟦Γ⟧) (ha : a ≠ 0),
  Eq (α := ArchimedeanClass (Lex R⟦Γ⟧))
    (↑(((OrderHom.comp (β := Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)))
                (finiteArchimedeanClassOrderHomInvLex Γ R) (finiteArchimedeanClassOrderHomLex Γ R) :
              FiniteArchimedeanClass (Lex R⟦Γ⟧) →o FiniteArchimedeanClass (Lex R⟦Γ⟧)) :
            (a : FiniteArchimedeanClass (Lex R⟦Γ⟧)) → FiniteArchimedeanClass (Lex R⟦Γ⟧))
          (FiniteArchimedeanClass.mk a ha)) :
      ArchimedeanClass (Lex R⟦Γ⟧))
    (↑((OrderHom.id : (a : FiniteArchimedeanClass (Lex R⟦Γ⟧)) → FiniteArchimedeanClass (Lex R⟦Γ⟧))
          (FiniteArchimedeanClass.mk a ha)) :
      ArchimedeanClass (Lex R⟦Γ⟧))
Tactic: induction x using FiniteArchimedeanClass.ind with | mk a ha
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 : Archimedean R
inst_5 : Nontrivial R
x : Lex R⟦Γ⟧
⊢ Eq.{u_1 + 1} (α := WithTop Γ)
    (((OrderIso.trans (OrderIso.symm (FiniteArchimedeanClass.withTopOrderIso (Lex R⟦Γ⟧)))
              (OrderIso.withTopCongr (finiteArchimedeanClassOrderIso Γ R)) :
            ArchimedeanClass (Lex R⟦Γ⟧) ≃o WithTop Γ) :
          (a : ArchimedeanClass (Lex R⟦Γ⟧)) → WithTop Γ)
        (ArchimedeanClass.mk x) :
      WithTop Γ)
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) : WithTop Γ)
have inl : Eq.{u_1 + 1} (α := WithTop Γ)
  (((OrderIso.trans (OrderIso.symm (FiniteArchimedeanClass.withTopOrderIso (Lex R⟦Γ⟧)))
            (OrderIso.withTopCongr (finiteArchimedeanClassOrderIso Γ R)) :
          ArchimedeanClass (Lex R⟦Γ⟧) ≃o WithTop Γ) :
        (a : ArchimedeanClass (Lex R⟦Γ⟧)) → WithTop Γ)
      (ArchimedeanClass.mk 0) :
    WithTop Γ)
  (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) : WithTop Γ)
Tactic: obtain rfl | h := 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 : Archimedean R
inst_5 : Nontrivial R
x : Lex R⟦Γ⟧
inl :
  Eq.{u_1 + 1} (α := WithTop Γ)
    (((OrderIso.trans (OrderIso.symm (FiniteArchimedeanClass.withTopOrderIso (Lex R⟦Γ⟧)))
              (OrderIso.withTopCongr (finiteArchimedeanClassOrderIso Γ R)) :
            ArchimedeanClass (Lex R⟦Γ⟧) ≃o WithTop Γ) :
          (a : ArchimedeanClass (Lex R⟦Γ⟧)) → WithTop Γ)
        (ArchimedeanClass.mk 0) :
      WithTop Γ)
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) : WithTop Γ)
⊢ Eq.{u_1 + 1} (α := WithTop Γ)
    (((OrderIso.trans (OrderIso.symm (FiniteArchimedeanClass.withTopOrderIso (Lex R⟦Γ⟧)))
              (OrderIso.withTopCongr (finiteArchimedeanClassOrderIso Γ R)) :
            ArchimedeanClass (Lex R⟦Γ⟧) ≃o WithTop Γ) :
          (a : ArchimedeanClass (Lex R⟦Γ⟧)) → WithTop Γ)
        (ArchimedeanClass.mk x) :
      WithTop Γ)
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) : WithTop Γ)
have inr : ∀ (h : x ≠ 0),
  Eq.{u_1 + 1} (α := WithTop Γ)
    (((OrderIso.trans (OrderIso.symm (FiniteArchimedeanClass.withTopOrderIso (Lex R⟦Γ⟧)))
              (OrderIso.withTopCongr (finiteArchimedeanClassOrderIso Γ R)) :
            ArchimedeanClass (Lex R⟦Γ⟧) ≃o WithTop Γ) :
          (a : ArchimedeanClass (Lex R⟦Γ⟧)) → WithTop Γ)
        (ArchimedeanClass.mk x) :
      WithTop Γ)
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) : WithTop Γ)
Tactic: obtain rfl | h := eq_or_ne 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 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : b ≤ c
⊢ a * b ≤ a * c
have rw : ∀ (hbc : 0 ≤ c - b), 0 ≤ a * c - a * b
Tactic: rw [← sub_nonneg] at hbc ⊢
Cleared hypotheses: hbc
-- 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 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
⊢ 0 ≤ a * c - a * b
have rw : 0 ≤
  HMul.hMul (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
    (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))
Tactic: rw [← mul_sub, ← leadingCoeff_nonneg_iff, ofLex_mul, leadingCoeff_mul]
-- 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 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
⊢ 0 ≤
    HMul.hMul (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
      (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))
have ha₁ : LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
Tactic: apply mul_nonneg
-- 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 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
ha₁ : LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
⊢ 0 ≤
    HMul.hMul (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
      (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))
have hb : LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))
Tactic: apply mul_nonneg
-- 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 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : b ≤ c
⊢ b * a ≤ c * a
have rw : ∀ (hbc : 0 ≤ c - b), 0 ≤ c * a - b * a
Tactic: rw [← sub_nonneg] at hbc ⊢
Cleared hypotheses: hbc
-- 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 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
⊢ 0 ≤ c * a - b * a
have rw : 0 ≤
  HMul.hMul (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))
    (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
Tactic: rw [← sub_mul, ← leadingCoeff_nonneg_iff, ofLex_mul, leadingCoeff_mul]
-- 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 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
⊢ 0 ≤
    HMul.hMul (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))
      (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
have ha₁ : LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))
Tactic: apply mul_nonneg
-- 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 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
ha₁ : LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))
⊢ 0 ≤
    HMul.hMul (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))
      (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
have hb : LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
Tactic: apply mul_nonneg
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
⊢ (∃ (i : Γ'),
        (∀ j < i,
            Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
              (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)) ∧
          LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
            (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)) ∨
      Eq (α := R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
        (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ↔
    (∃ (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)) ∨
      a = b
have mp : (∃ (i : Γ'),
      (∀ j < i,
          Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
            (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)) ∧
        LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
          (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)) ∨
    Eq (α := R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
      (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) →
  (∃ (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)) ∨
    a = b
Tactic: constructor