-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hnontrivial : Nontrivial M
hnonempty : Nonempty.{u_2 + 1} (FiniteArchimedeanClass M)
c : FiniteArchimedeanClass M
this : Nontrivial R
⊢ Eq.{u_2 + 1} (α := WithTop (FiniteArchimedeanClass M))
      (orderTop.{u_2, u_3} (R := R)
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
              ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
            x)))
      (orderTop.{u_2, u_3} (R := R)
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
              ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
            y))) ↔
    Eq (α := ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      (ArchimedeanClass.mk
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          x))
      (ArchimedeanClass.mk
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          y))
have inr : Eq.{u_2 + 1} (α := WithTop (FiniteArchimedeanClass M))
    (((archimedeanClassOrderIsoWithTop (FiniteArchimedeanClass M) R :
            ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ≃o
              WithTop (FiniteArchimedeanClass M)) :
          (a : ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧)) → WithTop (FiniteArchimedeanClass M))
        (ArchimedeanClass.mk
          ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
              ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
            x)) :
      WithTop (FiniteArchimedeanClass M))
    (((archimedeanClassOrderIsoWithTop (FiniteArchimedeanClass M) R :
            ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ≃o
              WithTop (FiniteArchimedeanClass M)) :
          (a : ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧)) → WithTop (FiniteArchimedeanClass M))
        (ArchimedeanClass.mk
          ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
              ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
            y)) :
      WithTop (FiniteArchimedeanClass M)) ↔
  Eq (α := ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
    (ArchimedeanClass.mk
      ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
          ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
        x))
    (ArchimedeanClass.mk
      ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
          ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
        y))
Tactic: simp_rw [← HahnSeries.archimedeanClassOrderIsoWithTop_apply]