-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HahnEmbedding (hypothesis)
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⟧)
⊢ ∃ (f : M →+o Lex ℝ⟦FiniteArchimedeanClass M⟧),
    Function.Injective (α := M) (β := Lex ℝ⟦FiniteArchimedeanClass M⟧)
        (⇑f : (a : M) → Lex ℝ⟦FiniteArchimedeanClass M⟧) ∧
      ∀ (a : M),
        Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
          ((FiniteArchimedeanClass.withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
            (orderTop (R := ℝ)
              ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass M⟧) → ℝ⟦FiniteArchimedeanClass M⟧)
                ((f : (a : M) → Lex ℝ⟦FiniteArchimedeanClass M⟧) a : Lex ℝ⟦FiniteArchimedeanClass M⟧))))
have hf₃class : ∀ (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧),
  Eq.{u_1 + 1} (α := WithTop (FiniteArchimedeanClass (DivisibleHull M)))
    (orderTop (R := ℝ)
      ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) → ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) a))
    ((OrderIso.withTopCongr (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M)) :
        (a : WithTop (FiniteArchimedeanClass M)) → WithTop (FiniteArchimedeanClass (DivisibleHull M)))
      (orderTop (R := ℝ)
        ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass M⟧) → ℝ⟦FiniteArchimedeanClass M⟧)
          ((f₃ : (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) → Lex ℝ⟦FiniteArchimedeanClass M⟧) a :
            Lex ℝ⟦FiniteArchimedeanClass M⟧))))
Tactic: have hf₃class (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) :
      (ofLex a).orderTop = OrderIso.withTopCongr
      ((FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M)))
      (ofLex (f₃ a)).orderTop := by
    rw [← OrderIso.symm_apply_eq]
    simp [f₃, ← OrderIso.withTopCongr_symm]