-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
M : Type w
inst : Language.order.Structure M
inst_1 : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst_2 : Language.order.Structure N
inst_3 : N ⊨ Language.order.dlo
inst_4 : Nonempty N
rw rw₁ rw₂ rw₃ :
  ∀ (S : Language.order.Substructure M) (S_fg : S.FG) (f : Embedding.{0, 0, w, w'} Language.order (↥S) N) (m : M),
    ∃ (g :
      Embedding.{0, 0, w, w'} Language.order
        (↥(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S)) N),
      f = g.comp (Substructure.inclusion ⋯)
rw₄ rw₅ :
  ∀ (S : Language.order.Substructure M) (S_fg : S.FG) (f : Embedding.{0, 0, w, w'} Language.order (↥S) N) (m : M),
    ∃ (g :
      Embedding.{0, 0, w, w'} Language.order
        (↥(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S)) N),
      f = g.comp (Substructure.inclusion ⋯)
rw₆ :
  ∀ (S : Language.order.Substructure M) (S_fg : S.FG) (f : Embedding.{0, 0, w, w'} Language.order (↥S) N) (m : M),
    let this := Language.order.linearOrderOfModels N;
    ∀ (this : DenselyOrdered N),
      ∃ (g :
        Embedding.{0, 0, w, w'} Language.order
          (↥(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S)) N),
        f = g.comp (Substructure.inclusion ⋯)
rw₇ :
  ∀ (S : Language.order.Substructure M) (S_fg : S.FG) (f : Embedding.{0, 0, w, w'} Language.order (↥S) N) (m : M),
    let this := Language.order.linearOrderOfModels N;
    ∀ (this_1 : DenselyOrdered N) (this : NoBotOrder N),
      ∃ (g :
        Embedding.{0, 0, w, w'} Language.order
          (↥(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S)) N),
        f = g.comp (Substructure.inclusion ⋯)
rw₈ :
  ∀ (S : Language.order.Substructure M) (S_fg : S.FG) (f : Embedding.{0, 0, w, w'} Language.order (↥S) N) (m : M),
    let this := Language.order.linearOrderOfModels N;
    ∀ (this_1 : DenselyOrdered N) (this_2 : NoBotOrder N) (this : NoTopOrder N),
      ∃ (g :
        Embedding.{0, 0, w, w'} Language.order
          (↥(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S)) N),
        f = g.comp (Substructure.inclusion ⋯)
rw₉ :
  ∀ (S : Language.order.Substructure M) (S_fg : S.FG) (f : Embedding.{0, 0, w, w'} Language.order (↥S) N) (m : M),
    let this := Language.order.linearOrderOfModels N;
    ∀ (this_1 : DenselyOrdered N) (this_2 : NoBotOrder N) (this_3 : NoTopOrder N) (this : NoMinOrder N),
      ∃ (g :
        Embedding.{0, 0, w, w'} Language.order
          (↥(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S)) N),
        f = g.comp (Substructure.inclusion ⋯)
rw₁₀ :
  ∀ (S : Language.order.Substructure M) (S_fg : S.FG) (f : Embedding.{0, 0, w, w'} Language.order (↥S) N) (m : M),
    let this := Language.order.linearOrderOfModels N;
    ∀ (this_1 : DenselyOrdered N) (this_2 : NoBotOrder N) (this_3 : NoTopOrder N) (this_4 : NoMinOrder N)
      (this : NoMaxOrder N),
      ∃ (g :
        Embedding.{0, 0, w, w'} Language.order
          (↥(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S)) N),
        f = g.comp (Substructure.inclusion ⋯)
⊢ Language.order.IsExtensionPair M N
have rw₁₁ : ∀ (S : Language.order.Substructure M) (S_fg : S.FG) (f : Embedding.{0, 0, w, w'} Language.order (↥S) N) (m : M),
  let this := Language.order.linearOrderOfModels N;
  ∀ (this_1 : DenselyOrdered N) (this_2 : NoBotOrder N) (this_3 : NoTopOrder N) (this_4 : NoMinOrder N)
    (this : NoMaxOrder N) (hS : (↑S : Set M).Finite),
    ∃ (g :
      Embedding.{0, 0, w, w'} Language.order
        (↥(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S)) N),
      f = g.comp (Substructure.inclusion sorry)
Tactic: classical
  rw [isExtensionPair_iff_exists_embedding_closure_singleton_sup]
  intro S S_fg f m
  letI := Language.order.linearOrderOfModels M
  letI := Language.order.linearOrderOfModels N
  have := Language.order.denselyOrdered_of_dlo N
  have := Language.order.noBotOrder_of_dlo N
  have := Language.order.noTopOrder_of_dlo N
  have := NoBotOrder.to_noMinOrder N
  have := NoTopOrder.to_noMaxOrder N
  have hS : Set.Finite (S : Set M) := (S.fg_iff_structure_fg.1 S_fg).finite
  obtain ⟨g, hg⟩ := Order.exists_orderEmbedding_insert hS.toFinset
    ((OrderIso.setCongr hS.toFinset (S : Set M) hS.coe_toFinset).toOrderEmbedding.trans
      (OrderEmbedding.ofStrictMono f (HomClass.strictMono f))) m
  let g' :
    ((Substructure.closure Language.order).toFun {m} ⊔ S : Language.order.Substructure M) ↪o N :=
    ((OrderIso.setCongr _ _ (by
      convert!
        LowerAdjoint.closure_eq_self_of_mem_closed _
          (Substructure.mem_closed_of_isRelational Language.order
            ((insert m hS.toFinset : Finset M) : Set M))
      simp only [Finset.coe_insert, Set.Finite.coe_toFinset, Substructure.closure_insert,
        Substructure.closure_eq])).toOrderEmbedding.trans g)
  use StrongHomClass.toEmbedding g'
  ext ⟨x, xS⟩
  refine congr_fun hg.symm ⟨x, (?_ : x ∈ hS.toFinset)⟩
  simp only [Set.Finite.mem_toFinset, SetLike.mem_coe, xS]