awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
M : Type w'
inst : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst_1 : Nonempty M
rw rw₁ rw₂ :
  Eq.{w' + 2} (α := Set (CategoryTheory.Bundled Language.order.Structure))
    {N : CategoryTheory.Bundled Language.order.Structure |
      FG.{w', 0, 0} Language.order (↑N : Type w') ∧ Nonempty.{w' + 1} ((↑N : Type w') ↪[Language.order] M)}
    {M : CategoryTheory.Bundled Language.order.Structure |
      Finite.{w' + 1} (↑M : Type w') ∧ Theory.Model.{0, 0, w'} (↑M : Type w') Language.order.linearOrderTheory}
h :
  ∀ (N : CategoryTheory.Bundled Language.order.Structure),
    Membership.mem (γ := Set (CategoryTheory.Bundled Language.order.Structure))
        {N : CategoryTheory.Bundled Language.order.Structure |
          FG.{w', 0, 0} Language.order (↑N : Type w') ∧ Nonempty.{w' + 1} ((↑N : Type w') ↪[Language.order] M)}
        N ↔
      Membership.mem (γ := Set (CategoryTheory.Bundled Language.order.Structure))
        {M : CategoryTheory.Bundled Language.order.Structure |
          Finite.{w' + 1} (↑M : Type w') ∧ Theory.Model.{0, 0, w'} (↑M : Type w') Language.order.linearOrderTheory}
        N
⊢ Language.order.age M =
    {M : CategoryTheory.Bundled Language.order.Structure |
      Finite.{w' + 1} (↑M : Type w') ∧ Theory.Model.{0, 0, w'} (↑M : Type w') Language.order.linearOrderTheory}
have h₁ : ∀ (N : CategoryTheory.Bundled Language.order.Structure),
  Membership.mem (γ := Set (CategoryTheory.Bundled Language.order.Structure))
      {M : CategoryTheory.Bundled Language.order.Structure |
        Finite.{w' + 1} (↑M : Type w') ∧ Theory.Model.{0, 0, w'} (↑M : Type w') Language.order.linearOrderTheory}
      N →
    ∀ (hF : Finite.{w' + 1} (↑N : Type w'))
      (h : Theory.Model.{0, 0, w'} (↑N : Type w') Language.order.linearOrderTheory),
      Nonempty.{w' + 1} ((↑N : Type w') ↪[Language.order] M)
Tactic: classical
  rw [age]
  ext N
  refine ⟨fun ⟨hF, h⟩ => ⟨hF.finite, Theory.IsUniversal.models_of_embedding h.some⟩,
    fun ⟨hF, h⟩ => ⟨FG.of_finite, ?_⟩⟩
  letI := Language.order.linearOrderOfModels M
  letI := Language.order.linearOrderOfModels N
  exact ⟨StrongHomClass.toEmbedding (nonempty_orderEmbedding_of_finite_infinite N M).some⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
M₁ M₂ : Language.order.dlo.ModelType
h₁ : #(↑M₁ : Type u_1) = ℵ₀
h₂ : #(↑M₂ : Type u_1) = ℵ₀
⊢ Nonempty.{u_1 + 1} ((↑M₁ : Type u_1) ≃[Language.order] (↑M₂ : Type u_1))
have obtain : ∀ (val : Denumerable (↑M₁ : Type u_1)), Nonempty.{u_1 + 1} ((↑M₁ : Type u_1) ≃[Language.order] (↑M₂ : Type u_1))
Tactic: obtain ⟨_⟩ := denumerable_iff.2 h₁
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
M₁ M₂ : Language.order.dlo.ModelType
h₁ : #(↑M₁ : Type u_1) = ℵ₀
h₂ : #(↑M₂ : Type u_1) = ℵ₀
val : Denumerable (↑M₁ : Type u_1)
⊢ Nonempty.{u_1 + 1} ((↑M₁ : Type u_1) ≃[Language.order] (↑M₂ : Type u_1))
have obtain : ∀ (val : Denumerable (↑M₂ : Type u_1)), Nonempty.{u_1 + 1} ((↑M₁ : Type u_1) ≃[Language.order] (↑M₂ : Type u_1))
Tactic: obtain ⟨_⟩ := denumerable_iff.2 h₂
-- 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
f g : M ≃ₚ[L] N
w : f.dom ≤ g.dom
eq_fun : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w)) = f.cod.subtype.comp f.toEquiv.toEmbedding
n : N
hn : n ∈ f.cod
m : ↥f.dom := (f.toEquiv.symm : (a : ↥f.cod) → ↥f.dom) (Subtype.mk (p := fun (x : N) ↦ x ∈ f.cod) n hn)
⊢ n ∈ g.cod
have this : (f.cod.subtype.comp f.toEquiv.toEmbedding : (a : ↥f.dom) → N) m = n
Tactic: have : ((subtype _).comp f.toEquiv.toEmbedding) m = n := by simp only [m, Embedding.comp_apply,
    Equiv.coe_toEmbedding, Equiv.apply_symm_apply, coe_subtype]
