-- 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 x_1 : { a : Lex R⟦Γ⟧ // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h :
  LE.le (α := FiniteArchimedeanClass (Lex R⟦Γ⟧))
    (FiniteArchimedeanClass.mk (↑(Subtype.mk (p := fun (a : Lex R⟦Γ⟧) ↦ a ≠ 0) a ha) : Lex R⟦Γ⟧) ⋯)
    (FiniteArchimedeanClass.mk (↑(Subtype.mk (p := fun (a : Lex R⟦Γ⟧) ↦ a ≠ 0) b hb) : Lex R⟦Γ⟧) ⋯)
simp :
  WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ⋯ <
      WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ⋯ ∨
    WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ⋯ =
        WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ⋯ ∧
      LE.le (α := FiniteArchimedeanClass R)
        (FiniteArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ⋯)
        (FiniteArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ⋯)
⊢ LT.lt.{u_1} (α := Γ)
      ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
          ((fun (x : { a : Lex R⟦Γ⟧ // a ≠ 0 }) ↦
              (match (motive := { a : Lex R⟦Γ⟧ // a ≠ 0 } → Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))) x with
                | ⟨x, hx⟩ =>
                  (toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
                    (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯,
                      FiniteArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
                        ⋯) :
                Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))))
            (Subtype.mk (p := fun (a : Lex R⟦Γ⟧) ↦ a ≠ 0) a ha))).1
      ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
          ((fun (x : { a : Lex R⟦Γ⟧ // a ≠ 0 }) ↦
              (match (motive := { a : Lex R⟦Γ⟧ // a ≠ 0 } → Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))) x with
                | ⟨x, hx⟩ =>
                  (toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
                    (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯,
                      FiniteArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
                        ⋯) :
                Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))))
            (Subtype.mk (p := fun (a : Lex R⟦Γ⟧) ↦ a ≠ 0) b hb))).1 ∨
    Eq.{u_1 + 1} (α := Γ)
        ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
            ((fun (x : { a : Lex R⟦Γ⟧ // a ≠ 0 }) ↦
                (match (motive := { a : Lex R⟦Γ⟧ // a ≠ 0 } → Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))) x with
                  | ⟨x, hx⟩ =>
                    (toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
                      (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯,
                        FiniteArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
                          ⋯) :
                  Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))))
              (Subtype.mk (p := fun (a : Lex R⟦Γ⟧) ↦ a ≠ 0) a ha))).1
        ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
            ((fun (x : { a : Lex R⟦Γ⟧ // a ≠ 0 }) ↦
                (match (motive := { a : Lex R⟦Γ⟧ // a ≠ 0 } → Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))) x with
                  | ⟨x, hx⟩ =>
                    (toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
                      (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯,
                        FiniteArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
                          ⋯) :
                  Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))))
              (Subtype.mk (p := fun (a : Lex R⟦Γ⟧) ↦ a ≠ 0) b hb))).1 ∧
      LE.le.{u_2} (α := FiniteArchimedeanClass R)
        ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
            ((fun (x : { a : Lex R⟦Γ⟧ // a ≠ 0 }) ↦
                (match (motive := { a : Lex R⟦Γ⟧ // a ≠ 0 } → Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))) x with
                  | ⟨x, hx⟩ =>
                    (toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
                      (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯,
                        FiniteArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
                          ⋯) :
                  Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))))
              (Subtype.mk (p := fun (a : Lex R⟦Γ⟧) ↦ a ≠ 0) a ha))).2
        ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R)
            ((fun (x : { a : Lex R⟦Γ⟧ // a ≠ 0 }) ↦
                (match (motive := { a : Lex R⟦Γ⟧ // a ≠ 0 } → Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))) x with
                  | ⟨x, hx⟩ =>
                    (toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
                      (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⋯,
                        FiniteArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
                          ⋯) :
                  Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))))
              (Subtype.mk (p := fun (a : Lex R⟦Γ⟧) ↦ a ≠ 0) b hb))).2

Tactic:
simp only [ofLex_toLex]

Premises used: ofLex_toLex