awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Order
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
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)
h₂ 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)
⊢ 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}

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⟩

Premises used: FirstOrder.Language.age
-- Module: Mathlib.ModelTheory.Order
Goal:
M : Type w
inst : Language.order.Structure M
inst_1 : Countable M
inst_2 : Nonempty M
inst_3 : M ⊨ Language.order.dlo
⊢ IsFraisseLimit (L := Language.order)
    {M : CategoryTheory.Bundled Language.order.Structure |
      Finite.{w + 1} (↑M : Type w) ∧ Theory.Model.{0, 0, w} (↑M : Type w) Language.order.linearOrderTheory}
    M

Tactic:
⟨(isUltrahomogeneous_iff_IsExtensionPair cg_of_countable).2 (dlo_isExtensionPair M M), dlo_age M⟩

Premises used: Iff.mpr, FirstOrder.Language.dlo_age, FirstOrder.Language.dlo_isExtensionPair, FirstOrder.Language.isUltrahomogeneous_iff_IsExtensionPair, FirstOrder.Language.IsFraisseLimit.mk, FirstOrder.Language.Structure.cg_of_countable
-- Module: Mathlib.ModelTheory.Order
Goal:
this : Language.order.Structure ℚ := orderStructure ℚ
⊢ IsFraisse (L := Language.order)
    {M : CategoryTheory.Bundled Language.order.Structure |
      Finite (↑M : Type) ∧ (↑M : Type) ⊨ Language.order.linearOrderTheory}

Tactic:
(isFraisseLimit_of_countable_nonempty_dlo ℚ).isFraisse

Premises used: Rat, FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo, FirstOrder.Language.IsFraisseLimit.isFraisse
-- Module: Mathlib.ModelTheory.Order
Goal:
this : Language.order.Structure ℚ := orderStructure ℚ
⊢ IsFraisse (L := Language.order)
    {M : CategoryTheory.Bundled Language.order.Structure |
      Finite (↑M : Type) ∧ (↑M : Type) ⊨ Language.order.linearOrderTheory}

Tactic:
exact (isFraisseLimit_of_countable_nonempty_dlo ℚ).isFraisse

Premises used: Rat, FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo, FirstOrder.Language.IsFraisseLimit.isFraisse
-- Module: Mathlib.ModelTheory.Order
Goal:
M₁ M₂ : Language.order.dlo.ModelType
h₁ : #(↑M₁ : Type u_1) = ℵ₀
h₂ : #(↑M₂ : Type u_1) = ℵ₀
obtain :
  ∀ (val : Denumerable (↑M₁ : Type u_1)), Nonempty.{u_1 + 1} ((↑M₁ : Type u_1) ≃[Language.order] (↑M₂ : Type u_1))
⊢ Nonempty.{u_1 + 1} ((↑M₁ : Type u_1) ≃[Language.order] (↑M₂ : Type u_1))

Tactic:
obtain ⟨_⟩ := denumerable_iff.2 h₁

Premises used: Iff.mpr, Cardinal.denumerable_iff
-- Module: Mathlib.ModelTheory.Order
Goal:
M₁ M₂ : Language.order.dlo.ModelType
h₁ : #(↑M₁ : Type u_1) = ℵ₀
h₂ : #(↑M₂ : Type u_1) = ℵ₀
val : Denumerable (↑M₁ : Type u_1)
obtain :
  ∀ (val : Denumerable (↑M₂ : Type u_1)), Nonempty.{u_1 + 1} ((↑M₁ : Type u_1) ≃[Language.order] (↑M₂ : Type u_1))
⊢ Nonempty.{u_1 + 1} ((↑M₁ : Type u_1) ≃[Language.order] (↑M₂ : Type u_1))

Tactic:
obtain ⟨_⟩ := denumerable_iff.2 h₂

Premises used: Iff.mpr, Cardinal.denumerable_iff
-- Module: Mathlib.ModelTheory.Order
Goal:
M₁ M₂ : Language.order.dlo.ModelType
h₁ : #(↑M₁ : Type u_1) = ℵ₀
h₂ : #(↑M₂ : Type u_1) = ℵ₀
val : Denumerable (↑M₁ : Type u_1)
val_1 : Denumerable (↑M₂ : Type u_1)
⊢ Nonempty.{u_1 + 1} ((↑M₁ : Type u_1) ≃[Language.order] (↑M₂ : Type u_1))

Tactic:
(isFraisseLimit_of_countable_nonempty_dlo M₁).nonempty_equiv
    (isFraisseLimit_of_countable_nonempty_dlo M₂)

Premises used: FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo, FirstOrder.Language.IsFraisseLimit.nonempty_equiv, FirstOrder.Language.Theory.ModelType.Carrier
-- Module: Mathlib.ModelTheory.Order
Goal:
M₁ M₂ : Language.order.dlo.ModelType
h₁ : #(↑M₁ : Type u_1) = ℵ₀
h₂ : #(↑M₂ : Type u_1) = ℵ₀
val : Denumerable (↑M₁ : Type u_1)
val_1 : Denumerable (↑M₂ : Type u_1)
⊢ Nonempty.{u_1 + 1} ((↑M₁ : Type u_1) ≃[Language.order] (↑M₂ : Type u_1))

