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_f : L.Substructure M
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥dom_f ↥cod_f
⊢ ∃ (h_dom :
    { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom =
      { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    ∀ (x : M) (h : x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
      Eq (α := N)
        (({ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
              (a : ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod) → N)
            (({ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                  (a : ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom) →
                    ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod)
                (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom)
                  x h) :
              ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
          N)
        (({ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
              (a : ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod) → N)
            (({ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                  (a : ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom) →
                    ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod)
                (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom)
                  x ⋯) :
              ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
          N)

Tactic:
exact ⟨rfl, fun _ _ ↦ rfl⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f g : M ≃ₚ[L] N
h : f.dom = g.dom
H :
  ∀ (x : M) (h_1 : x ∈ f.dom),
    Eq (α := N)
      ((f.cod.subtype : (a : ↥f.cod) → N)
          ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.dom) x h_1) : ↥f.cod) :
        N)
      ((g.cod.subtype : (a : ↥g.cod) → N)
          ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
        N)
⊢ f = g

Tactic:
ext h H

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
f g : M ≃ₚ[L] N
h : f.dom = g.dom
H :
  ∀ (x : M) (h_1 : x ∈ f.dom),
    Eq (α := N)
      ((f.cod.subtype : (a : ↥f.cod) → N)
          ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.dom) x h_1) : ↥f.cod) :
        N)
      ((g.cod.subtype : (a : ↥g.cod) → N)
          ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
        N)
⊢ f = g

Tactic:
exact ext h H

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
⊢ Monotone (β := L.Substructure M) fun (f : M ≃ₚ[L] N) ↦ f.dom

Tactic:
fun _ _ ↦ dom_le_dom

Premises used: FirstOrder.Language.PartialEquiv.dom_le_dom, Set.Mem, Monotone
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
⊢ Monotone (β := L.Substructure N) fun (f : M ≃ₚ[L] N) ↦ f.cod

Tactic:
fun _ _ ↦ cod_le_cod

Premises used: Set.Mem, Monotone, FirstOrder.Language.PartialEquiv.cod_le_cod
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃ₚ[L] N
A : L.Substructure M
h : A ≤ f.dom
g : Embedding.{u, v, w, w'} L (↥A) N := f.cod.subtype.comp (f.toEquiv.toEmbedding.comp (inclusion h))
⊢ M ≃ₚ[L] N

Tactic:
exact {
    dom := A
    cod := g.toHom.range
    toEquiv := g.equivRange
  }
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃ₚ[L] N
A : L.Substructure M
h : A ≤ f.dom
⊢ f.domRestrict h ≤ f

Tactic:
⟨h, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f g : M ≃ₚ[L] N
A : L.Substructure M
hf : f.dom ≤ A
hg : A ≤ g.dom
hfg : f ≤ g
rw :
  (g.domRestrict hg).cod.subtype.comp ((g.domRestrict hg).toEquiv.toEmbedding.comp (inclusion hf)) =
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯))
⊢ (g.domRestrict hg).cod.subtype.comp ((g.domRestrict hg).toEquiv.toEmbedding.comp (inclusion hf)) =
    f.cod.subtype.comp f.toEquiv.toEmbedding

Tactic:
rw [← (subtype_toEquiv_inclusion hfg)]

Premises used: FirstOrder.Language.PartialEquiv.subtype_toEquiv_inclusion
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f g : M ≃ₚ[L] N
A : L.Substructure M
hf : f.dom ≤ A
hg : A ≤ g.dom
hfg : f ≤ g
⊢ (g.domRestrict hg).cod.subtype.comp ((g.domRestrict hg).toEquiv.toEmbedding.comp (inclusion hf)) =
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯))

Tactic:
rfl
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃ₚ[L] N
A : L.Substructure N
h : A ≤ f.cod
⊢ f.codRestrict h ≤ f

Tactic:
symm_le_iff.2 (f.symm.domRestrict_le h)

Premises used: Iff.mpr, FirstOrder.Language.PartialEquiv.symm, Set.Mem, FirstOrder.Language.PartialEquiv.domRestrict_le, FirstOrder.Language.PartialEquiv.symm_le_iff
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f g : M ≃ₚ[L] N
A : L.Substructure N
hf : f.cod ≤ A
hg : A ≤ g.cod
hfg : f ≤ g
⊢ f ≤ g.codRestrict hg

