-- 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 :
  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⟦Γ⟧))
⊢ LE.le (α := FiniteArchimedeanClass (Lex R⟦Γ⟧))
    ((fun (x : Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))) ↦
        ((FiniteArchimedeanClass.liftOrderHom
                (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)))
                    ⋯)
                ⋯ :
              (a : FiniteArchimedeanClass R) → FiniteArchimedeanClass (Lex R⟦Γ⟧))
            ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).2 :
          FiniteArchimedeanClass (Lex R⟦Γ⟧)))
      ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
        (ao, FiniteArchimedeanClass.mk a ha)))
    ((fun (x : Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))) ↦
        ((FiniteArchimedeanClass.liftOrderHom
                (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)))
                    ⋯)
                ⋯ :
              (a : FiniteArchimedeanClass R) → FiniteArchimedeanClass (Lex R⟦Γ⟧))
            ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).2 :
          FiniteArchimedeanClass (Lex R⟦Γ⟧)))
      ((toLex : (a : Γ × FiniteArchimedeanClass R) → Lex (Γ × FiniteArchimedeanClass R))
        (bo, FiniteArchimedeanClass.mk b hb)))

Tactic:
simp only [ne_eq, ofLex_toLex, FiniteArchimedeanClass.liftOrderHom_mk]

Premises used: FiniteArchimedeanClass.liftOrderHom_mk, ofLex_toLex, ne_eq