awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
inst : L.Structure M
inst_1 : Countable M
g : L.FGEquiv M M → (U : { S : L.Substructure M // S.FG }) × (↥(↑U : L.Substructure M) →[L] M) :=
  fun (f : L.FGEquiv M M) ↦
    Sigma.mk (β := fun (U : { S : L.Substructure M // S.FG }) ↦ ↥(↑U : L.Substructure M) →[L] M)
      (Subtype.mk (p := fun (S : L.Substructure M) ↦ S.FG) (↑f : M ≃ₚ[L] M).dom ⋯)
      ((↑f : M ≃ₚ[L] M).cod.subtype.toHom.comp (↑f : M ≃ₚ[L] M).toEquiv.toHom)
f f' : L.FGEquiv M M
cod_f : L.Substructure M
equiv_f : ↥(↑f' : M ≃ₚ[L] M).1 ≃[L] ↥cod_f
f_fin : { dom := (↑f' : M ≃ₚ[L] M).1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] M }.dom.FG
h : cod_f.subtype.toHom.comp equiv_f.toHom = (↑f' : M ≃ₚ[L] M).cod.subtype.toHom.comp (↑f' : M ≃ₚ[L] M).toEquiv.toHom
⊢ ∀ (x : M)
    (h :
      x ∈
        (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                { dom := (↑f' : M ≃ₚ[L] M).1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] M } f_fin) :
            M ≃ₚ[L] M).dom),
    Eq (α := M)
      (((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                      { dom := (↑f' : M ≃ₚ[L] M).1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] M } f_fin) :
                  M ≃ₚ[L] M).cod.subtype :
            (a : ↥(↑⟨{ dom := (↑f' : M ≃ₚ[L] M).1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩ : M ≃ₚ[L] M).cod) → M)
          (((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                        { dom := (↑f' : M ≃ₚ[L] M).1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] M } f_fin) :
                    M ≃ₚ[L] M).toEquiv :
                (a : ↥(↑⟨{ dom := (↑f' : M ≃ₚ[L] M).1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩ : M ≃ₚ[L] M).dom) →
                  ↥(↑⟨{ dom := (↑f' : M ≃ₚ[L] M).1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩ : M ≃ₚ[L] M).cod)
              (Subtype.mk (p := fun (x : M) ↦
                x ∈
                  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                          { dom := (↑f' : M ≃ₚ[L] M).1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] M } f_fin) :
                      M ≃ₚ[L] M).dom)
                x h) :
            ↥(↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                      { dom := (↑f' : M ≃ₚ[L] M).1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] M } f_fin) :
                  M ≃ₚ[L] M).cod) :
        M)
      (((↑f' : M ≃ₚ[L] M).cod.subtype : (a : ↥(↑f' : M ≃ₚ[L] M).cod) → M)
          (((↑f' : M ≃ₚ[L] M).toEquiv : (a : ↥(↑f' : M ≃ₚ[L] M).dom) → ↥(↑f' : M ≃ₚ[L] M).cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f' : M ≃ₚ[L] M).dom) x ⋯) :
            ↥(↑f' : M ≃ₚ[L] M).cod) :
        M)

Tactic:
exact fun x hx ↦ congr_fun (congr_arg (↑) h) ⟨x, hx⟩

Premises used: congr_arg, congr_fun
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
inst : L.Structure M
inst_1 : Countable M
g : L.FGEquiv M M → (U : { S : L.Substructure M // S.FG }) × (↥(↑U : L.Substructure M) →[L] M) :=
  fun (f : L.FGEquiv M M) ↦
    Sigma.mk (β := fun (U : { S : L.Substructure M // S.FG }) ↦ ↥(↑U : L.Substructure M) →[L] M)
      (Subtype.mk (p := fun (S : L.Substructure M) ↦ S.FG) (↑f : M ≃ₚ[L] M).dom ⋯)
      ((↑f : M ≃ₚ[L] M).cod.subtype.toHom.comp (↑f : M ≃ₚ[L] M).toEquiv.toHom)
⊢ Function.Injective g

Tactic:
have g_inj : Function.Injective g := by
    intro f f' h
    ext
    let ⟨⟨dom_f, cod_f, equiv_f⟩, f_fin⟩ := f
    cases congr_arg (·.1) h
    apply PartialEquiv.ext (by rfl)
    simp only [g, Sigma.mk.inj_iff, heq_eq_eq, true_and] at h
    exact fun x hx ↦ congr_fun (congr_arg (↑) h) ⟨x, hx⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
inst : L.Structure M
inst_1 : Countable M
g : L.FGEquiv M M → (U : { S : L.Substructure M // S.FG }) × (↥(↑U : L.Substructure M) →[L] M) :=
  fun (f : L.FGEquiv M M) ↦
    Sigma.mk (β := fun (U : { S : L.Substructure M // S.FG }) ↦ ↥(↑U : L.Substructure M) →[L] M)
      (Subtype.mk (p := fun (S : L.Substructure M) ↦ S.FG) (↑f : M ≃ₚ[L] M).dom ⋯)
      ((↑f : M ≃ₚ[L] M).cod.subtype.toHom.comp (↑f : M ≃ₚ[L] M).toEquiv.toHom)
g_inj : Function.Injective g
⊢ ∀ (U : { S : L.Substructure M // S.FG }), Structure.FG.{w, u, v} L ↥(↑U : L.Substructure M)

Tactic:
have : ∀ U : { S : L.Substructure M // S.FG }, Structure.FG L U.val :=
    fun U ↦ (U.val.fg_iff_structure_fg.1 U.prop)
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
inst : L.Structure M
inst_1 : Countable M
g : L.FGEquiv M M → (U : { S : L.Substructure M // S.FG }) × (↥(↑U : L.Substructure M) →[L] M) :=
  fun (f : L.FGEquiv M M) ↦
    Sigma.mk (β := fun (U : { S : L.Substructure M // S.FG }) ↦ ↥(↑U : L.Substructure M) →[L] M)
      (Subtype.mk (p := fun (S : L.Substructure M) ↦ S.FG) (↑f : M ≃ₚ[L] M).dom ⋯)
      ((↑f : M ≃ₚ[L] M).cod.subtype.toHom.comp (↑f : M ≃ₚ[L] M).toEquiv.toHom)
g_inj : Function.Injective g
this : ∀ (U : { S : L.Substructure M // S.FG }), Structure.FG.{w, u, v} L ↥(↑U : L.Substructure M)
⊢ Countable.{w + 1} (L.FGEquiv M M)

Tactic:
Function.Embedding.countable ⟨g, g_inj⟩

Premises used: Function.Embedding.mk, Function.Embedding.countable
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
inst : L.Structure M
inst_1 : Countable M
g : L.FGEquiv M M → (U : { S : L.Substructure M // S.FG }) × (↥(↑U : L.Substructure M) →[L] M) :=
  fun (f : L.FGEquiv M M) ↦
    Sigma.mk (β := fun (U : { S : L.Substructure M // S.FG }) ↦ ↥(↑U : L.Substructure M) →[L] M)
      (Subtype.mk (p := fun (S : L.Substructure M) ↦ S.FG) (↑f : M ≃ₚ[L] M).dom ⋯)
      ((↑f : M ≃ₚ[L] M).cod.subtype.toHom.comp (↑f : M ≃ₚ[L] M).toEquiv.toHom)
g_inj : Function.Injective g
this : ∀ (U : { S : L.Substructure M // S.FG }), Structure.FG.{w, u, v} L ↥(↑U : L.Substructure M)
⊢ Countable.{w + 1} (L.FGEquiv M M)

Tactic:
exact Function.Embedding.countable ⟨g, g_inj⟩

Premises used: Function.Embedding.mk, Function.Embedding.countable
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : IsEmpty.{u + 1} L.Constants
inst_3 : IsEmpty.{v + 1} (L.Relations 0)
n : ℕ
f : L.Functions n
x : Fin n → ↥⊥
⊢ Eq.{w' + 1} (α := ↥⊥) (isEmptyElim (p := fun (x : ↥⊥) ↦ ↥⊥) (funMap f x) : ↥⊥)
    (funMap f ((fun (a : ↥⊥) ↦ isEmptyElim (p := fun (x : ↥⊥) ↦ ↥⊥) a) ∘ x) : ↥⊥)

Tactic:
subsingleton
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : IsEmpty.{u + 1} L.Constants
inst_3 : IsEmpty.{v + 1} (L.Relations 0)
n : ℕ
r : L.Relations n
x : Fin n → ↥⊥
zero :
  ∀ (r : L.Relations 0) (x : Fin 0 → ↥⊥),
    RelMap.{u, v, w'} (M := ↥⊥) r ((fun (a : ↥⊥) ↦ isEmptyElim (p := fun (x : ↥⊥) ↦ ↥⊥) a) ∘ x) ↔ RelMap r x
succ :
  ∀ (n : ℕ) (r : L.Relations (n + 1)) (x : Fin (n + 1) → ↥⊥),
    RelMap.{u, v, w'} (M := ↥⊥) r ((fun (a : ↥⊥) ↦ isEmptyElim (p := fun (x : ↥⊥) ↦ ↥⊥) a) ∘ x) ↔ RelMap r x
⊢ RelMap.{u, v, w'} (M := ↥⊥) r ((fun (a : ↥⊥) ↦ isEmptyElim (p := fun (x : ↥⊥) ↦ ↥⊥) a) ∘ x) ↔ RelMap r x

Tactic:
cases n
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : IsEmpty.{u + 1} L.Constants
inst_3 : IsEmpty.{v + 1} (L.Relations 0)
r : L.Relations 0
x : Fin 0 → ↥⊥
⊢ RelMap.{u, v, w'} (M := ↥⊥) r ((fun (a : ↥⊥) ↦ isEmptyElim (p := fun (x : ↥⊥) ↦ ↥⊥) a) ∘ x) ↔ RelMap r x

Tactic:
isEmptyElim r

Premises used: isEmptyElim
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : IsEmpty.{u + 1} L.Constants
inst_3 : IsEmpty.{v + 1} (L.Relations 0)
r : L.Relations 0
x : Fin 0 → ↥⊥
⊢ RelMap.{u, v, w'} (M := ↥⊥) r ((fun (a : ↥⊥) ↦ isEmptyElim (p := fun (x : ↥⊥) ↦ ↥⊥) a) ∘ x) ↔ RelMap r x

Tactic:
exact isEmptyElim r
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : IsEmpty.{u + 1} L.Constants
inst_3 : IsEmpty.{v + 1} (L.Relations 0)
n : ℕ
r : L.Relations (n + 1)
x : Fin (n + 1) → ↥⊥
⊢ RelMap.{u, v, w'} (M := ↥⊥) r ((fun (a : ↥⊥) ↦ isEmptyElim (p := fun (x : ↥⊥) ↦ ↥⊥) a) ∘ x) ↔ RelMap r x

Tactic:
isEmptyElim (x 0)

Premises used: isEmptyElim, OfNat.ofNat
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : IsEmpty.{u + 1} L.Constants
inst_3 : IsEmpty.{v + 1} (L.Relations 0)
n : ℕ
r : L.Relations (n + 1)
x : Fin (n + 1) → ↥⊥
⊢ RelMap.{u, v, w'} (M := ↥⊥) r ((fun (a : ↥⊥) ↦ isEmptyElim (p := fun (x : ↥⊥) ↦ ↥⊥) a) ∘ x) ↔ RelMap r x

Tactic:
exact isEmptyElim (x 0)
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
⊢ L.IsExtensionPair M N ↔ ∀ (f : L.FGEquiv N M) (m : M), ∃ (g : L.FGEquiv N M), m ∈ (↑g : N ≃ₚ[L] M).cod ∧ f ≤ g

Tactic:
Iff.intro ?_ ?_

Premises used: Iff.intro
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
refine_1 :
  L.IsExtensionPair M N → ∀ (f : L.FGEquiv N M) (m : M), ∃ (g : L.FGEquiv N M), m ∈ (↑g : N ≃ₚ[L] M).cod ∧ f ≤ g
refine_2 :
  (∀ (f : L.FGEquiv N M) (m : M), ∃ (g : L.FGEquiv N M), m ∈ (↑g : N ≃ₚ[L] M).cod ∧ f ≤ g) → L.IsExtensionPair M N
⊢ L.IsExtensionPair M N ↔ ∀ (f : L.FGEquiv N M) (m : M), ∃ (g : L.FGEquiv N M), m ∈ (↑g : N ≃ₚ[L] M).cod ∧ f ≤ g

Tactic:
refine Iff.intro ?_ ?_

Premises used: Iff.intro
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
h : L.IsExtensionPair M N
f : L.FGEquiv N M
m : M
refine_1 :
  ∀ (g : L.FGEquiv M N) (h1 : m ∈ (↑g : M ≃ₚ[L] N).dom) (h2 : f.symm ≤ g),
    ∃ (g : L.FGEquiv N M), m ∈ (↑g : N ≃ₚ[L] M).cod ∧ f ≤ g
⊢ ∃ (g : L.FGEquiv N M), m ∈ (↑g : N ≃ₚ[L] M).cod ∧ f ≤ g

Tactic:
obtain ⟨g, h1, h2⟩ := h f.symm m

Premises used: FirstOrder.Language.FGEquiv.symm
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
h : L.IsExtensionPair M N
f : L.FGEquiv N M
m : M
g : L.FGEquiv M N
h1 : m ∈ (↑g : M ≃ₚ[L] N).dom
h2 : f.symm ≤ g
⊢ ∃ (g : L.FGEquiv N M), m ∈ (↑g : N ≃ₚ[L] M).cod ∧ f ≤ g

Tactic:
⟨g.symm, h1, monotone_symm h2⟩

Premises used: FirstOrder.Language.PartialEquiv.monotone_symm, FirstOrder.Language.FGEquiv.symm, And.intro, Exists.intro
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
h : L.IsExtensionPair M N
f : L.FGEquiv N M
m : M
g : L.FGEquiv M N
h1 : m ∈ (↑g : M ≃ₚ[L] N).dom
h2 : f.symm ≤ g
⊢ ∃ (g : L.FGEquiv N M), m ∈ (↑g : N ≃ₚ[L] M).cod ∧ f ≤ g

Tactic:
exact ⟨g.symm, h1, monotone_symm h2⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
h : ∀ (f : L.FGEquiv N M) (m : M), ∃ (g : L.FGEquiv N M), m ∈ (↑g : N ≃ₚ[L] M).cod ∧ f ≤ g
f : L.FGEquiv M N
m : M
refine_2 :
  ∀ (g : L.FGEquiv N M) (h1 : m ∈ (↑g : N ≃ₚ[L] M).cod) (h2 : f.symm ≤ g),
    ∃ (g : L.FGEquiv M N), m ∈ (↑g : M ≃ₚ[L] N).dom ∧ f ≤ g
⊢ ∃ (g : L.FGEquiv M N), m ∈ (↑g : M ≃ₚ[L] N).dom ∧ f ≤ g

Tactic:
obtain ⟨g, h1, h2⟩ := h f.symm m

Premises used: FirstOrder.Language.FGEquiv.symm
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
h : ∀ (f : L.FGEquiv N M) (m : M), ∃ (g : L.FGEquiv N M), m ∈ (↑g : N ≃ₚ[L] M).cod ∧ f ≤ g
f : L.FGEquiv M N
m : M
g : L.FGEquiv N M
h1 : m ∈ (↑g : N ≃ₚ[L] M).cod
h2 : f.symm ≤ g
⊢ ∃ (g : L.FGEquiv M N), m ∈ (↑g : M ≃ₚ[L] N).dom ∧ f ≤ g

Tactic:
⟨g.symm, h1, monotone_symm h2⟩

Premises used: FirstOrder.Language.PartialEquiv.monotone_symm, FirstOrder.Language.FGEquiv.symm, And.intro, Exists.intro
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
h : ∀ (f : L.FGEquiv N M) (m : M), ∃ (g : L.FGEquiv N M), m ∈ (↑g : N ≃ₚ[L] M).cod ∧ f ≤ g
f : L.FGEquiv M N
m : M
g : L.FGEquiv N M
h1 : m ∈ (↑g : N ≃ₚ[L] M).cod
h2 : f.symm ≤ g
⊢ ∃ (g : L.FGEquiv M N), m ∈ (↑g : M ≃ₚ[L] N).dom ∧ f ≤ g

Tactic:
exact ⟨g.symm, h1, monotone_symm h2⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
⊢ L.IsExtensionPair M N ↔
    ∀ (S : L.Substructure M),
      S.FG →
        ∀ (f : Embedding.{u, v, w, w'} L (↥S) N) (m : M),
          ∃ (g : Embedding.{u, v, w, w'} L (↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S)) N),
            f = g.comp (Substructure.inclusion ⋯)

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

Premises used: FirstOrder.Language.PartialEquiv.dom, Membership.mem, Exists, _private.0.FirstOrder.Language.isExtensionPair_iff_exists_embedding_closure_singleton_sup.match_1, LE.le, And, Iff.intro, Subtype.val
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
refine_1 :
  ∀ (h : L.IsExtensionPair M N) (S : L.Substructure M) (S_FG : S.FG) (f : Embedding.{u, v, w, w'} L (↥S) N) (m : M),
    ∃ (g : Embedding.{u, v, w, w'} L (↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S)) N),
      f = g.comp (Substructure.inclusion ⋯)
refine_2 :
  ∀
    (h :
      ∀ (S : L.Substructure M),
        S.FG →
          ∀ (f : Embedding.{u, v, w, w'} L (↥S) N) (m : M),
            ∃ (g : Embedding.{u, v, w, w'} L (↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S)) N),
              f = g.comp (Substructure.inclusion ⋯))
    (x : L.FGEquiv M N) (m : M) (f : M ≃ₚ[L] N) (f_FG : f.dom.FG),
    ∃ (g : L.FGEquiv M N), m ∈ (↑g : M ≃ₚ[L] N).dom ∧ Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG ≤ g
⊢ L.IsExtensionPair M N ↔
    ∀ (S : L.Substructure M),
      S.FG →
        ∀ (f : Embedding.{u, v, w, w'} L (↥S) N) (m : M),
          ∃ (g : Embedding.{u, v, w, w'} L (↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S)) N),
            f = g.comp (Substructure.inclusion ⋯)

Tactic:
refine ⟨fun h S S_FG f m => ?_, fun h ⟨f, f_FG⟩ m => ?_⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : Embedding.{u, v, w, w'} L (↥S) N
m : M
refine_1 :
  ∀ (f' : M ≃ₚ[L] N) (hf' : f'.dom.FG)
    (mf' : m ∈ (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).dom)
    (ff'1 :
      (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] N } S_FG) :
            M ≃ₚ[L] N).dom ≤
        (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).dom)
    (ff'2 :
      (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).cod.subtype.comp
          ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).toEquiv.toEmbedding.comp
            (Substructure.inclusion ff'1)) =
        (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                      { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] N } S_FG) :
                  M ≃ₚ[L] N).cod.subtype.comp
          (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                    { dom := S, cod := f.toHom.range, toEquiv := f.equivRange } S_FG) :
                M ≃ₚ[L] N).toEquiv.toEmbedding),
    ∃ (g : Embedding.{u, v, w, w'} L (↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S)) N),
      f = g.comp (Substructure.inclusion ⋯)
⊢ ∃ (g : Embedding.{u, v, w, w'} L (↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S)) N),
    f = g.comp (Substructure.inclusion ⋯)

Tactic:
obtain ⟨⟨f', hf'⟩, mf', ff'1, ff'2⟩ := h ⟨⟨S, _, f.equivRange⟩, S_FG⟩ m

Premises used: Subtype.mk, FirstOrder.Language.Embedding.equivRange, FirstOrder.Language.PartialEquiv.mk
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : Embedding.{u, v, w, w'} L (↥S) N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).dom
ff'1 :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
            { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] N } S_FG) :
        M ≃ₚ[L] N).dom ≤
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).dom
ff'2 :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).cod.subtype.comp
      ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).toEquiv.toEmbedding.comp
        (Substructure.inclusion ff'1)) =
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                  { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] N } S_FG) :
              M ≃ₚ[L] N).cod.subtype.comp
      (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) { dom := S, cod := f.toHom.range, toEquiv := f.equivRange }
                S_FG) :
            M ≃ₚ[L] N).toEquiv.toEmbedding
⊢ ∃ (g : Embedding.{u, v, w, w'} L (↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S)) N),
    f = g.comp (Substructure.inclusion ⋯)

Tactic:
⟨f'.toEmbedding.comp (Substructure.inclusion ?_), ?_⟩

Premises used: FirstOrder.Language.Embedding.comp, FirstOrder.Language.PartialEquiv.toEmbedding, FirstOrder.Language.Substructure.inclusion, Exists.intro
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : Embedding.{u, v, w, w'} L (↥S) N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).dom
ff'1 :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
            { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] N } S_FG) :
        M ≃ₚ[L] N).dom ≤
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).dom
ff'2 :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).cod.subtype.comp
      ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).toEquiv.toEmbedding.comp
        (Substructure.inclusion ff'1)) =
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                  { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] N } S_FG) :
              M ≃ₚ[L] N).cod.subtype.comp
      (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) { dom := S, cod := f.toHom.range, toEquiv := f.equivRange }
                S_FG) :
            M ≃ₚ[L] N).toEquiv.toEmbedding
refine_1 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S ≤ f'.dom
refine_1₁ :
  f =
    Embedding.comp (N := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S))
      (f'.toEmbedding.comp (Substructure.inclusion ⋯)) (Substructure.inclusion ⋯)
⊢ ∃ (g : Embedding.{u, v, w, w'} L (↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S)) N),
    f = g.comp (Substructure.inclusion ⋯)

Tactic:
refine ⟨f'.toEmbedding.comp (Substructure.inclusion ?_), ?_⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : Embedding.{u, v, w, w'} L (↥S) N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).dom
ff'1 :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
            { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] N } S_FG) :
        M ≃ₚ[L] N).dom ≤
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).dom
ff'2 :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).cod.subtype.comp
      ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).toEquiv.toEmbedding.comp
        (Substructure.inclusion ff'1)) =
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                  { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] N } S_FG) :
              M ≃ₚ[L] N).cod.subtype.comp
      (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) { dom := S, cod := f.toHom.range, toEquiv := f.equivRange }
                S_FG) :
            M ≃ₚ[L] N).toEquiv.toEmbedding
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S ≤ f'.dom

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

Premises used: Set.singleton_subset_iff, and_self, sup_le_iff, SetLike.mem_coe, FirstOrder.Language.Substructure.closure_le
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : Embedding.{u, v, w, w'} L (↥S) N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).dom
ff'1 :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
            { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] N } S_FG) :
        M ≃ₚ[L] N).dom ≤
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).dom
ff'2 :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).cod.subtype.comp
      ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f' hf') : M ≃ₚ[L] N).toEquiv.toEmbedding.comp
        (Substructure.inclusion ff'1)) =
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                  { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] N } S_FG) :
              M ≃ₚ[L] N).cod.subtype.comp
      (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) { dom := S, cod := f.toHom.range, toEquiv := f.equivRange }
                S_FG) :
            M ≃ₚ[L] N).toEquiv.toEmbedding
refine_1 :
  ∀ (x : M) (hx : x ∈ S),
    Eq.{w' + 1} (α := N) ((f : (a : ↥S) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx) : N)
      ((Embedding.comp (N := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S))
              (f'.toEmbedding.comp (Substructure.inclusion ⋯)) (Substructure.inclusion ⋯) :
            (a : ↥S) → N)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx) :
        N)
⊢ f =
    Embedding.comp (N := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S))
      (f'.toEmbedding.comp (Substructure.inclusion ⋯)) (Substructure.inclusion ⋯)

Tactic:
ext ⟨x, hx⟩