-- Module: Mathlib.ModelTheory.Order
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 ⋯)
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 ⋯)
rw₁₂ 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 M;
    let this_1 := Language.order.linearOrderOfModels N;
    ∀ (this_2 : DenselyOrdered N) (this_3 : NoBotOrder N) (this_4 : NoTopOrder N) (this_5 : NoMinOrder N)
      (this_6 : NoMaxOrder N) (hS : (↑S : Set M).Finite)
      (g : OrderEmbedding.{w, w'} (↥(insert m (hS.toFinset (s := (↑S : Set M))))) N)
      (hg :
        Eq (α := (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w) → N)
          (Function.comp (β := ↥(insert m (hS.toFinset (s := (↑S : Set M))))) (⇑g : (a : ↥(insert m hS.toFinset)) → N)
            (Set.inclusion (s := (↑(hS.toFinset (s := (↑S : Set M))) : Set M)) (t :=
              (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)) ⋯))
          (⇑(RelEmbedding.trans (r := fun (x1 x2 : (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w)) ↦ x1 ≤ x2)
                (s := fun (x1 x2 : (↑(↑S : Set M) : Type w)) ↦ x1 ≤ x2) (t := fun (x1 x2 : N) ↦ x1 ≤ x2)
                (OrderIso.toOrderEmbedding
                  (OrderIso.setCongr (↑(hS.toFinset (s := (↑S : Set M))) : Set M) (↑S : Set M) ⋯))
                (OrderEmbedding.ofStrictMono (⇑f : (a : ↥S) → N) ⋯)) :
            (a : ↥hS.toFinset) → 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 ⋯)
h :
  ∀ (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 M;
    let this_1 := Language.order.linearOrderOfModels N;
    ∀ (this_2 : DenselyOrdered N) (this_3 : NoBotOrder N) (this_4 : NoTopOrder N) (this_5 : NoMinOrder N)
      (this_6 : NoMaxOrder N) (hS : (↑S : Set M).Finite)
      (g : OrderEmbedding.{w, w'} (↥(insert m (hS.toFinset (s := (↑S : Set M))))) N)
      (hg :
        Eq (α := (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w) → N)
          (Function.comp (β := ↥(insert m (hS.toFinset (s := (↑S : Set M))))) (⇑g : (a : ↥(insert m hS.toFinset)) → N)
            (Set.inclusion (s := (↑(hS.toFinset (s := (↑S : Set M))) : Set M)) (t :=
              (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)) ⋯))
          (⇑(RelEmbedding.trans (r := fun (x1 x2 : (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w)) ↦ x1 ≤ x2)
                (s := fun (x1 x2 : (↑(↑S : Set M) : Type w)) ↦ x1 ≤ x2) (t := fun (x1 x2 : N) ↦ x1 ≤ x2)
                (OrderIso.toOrderEmbedding
                  (OrderIso.setCongr (↑(hS.toFinset (s := (↑S : Set M))) : Set M) (↑S : Set M) ⋯))
                (OrderEmbedding.ofStrictMono (⇑f : (a : ↥S) → N) ⋯)) :
            (a : ↥hS.toFinset) → N)),
      let g' :=
        RelEmbedding.trans (r :=
          fun
            (x1 x2 :
              (↑(↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S) : Set M) :
                Type w)) ↦
          x1 ≤ x2) (s := fun (x1 x2 : (↑(↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M) : Type w)) ↦ x1 ≤ x2)
          (t := fun (x1 x2 : N) ↦ x1 ≤ x2)
          (OrderIso.toOrderEmbedding
            (OrderIso.setCongr
              (↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S) : Set M)
              (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M) ⋯))
          g;
      f = Embedding.comp (StrongHomClass.toEmbedding g') (Substructure.inclusion ⋯)
h₁ :
  ∀ (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 M;
    let this_1 := Language.order.linearOrderOfModels N;
    ∀ (this_2 : DenselyOrdered N) (this_3 : NoBotOrder N) (this_4 : NoTopOrder N) (this_5 : NoMinOrder N)
      (this_6 : NoMaxOrder N) (hS : (↑S : Set M).Finite)
      (g : OrderEmbedding.{w, w'} (↥(insert m (hS.toFinset (s := (↑S : Set M))))) N)
      (hg :
        Eq (α := (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w) → N)
          (Function.comp (β := ↥(insert m (hS.toFinset (s := (↑S : Set M))))) (⇑g : (a : ↥(insert m hS.toFinset)) → N)
            (Set.inclusion (s := (↑(hS.toFinset (s := (↑S : Set M))) : Set M)) (t :=
              (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)) ⋯))
          (⇑(RelEmbedding.trans (r := fun (x1 x2 : (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w)) ↦ x1 ≤ x2)
                (s := fun (x1 x2 : (↑(↑S : Set M) : Type w)) ↦ x1 ≤ x2) (t := fun (x1 x2 : N) ↦ x1 ≤ x2)
                (OrderIso.toOrderEmbedding
                  (OrderIso.setCongr (↑(hS.toFinset (s := (↑S : Set M))) : Set M) (↑S : Set M) ⋯))
                (OrderEmbedding.ofStrictMono (⇑f : (a : ↥S) → N) ⋯)) :
            (a : ↥hS.toFinset) → N)),
      let g' :=
        RelEmbedding.trans (r :=
          fun
            (x1 x2 :
              (↑(↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S) : Set M) :
                Type w)) ↦
          x1 ≤ x2) (s := fun (x1 x2 : (↑(↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M) : Type w)) ↦ x1 ≤ x2)
          (t := fun (x1 x2 : N) ↦ x1 ≤ x2)
          (OrderIso.toOrderEmbedding
            (OrderIso.setCongr
              (↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure Language.order) {m} ⊔ S) : Set M)
              (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M) ⋯))
          g;
      ∀ (x : M) (xS : x ∈ S),
        Eq.{w' + 1} (α := N) ((f : (a : ↥S) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xS) : N)
          ((Embedding.comp (StrongHomClass.toEmbedding g') (Substructure.inclusion ⋯) : (a : ↥S) → N)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x xS) :
            N)
h₂ :
  ∀ (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 M;
    let this_1 := Language.order.linearOrderOfModels N;
    ∀ (this_2 : DenselyOrdered N) (this_3 : NoBotOrder N) (this_4 : NoTopOrder N) (this_5 : NoMinOrder N)
      (this_6 : NoMaxOrder N) (hS : (↑S : Set M).Finite)
      (g : OrderEmbedding.{w, w'} (↥(insert m (hS.toFinset (s := (↑S : Set M))))) N)
      (hg :
        Eq (α := (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w) → N)
          (Function.comp (β := ↥(insert m (hS.toFinset (s := (↑S : Set M))))) (⇑g : (a : ↥(insert m hS.toFinset)) → N)
            (Set.inclusion (s := (↑(hS.toFinset (s := (↑S : Set M))) : Set M)) (t :=
              (↑(insert m (hS.toFinset (s := (↑S : Set M)))) : Set M)) ⋯))
          (⇑(RelEmbedding.trans (r := fun (x1 x2 : (↑(↑(hS.toFinset (s := (↑S : Set M))) : Set M) : Type w)) ↦ x1 ≤ x2)
                (s := fun (x1 x2 : (↑(↑S : Set M) : Type w)) ↦ x1 ≤ x2) (t := fun (x1 x2 : N) ↦ x1 ≤ x2)
                (OrderIso.toOrderEmbedding
                  (OrderIso.setCongr (↑(hS.toFinset (s := (↑S : Set M))) : Set M) (↑S : Set M) ⋯))
                (OrderEmbedding.ofStrictMono (⇑f : (a : ↥S) → N) ⋯)) :
            (a : ↥hS.toFinset) → N))
      (x : M) (xS : x ∈ S), x ∈ hS.toFinset (s := (↑S : Set M))
⊢ Language.order.IsExtensionPair M N

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]

Premises used: Set.Finite.mem_toFinset, FirstOrder.Language.isExtensionPair_iff_exists_embedding_closure_singleton_sup, SetLike.mem_coe