-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective (α := M) (β := DivisibleHull M) (⇑f₁ : (a : M) → DivisibleHull M)
hf₁class :
  ∀ (a : M),
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
      ((OrderIso.symm (DivisibleHull.archimedeanClassOrderIso M) :
          (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass M)
        (ArchimedeanClass.mk ((f₁ : (a : M) → DivisibleHull M) a)))
f₂' : DivisibleHull M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
hf₂' :
  StrictMono (α := DivisibleHull M) (β := Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
    (⇑f₂' : (a : DivisibleHull M) → Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
hf₂class' :
  ∀ (a : DivisibleHull M),
    Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk a)
      ((FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M) :
          (a : WithTop (FiniteArchimedeanClass (DivisibleHull M))) → ArchimedeanClass (DivisibleHull M))
        (orderTop (R := ℝ)
          ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) → ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
            ((f₂' : (a : DivisibleHull M) → Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) a :
              Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧))))
f₂ : DivisibleHull M →+o Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ :=
  { toAddMonoidHom := f₂'.toAddMonoidHom, monotone' := ⋯ }
hf₂ :
  Function.Injective (α := DivisibleHull M) (β := Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
    (⇑f₂ : (a : DivisibleHull M) → Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
hf₂class :
  ∀ (a : DivisibleHull M),
    Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk a)
      ((FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M) :
          (a : WithTop (FiniteArchimedeanClass (DivisibleHull M))) → ArchimedeanClass (DivisibleHull M))
        (orderTop (R := ℝ)
          ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) → ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
            ((f₂ : (a : DivisibleHull M) → Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) a :
              Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧))))
f₃ : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ →+o Lex ℝ⟦FiniteArchimedeanClass M⟧ :=
  embDomainOrderAddMonoidHom
    (RelIso.toRelEmbedding (r := fun (x1 x2 : FiniteArchimedeanClass (DivisibleHull M)) ↦ x1 ≤ x2) (s :=
      fun (x1 x2 : FiniteArchimedeanClass M) ↦ x1 ≤ x2)
      (FiniteArchimedeanClass.congrOrderIso (OrderIso.symm (DivisibleHull.archimedeanClassOrderIso M))))
hf₃ :
  Function.Injective (α := Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) (β := Lex ℝ⟦FiniteArchimedeanClass M⟧)
    (⇑f₃ : (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) → Lex ℝ⟦FiniteArchimedeanClass M⟧)
a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
⊢ Eq (α := WithTop (FiniteArchimedeanClass M))
    ((OrderIso.symm
            (OrderIso.withTopCongr (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M))) :
          (a : WithTop (FiniteArchimedeanClass (DivisibleHull M))) → WithTop (FiniteArchimedeanClass M))
        (orderTop (R := ℝ)
          ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) → ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
            a)) :
      WithTop (FiniteArchimedeanClass M))
    (orderTop (R := ℝ)
        ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass M⟧) → ℝ⟦FiniteArchimedeanClass M⟧)
          ((f₃ : (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) → Lex ℝ⟦FiniteArchimedeanClass M⟧) a :
            Lex ℝ⟦FiniteArchimedeanClass M⟧)) :
      WithTop (FiniteArchimedeanClass M))

Tactic:
simp [f₃, ← OrderIso.withTopCongr_symm]

Premises used: OrderIso.withTopCongr_symm