-- Mathlib/ModelTheory/Order.lean
lemma dlo_isExtensionPair
    (M : Type w) [Language.order.Structure M] [M ⊨ Language.order.linearOrderTheory]
    (N : Type w') [Language.order.Structure N] [N ⊨ Language.order.dlo] [Nonempty N] :
    Language.order.IsExtensionPair M N

Proof state:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
⊢ 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]

Result:
no goals

Proof state:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝¹ : LinearOrder M := Language.order.linearOrderOfModels M
this✝ : LinearOrder N := Language.order.linearOrderOfModels N
this : DenselyOrdered N
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
have := Language.order.noBotOrder_of_dlo N

Result:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝² : LinearOrder M := Language.order.linearOrderOfModels M
this✝¹ : LinearOrder N := Language.order.linearOrderOfModels N
this✝ : DenselyOrdered N
this : NoBotOrder N
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Proof state:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
⊢ ∀ (S : Language.order.Substructure M),
    S.FG → ∀ (f : ↥S ↪[Language.order] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
intro S S_fg f m

Result:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Proof state:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝² : LinearOrder M := Language.order.linearOrderOfModels M
this✝¹ : LinearOrder N := Language.order.linearOrderOfModels N
this✝ : DenselyOrdered N
this : NoBotOrder N
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
have := Language.order.noTopOrder_of_dlo N

Result:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝³ : LinearOrder M := Language.order.linearOrderOfModels M
this✝² : LinearOrder N := Language.order.linearOrderOfModels N
this✝¹ : DenselyOrdered N
this✝ : NoBotOrder N
this : NoTopOrder N
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Proof state:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝⁵ : LinearOrder M := Language.order.linearOrderOfModels M
this✝⁴ : LinearOrder N := Language.order.linearOrderOfModels N
this✝³ : DenselyOrdered N
this✝² : NoBotOrder N
this✝¹ : NoTopOrder N
this✝ : NoMinOrder N
this : NoMaxOrder N
hS : (↑S).Finite
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
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

Result:
case intro
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝⁵ : LinearOrder M := Language.order.linearOrderOfModels M
this✝⁴ : LinearOrder N := Language.order.linearOrderOfModels N
this✝³ : DenselyOrdered N
this✝² : NoBotOrder N
this✝¹ : NoTopOrder N
this✝ : NoMinOrder N
this : NoMaxOrder N
hS : (↑S).Finite
g : { x // x ∈ insert m hS.toFinset } ↪o N
hg :
  ⇑g ∘ Set.inclusion ⋯ =
    ⇑(RelEmbedding.trans (OrderIso.setCongr ↑hS.toFinset ↑S ⋯).toOrderEmbedding (OrderEmbedding.ofStrictMono ⇑f ⋯))
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Proof state:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
⊢ Language.order.IsExtensionPair M N

Tactic:
rw [isExtensionPair_iff_exists_embedding_closure_singleton_sup]

Result:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
⊢ ∀ (S : Language.order.Substructure M),
    S.FG → ∀ (f : ↥S ↪[Language.order] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)

Proof state:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝⁴ : LinearOrder M := Language.order.linearOrderOfModels M
this✝³ : LinearOrder N := Language.order.linearOrderOfModels N
this✝² : DenselyOrdered N
this✝¹ : NoBotOrder N
this✝ : NoTopOrder N
this : NoMinOrder N
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
have := NoTopOrder.to_noMaxOrder N

Result:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝⁵ : LinearOrder M := Language.order.linearOrderOfModels M
this✝⁴ : LinearOrder N := Language.order.linearOrderOfModels N
this✝³ : DenselyOrdered N
this✝² : NoBotOrder N
this✝¹ : NoTopOrder N
this✝ : NoMinOrder N
this : NoMaxOrder N
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)