-- 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
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
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
have := Language.order.denselyOrdered_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
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Proof state:
case h.h.mk
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' : ↥((Substructure.closure Language.order).toFun {m} ⊔ S) ↪o N :=
  RelEmbedding.trans
    (OrderIso.setCongr (↑((Substructure.closure Language.order).toFun {m} ⊔ S))
        (Membership.mem (insert m hS.toFinset).val) ⋯).toOrderEmbedding
    g
x : M
xS : x ∈ S
⊢ f ⟨x, xS⟩ = ((StrongHomClass.toEmbedding g').comp (Substructure.inclusion ⋯)) ⟨x, xS⟩

Tactic:
refine congr_fun hg.symm ⟨x, (?_ : x ∈ hS.toFinset)⟩

Result:
case h.h.mk
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' : ↥((Substructure.closure Language.order).toFun {m} ⊔ S) ↪o N :=
  RelEmbedding.trans
    (OrderIso.setCongr (↑((Substructure.closure Language.order).toFun {m} ⊔ S))
        (Membership.mem (insert m hS.toFinset).val) ⋯).toOrderEmbedding
    g
x : M
xS : x ∈ S
⊢ x ∈ hS.toFinset

Proof state:
case h.h.mk
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' : ↥((Substructure.closure Language.order).toFun {m} ⊔ S) ↪o N :=
  RelEmbedding.trans
    (OrderIso.setCongr (↑((Substructure.closure Language.order).toFun {m} ⊔ S))
        (Membership.mem (insert m hS.toFinset).val) ⋯).toOrderEmbedding
    g
x : M
xS : x ∈ S
⊢ x ∈ hS.toFinset

Tactic:
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
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
letI := Language.order.linearOrderOfModels 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
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Proof state:
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' : ↥((Substructure.closure Language.order).toFun {m} ⊔ S) ↪o N :=
  RelEmbedding.trans
    (OrderIso.setCongr (↑((Substructure.closure Language.order).toFun {m} ⊔ S))
        (Membership.mem (insert m hS.toFinset).val) ⋯).toOrderEmbedding
    g
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
use StrongHomClass.toEmbedding g'

Result:
case h
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' : ↥((Substructure.closure Language.order).toFun {m} ⊔ S) ↪o N :=
  RelEmbedding.trans
    (OrderIso.setCongr (↑((Substructure.closure Language.order).toFun {m} ⊔ S))
        (Membership.mem (insert m hS.toFinset).val) ⋯).toOrderEmbedding
    g
⊢ f = (StrongHomClass.toEmbedding g').comp (Substructure.inclusion ⋯)