-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
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⟦Γ⟧
⊢ 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
have 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' := sorry } :
                    (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' := sorry } :
                    (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' := sorry } :
                  (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' := sorry } :
                  (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' := sorry } :
            (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' := sorry } :
            (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
Tactic: simp_rw [le_iff_lt_or_eq, lt_iff]