awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
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)
        ((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)
⊢ 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:
rw [← h_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
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)
        ((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:
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
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 : f.dom ≤ g.dom),
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion h)) = f.cod.subtype.comp f.toEquiv.toEmbedding

Tactic:
exact ⟨dom_le_dom, by ext; change subtype _ (g.toEquiv _) = _; rw [← h_eq]; 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 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

Tactic:
⟨le_fg.trans le_gh, ?_⟩

Premises used: Exists.intro, LE.le.trans
-- Module: Mathlib.ModelTheory.PartialEquiv
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
refine : h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion ⋯)) = f.cod.subtype.comp f.toEquiv.toEmbedding
⊢ f ≤ h

Tactic:
refine ⟨le_fg.trans le_gh, ?_⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
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
rw :
  h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion ⋯)) =
    (h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion le_gh))).comp (inclusion le_fg)
⊢ h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion ⋯)) = f.cod.subtype.comp f.toEquiv.toEmbedding

Tactic:
rw [← eq_fg, ← Embedding.comp_assoc (g := g.toEquiv.toEmbedding), ← eq_gh]

Premises used: FirstOrder.Language.PartialEquiv.toEquiv, FirstOrder.Language.Equiv.toEmbedding, FirstOrder.Language.Embedding.comp_assoc
-- Module: Mathlib.ModelTheory.PartialEquiv
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₁ :
  ∀ (x : ↥f.dom),
    Eq.{w' + 1} (α := N) ((h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion ⋯)) : (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)
⊢ h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion ⋯)) =
    (h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion le_gh))).comp (inclusion le_fg)

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 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
x : ↥f.dom
⊢ Eq.{w' + 1} (α := N) ((h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion ⋯)) : (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:
simp
-- 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 ≤ f

Tactic:
⟨le_rfl, rfl⟩

Premises used: le_rfl, Exists.intro, rfl
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f g : M ≃ₚ[L] N
le_fg : f ≤ g
le_gf : g ≤ f
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
⊢ f = g

Tactic:
let ⟨dom_f, cod_f, equiv_f⟩ := f
-- 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_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 }
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
⊢ { dom := dom_f, 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)

Premises used: FirstOrder.Language.PartialEquiv.dom_le_dom, le_antisymm
-- 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
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 }
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
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g

Tactic:
cases _root_.le_antisymm (cod_le_cod le_fg) (cod_le_cod le_gf)

Premises used: le_antisymm, FirstOrder.Language.PartialEquiv.cod_le_cod
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f 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 } = { dom := g.1, cod := g.2, toEquiv := equiv_f }

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
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 }
h : HEq g.dom (β := L.Substructure M) g.1 → HEq g.cod (β := L.Substructure N) g.2 → g.toEquiv = equiv_f
⊢ { dom := g.1, cod := g.2, toEquiv := equiv_f : M ≃ₚ[L] N } = g

Tactic:
convert! 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
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 }
e_6 : HEq g.dom (β := L.Substructure M) g.1
e_7 : HEq g.cod (β := L.Substructure N) g.2
⊢ g.toEquiv = equiv_f

Tactic:
Equiv.injective_toEmbedding ((subtype _).comp_injective (subtype_toEquiv_inclusion le_fg))

Premises used: FirstOrder.Language.Equiv.injective_toEmbedding, FirstOrder.Language.PartialEquiv.subtype_toEquiv_inclusion, FirstOrder.Language.Substructure.subtype, FirstOrder.Language.Embedding.comp_injective
-- 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
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 }
e_6 : HEq g.dom (β := L.Substructure M) g.1
e_7 : HEq g.cod (β := L.Substructure N) g.2
⊢ g.toEquiv = equiv_f

Tactic:
exact Equiv.injective_toEmbedding ((subtype _).comp_injective (subtype_toEquiv_inclusion le_fg))

Premises used: FirstOrder.Language.Equiv.injective_toEmbedding, FirstOrder.Language.PartialEquiv.subtype_toEquiv_inclusion, FirstOrder.Language.Substructure.subtype, FirstOrder.Language.Embedding.comp_injective
-- 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
hfg : f ≤ g
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)
⊢ f.symm ≤ g.symm