Tactic:
exact (isFraisseLimit_of_countable_nonempty_dlo M₁).nonempty_equiv
    (isFraisseLimit_of_countable_nonempty_dlo M₂)

Premises used: FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo, FirstOrder.Language.IsFraisseLimit.nonempty_equiv, FirstOrder.Language.Theory.ModelType.Carrier
-- Module: Mathlib.ModelTheory.Order
Goal:
⊢ lift.{0, 0} Language.order.card ≤ lift.{0, 0} ℵ₀

Tactic:
simp [one_le_aleph0]

Premises used: Cardinal.one_le_aleph0
-- Module: Mathlib.ModelTheory.Order
Goal:
this : Language.order.Structure ℚ := orderStructure ℚ
⊢ Language.order.dlo.ModelType

Tactic:
exact Theory.ModelType.of _ ℚ

Premises used: Rat, FirstOrder.Language.Theory.ModelType.of
-- Module: Mathlib.ModelTheory.Order
Goal:
α β : Type w'
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
inst_6 : Nonempty α
inst_7 : Countable β
inst_8 : DenselyOrdered β
inst_9 : NoMinOrder β
inst_10 : NoMaxOrder β
inst_11 : Nonempty β
this_1 : Language.order.Structure α := orderStructure α
this_2 : Language.order.Structure β := orderStructure β
this : OrderIsoClass (α ≃[Language.order] β) α β := ⋯
⊢ Nonempty.{w' + 1} (α ≃o β)

Tactic:
⟨(IsFraisseLimit.nonempty_equiv (isFraisseLimit_of_countable_nonempty_dlo α)
    (isFraisseLimit_of_countable_nonempty_dlo β)).some⟩

Premises used: Nonempty.some, FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo, Nonempty.intro, OrderIsoClass.toOrderIso, FirstOrder.Language.IsFraisseLimit.nonempty_equiv
-- Module: Mathlib.ModelTheory.Order
Goal:
α β : Type w'
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : Countable α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
inst_6 : Nonempty α
inst_7 : Countable β
inst_8 : DenselyOrdered β
inst_9 : NoMinOrder β
inst_10 : NoMaxOrder β
inst_11 : Nonempty β
this_1 : Language.order.Structure α := orderStructure α
this_2 : Language.order.Structure β := orderStructure β
this : OrderIsoClass (α ≃[Language.order] β) α β := ⋯
⊢ Nonempty.{w' + 1} (α ≃o β)

Tactic:
exact ⟨(IsFraisseLimit.nonempty_equiv (isFraisseLimit_of_countable_nonempty_dlo α)
    (isFraisseLimit_of_countable_nonempty_dlo β)).some⟩
-- 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
⊢ f.symm.symm = f

Tactic:
rfl

Premises used: FirstOrder.Language.PartialEquiv.symm, Set.Mem, Equiv.symm, rfl, FirstOrder.Language.Equiv.symm
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
⊢ Function.Bijective (α := M ≃ₚ[L] N) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, FirstOrder.Language.PartialEquiv.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- 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
x : ↥f.cod
⊢ Eq.{w + 1} (α := ↥f.symm.cod) ((f.symm.toEquiv : (a : ↥f.symm.dom) → ↥f.symm.cod) x : ↥f.symm.cod)
    ((f.toEquiv.symm : (a : ↥f.cod) → ↥f.dom) x : ↥f.dom)

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 g : M ≃ₚ[L] N
⊢ f ≤ g ↔
    ∃ (h : f.dom ≤ g.dom),
      g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion h)) = f.cod.subtype.comp f.toEquiv.toEmbedding

Tactic:
Iff.rfl

Premises used: Iff.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
⊢ f ≤ g → f.dom ≤ g.dom

Tactic:
fun ⟨le, _⟩ ↦ le

Premises used: FirstOrder.Language.PartialEquiv.dom, LE.le, _private.0.FirstOrder.Language.PartialEquiv.dom_le_dom.match_1
-- 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
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)
⊢ (f.cod.subtype.comp f.toEquiv.toEmbedding : (a : ↥f.dom) → N) m = n

Tactic:
simp only [m, Embedding.comp_apply,
    Equiv.coe_toEmbedding, Equiv.apply_symm_apply, coe_subtype]

Premises used: FirstOrder.Language.Substructure.coe_subtype, FirstOrder.Language.Equiv.apply_symm_apply, FirstOrder.Language.Embedding.comp_apply, FirstOrder.Language.Equiv.coe_toEmbedding
-- 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
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)
⊢ (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]
-- 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
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
rw :
  Membership.mem (α := N) g.cod
    ((g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w)) : (a : ↥f.dom) → N) m : N)
⊢ n ∈ g.cod

Tactic:
rw [← this, ← eq_fun]
-- 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
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
⊢ Membership.mem (α := N) g.cod
    ((g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w)) : (a : ↥f.dom) → N) m : N)

