awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
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
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)))))
⊢ 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⟦Γ⟧))

Tactic:
rw [FiniteArchimedeanClass.mk_le_mk, archimedeanClassMk_le_archimedeanClassMk_iff]

Premises used: FiniteArchimedeanClass.mk_le_mk, HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
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
⊢ 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))))

Tactic:
simpa [ha, hb] using h
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
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
⊢ 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:
exact .inl (by simpa [ha, hb] using h)
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
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
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⟦Γ⟧))
⊢ FiniteArchimedeanClass (Lex R⟦Γ⟧) ≃o Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))

Tactic:
apply OrderIso.ofHomInv (finiteArchimedeanClassOrderHomLex Γ R)
    (finiteArchimedeanClassOrderHomInvLex Γ R)

Premises used: HahnSeries.finiteArchimedeanClassOrderHomInvLex, HahnSeries.finiteArchimedeanClassOrderHomLex, OrderIso.ofHomInv
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
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)))
⊢ 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:
ext x
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x : Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))
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)))
⊢ 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:
cases x with | h x
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x : Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R)
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)))
⊢ 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:
obtain ⟨order, coeff⟩ := x

Premises used: HahnSeries.order, HahnSeries.coeff
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
order : Γ
coeff : FiniteArchimedeanClass R
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)))
⊢ 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:
induction coeff using FiniteArchimedeanClass.ind with | mk a ha

Premises used: HahnSeries.mk
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
order : Γ
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:
simp [finiteArchimedeanClassOrderHomLex, finiteArchimedeanClassOrderHomInvLex, ha]

Premises used: HahnSeries.finiteArchimedeanClassOrderHomInvLex, HahnSeries.finiteArchimedeanClassOrderHomLex
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
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⟦Γ⟧))
⊢ 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:
ext x
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x : FiniteArchimedeanClass (Lex R⟦Γ⟧)
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⟦Γ⟧))
⊢ 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:
induction x using FiniteArchimedeanClass.ind with | mk a ha

Premises used: HahnSeries.mk
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
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:
simp [finiteArchimedeanClassOrderHomLex, finiteArchimedeanClassOrderHomInvLex,
      archimedeanClassMk_eq_archimedeanClassMk_iff, ha]

Premises used: HahnSeries.finiteArchimedeanClassOrderHomInvLex, HahnSeries.archimedeanClassMk_eq_archimedeanClassMk_iff, HahnSeries.finiteArchimedeanClassOrderHomLex
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
h : x ≠ 0
⊢ Eq.{u_1 + 1} (α := WithTop Γ)
    (↑((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
            ((finiteArchimedeanClassOrderIsoLex Γ R :
                (a : FiniteArchimedeanClass (Lex R⟦Γ⟧)) → Lex (Γ × FiniteArchimedeanClass R))
              (FiniteArchimedeanClass.mk x h))).1 :
      WithTop Γ)
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))

Tactic:
simp [finiteArchimedeanClassOrderIsoLex, finiteArchimedeanClassOrderHomLex]

Premises used: HahnSeries.finiteArchimedeanClassOrderHomLex, HahnSeries.finiteArchimedeanClassOrderIsoLex
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
h : x ≠ 0
⊢ Eq.{u_2 + 1} (α := ArchimedeanClass R)
    (↑((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
            ((finiteArchimedeanClassOrderIsoLex Γ R :
                (a : FiniteArchimedeanClass (Lex R⟦Γ⟧)) → Lex (Γ × FiniteArchimedeanClass R))
              (FiniteArchimedeanClass.mk x h))).2 :
      ArchimedeanClass R)
    (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))

Tactic:
simp [finiteArchimedeanClassOrderIsoLex, finiteArchimedeanClassOrderHomLex]

Premises used: HahnSeries.finiteArchimedeanClassOrderHomLex, HahnSeries.finiteArchimedeanClassOrderIsoLex
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
inst_4 : Archimedean R
inst_5 : Nontrivial R
x : Lex R⟦Γ⟧
h : x ≠ 0
⊢ Eq.{u_1 + 1} (α := WithTop Γ)
    ((↑(((finiteArchimedeanClassOrderIso Γ R : FiniteArchimedeanClass (Lex R⟦Γ⟧) ≃o Γ) :
              (a : FiniteArchimedeanClass (Lex R⟦Γ⟧)) → Γ)
            (FiniteArchimedeanClass.mk x h)) :
        WithTop Γ) :
      WithTop Γ)
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) : WithTop Γ)

Tactic:
simp [finiteArchimedeanClassOrderIso]

Premises used: HahnSeries.finiteArchimedeanClassOrderIso
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
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 Γ)
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 Γ)
⊢ 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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
inst_4 : Archimedean R
inst_5 : Nontrivial 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 0) :
      WithTop Γ)
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) : WithTop Γ)

Tactic:
simp [FiniteArchimedeanClass.withTopOrderIso_symm_apply, *]

Premises used: FiniteArchimedeanClass.withTopOrderIso_symm_apply