Tactic:
symm_le_iff.1 (le_domRestrict f.symm g.symm hf hg (monotone_symm hfg))

Premises used: FirstOrder.Language.PartialEquiv.monotone_symm, FirstOrder.Language.PartialEquiv.symm, Set.Mem, FirstOrder.Language.PartialEquiv.le_domRestrict, FirstOrder.Language.PartialEquiv.symm_le_iff, Iff.mp
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃ₚ[L] N
m : ↥f.dom
⊢ Eq.{w' + 1} (α := N) ((f.toEmbedding : (a : ↥f.dom) → N) m : N) ((↑((f.toEquiv : (a : ↥f.dom) → ↥f.cod) m) : N) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃ₚ[L] N
h : f.dom = ⊤
m : M
rcases :
  ∀ (dom : L.Substructure M) (cod : L.Substructure N) (g : Equiv.{u, v, w, w'} L ↥dom ↥cod)
    (h : { dom := dom, cod := cod, toEquiv := g : M ≃ₚ[L] N }.dom = ⊤),
    Eq.{w' + 1} (α := N) ((toEmbeddingOfEqTop h : (a : M) → N) m : N)
      ((↑(({ dom := dom, cod := cod, toEquiv := g : M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := dom, cod := cod, toEquiv := g }.dom) → ↥{ dom := dom, cod := cod, toEquiv := g }.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := dom, cod := cod, toEquiv := g : M ≃ₚ[L] N }.dom) m ⋯)) :
          N) :
        N)
⊢ Eq.{w' + 1} (α := N) ((toEmbeddingOfEqTop h : (a : M) → N) m : N)
    ((↑((f.toEquiv : (a : ↥f.dom) → ↥f.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.dom) m ⋯)) : N) : N)

Tactic:
rcases f with ⟨dom, cod, g⟩

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

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
m : M
cod : L.Substructure N
g : Equiv.{u, v, w, w'} L ↥{ carrier := Set.univ, fun_mem := ⋯ } ↥cod
⊢ Eq.{w' + 1} (α := N) ((toEmbeddingOfEqTop ⋯ : (a : M) → N) m : N)
    ((↑(({ dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := g :
                  M ≃ₚ[L] N }.toEquiv :
              (a : ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := g }.dom) →
                ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := g }.cod)
            (Subtype.mk (p := fun (x : M) ↦
              x ∈
                { dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := g :
                    M ≃ₚ[L] N }.dom)
              m ⋯)) :
        N) :
      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
f : M ≃ₚ[L] N
h_dom : f.dom = ⊤
h_cod : f.cod = ⊤
rcases :
  ∀ (dom : L.Substructure M) (cod : L.Substructure N) (g : Equiv.{u, v, w, w'} L ↥dom ↥cod)
    (h_dom : { dom := dom, cod := cod, toEquiv := g : M ≃ₚ[L] N }.dom = ⊤)
    (h_cod : { dom := dom, cod := cod, toEquiv := g : M ≃ₚ[L] N }.cod = ⊤),
    (toEquivOfEqTop h_dom h_cod).toEmbedding = toEmbeddingOfEqTop h_dom
⊢ (toEquivOfEqTop h_dom h_cod).toEmbedding = toEmbeddingOfEqTop h_dom

Tactic:
rcases f with ⟨dom, cod, g⟩

Premises used: FirstOrder.Language.PartialEquiv.dom, FirstOrder.Language.PartialEquiv.cod
-- 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
g : Equiv.{u, v, w, w'} L ↥dom ↥cod
h_dom : { dom := dom, cod := cod, toEquiv := g : M ≃ₚ[L] N }.dom = ⊤
h_cod : { dom := dom, cod := cod, toEquiv := g : M ≃ₚ[L] N }.cod = ⊤
refl :
  ∀ (g : Equiv.{u, v, w, w'} L ↥{ carrier := Set.univ, fun_mem := ⋯ } ↥cod)
    (h_cod :
      { dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := g : M ≃ₚ[L] N }.cod =
        ⊤),
    (toEquivOfEqTop ⋯ h_cod).toEmbedding = toEmbeddingOfEqTop ⋯
⊢ (toEquivOfEqTop h_dom h_cod).toEmbedding = toEmbeddingOfEqTop h_dom

Tactic:
cases h_dom
-- 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
g : Equiv.{u, v, w, w'} L ↥{ carrier := Set.univ, fun_mem := ⋯ } ↥cod
h_cod :
  { dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := g : M ≃ₚ[L] N }.cod = ⊤
refl :
  ∀ (g : Equiv.{u, v, w, w'} L ↥{ carrier := Set.univ, fun_mem := ⋯ } ↥{ carrier := Set.univ, fun_mem := ⋯ }),
    (toEquivOfEqTop ⋯ ⋯).toEmbedding = toEmbeddingOfEqTop ⋯
⊢ (toEquivOfEqTop ⋯ h_cod).toEmbedding = toEmbeddingOfEqTop ⋯

Tactic:
cases h_cod
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : Equiv.{u, v, w, w'} L ↥{ carrier := Set.univ, fun_mem := ⋯ } ↥{ carrier := Set.univ, fun_mem := ⋯ }
⊢ (toEquivOfEqTop ⋯ ⋯).toEmbedding = toEmbeddingOfEqTop ⋯

Tactic:
rfl
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
inst : L.Structure M
N : Type u_1
inst_1 : L.Structure N
f : M ≃ₚ[L] N
rw : Structure.FG.{w, u, v} L ↥f.dom ↔ f.cod.FG
rw₁ : Structure.FG.{u_1, u, v} L ↥f.cod ↔ f.cod.FG
rw₂ rw₃ : Structure.FG.{u_1, u, v} L ↥f.cod ↔ Structure.FG.{u_1, u, v} L ↥f.cod
⊢ f.dom.FG ↔ f.cod.FG

Tactic:
rw [Substructure.fg_iff_structure_fg, f.toEquiv.fg_iff, Substructure.fg_iff_structure_fg]

Premises used: FirstOrder.Language.PartialEquiv.toEquiv, FirstOrder.Language.Equiv.fg_iff, FirstOrder.Language.Substructure.fg_iff_structure_fg
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
a₁ : M ↪[L] N
_ :
  ∀ ⦃a₂ : M ↪[L] N⦄,
    Eq (α := M ≃ₚ[L] N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂) →
      a₁ = a₂
⊢ ∀ ⦃a₂ : M ↪[L] N⦄,
    Eq (α := M ≃ₚ[L] N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂) →
      a₁ = a₂

Tactic:
_
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
a₁ a₂ : M ↪[L] N
h : Eq (α := M ≃ₚ[L] N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂)
h₁ : ∀ (x : M), Eq.{w' + 1} (α := N) ((a₁ : (a : M) → N) x : N) ((a₂ : (a : M) → N) x : N)
⊢ a₁ = a₂

Tactic:
ext
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
a₁ a₂ : M ↪[L] N
h : Eq (α := M ≃ₚ[L] N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂)
x : M
h₁ :
  ∀
    (h :
      ∃ (h_dom :
        Eq.{w + 1} (α := L.Substructure M)
          (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁))
          (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂))),
        ∀ (x : M)
          (h :
            Membership.mem (γ := L.Substructure M)
              (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) x),
          Eq.{w' + 1} (α := N)
            ((subtype (PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) :
                  (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).cod) → N)
                ((PartialEquiv.toEquiv ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁) :
                      (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).dom) →
                        ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).cod)
                    (Subtype.mk (p := fun (x : M) ↦
                      Membership.mem (γ := L.Substructure M)
                        (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) x)
                      x h) :
                  ↥(PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁))) :
              N)
            ((subtype (PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂)) :
                  (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).cod) → N)
                ((PartialEquiv.toEquiv ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂) :
                      (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).dom) →
                        ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).cod)
                    (Subtype.mk (p := fun (x : M) ↦
                      Membership.mem (γ := L.Substructure M)
                        (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂)) x)
                      x ⋯) :
                  ↥(PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂))) :
              N))
    (x : M), Eq.{w' + 1} (α := N) ((a₁ : (a : M) → N) x : N) ((a₂ : (a : M) → N) x : N)
⊢ Eq.{w' + 1} (α := N) ((a₁ : (a : M) → N) x : N) ((a₂ : (a : M) → N) x : N)

Tactic:
rw [PartialEquiv.ext_iff] at h

Premises used: FirstOrder.Language.PartialEquiv.ext_iff
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
a₁ a₂ : M ↪[L] N
h :
  ∃ (h_dom :
    Eq.{w + 1} (α := L.Substructure M)
      (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁))
      (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂))),
    ∀ (x : M)
      (h :
        Membership.mem (γ := L.Substructure M)
          (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) x),
      Eq.{w' + 1} (α := N)
        ((subtype (PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) :
              (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).cod) → N)
            ((PartialEquiv.toEquiv ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁) :
                  (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).dom) →
                    ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).cod)
                (Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := L.Substructure M)
                    (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) x)
                  x h) :
              ↥(PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁))) :
          N)
        ((subtype (PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂)) :
              (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).cod) → N)
            ((PartialEquiv.toEquiv ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂) :
                  (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).dom) →
                    ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).cod)
                (Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := L.Substructure M)
                    (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂)) x)
                  x ⋯) :
              ↥(PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂))) :
          N)
