-- 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⟧)
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⟧))))
a : M
simp_rw :
  Eq (α := ArchimedeanClass M)
    ((OrderIso.symm (DivisibleHull.archimedeanClassOrderIso M) :
          (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass M)
        ((FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M) :
            (a : WithTop (FiniteArchimedeanClass (DivisibleHull M))) → ArchimedeanClass (DivisibleHull M))
          ((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⟧)
                    ((f₂ : (a : DivisibleHull M) → Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
                        ((f₁ : (a : M) → DivisibleHull M) a : DivisibleHull M) :
                      Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) :
                  Lex ℝ⟦FiniteArchimedeanClass M⟧))))) :
      ArchimedeanClass M)
    ((FiniteArchimedeanClass.withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
        (orderTop (R := ℝ)
          ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass M⟧) → ℝ⟦FiniteArchimedeanClass M⟧)
            ((f₃ : (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) → Lex ℝ⟦FiniteArchimedeanClass M⟧)
                ((f₂ : (a : DivisibleHull M) → Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
                    ((f₁ : (a : M) → DivisibleHull M) a : DivisibleHull M) :
                  Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) :
              Lex ℝ⟦FiniteArchimedeanClass M⟧))) :
      ArchimedeanClass 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₃.comp (f₂.comp f₁) : (a : M) → Lex ℝ⟦FiniteArchimedeanClass M⟧) a : Lex ℝ⟦FiniteArchimedeanClass M⟧))))

Tactic:
simp_rw [hf₁class, hf₂class, hf₃class, OrderAddMonoidHom.comp_apply]

Premises used: OrderAddMonoidHom.comp_apply