-- 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
w : f.dom ≤ g.dom
eq_fun : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w)) = f.cod.subtype.comp f.toEquiv.toEmbedding
n : N
hn : n ∈ f.cod
m : ↥f.dom := (f.toEquiv.symm : (a : ↥f.cod) → ↥f.dom) (Subtype.mk (p := fun (x : N) ↦ x ∈ f.cod) n hn)
this : (f.cod.subtype.comp f.toEquiv.toEmbedding : (a : ↥f.dom) → N) m = n
⊢ n ∈ g.cod
have rw : Membership.mem (α := N) g.cod ((g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w)) : (a : ↥f.dom) → N) m : N)
Tactic: rw [← this, ← eq_fun]
-- 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
f g : M ≃ₚ[L] N
h : f ≤ g
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) = f.cod.subtype.comp f.toEquiv.toEmbedding
have w : f.dom ≤ g.dom
Tactic: let ⟨_, eq⟩ := 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 g : M ≃ₚ[L] N
h : f ≤ g
⊢ g.toEquiv.toEmbedding.comp (inclusion ⋯) = (inclusion ⋯).comp f.toEquiv.toEmbedding
have rw : f.cod.subtype.comp f.toEquiv.toEmbedding = g.cod.subtype.comp ((inclusion sorry).comp f.toEquiv.toEmbedding)
Tactic: rw [← (subtype _).comp_inj, subtype_toEquiv_inclusion 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 g : M ≃ₚ[L] N
h : f ≤ g
⊢ f.cod.subtype.comp f.toEquiv.toEmbedding = g.cod.subtype.comp ((inclusion ⋯).comp f.toEquiv.toEmbedding)
have h₁ : ∀ (x : ↥f.dom),
  Eq.{w' + 1} (α := N) ((f.cod.subtype.comp f.toEquiv.toEmbedding : (a : ↥f.dom) → N) x : N)
    ((g.cod.subtype.comp ((inclusion sorry).comp f.toEquiv.toEmbedding) : (a : ↥f.dom) → 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
f g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ Eq.{w' + 1} (α := ↥g.cod) ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) ((inclusion ⋯ : (a : ↥f.dom) → ↥g.dom) x) : ↥g.cod)
    ((inclusion ⋯ : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod)
have a : Eq (α := N)
  ((g.cod.subtype : (a : ↥g.cod) → N)
      ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) ((inclusion sorry : (a : ↥f.dom) → ↥g.dom) x) : ↥g.cod) :
    N)
  ((g.cod.subtype : (a : ↥g.cod) → N)
      ((inclusion sorry : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod) :
    N)
Tactic: apply (subtype _).injective
-- 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 : f ≤ g
x : ↥f.dom
⊢ Eq (α := N)
    ((g.cod.subtype : (a : ↥g.cod) → N)
        ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) ((inclusion ⋯ : (a : ↥f.dom) → ↥g.dom) x) : ↥g.cod) :
      N)
    ((g.cod.subtype : (a : ↥g.cod) → N)
        ((inclusion ⋯ : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod) :
      N)
have a : Eq.{w' + 1} (α := N) ((g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion sorry)) : (a : ↥f.dom) → N) x : N)
  ((g.cod.subtype : (a : ↥g.cod) → N)
      ((inclusion sorry : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod) :
    N)
Tactic: change (subtype _).comp (g.toEquiv.toEmbedding.comp (inclusion _)) x = _
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ Eq.{w' + 1} (α := N) ((g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) : (a : ↥f.dom) → N) x : N)
    ((g.cod.subtype : (a : ↥g.cod) → N)
        ((inclusion ⋯ : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod) :
      N)
have a : Eq.{w' + 1} (α := N) ((f.cod.subtype.comp f.toEquiv.toEmbedding : (a : ↥f.dom) → N) x : N)
  ((g.cod.subtype : (a : ↥g.cod) → N)
      ((inclusion sorry : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod) :
    N)
Tactic: rw [subtype_toEquiv_inclusion 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 g : M ≃ₚ[L] N
⊢ f ≤ g ↔
    ∃ (dom_le_dom : f.dom ≤ g.dom) (cod_le_cod : f.cod ≤ g.cod),
      ∀ (x : ↥f.dom),
        Eq (α := ↥g.cod)
          ((inclusion cod_le_cod : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod)
          ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) ((inclusion dom_le_dom : (a : ↥f.dom) → ↥g.dom) x) : ↥g.cod)
have mp : f ≤ g →
  ∃ (dom_le_dom : f.dom ≤ g.dom) (cod_le_cod : f.cod ≤ g.cod),
    ∀ (x : ↥f.dom),
      Eq (α := ↥g.cod) ((inclusion cod_le_cod : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod)
        ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) ((inclusion dom_le_dom : (a : ↥f.dom) → ↥g.dom) x) : ↥g.cod)
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 →
    ∃ (dom_le_dom : f.dom ≤ g.dom) (cod_le_cod : f.cod ≤ g.cod),
      ∀ (x : ↥f.dom),
        Eq (α := ↥g.cod)
          ((inclusion cod_le_cod : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod)
          ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) ((inclusion dom_le_dom : (a : ↥f.dom) → ↥g.dom) x) : ↥g.cod)
⊢ f ≤ g ↔
    ∃ (dom_le_dom : f.dom ≤ g.dom) (cod_le_cod : f.cod ≤ g.cod),
      ∀ (x : ↥f.dom),
        Eq (α := ↥g.cod)
          ((inclusion cod_le_cod : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod)
          ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) ((inclusion dom_le_dom : (a : ↥f.dom) → ↥g.dom) x) : ↥g.cod)
have mpr : (∃ (dom_le_dom : f.dom ≤ g.dom) (cod_le_cod : f.cod ≤ g.cod),
    ∀ (x : ↥f.dom),
      Eq (α := ↥g.cod) ((inclusion cod_le_cod : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod)
        ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) ((inclusion dom_le_dom : (a : ↥f.dom) → ↥g.dom) x) : ↥g.cod)) →
  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 : f ≤ g
x : ↥f.dom
⊢ Eq (α := ↥g.cod) ((inclusion ⋯ : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod)
    ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) ((inclusion ⋯ : (a : ↥f.dom) → ↥g.dom) x) : ↥g.cod)
have a : g.cod.subtype.toFun ((inclusion sorry : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x)) =
  g.cod.subtype.toFun ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) ((inclusion sorry : (a : ↥f.dom) → ↥g.dom) x))
Tactic: apply (subtype _).inj'
-- 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 : f ≤ g
x : ↥f.dom
⊢ g.cod.subtype.toFun ((inclusion ⋯ : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x)) =
    g.cod.subtype.toFun ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) ((inclusion ⋯ : (a : ↥f.dom) → ↥g.dom) x))
have a : g.cod.subtype.toFun ((inclusion sorry : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x)) =
  g.cod.subtype.toFun ((inclusion sorry : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x))
Tactic: rwa [toEquiv_inclusion_apply]
-- 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
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq :
  ∀ (x : ↥f.dom),
    Eq (α := ↥g.cod) ((inclusion le_cod : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod)
      ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) ((inclusion dom_le_dom : (a : ↥f.dom) → ↥g.dom) x) : ↥g.cod)
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion dom_le_dom)) = f.cod.subtype.comp f.toEquiv.toEmbedding
have h : ∀ (x : ↥f.dom),
  Eq.{w' + 1} (α := N)
    ((g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion dom_le_dom)) : (a : ↥f.dom) → N) x : N)
    ((f.cod.subtype.comp f.toEquiv.toEmbedding : (a : ↥f.dom) → 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
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq :
  ∀ (x : ↥f.dom),
    Eq (α := ↥g.cod) ((inclusion le_cod : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod)
      ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) ((inclusion dom_le_dom : (a : ↥f.dom) → ↥g.dom) x) : ↥g.cod)
x : ↥f.dom
⊢ Eq.{w' + 1} (α := N)
    ((g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion dom_le_dom)) : (a : ↥f.dom) → N) x : N)
    ((f.cod.subtype.comp f.toEquiv.toEmbedding : (a : ↥f.dom) → N) x : N)