x : M
⊢ Eq.{w + 1} (α := L.Substructure M)
    (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁))
    (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂))

Tactic:
rcases h with ⟨_, H⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
a₁ a₂ : M ↪[L] N
x : M
w :
  Eq.{w + 1} (α := L.Substructure M)
    (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁))
    (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂))
H :
  ∀ (x : M)
    (h :
      Membership.mem (γ := L.Substructure M)
        (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) x),
    Eq.{w' + 1} (α := N)
      ((subtype (PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) :
            (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).cod) → N)
          ((PartialEquiv.toEquiv ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁) :
                (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).dom) →
                  ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).cod)
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := L.Substructure M)
                  (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) x)
                x h) :
            ↥(PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁))) :
        N)
      ((subtype (PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂)) :
            (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).cod) → N)
          ((PartialEquiv.toEquiv ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂) :
                (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).dom) →
                  ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).cod)
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := L.Substructure M)
                  (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂)) x)
                x ⋯) :
            ↥(PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂))) :
        N)
⊢ Eq.{w' + 1} (α := N) ((a₁ : (a : M) → N) x : N) ((a₂ : (a : M) → N) x : N)

Tactic:
H _ (Substructure.mem_top _)

Premises used: FirstOrder.Language.Substructure.mem_top
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
a₁ a₂ : M ↪[L] N
x : M
w :
  Eq.{w + 1} (α := L.Substructure M)
    (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁))
    (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂))
