-- Mathlib/ModelTheory/PartialEquiv.lean
theorem isExtensionPair_iff_exists_embedding_closure_singleton_sup :
    L.IsExtensionPair M N ↔
    ∀ (S : L.Substructure M) (_ : S.FG) (f : S ↪[L] N) (m : M),
      ∃ g : (closure L {m} ⊔ S : L.Substructure M) ↪[L] N, f =
        g.comp (Substructure.inclusion le_sup_right)

Proof state:
case refine_1.intro.mk.intro.intro.refine_2.h.mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑⟨f', hf'⟩).dom
ff'1 : (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).dom ≤ (↑⟨f', hf'⟩).dom
ff'2 :
  (↑⟨f', hf'⟩).cod.subtype.comp ((↑⟨f', hf'⟩).toEquiv.toEmbedding.comp (Substructure.inclusion ff'1)) =
    (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).cod.subtype.comp
      (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).toEquiv.toEmbedding
x : M
hx : x ∈ S
⊢ f ⟨x, hx⟩ = ((f'.toEmbedding.comp (Substructure.inclusion ⋯)).comp (Substructure.inclusion ⋯)) ⟨x, hx⟩

Tactic:
rw [Embedding.subtype_equivRange] at ff'2

Result:
case refine_1.intro.mk.intro.intro.refine_2.h.mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑⟨f', hf'⟩).dom
ff'1 : (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).dom ≤ (↑⟨f', hf'⟩).dom
ff'2 : (↑⟨f', hf'⟩).cod.subtype.comp ((↑⟨f', hf'⟩).toEquiv.toEmbedding.comp (Substructure.inclusion ff'1)) = f
x : M
hx : x ∈ S
⊢ f ⟨x, hx⟩ = ((f'.toEmbedding.comp (Substructure.inclusion ⋯)).comp (Substructure.inclusion ⋯)) ⟨x, hx⟩

Proof state:
case refine_2.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (S : L.Substructure M), S.FG → ∀ (f : ↥S ↪[L] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)
x✝¹ : L.FGEquiv M N
m : M
f : M ≃ₚ[L] N
f_FG : f.dom.FG
f' : ↥((closure L).toFun {m} ⊔ f.dom) ↪[L] N
eq_f' : f.cod.subtype.comp f.toEquiv.toEmbedding = f'.comp (Substructure.inclusion ⋯)
x✝ : ↥(↑⟨f, f_FG⟩).dom
⊢ ((↑⟨{ dom := (closure L).toFun {m} ⊔ f.dom, cod := f'.toHom.range, toEquiv := f'.equivRange }, ⋯⟩).cod.subtype.comp
        ((↑⟨{ dom := (closure L).toFun {m} ⊔ f.dom, cod := f'.toHom.range, toEquiv := f'.equivRange },
                    ⋯⟩).toEquiv.toEmbedding.comp
          (Substructure.inclusion ⋯)))
      x✝ =
    ((↑⟨f, f_FG⟩).cod.subtype.comp (↑⟨f, f_FG⟩).toEquiv.toEmbedding) x✝

Tactic:
simp only [Embedding.comp_apply, Substructure.coe_inclusion, Equiv.coe_toEmbedding, coe_subtype,
  Embedding.equivRange_apply, eq_f']

Result:
no goals

Proof state:
case refine_2.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (S : L.Substructure M), S.FG → ∀ (f : ↥S ↪[L] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)
x✝ : L.FGEquiv M N
m : M
f : M ≃ₚ[L] N
f_FG : f.dom.FG
f' : ↥((closure L).toFun {m} ⊔ f.dom) ↪[L] N
eq_f' : f.toEmbedding = f'.comp (Substructure.inclusion ⋯)
⊢ ∃ g, m ∈ (↑g).dom ∧ ⟨f, f_FG⟩ ≤ g

Tactic:
refine ⟨⟨⟨closure L {m} ⊔ f.dom, f'.toHom.range, f'.equivRange⟩,
  (fg_closure_singleton _).sup f_FG⟩,
  subset_closure.trans (le_sup_left : (closure L) {m} ≤ _) (mem_singleton m),
  ⟨le_sup_right, Embedding.ext (fun _ => ?_)⟩⟩

Result:
case refine_2.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (S : L.Substructure M), S.FG → ∀ (f : ↥S ↪[L] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)
x✝¹ : L.FGEquiv M N
m : M
f : M ≃ₚ[L] N
f_FG : f.dom.FG
f' : ↥((closure L).toFun {m} ⊔ f.dom) ↪[L] N
eq_f' : f.toEmbedding = f'.comp (Substructure.inclusion ⋯)
x✝ : ↥(↑⟨f, f_FG⟩).dom
⊢ ((↑⟨{ dom := (closure L).toFun {m} ⊔ f.dom, cod := f'.toHom.range, toEquiv := f'.equivRange }, ⋯⟩).cod.subtype.comp
        ((↑⟨{ dom := (closure L).toFun {m} ⊔ f.dom, cod := f'.toHom.range, toEquiv := f'.equivRange },
                    ⋯⟩).toEquiv.toEmbedding.comp
          (Substructure.inclusion ⋯)))
      x✝ =
    ((↑⟨f, f_FG⟩).cod.subtype.comp (↑⟨f, f_FG⟩).toEquiv.toEmbedding) x✝

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ L.IsExtensionPair M N ↔
    ∀ (S : L.Substructure M), S.FG → ∀ (f : ↥S ↪[L] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
refine ⟨fun h S S_FG f m => ?_, fun h ⟨f, f_FG⟩ m => ?_⟩

Result:
case refine_1
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] N
m : M
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

case refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (S : L.Substructure M), S.FG → ∀ (f : ↥S ↪[L] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)
x✝ : L.FGEquiv M N
m : M
f : M ≃ₚ[L] N
f_FG : f.dom.FG
⊢ ∃ g, m ∈ (↑g).dom ∧ ⟨f, f_FG⟩ ≤ g

Proof state:
case refine_1.intro.mk.intro.intro.refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑⟨f', hf'⟩).dom
ff'1 : (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).dom ≤ (↑⟨f', hf'⟩).dom
ff'2 :
  (↑⟨f', hf'⟩).cod.subtype.comp ((↑⟨f', hf'⟩).toEquiv.toEmbedding.comp (Substructure.inclusion ff'1)) =
    (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).cod.subtype.comp
      (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).toEquiv.toEmbedding
⊢ f = (f'.toEmbedding.comp (Substructure.inclusion ⋯)).comp (Substructure.inclusion ⋯)

Tactic:
ext ⟨x, hx⟩

Result:
case refine_1.intro.mk.intro.intro.refine_2.h.mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑⟨f', hf'⟩).dom
ff'1 : (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).dom ≤ (↑⟨f', hf'⟩).dom
ff'2 :
  (↑⟨f', hf'⟩).cod.subtype.comp ((↑⟨f', hf'⟩).toEquiv.toEmbedding.comp (Substructure.inclusion ff'1)) =
    (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).cod.subtype.comp
      (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).toEquiv.toEmbedding
x : M
hx : x ∈ S
⊢ f ⟨x, hx⟩ = ((f'.toEmbedding.comp (Substructure.inclusion ⋯)).comp (Substructure.inclusion ⋯)) ⟨x, hx⟩

Proof state:
case refine_1.intro.mk.intro.intro.refine_1
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑⟨f', hf'⟩).dom
ff'1 : (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).dom ≤ (↑⟨f', hf'⟩).dom
ff'2 :
  (↑⟨f', hf'⟩).cod.subtype.comp ((↑⟨f', hf'⟩).toEquiv.toEmbedding.comp (Substructure.inclusion ff'1)) =
    (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).cod.subtype.comp
      (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).toEquiv.toEmbedding
⊢ (closure L).toFun {m} ⊔ S ≤ f'.dom

Tactic:
simp only [sup_le_iff, ff'1, closure_le, singleton_subset_iff, SetLike.mem_coe, mf',
  and_self]

Result:
no goals