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
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 = ⊤
⊢ 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)
have refl : ∀ (g : Equiv.{u, v, w, w'} L ↥{ carrier := Set.univ, fun_mem := sorry } ↥cod),
  Eq.{w' + 1} (α := N) ((toEmbeddingOfEqTop sorry : (a : M) → N) m : N)
    ((↑(({ dom := { carrier := Set.univ, fun_mem := sorry : L.Substructure M }, cod := cod, toEquiv := g :
                  M ≃ₚ[L] N }.toEquiv :
              (a : ↥{ dom := { carrier := Set.univ, fun_mem := sorry }, cod := cod, toEquiv := g }.dom) →
                ↥{ dom := { carrier := Set.univ, fun_mem := sorry }, cod := cod, toEquiv := g }.cod)
            (Subtype.mk (p := fun (x : M) ↦
              x ∈
                { dom := { carrier := Set.univ, fun_mem := sorry : L.Substructure M }, cod := cod, toEquiv := g :
                    M ≃ₚ[L] N }.dom)
              m sorry)) :
        N) :
      N)
Tactic: cases h
Cleared hypotheses: dom, g, 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
f : M ≃ₚ[L] N
h_dom : f.dom = ⊤
h_cod : f.cod = ⊤
⊢ (toEquivOfEqTop h_dom h_cod).toEmbedding = toEmbeddingOfEqTop h_dom
have 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
Tactic: rcases f with ⟨dom, cod, g⟩
Cleared hypotheses: f, h_dom, h_cod
-- 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
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
have refl : ∀ (g : Equiv.{u, v, w, w'} L ↥{ carrier := Set.univ, fun_mem := sorry } ↥cod)
  (h_cod :
    { dom := { carrier := Set.univ, fun_mem := sorry : L.Substructure M }, cod := cod, toEquiv := g : M ≃ₚ[L] N }.cod = ⊤),
  (toEquivOfEqTop sorry h_cod).toEmbedding = toEmbeddingOfEqTop sorry
Tactic: cases h_dom
Cleared hypotheses: dom, g, h_dom, h_cod
-- 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
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 = ⊤
⊢ (toEquivOfEqTop ⋯ h_cod).toEmbedding = toEmbeddingOfEqTop ⋯
have refl : ∀ (g : Equiv.{u, v, w, w'} L ↥{ carrier := Set.univ, fun_mem := sorry } ↥{ carrier := Set.univ, fun_mem := sorry }),
  (toEquivOfEqTop sorry sorry).toEmbedding = toEmbeddingOfEqTop sorry
Tactic: cases h_cod
Cleared hypotheses: cod, g, h_cod
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
N : Type u_1
inst_1 : L.Structure N
f : M ≃ₚ[L] N
⊢ f.dom.FG ↔ f.cod.FG
have rw : Structure.FG.{w, u, v} L ↥f.dom ↔ f.cod.FG
Tactic: rw [Substructure.fg_iff_structure_fg, f.toEquiv.fg_iff, Substructure.fg_iff_structure_fg]
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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
⊢ f.dom.FG ↔ f.cod.FG
have rw₁ : Structure.FG.{u_1, u, v} L ↥f.cod ↔ f.cod.FG
Tactic: rw [Substructure.fg_iff_structure_fg, f.toEquiv.fg_iff, Substructure.fg_iff_structure_fg]
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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
⊢ f.dom.FG ↔ f.cod.FG
have rw₂ : Structure.FG.{u_1, u, v} L ↥f.cod ↔ Structure.FG.{u_1, u, v} L ↥f.cod
Tactic: rw [Substructure.fg_iff_structure_fg, f.toEquiv.fg_iff, Substructure.fg_iff_structure_fg]
-- 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
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₂)
⊢ a₁ = a₂
have h₁ : ∀ (x : M), Eq.{w' + 1} (α := N) ((a₁ : (a : M) → N) x : N) ((a₂ : (a : M) → N) x : N)
Tactic: ext
-- 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
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
⊢ Eq.{w' + 1} (α := N) ((a₁ : (a : M) → N) x : N) ((a₂ : (a : M) → N) x : N)
have 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 sorry) :
                ↥(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)
Tactic: rw [PartialEquiv.ext_iff] at h
Cleared hypotheses: h, x
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
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} (α := N) ((a₁ : (a : M) → N) x : N) ((a₂ : (a : M) → N) x : N)
have 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₂))
Tactic: rcases h with ⟨_, H⟩
Cleared hypotheses: 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
f : M ≃ₚ[L] N
h : f.dom = ⊤
⊢ (PartialEquiv.toEmbeddingOfEqTop h).toPartialEquiv = f
have 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 }
Tactic: rcases f with ⟨_, _, _⟩
Cleared hypotheses: f, 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
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 }
have refl : ∀ (toEquiv : Equiv.{u, v, w, w'} L ↥{ carrier := Set.univ, fun_mem := sorry } ↥cod),
  (PartialEquiv.toEmbeddingOfEqTop sorry).toPartialEquiv =
    { dom := { carrier := Set.univ, fun_mem := sorry }, cod := cod, toEquiv := toEquiv }
Tactic: cases h
Cleared hypotheses: dom, toEquiv, 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
cod : L.Substructure N
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 }
have refl : ∀ (x : M) (h : x ∈ (PartialEquiv.toEmbeddingOfEqTop sorry).toPartialEquiv.dom),
  Eq (α := N)
    (((PartialEquiv.toEmbeddingOfEqTop sorry).toPartialEquiv.cod.subtype :
          (a : ↥(PartialEquiv.toEmbeddingOfEqTop sorry).toPartialEquiv.cod) → N)
        (((PartialEquiv.toEmbeddingOfEqTop sorry).toPartialEquiv.toEquiv :
              (a : ↥(PartialEquiv.toEmbeddingOfEqTop sorry).toPartialEquiv.dom) →
                ↥(PartialEquiv.toEmbeddingOfEqTop sorry).toPartialEquiv.cod)
            (Subtype.mk (p := fun (x : M) ↦ x ∈ (PartialEquiv.toEmbeddingOfEqTop sorry).toPartialEquiv.dom) x h) :
          ↥(PartialEquiv.toEmbeddingOfEqTop sorry).toPartialEquiv.cod) :
      N)
    (({ dom := { carrier := Set.univ, fun_mem := sorry : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                M ≃ₚ[L] N }.cod.subtype :
          (a : ↥{ dom := { carrier := Set.univ, fun_mem := sorry }, cod := cod, toEquiv := toEquiv }.cod) → N)
        (({ dom := { carrier := Set.univ, fun_mem := sorry : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                  M ≃ₚ[L] N }.toEquiv :
              (a : ↥{ dom := { carrier := Set.univ, fun_mem := sorry }, cod := cod, toEquiv := toEquiv }.dom) →
                ↥{ dom := { carrier := Set.univ, fun_mem := sorry }, cod := cod, toEquiv := toEquiv }.cod)
            (Subtype.mk (p := fun (x : M) ↦
              x ∈
                { dom := { carrier := Set.univ, fun_mem := sorry : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                    M ≃ₚ[L] N }.dom)
              x sorry) :
          ↥{ dom := { carrier := Set.univ, fun_mem := sorry : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                M ≃ₚ[L] N }.cod) :
      N)
Tactic: apply PartialEquiv.ext
-- 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
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)
⊢ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv =
    { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := toEquiv }
have refl₁ : (PartialEquiv.toEmbeddingOfEqTop sorry).toPartialEquiv.dom =
  { dom := { carrier := Set.univ, fun_mem := sorry : L.Substructure M }, cod := cod, toEquiv := toEquiv : M ≃ₚ[L] N }.dom
Tactic: apply PartialEquiv.ext
-- 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
ι : Type u_1
inst_2 : Preorder ι
inst_3 : Nonempty ι
inst_4 : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (partialEquivLimit S).toEquiv.toEmbedding.comp (inclusion ⋯) =
    Embedding.comp (inclusion ⋯) (Equiv.toEmbedding (toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i)))
have 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' := sorry :
                  OrderHom.{u_1, w'} ι (L.Substructure N) } :
                (a : ι) → L.Substructure N)
              i :
            L.Substructure N))
      fun (x x_1 : ι) (h : x ≤ x_1) ↦ inclusion sorry)
    (Equiv.toEmbedding
      (Equiv_iSup
        { toFun := fun (i : ι) ↦ cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i), monotone' := sorry :
          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 sorry)
          (fun (i : ι) ↦ ↥(cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i)))
          (fun (x x_1 : ι) (hij : x ≤ x_1) ↦ inclusion sorry) (fun (i : ι) ↦ toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i)) sorry))
      (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' := sorry :
                OrderHom.{u_1, w} ι (L.Substructure M) })))
        (inclusion sorry))) =
  Embedding.comp (inclusion sorry) (Equiv.toEmbedding (toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i)))
Tactic: simp only [partialEquivLimit, Equiv.comp_toEmbedding, Embedding.comp_assoc]
-- 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
ι : Type u_1
inst_2 : Preorder ι
inst_3 : Nonempty ι
inst_4 : IsDirectedOrder ι
S : ι →o 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)))
have 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 sorry) (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 [partialEquivLimit_comp_inclusion]
-- 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
h : g f = g f'
⊢ f = f'
have a : (↑f : M ≃ₚ[L] M) = (↑f' : M ≃ₚ[L] M)
Tactic: ext
-- 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
h : g f = g f'
⊢ (↑f : M ≃ₚ[L] M) = (↑f' : M ≃ₚ[L] M)
have 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)
Tactic: let ⟨⟨dom_f, cod_f, equiv_f⟩, f_fin⟩ := f
Cleared hypotheses: h
-- 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
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)
have 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)
Tactic: cases congr_arg (·.1) h
Cleared hypotheses: dom_f, equiv_f, f_fin, h