have h : Eq (α := N)
  ((g.cod.subtype : (a : ↥g.cod) → N)
      ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) ((inclusion dom_le_dom : (a : ↥f.dom) → ↥g.dom) x) : ↥g.cod) :
    N)
  ((f.cod.subtype.comp f.toEquiv.toEmbedding : (a : ↥f.dom) → N) x : N)
Tactic: change subtype _ (g.toEquiv _) = _
-- 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
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq :
  ∀ (x : ↥f.dom),
    Eq (α := ↥g.cod) ((inclusion le_cod : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod)
      ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) ((inclusion dom_le_dom : (a : ↥f.dom) → ↥g.dom) x) : ↥g.cod)
x : ↥f.dom
⊢ Eq (α := N)
    ((g.cod.subtype : (a : ↥g.cod) → N)
        ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) ((inclusion dom_le_dom : (a : ↥f.dom) → ↥g.dom) x) : ↥g.cod) :
      N)
    ((f.cod.subtype.comp f.toEquiv.toEmbedding : (a : ↥f.dom) → N) x : N)
have h : Eq (α := N)
  ((g.cod.subtype : (a : ↥g.cod) → N)
      ((inclusion le_cod : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod) :
    N)
  ((f.cod.subtype.comp f.toEquiv.toEmbedding : (a : ↥f.dom) → N) x : N)
Tactic: rw [← 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 h : M ≃ₚ[L] N
le_fg : f.dom ≤ g.dom
eq_fg : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion le_fg)) = f.cod.subtype.comp f.toEquiv.toEmbedding
le_gh : g.dom ≤ h.dom
eq_gh : h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion le_gh)) = g.cod.subtype.comp g.toEquiv.toEmbedding
⊢ f ≤ h
have refine : h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion sorry)) = f.cod.subtype.comp f.toEquiv.toEmbedding
Tactic: refine ⟨le_fg.trans le_gh, ?_⟩
-- 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 h : M ≃ₚ[L] N
le_fg : f.dom ≤ g.dom
eq_fg : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion le_fg)) = f.cod.subtype.comp f.toEquiv.toEmbedding
le_gh : g.dom ≤ h.dom
eq_gh : h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion le_gh)) = g.cod.subtype.comp g.toEquiv.toEmbedding
⊢ h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion ⋯)) = f.cod.subtype.comp f.toEquiv.toEmbedding
have rw : h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion sorry)) =
  (h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion le_gh))).comp (inclusion le_fg)
