-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
simp_rw :
  (∃ (i : Γ'),
        (∀ j < i,
            Eq.{u_2 + 1} (α := R)
              (coeff
                ((ofLex : (a : Lex R⟦Γ'⟧) → R⟦Γ'⟧)
                  (({
                        toFun := fun (a : Lex R⟦Γ⟧) ↦
                          (toLex : (a : R⟦Γ'⟧) → Lex R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)),
                        inj' := ⋯ } :
                      (a : Lex R⟦Γ⟧) → Lex R⟦Γ'⟧)
                    a))
                j)
              (coeff
                ((ofLex : (a : Lex R⟦Γ'⟧) → R⟦Γ'⟧)
                  (({
                        toFun := fun (a : Lex R⟦Γ⟧) ↦
                          (toLex : (a : R⟦Γ'⟧) → Lex R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)),
                        inj' := ⋯ } :
                      (a : Lex R⟦Γ⟧) → Lex R⟦Γ'⟧)
                    b))
                j)) ∧
          LT.lt.{u_2} (α := R)
            (coeff
              ((ofLex : (a : Lex R⟦Γ'⟧) → R⟦Γ'⟧)
                (({
                      toFun := fun (a : Lex R⟦Γ⟧) ↦
                        (toLex : (a : R⟦Γ'⟧) → Lex R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)),
                      inj' := ⋯ } :
                    (a : Lex R⟦Γ⟧) → Lex R⟦Γ'⟧)
                  a))
              i)
            (coeff
              ((ofLex : (a : Lex R⟦Γ'⟧) → R⟦Γ'⟧)
                (({
                      toFun := fun (a : Lex R⟦Γ⟧) ↦
                        (toLex : (a : R⟦Γ'⟧) → Lex R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)),
                      inj' := ⋯ } :
                    (a : Lex R⟦Γ⟧) → Lex R⟦Γ'⟧)
                  b))
              i)) ∨
      Eq (α := Lex R⟦Γ'⟧)
        (({
                toFun := fun (a : Lex R⟦Γ⟧) ↦
                  (toLex : (a : R⟦Γ'⟧) → Lex R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)),
                inj' := ⋯ } :
              (a : Lex R⟦Γ⟧) → Lex R⟦Γ'⟧)
            a :
          Lex R⟦Γ'⟧)
        (({
                toFun := fun (a : Lex R⟦Γ⟧) ↦
                  (toLex : (a : R⟦Γ'⟧) → Lex R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)),
                inj' := ⋯ } :
              (a : Lex R⟦Γ⟧) → Lex R⟦Γ'⟧)
            b :
          Lex R⟦Γ'⟧) ↔
    (∃ (i : Γ),
        (∀ j < i,
            Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j)
              (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)) ∧
          LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i)
            (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)) ∨
      a = b
⊢ LE.le (α := Lex R⟦Γ'⟧)
      (({
              toFun := fun (a : Lex R⟦Γ⟧) ↦
                (toLex : (a : R⟦Γ'⟧) → Lex R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)),
              inj' := ⋯ } :
            (a : Lex R⟦Γ⟧) → Lex R⟦Γ'⟧)
          a :
        Lex R⟦Γ'⟧)
      (({
              toFun := fun (a : Lex R⟦Γ⟧) ↦
                (toLex : (a : R⟦Γ'⟧) → Lex R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)),
              inj' := ⋯ } :
            (a : Lex R⟦Γ⟧) → Lex R⟦Γ'⟧)
          b :
        Lex R⟦Γ'⟧) ↔
    a ≤ b

Tactic:
simp_rw [le_iff_lt_or_eq, lt_iff]

Premises used: le_iff_lt_or_eq, HahnSeries.lt_iff