awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
dom : L.Substructure M
cod : L.Substructure N
toEquiv : Equiv.{u, v, w, w'} L ↥dom ↥cod
h : { dom := dom, cod := cod, toEquiv := toEquiv : M ≃ₚ[L] N }.dom = ⊤
refl :
  ∀ (toEquiv : Equiv.{u, v, w, w'} L ↥{ carrier := Set.univ, fun_mem := ⋯ } ↥cod),
    (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv =
      { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := toEquiv }
⊢ (PartialEquiv.toEmbeddingOfEqTop h).toPartialEquiv = { dom := dom, cod := cod, toEquiv := toEquiv }

Tactic:
cases h
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
cod : L.Substructure N
toEquiv : Equiv.{u, v, w, w'} L ↥{ carrier := Set.univ, fun_mem := ⋯ } ↥cod
refl :
  ∀ (x : M) (h : x ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom),
    Eq (α := N)
      (((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod.subtype :
            (a : ↥(PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod) → N)
          (((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.toEquiv :
                (a : ↥(PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom) →
                  ↥(PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom) x h) :
            ↥(PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod) :
        N)
      (({ dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                  M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := toEquiv }.cod) → N)
          (({ dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                    M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := toEquiv }.dom) →
                  ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := toEquiv }.cod)
              (Subtype.mk (p := fun (x : M) ↦
                x ∈
                  { dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                      M ≃ₚ[L] N }.dom)
                x ⋯) :
            ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                  M ≃ₚ[L] N }.cod) :
        N)
refl₁ :
  (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom =
    { dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv : M ≃ₚ[L] N }.dom
⊢ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv =
    { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := toEquiv }

Tactic:
apply PartialEquiv.ext

Premises used: FirstOrder.Language.PartialEquiv.ext
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
cod : L.Substructure N
toEquiv : Equiv.{u, v, w, w'} L ↥{ carrier := Set.univ, fun_mem := ⋯ } ↥cod
x : M
h : x ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom
⊢ Eq (α := N)
    (((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod.subtype :
          (a : ↥(PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod) → N)
        (((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.toEquiv :
              (a : ↥(PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom) →
                ↥(PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod)
            (Subtype.mk (p := fun (x : M) ↦ x ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom) x h) :
          ↥(PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod) :
      N)
    (({ dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                M ≃ₚ[L] N }.cod.subtype :
          (a : ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := toEquiv }.cod) → N)
        (({ dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                  M ≃ₚ[L] N }.toEquiv :
              (a : ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := toEquiv }.dom) →
                ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := toEquiv }.cod)
            (Subtype.mk (p := fun (x : M) ↦
              x ∈
                { dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                    M ≃ₚ[L] N }.dom)
              x ⋯) :
          ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                M ≃ₚ[L] N }.cod) :
      N)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
cod : L.Substructure N
toEquiv : Equiv.{u, v, w, w'} L ↥{ carrier := Set.univ, fun_mem := ⋯ } ↥cod
⊢ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom =
    { dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv : M ≃ₚ[L] N }.dom

Tactic:
rfl
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
ι : Type u_1
inst_2 : Preorder ι
inst_3 : Nonempty ι
inst_4 : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
⊢ (partialEquivLimit S).dom = ⨆ (x : ι), dom.{u, v, w, w'} (N := N) ((S : (a : ι) → M ≃ₚ[L] N) x)

Tactic:
rfl

Premises used: iSup, rfl
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
ι : Type u_1
inst_2 : Preorder ι
inst_3 : Nonempty ι
inst_4 : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
⊢ (partialEquivLimit S).cod = ⨆ (x : ι), cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) x)

Tactic:
rfl

Premises used: iSup, rfl
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
ι : Type u_1
inst_2 : Preorder ι
inst_3 : Nonempty ι
inst_4 : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
i : ι
simp :
  Embedding.comp (N :=
      DirectLimit.{u_1, w', u, v} (L := L)
        (fun (i : ι) ↦
          ↥(({ toFun := fun (i : ι) ↦ cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i), monotone' := ⋯ :
                    OrderHom.{u_1, w'} ι (L.Substructure N) } :
                  (a : ι) → L.Substructure N)
                i :
              L.Substructure N))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ inclusion ⋯)
      (Equiv.toEmbedding
        (Equiv_iSup
          { toFun := fun (i : ι) ↦ cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i), monotone' := ⋯ :
            OrderHom.{u_1, w'} ι (L.Substructure N) }))
      (Embedding.comp
        (Equiv.toEmbedding
          (equiv_lift L ι (fun (i : ι) ↦ ↥(dom.{u, v, w, w'} (N := N) ((S : (a : ι) → M ≃ₚ[L] N) i)))
            (fun (x x_1 : ι) (hij : x ≤ x_1) ↦ inclusion ⋯)
            (fun (i : ι) ↦ ↥(cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i)))
            (fun (x x_1 : ι) (hij : x ≤ x_1) ↦ inclusion ⋯) (fun (i : ι) ↦ toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i)) ⋯))
        (Embedding.comp
          (Equiv.toEmbedding
            (Equiv.symm
              (Equiv_iSup
                { toFun := fun (i : ι) ↦ dom.{u, v, w, w'} (N := N) ((S : (a : ι) → M ≃ₚ[L] N) i), monotone' := ⋯ :
                  OrderHom.{u_1, w} ι (L.Substructure M) })))
          (inclusion ⋯))) =
    Embedding.comp (inclusion ⋯) (Equiv.toEmbedding (toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i)))
⊢ (partialEquivLimit S).toEquiv.toEmbedding.comp (inclusion ⋯) =
    Embedding.comp (inclusion ⋯) (Equiv.toEmbedding (toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i)))

Tactic:
simp only [partialEquivLimit, Equiv.comp_toEmbedding, Embedding.comp_assoc]

Premises used: FirstOrder.Language.Equiv.comp_toEmbedding, FirstOrder.Language.DirectLimit.partialEquivLimit, FirstOrder.Language.Embedding.comp_assoc
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
ι : Type u_1
inst_2 : Preorder ι
inst_3 : Nonempty ι
inst_4 : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
i : ι
⊢ Embedding.comp (N :=
      DirectLimit.{u_1, w', u, v} (L := L)
        (fun (i : ι) ↦
          ↥(({ toFun := fun (i : ι) ↦ cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i), monotone' := ⋯ :
                    OrderHom.{u_1, w'} ι (L.Substructure N) } :
                  (a : ι) → L.Substructure N)
                i :
              L.Substructure N))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ inclusion ⋯)
      (Equiv.toEmbedding
        (Equiv_iSup
          { toFun := fun (i : ι) ↦ cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i), monotone' := ⋯ :
            OrderHom.{u_1, w'} ι (L.Substructure N) }))
      (Embedding.comp (N :=
        DirectLimit.{u_1, w, u, v} (L := L) (fun (i : ι) ↦ ↥(dom.{u, v, w, w'} (N := N) ((S : (a : ι) → M ≃ₚ[L] N) i)))
          fun (x x_1 : ι) (hij : x ≤ x_1) ↦ inclusion ⋯)
        (Equiv.toEmbedding
          (equiv_lift L ι (fun (i : ι) ↦ ↥(dom.{u, v, w, w'} (N := N) ((S : (a : ι) → M ≃ₚ[L] N) i)))
            (fun (x x_1 : ι) (hij : x ≤ x_1) ↦ inclusion ⋯)
            (fun (i : ι) ↦ ↥(cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i)))
            (fun (x x_1 : ι) (hij : x ≤ x_1) ↦ inclusion ⋯) (fun (i : ι) ↦ toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i)) ⋯))
        (of.{u_1, w, u, v} L ι
          (fun (x : ι) ↦
            ↥(({ toFun := fun (i : ι) ↦ dom.{u, v, w, w'} (N := N) ((S : (a : ι) → M ≃ₚ[L] N) i), monotone' := ⋯ :
                      OrderHom.{u_1, w} ι (L.Substructure M) } :
                    (a : ι) → L.Substructure M)
                  x :
                L.Substructure M))
          (fun (x x_1 : ι) (h : x ≤ x_1) ↦ inclusion ⋯) i)) =
    Embedding.comp (inclusion ⋯) (Equiv.toEmbedding (toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i)))

Tactic:
congr
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
ι : Type u_1
inst_2 : Preorder ι
inst_3 : Nonempty ι
inst_4 : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
i : ι
simp :
  Eq (α := Embedding.{u, v, w, w'} L (↥(dom.{u, v, w, w'} (N := N) ((S : (a : ι) → M ≃ₚ[L] N) i))) N)
    ((partialEquivLimit S).cod.subtype.comp
      (Embedding.comp (inclusion ⋯) (Equiv.toEmbedding (toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i)))))
    (Embedding.comp (subtype (cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i)))
      (Equiv.toEmbedding (toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i))))
⊢ (partialEquivLimit S).cod.subtype.comp ((partialEquivLimit S).toEquiv.toEmbedding.comp (inclusion ⋯)) =
    Embedding.comp (subtype (cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i)))
      (Equiv.toEmbedding (toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i)))

Tactic:
simp only [partialEquivLimit_comp_inclusion]

Premises used: FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
ι : Type u_1
inst_2 : Preorder ι
inst_3 : Nonempty ι
inst_4 : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
i : ι
⊢ Eq (α := Embedding.{u, v, w, w'} L (↥(dom.{u, v, w, w'} (N := N) ((S : (a : ι) → M ≃ₚ[L] N) i))) N)
    ((partialEquivLimit S).cod.subtype.comp
      (Embedding.comp (inclusion ⋯) (Equiv.toEmbedding (toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i)))))
    (Embedding.comp (subtype (cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i)))
      (Equiv.toEmbedding (toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i))))

Tactic:
simp only [cod_partialEquivLimit, ← Embedding.comp_assoc,
      subtype_comp_inclusion]

Premises used: FirstOrder.Language.Substructure.subtype_comp_inclusion, FirstOrder.Language.Embedding.comp_assoc, FirstOrder.Language.DirectLimit.cod_partialEquivLimit
-- 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
h : g f = g f'
a : (↑f : M ≃ₚ[L] M) = (↑f' : M ≃ₚ[L] M)
⊢ f = f'

Tactic:
ext
-- 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
h : g f = g f'
a :
  ∀ (dom_f cod_f : L.Substructure M) (equiv_f : ↥dom_f ≃[L] ↥cod_f)
    (f_fin : { dom := dom_f, 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 := dom_f, 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 := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] M }
            f_fin) :
        M ≃ₚ[L] M) =
      (↑f' : M ≃ₚ[L] M)
⊢ (↑f : M ≃ₚ[L] M) = (↑f' : M ≃ₚ[L] M)

Tactic:
let ⟨⟨dom_f, cod_f, equiv_f⟩, f_fin⟩ := f
-- 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
dom_f cod_f : L.Substructure M
equiv_f : ↥dom_f ≃[L] ↥cod_f
f_fin : { dom := dom_f, 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 := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] M }
        f_fin) =
    g f'
a :
  ∀ (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)
⊢ (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] M }
          f_fin) :
      M ≃ₚ[L] M) =
    (↑f' : M ≃ₚ[L] M)

Tactic:
cases congr_arg (·.1) h

Premises used: congr_arg
-- 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 :
  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).dom =
    (↑f' : M ≃ₚ[L] M).dom

Tactic:
rfl
-- 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 :
  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'
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 ⋯) :
            ↥(↑f' : 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) =
    (↑f' : M ≃ₚ[L] M)

Tactic:
apply PartialEquiv.ext (by rfl)

Premises used: FirstOrder.Language.PartialEquiv.ext
-- 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 :
  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'
⊢ 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

Premises used: heq_eq_eq, Sigma.mk.inj_iff, true_and
-- 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:
fun x hx ↦ congr_fun (congr_arg (↑) h) ⟨x, hx⟩