Tactic: rw [← eq_fg, ← Embedding.comp_assoc (g := g.toEquiv.toEmbedding), ← eq_gh]
-- 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 h : M ≃ₚ[L] N
le_fg : f.dom ≤ g.dom
eq_fg : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion le_fg)) = f.cod.subtype.comp f.toEquiv.toEmbedding
le_gh : g.dom ≤ h.dom
eq_gh : h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion le_gh)) = g.cod.subtype.comp g.toEquiv.toEmbedding
⊢ h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion ⋯)) =
    (h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion le_gh))).comp (inclusion le_fg)
have h₁ : ∀ (x : ↥f.dom),
  Eq.{w' + 1} (α := N) ((h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion sorry)) : (a : ↥f.dom) → N) x : N)
    (((h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion le_gh))).comp (inclusion le_fg) : (a : ↥f.dom) → 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
f g : M ≃ₚ[L] N
le_fg : f ≤ g
le_gf : g ≤ f
⊢ f = g
have let : ∀ (dom_f : L.Substructure M) (cod_f : L.Substructure N) (equiv_f : Equiv.{u, v, w, w'} L ↥dom_f ↥cod_f)
  (le_fg : { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } ≤ g)
  (le_gf : g ≤ { dom := dom_f, cod := cod_f, toEquiv := equiv_f }),
  { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g
Tactic: let ⟨dom_f, cod_f, equiv_f⟩ := f
Cleared hypotheses: le_fg, le_gf
-- 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
dom_f : L.Substructure M
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥dom_f ↥cod_f
le_fg : { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } ≤ g
le_gf : g ≤ { dom := dom_f, cod := cod_f, toEquiv := equiv_f }
⊢ { 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)
  (le_fg : { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } ≤ g)
  (le_gf : g ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f }),
  { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g
Tactic: cases _root_.le_antisymm (dom_le_dom le_fg) (dom_le_dom le_gf)
Cleared hypotheses: dom_f, equiv_f, le_fg, le_gf
-- 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
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f
le_fg : { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } ≤ g
le_gf : g ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f }
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g
have refl : ∀ (equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥g.2) (le_fg : { dom := g.1, cod := g.2, toEquiv := equiv_f : M ≃ₚ[L] N } ≤ g)
  (le_gf : g ≤ { dom := g.1, cod := g.2, toEquiv := equiv_f }),
  { dom := g.1, cod := g.2, toEquiv := equiv_f : M ≃ₚ[L] N } = g
Tactic: cases _root_.le_antisymm (cod_le_cod le_fg) (cod_le_cod le_gf)
Cleared hypotheses: cod_f, equiv_f, le_fg, le_gf
-- 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
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥g.2
le_fg : { dom := g.1, cod := g.2, toEquiv := equiv_f : M ≃ₚ[L] N } ≤ g
le_gf : g ≤ { dom := g.1, cod := g.2, toEquiv := equiv_f }
⊢ { dom := g.1, cod := g.2, toEquiv := equiv_f : M ≃ₚ[L] N } = g
have h : HEq g.dom (β := L.Substructure M) g.1 → HEq g.cod (β := L.Substructure N) g.2 → g.toEquiv = equiv_f
Tactic: convert! 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
f g : M ≃ₚ[L] N
hfg : f ≤ g
⊢ f.symm ≤ g.symm
have rw : ∃ (dom_le_dom : f.symm.dom ≤ g.symm.dom) (cod_le_cod : f.symm.cod ≤ g.symm.cod),
  ∀ (x : ↥f.symm.dom),
    Eq (α := ↥g.symm.cod)
      ((inclusion cod_le_cod : (a : ↥f.symm.cod) → ↥g.symm.cod) ((f.symm.toEquiv : (a : ↥f.symm.dom) → ↥f.symm.cod) x) :
        ↥g.symm.cod)
      ((g.symm.toEquiv : (a : ↥g.symm.dom) → ↥g.symm.cod) ((inclusion dom_le_dom : (a : ↥f.symm.dom) → ↥g.symm.dom) x) :
        ↥g.symm.cod)
Tactic: rw [le_iff]
-- 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
hfg : f ≤ g
⊢ ∃ (dom_le_dom : f.symm.dom ≤ g.symm.dom) (cod_le_cod : f.symm.cod ≤ g.symm.cod),
    ∀ (x : ↥f.symm.dom),
      Eq (α := ↥g.symm.cod)
        ((inclusion cod_le_cod : (a : ↥f.symm.cod) → ↥g.symm.cod)
            ((f.symm.toEquiv : (a : ↥f.symm.dom) → ↥f.symm.cod) x) :
          ↥g.symm.cod)
        ((g.symm.toEquiv : (a : ↥g.symm.dom) → ↥g.symm.cod)
            ((inclusion dom_le_dom : (a : ↥f.symm.dom) → ↥g.symm.dom) x) :
          ↥g.symm.cod)
have refine : ∀ (x : ↥f.symm.dom),
  Eq (α := ↥g.symm.cod)
    ((inclusion sorry : (a : ↥f.symm.cod) → ↥g.symm.cod) ((f.symm.toEquiv : (a : ↥f.symm.dom) → ↥f.symm.cod) x) :
      ↥g.symm.cod)
    ((g.symm.toEquiv : (a : ↥g.symm.dom) → ↥g.symm.cod) ((inclusion sorry : (a : ↥f.symm.dom) → ↥g.symm.dom) x) :
      ↥g.symm.cod)
Tactic: refine ⟨cod_le_cod hfg, dom_le_dom 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 g : M ≃ₚ[L] N
hfg : f ≤ g
x : ↥f.symm.dom
⊢ Eq (α := ↥g.symm.cod)
    ((inclusion ⋯ : (a : ↥f.symm.cod) → ↥g.symm.cod) ((f.symm.toEquiv : (a : ↥f.symm.dom) → ↥f.symm.cod) x) :
      ↥g.symm.cod)
    ((g.symm.toEquiv : (a : ↥g.symm.dom) → ↥g.symm.cod) ((inclusion ⋯ : (a : ↥f.symm.dom) → ↥g.symm.dom) x) :
      ↥g.symm.cod)
have a : Eq.{w' + 1} (α := ↥g.cod)
  ((g.toEquiv : (a : ↥g.dom) → ↥g.cod)
      ((inclusion sorry : (a : ↥f.symm.cod) → ↥g.symm.cod) ((f.symm.toEquiv : (a : ↥f.symm.dom) → ↥f.symm.cod) x)) :
    ↥g.cod)
  ((g.toEquiv : (a : ↥g.dom) → ↥g.cod)
      ((g.symm.toEquiv : (a : ↥g.symm.dom) → ↥g.symm.cod) ((inclusion sorry : (a : ↥f.symm.dom) → ↥g.symm.dom) x)) :
    ↥g.cod)
Tactic: apply g.toEquiv.injective
-- 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
hfg : f ≤ g
x : ↥f.symm.dom
⊢ Eq.{w' + 1} (α := ↥g.cod)
    ((g.toEquiv : (a : ↥g.dom) → ↥g.cod)
        ((inclusion ⋯ : (a : ↥f.symm.cod) → ↥g.symm.cod) ((f.symm.toEquiv : (a : ↥f.symm.dom) → ↥f.symm.cod) x)) :
      ↥g.cod)
    ((g.toEquiv : (a : ↥g.dom) → ↥g.cod)
        ((g.symm.toEquiv : (a : ↥g.symm.dom) → ↥g.symm.cod) ((inclusion ⋯ : (a : ↥f.symm.dom) → ↥g.symm.dom) x)) :
      ↥g.cod)
have a : Eq.{w' + 1} (α := ↥g.cod)
  ((g.toEquiv : (a : ↥g.dom) → ↥g.cod)
      ((inclusion sorry : (a : ↥f.dom) → ↥g.dom) ((f.toEquiv.symm : (a : ↥f.cod) → ↥f.dom) x)) :
    ↥g.cod)
  ((g.toEquiv : (a : ↥g.dom) → ↥g.cod)
      ((g.toEquiv.symm : (a : ↥g.cod) → ↥g.dom) ((inclusion sorry : (a : ↥f.symm.dom) → ↥g.symm.dom) x)) :
    ↥g.cod)
Tactic: change g.toEquiv (inclusion _ (f.toEquiv.symm x)) = g.toEquiv (g.toEquiv.symm _)
-- 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
hfg : f ≤ g
x : ↥f.symm.dom
⊢ Eq.{w' + 1} (α := ↥g.cod)
    ((g.toEquiv : (a : ↥g.dom) → ↥g.cod)
        ((inclusion ⋯ : (a : ↥f.dom) → ↥g.dom) ((f.toEquiv.symm : (a : ↥f.cod) → ↥f.dom) x)) :
      ↥g.cod)
    ((g.toEquiv : (a : ↥g.dom) → ↥g.cod)
        ((g.toEquiv.symm : (a : ↥g.cod) → ↥g.dom) ((inclusion ⋯ : (a : ↥f.symm.dom) → ↥g.symm.dom) x)) :
      ↥g.cod)
have a : Eq.{w' + 1} (α := ↥g.cod)
  ((g.toEquiv : (a : ↥g.dom) → ↥g.cod)
      ((inclusion sorry : (a : ↥f.dom) → ↥g.dom) ((f.toEquiv.symm : (a : ↥f.cod) → ↥f.dom) x)) :
    ↥g.cod)
  ((inclusion sorry : (a : ↥f.symm.dom) → ↥g.symm.dom)
      ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) ((f.toEquiv.symm : (a : ↥f.cod) → ↥f.dom) x)) :
    ↥g.symm.dom)
Tactic: rw [g.toEquiv.apply_symm_apply, (Equiv.apply_symm_apply f.toEquiv x).symm,
    f.toEquiv.symm_apply_apply]
-- 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
g : N ≃ₚ[L] M
h : f.symm ≤ g
⊢ f ≤ g.symm
have rw : f.symm.symm ≤ g.symm
Tactic: rw [← f.symm_symm]
-- 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
g : N ≃ₚ[L] M
h : f ≤ g.symm
⊢ f.symm ≤ g
have rw : f.symm ≤ g.symm.symm
Tactic: rw  [← g.symm_symm]