H :
  ∀ (x : M)
    (h :
      Membership.mem (γ := L.Substructure M)
        (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) x),
    Eq.{w' + 1} (α := N)
      ((subtype (PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) :
            (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).cod) → N)
          ((PartialEquiv.toEquiv ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁) :
                (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).dom) →
                  ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).cod)
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := L.Substructure M)
                  (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) x)
                x h) :
            ↥(PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁))) :
        N)
      ((subtype (PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂)) :
            (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).cod) → N)
          ((PartialEquiv.toEquiv ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂) :
                (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).dom) →
                  ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).cod)
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := L.Substructure M)
                  (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂)) x)
                x ⋯) :
            ↥(PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂))) :
        N)
⊢ Eq.{w' + 1} (α := N) ((a₁ : (a : M) → N) x : N) ((a₂ : (a : M) → N) x : N)

Tactic:
exact H _ (Substructure.mem_top _)

Premises used: FirstOrder.Language.Substructure.mem_top
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
⊢ PartialEquiv.toEmbeddingOfEqTop (f := f.toPartialEquiv) ⋯ = f

Tactic:
rfl

Premises used: FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop, FirstOrder.Language.Embedding.comp, rfl
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃ₚ[L] N
h : f.dom = ⊤
rcases :
  ∀ (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 = ⊤),
    (PartialEquiv.toEmbeddingOfEqTop h).toPartialEquiv = { dom := dom, cod := cod, toEquiv := toEquiv }
⊢ (PartialEquiv.toEmbeddingOfEqTop h).toPartialEquiv = f

Tactic:
rcases f with ⟨_, _, _⟩