-- 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⟦Γ⟧
⊢ (∃ (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
have simp : (∃ (i : Γ'),
      (∀ j < i,
          Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
            (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)) ∧
        LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
          (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)) ∨
    Eq (α := R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
      (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ↔
  (∃ (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 only [Function.Embedding.coeFn_mk, ofLex_toLex, EmbeddingLike.apply_eq_iff_eq]