-- 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))
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) ⋯)
⊢ 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))
have 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))))))
Tactic: rw [FiniteArchimedeanClass.mk_le_mk, archimedeanClassMk_le_archimedeanClassMk_iff]