Tactic:
rw [le_iff]

Premises used: FirstOrder.Language.PartialEquiv.le_iff
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f g : M ≃ₚ[L] N
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)

Tactic:
⟨cod_le_cod hfg, dom_le_dom hfg, ?_⟩

Premises used: FirstOrder.Language.PartialEquiv.dom_le_dom, Exists.intro, FirstOrder.Language.PartialEquiv.cod_le_cod
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
refine :
  ∀ (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)
⊢ ∃ (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:
refine ⟨cod_le_cod hfg, dom_le_dom hfg, ?_⟩
-- 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
hfg : f ≤ g
x : ↥f.symm.dom
a :
  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)
⊢ 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)

Tactic:
apply g.toEquiv.injective

Premises used: FirstOrder.Language.PartialEquiv.toEquiv, FirstOrder.Language.Equiv.injective
-- 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
hfg : f ≤ g
x : ↥f.symm.dom
a :
  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)
⊢ 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)

Tactic:
change g.toEquiv (inclusion _ (f.toEquiv.symm x)) = g.toEquiv (g.toEquiv.symm _)

Premises used: FirstOrder.Language.PartialEquiv.toEquiv, FirstOrder.Language.Substructure.inclusion, DFunLike.coe, 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
f g : M ≃ₚ[L] N
hfg : f ≤ g
x : ↥f.symm.dom
a :
  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)
    ((inclusion ⋯ : (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)
⊢ 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)

Tactic:
rw [g.toEquiv.apply_symm_apply, (Equiv.apply_symm_apply f.toEquiv x).symm,
    f.toEquiv.symm_apply_apply]

Premises used: FirstOrder.Language.PartialEquiv.toEquiv, FirstOrder.Language.Equiv.symm_apply_apply, FirstOrder.Language.Equiv.apply_symm_apply, Eq.symm
-- 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
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)
    ((inclusion ⋯ : (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:
toEquiv_inclusion_apply hfg _

Premises used: Set.Mem, 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
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)
    ((inclusion ⋯ : (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:
exact toEquiv_inclusion_apply hfg _

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

Tactic:
fun _ _ => symm_le_symm

Premises used: Set.Mem, Monotone, FirstOrder.Language.PartialEquiv.symm_le_symm
-- 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
g : N ≃ₚ[L] M
h : f.symm ≤ g
rw : f.symm.symm ≤ g.symm
⊢ f ≤ g.symm

Tactic:
rw [← f.symm_symm]

Premises used: FirstOrder.Language.PartialEquiv.symm_symm
-- 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
g : N ≃ₚ[L] M
h : f.symm ≤ g
⊢ f.symm.symm ≤ g.symm

Tactic:
monotone_symm h

Premises used: FirstOrder.Language.PartialEquiv.monotone_symm, Set.Mem
-- 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
g : N ≃ₚ[L] M
h : f.symm ≤ g
⊢ f.symm.symm ≤ g.symm

Tactic:
exact monotone_symm h

Premises used: FirstOrder.Language.PartialEquiv.monotone_symm
-- 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
g : N ≃ₚ[L] M
h : f ≤ g.symm
rw : f.symm ≤ g.symm.symm
⊢ f.symm ≤ g

Tactic:
rw  [← g.symm_symm]

Premises used: FirstOrder.Language.PartialEquiv.symm_symm
-- 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
g : N ≃ₚ[L] M
h : f ≤ g.symm
⊢ f.symm ≤ g.symm.symm

Tactic:
monotone_symm h

Premises used: FirstOrder.Language.PartialEquiv.monotone_symm, Set.Mem
-- 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
g : N ≃ₚ[L] M
h : f ≤ g.symm
⊢ f.symm ≤ g.symm.symm

Tactic:
exact monotone_symm h

Premises used: FirstOrder.Language.PartialEquiv.monotone_symm
-- 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_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)
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 ⋯) : ↥g.cod) :
            N)),
    { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g
⊢ f = g

Tactic:
rcases f with ⟨dom_f, cod_f, equiv_f⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
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)
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 ⋯) : ↥g.cod) :
            N)),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g
⊢ { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g

Tactic:
cases h_dom