awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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 :
  g
      (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) =
    g f'
⊢ (↑(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) =
    (↑f' : M ≃ₚ[L] M)
have a : ∀ (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 sorry) :
          ↥(↑f' : M ≃ₚ[L] M).cod) :
      M)
Tactic: apply PartialEquiv.ext (by rfl)
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
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 :
  g
      (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) =
    g f'
⊢ ∀ (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)
have h₁ : cod_f.subtype.toHom.comp equiv_f.toHom = (↑f' : M ≃ₚ[L] M).cod.subtype.toHom.comp (↑f' : M ≃ₚ[L] M).toEquiv.toHom
Tactic: simp only [g, Sigma.mk.inj_iff, heq_eq_eq, true_and] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
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)
⊢ Countable.{w + 1} (L.FGEquiv M M)
have g_inj : 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⟩
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
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
⊢ Countable.{w + 1} (L.FGEquiv M M)
have this : ∀ (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)
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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 → ↥⊥
⊢ RelMap.{u, v, w'} (M := ↥⊥) r ((fun (a : ↥⊥) ↦ isEmptyElim (p := fun (x : ↥⊥) ↦ ↥⊥) a) ∘ x) ↔ RelMap r x
have 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
Tactic: cases n
Cleared hypotheses: n, r, x
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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
⊢ RelMap.{u, v, w'} (M := ↥⊥) r ((fun (a : ↥⊥) ↦ isEmptyElim (p := fun (x : ↥⊥) ↦ ↥⊥) a) ∘ x) ↔ RelMap r x
have 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
Tactic: cases n
Cleared hypotheses: n, r, x
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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
have 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
Tactic: refine Iff.intro ?_ ?_
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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
⊢ L.IsExtensionPair M N ↔ ∀ (f : L.FGEquiv N M) (m : M), ∃ (g : L.FGEquiv N M), m ∈ (↑g : N ≃ₚ[L] M).cod ∧ f ≤ g
have 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
Tactic: refine Iff.intro ?_ ?_
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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 N M), m ∈ (↑g : N ≃ₚ[L] M).cod ∧ f ≤ g
have 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
Tactic: obtain ⟨g, h1, h2⟩ := h f.symm m
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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 M N), m ∈ (↑g : M ≃ₚ[L] N).dom ∧ f ≤ g
have 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
Tactic: obtain ⟨g, h1, h2⟩ := h f.symm m
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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 ⋯)
have 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 sorry)
Tactic: refine ⟨fun h S S_FG f m => ?_, fun h ⟨f, f_FG⟩ m => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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 ⋯)
⊢ 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 ⋯)
have 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 sorry))
  (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
Tactic: refine ⟨fun h S S_FG f m => ?_, fun h ⟨f, f_FG⟩ m => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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
⊢ ∃ (g : Embedding.{u, v, w, w'} L (↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S)) N),
    f = g.comp (Substructure.inclusion ⋯)
have 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 sorry)
Tactic: obtain ⟨⟨f', hf'⟩, mf', ff'1, ff'2⟩ := h ⟨⟨S, _, f.equivRange⟩, S_FG⟩ m
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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 ⋯)
have refine_1 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S ≤ f'.dom
Tactic: refine ⟨f'.toEmbedding.comp (Substructure.inclusion ?_), ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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
⊢ ∃ (g : Embedding.{u, v, w, w'} L (↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S)) N),
    f = g.comp (Substructure.inclusion ⋯)
have refine_1₁ : f =
  Embedding.comp (N := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S))
    (f'.toEmbedding.comp (Substructure.inclusion sorry)) (Substructure.inclusion sorry)
Tactic: refine ⟨f'.toEmbedding.comp (Substructure.inclusion ?_), ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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
⊢ f =
    Embedding.comp (N := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ S))
      (f'.toEmbedding.comp (Substructure.inclusion ⋯)) (Substructure.inclusion ⋯)
have 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 sorry)) (Substructure.inclusion sorry) :
          (a : ↥S) → N)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx) :
      N)
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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
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)
have refine_1 : ∀
  (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)) =
      f)
  (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 sorry)) (Substructure.inclusion sorry) :
          (a : ↥S) → N)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ S) x hx) :
      N)
Tactic: rw [Embedding.subtype_equivRange] at ff'2
Cleared hypotheses: ff'2, x, hx
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
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
have refine_2 : ∀ (f' : Embedding.{u, v, w, w'} L (↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m} ⊔ f.dom)) N)
  (eq_f' : f.toEmbedding = f'.comp (Substructure.inclusion sorry)),
  ∃ (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
Tactic: obtain ⟨f', eq_f'⟩ := h f.dom f_FG f.toEmbedding m