Tactic:
simp only [Embedding.comp_apply, coe_inclusion, Equiv.coe_toEmbedding, coe_subtype,
    SetLike.coe_mem]

Premises used: SetLike.coe_mem, FirstOrder.Language.Substructure.coe_inclusion, FirstOrder.Language.Substructure.coe_subtype, FirstOrder.Language.Embedding.comp_apply, FirstOrder.Language.Equiv.coe_toEmbedding
-- 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 ≤ g
⊢ f.dom ≤ g.dom

Tactic:
let ⟨_, eq⟩ := h
-- 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 ≤ g
w : f.dom ≤ g.dom
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w)) = f.cod.subtype.comp f.toEquiv.toEmbedding

Tactic:
let ⟨_, eq⟩ := h
-- 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 ≤ g
w : f.dom ≤ g.dom
eq : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w)) = f.cod.subtype.comp f.toEquiv.toEmbedding
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) = f.cod.subtype.comp f.toEquiv.toEmbedding

Tactic:
eq
-- 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 ≤ g
w : f.dom ≤ g.dom
eq : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w)) = f.cod.subtype.comp f.toEquiv.toEmbedding
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) = f.cod.subtype.comp f.toEquiv.toEmbedding

Tactic:
exact eq
-- 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 ≤ g
rw : f.cod.subtype.comp f.toEquiv.toEmbedding = g.cod.subtype.comp ((inclusion ⋯).comp f.toEquiv.toEmbedding)
⊢ g.toEquiv.toEmbedding.comp (inclusion ⋯) = (inclusion ⋯).comp f.toEquiv.toEmbedding

Tactic:
rw [← (subtype _).comp_inj, subtype_toEquiv_inclusion h]

Premises used: FirstOrder.Language.PartialEquiv.subtype_toEquiv_inclusion, FirstOrder.Language.Embedding.comp_inj, FirstOrder.Language.Substructure.subtype
-- 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 ≤ g
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 ⋯).comp f.toEquiv.toEmbedding) : (a : ↥f.dom) → N) x : N)
⊢ f.cod.subtype.comp f.toEquiv.toEmbedding = g.cod.subtype.comp ((inclusion ⋯).comp f.toEquiv.toEmbedding)

Tactic:
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 ≤ g
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 ⋯).comp f.toEquiv.toEmbedding) : (a : ↥f.dom) → N) x : N)

Tactic:
simp
-- 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 ≤ g
x : ↥f.dom
a :
  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)
⊢ 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)

Tactic:
apply (subtype _).injective

Premises used: FirstOrder.Language.Embedding.injective, FirstOrder.Language.Substructure.subtype
-- 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 ≤ g
x : ↥f.dom
a :
  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)
⊢ 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)

Tactic:
change (subtype _).comp (g.toEquiv.toEmbedding.comp (inclusion _)) x = _

Premises used: FirstOrder.Language.PartialEquiv.toEquiv, FirstOrder.Language.Embedding.comp, FirstOrder.Language.Equiv.toEmbedding, FirstOrder.Language.Substructure.inclusion, FirstOrder.Language.Substructure.subtype, DFunLike.coe
-- 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 ≤ g
x : ↥f.dom
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 ⋯ : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod) :
      N)
⊢ 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)

Tactic:
rw [subtype_toEquiv_inclusion h]

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
h : f ≤ g
x : ↥f.dom
⊢ 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 ⋯ : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x) : ↥g.cod) :
      N)

Tactic:
simp
-- 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
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)
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
⊢ 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
-- 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 ≤ g
x : ↥f.dom
a :
  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))
⊢ 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)

Tactic:
apply (subtype _).inj'

Premises used: FirstOrder.Language.Embedding.toEmbedding, Function.Embedding.inj', FirstOrder.Language.Substructure.subtype
-- 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 ≤ g
x : ↥f.dom
a :
  g.cod.subtype.toFun ((inclusion ⋯ : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x)) =
    g.cod.subtype.toFun ((inclusion ⋯ : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x))
a₁ : f ≤ g
a₂ :
  g.cod.subtype.toFun ((inclusion ⋯ : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x)) =
    g.cod.subtype.toFun ((inclusion ⋯ : (a : ↥f.cod) → ↥g.cod) ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) x))
a₃ a₄ a₅ : f ≤ g
⊢ 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))

Tactic:
rwa [toEquiv_inclusion_apply]

Premises used: FirstOrder.Language.PartialEquiv.toEquiv_inclusion_apply
-- 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
⊢ 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:
exact fun h ↦ ⟨dom_le_dom h, cod_le_cod h,
      by intro x; apply (subtype _).inj'; rwa [toEquiv_inclusion_apply]⟩
-- 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
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)
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)
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion dom_le_dom)) = f.cod.subtype.comp f.toEquiv.toEmbedding

Tactic:
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
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
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)
⊢ 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:
change subtype _ (g.toEquiv _) = _

Premises used: FirstOrder.Language.PartialEquiv.toEquiv, FirstOrder.Language.Substructure.subtype, DFunLike.coe