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

Tactic:
rw [FiniteArchimedeanClass.mk_le_mk, archimedeanClassMk_le_archimedeanClassMk_iff]

Premises used: FiniteArchimedeanClass.mk_le_mk, HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff