awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
f g : M ≃ₚ[L] N
h_dom : f.dom = g.dom
h :
  ∀ (x : M) (h : 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) : ↥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
have rcases : ∀ (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 = g.dom)
  (h :
    ∀ (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)
        ((g.cod.subtype : (a : ↥g.cod) → N)
            ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x sorry) : ↥g.cod) :
          N)),
  { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g
Tactic: rcases f with ⟨dom_f, cod_f, equiv_f⟩
Cleared hypotheses: f, h_dom, h
-- 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
g : M ≃ₚ[L] 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 = g.dom
h :
  ∀ (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)
      ((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)
⊢ { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g
have refl : ∀ (equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f)
  (h :
    ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
      Eq (α := N)
        (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
              (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod) → N)
            (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                  (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) →
                    ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod)
                (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x
                  h) :
              ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.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 sorry) : ↥g.cod) :
          N)),
  { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g
Tactic: cases h_dom
Cleared hypotheses: dom_f, equiv_f, h_dom, h
-- 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
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    Eq (α := N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod) → N)
          (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) →
                  ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x
                h) :
            ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.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)
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g
have refl : { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } ≤ g
Tactic: apply le_antisymm
-- 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
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    Eq (α := N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod) → N)
          (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) →
                  ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x
                h) :
            ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.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)
refl : { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } ≤ g
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g
have refl₁ : g ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f }
Tactic: apply le_antisymm
-- 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
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    Eq (α := N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod) → N)
          (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) →
                  ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x
                h) :
            ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.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)
⊢ ∃ (h : { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom ≤ g.dom),
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion h)) =
      { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
        { dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding
have h₁ : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion sorry)) =
  { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding
Tactic: use le_rfl
-- 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
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    Eq (α := N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod) → N)
          (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) →
                  ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x
                h) :
            ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.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)
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) =
    { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
      { dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding
have h₁ : ∀ (x : M) (hx : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
  Eq.{w' + 1} (α := N)
    ((g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion sorry)) :
          (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) → N)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x hx) :
      N)
    (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
            { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv.toEmbedding :
          (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) → N)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) 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
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    Eq (α := N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod) → N)
          (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) →
                  ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x
                h) :
            ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.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)
⊢ ∃ (h : g.dom ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv.toEmbedding.comp (inclusion h)) =
      g.cod.subtype.comp g.toEquiv.toEmbedding
have h₁ : { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
    ({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv.toEmbedding.comp (inclusion sorry)) =
  g.cod.subtype.comp g.toEquiv.toEmbedding
Tactic: use le_rfl
-- 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
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    Eq (α := N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod) → N)
          (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) →
                  ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x
                h) :
            ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.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)
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
      ({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv.toEmbedding.comp (inclusion ⋯)) =
    g.cod.subtype.comp g.toEquiv.toEmbedding
have h₁ : ∀ (x : M) (hx : x ∈ g.dom),
  Eq.{w' + 1} (α := N)
    (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
            ({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv.toEmbedding.comp (inclusion sorry)) :
          (a : ↥g.dom) → N)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x hx) :
      N)
    ((g.cod.subtype.comp g.toEquiv.toEmbedding : (a : ↥g.dom) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) 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
f g : M ≃ₚ[L] N
⊢ f = g ↔
    ∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : 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) : ↥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)
have mp : f = g →
  ∃ (h_dom : f.dom = g.dom),
    ∀ (x : M) (h : 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) : ↥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 sorry) : ↥g.cod) :
          N)
Tactic: constructor
-- 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
f g : M ≃ₚ[L] N
mp :
  f = g →
    ∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : 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) : ↥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 ↔
    ∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : 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) : ↥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)
have mpr : (∃ (h_dom : f.dom = g.dom),
    ∀ (x : M) (h : 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) : ↥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 sorry) : ↥g.cod) :
          N)) →
  f = g
Tactic: constructor
-- 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
f g : M ≃ₚ[L] N
h_eq : f = g
⊢ ∃ (h_dom : f.dom = g.dom),
    ∀ (x : M) (h : 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) : ↥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)
have mp : ∀ (dom_f : L.Substructure M) (cod_f : L.Substructure N) (equiv_f : Equiv.{u, v, w, w'} L ↥dom_f ↥cod_f)
  (h_eq : { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g),
  ∃ (h_dom : { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom = g.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)
        ((g.cod.subtype : (a : ↥g.cod) → N)
            ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x sorry) : ↥g.cod) :
          N)
Tactic: rcases f with ⟨dom_f, cod_f, equiv_f⟩
Cleared hypotheses: f, h_eq
-- 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
g : M ≃ₚ[L] N
dom_f : L.Substructure M
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥dom_f ↥cod_f
h_eq : { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g
⊢ ∃ (h_dom : { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom = g.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)
        ((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)
have mp : ∃ (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
                sorry) :
            ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
        N)
Tactic: cases h_eq
Cleared hypotheses: g, h_eq
-- 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
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)) =
    f.cod.subtype.comp f.toEquiv.toEmbedding
have rw : (g.domRestrict hg).cod.subtype.comp ((g.domRestrict hg).toEquiv.toEmbedding.comp (inclusion hf)) =
  g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion sorry))
Tactic: rw [← (subtype_toEquiv_inclusion hfg)]
-- 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
f : M ≃ₚ[L] N
h : f.dom = ⊤
m : M
⊢ 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)
have 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 sorry)) :
        N) :
      N)
Tactic: rcases f with ⟨dom, cod, g⟩
Cleared hypotheses: f, h