awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst_1 : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst_2 : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := r.comp g
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
x : S
eq' :
  Eq.{w + 1} (α := M)
    ((f : (a : S) → M)
        ((s.equivRange.symm.toEmbedding : (a : ↥s.toHom.range) → S)
            (Subtype.mk (p := fun (x : M) ↦ x ∈ s.toHom.range) ((s : (a : S) → M) x) ⋯ : ↥s.toHom.range) :
          S) :
      M)
    ((t.toEmbedding : (a : M) → M) ((s : (a : S) → M) x : M) : M)
h₁ :
  Eq.{w + 1} (α := M) (↑(((r.comp g).equivRange : (a : S) → ↥(r.comp g).toHom.range) x) : M)
    (↑(((r.comp g).equivRange : (a : S) → ↥(r.comp g).toHom.range)
          ((s.equivRange.symm : (a : ↥s.toHom.range) → S)
            (Subtype.mk (p := fun (x : M) ↦ x ∈ s.toHom.range) ((s : (a : S) → M) x) ⋯ : ↥s.toHom.range))) :
      M)
⊢ Eq.{w + 1} (α := ↥(r.comp g).toHom.range)
    (((r.comp g).equivRange : (a : S) → ↥(r.comp g).toHom.range) x : ↥(r.comp g).toHom.range)
    (((r.comp g).equivRange : (a : S) → ↥(r.comp g).toHom.range)
        ((s.equivRange.symm : (a : ↥s.toHom.range) → S)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ s.toHom.range) ((s : (a : S) → M) x) ⋯ : ↥s.toHom.range)) :
      ↥(r.comp g).toHom.range)

Tactic:
ext
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst_1 : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst_2 : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := r.comp g
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
x : S
eq' :
  Eq.{w + 1} (α := M)
    ((f : (a : S) → M)
        ((s.equivRange.symm.toEmbedding : (a : ↥s.toHom.range) → S)
            (Subtype.mk (p := fun (x : M) ↦ x ∈ s.toHom.range) ((s : (a : S) → M) x) ⋯ : ↥s.toHom.range) :
          S) :
      M)
    ((t.toEmbedding : (a : M) → M) ((s : (a : S) → M) x : M) : M)
⊢ Eq.{w + 1} (α := M) (↑(((r.comp g).equivRange : (a : S) → ↥(r.comp g).toHom.range) x) : M)
    (↑(((r.comp g).equivRange : (a : S) → ↥(r.comp g).toHom.range)
          ((s.equivRange.symm : (a : ↥s.toHom.range) → S)
            (Subtype.mk (p := fun (x : M) ↦ x ∈ s.toHom.range) ((s : (a : S) → M) x) ⋯ : ↥s.toHom.range))) :
      M)

Tactic:
simp only [Equiv.apply_symm_apply, Embedding.equivRange_apply, s]

Premises used: FirstOrder.Language.Equiv.apply_symm_apply, FirstOrder.Language.Embedding.equivRange_apply
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
M_CG : Structure.CG L M
mp : L.IsUltrahomogeneous M → L.IsExtensionPair M M
mpr : L.IsExtensionPair M M → L.IsUltrahomogeneous M
⊢ L.IsUltrahomogeneous M ↔ L.IsExtensionPair M M

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
mp :
  ∀ (f : M ≃ₚ[L] M) (f_FG : f.dom.FG) (m : M),
    ∃ (g : L.FGEquiv M M), m ∈ (↑g : M ≃ₚ[L] M).dom ∧ Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) f f_FG ≤ g
⊢ L.IsExtensionPair M M

Tactic:
⟨f, f_FG⟩
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
f : M ≃ₚ[L] M
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
⊢ f.dom ≤ S

Tactic:
have dom_le_S : f.dom ≤ S := le_sup_left
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
f : M ≃ₚ[L] M
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
dom_le_S : f.dom ≤ S
mp :
  ∀ (f' : ↥S ↪[L] M) (eq_f' : f.cod.subtype.comp f.toEquiv.toEmbedding = f'.comp (Substructure.inclusion dom_le_S)),
    ∃ (g : L.FGEquiv M M), m ∈ (↑g : M ≃ₚ[L] M).dom ∧ Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) f f_FG ≤ g
⊢ ∃ (g : L.FGEquiv M M), m ∈ (↑g : M ≃ₚ[L] M).dom ∧ Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) f f_FG ≤ g

Tactic:
let ⟨f', eq_f'⟩ := M_homog.extend_embedding (f.dom.fg_iff_structure_fg.1 f_FG)
      ((subtype _).comp f.toEquiv.toEmbedding) (inclusion dom_le_S) (h := ⟨subtype _⟩)
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
f : M ≃ₚ[L] M
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
dom_le_S : f.dom ≤ S
f' : ↥S ↪[L] M
eq_f' : f.cod.subtype.comp f.toEquiv.toEmbedding = f'.comp (Substructure.inclusion dom_le_S)
⊢ ∃ (g : L.FGEquiv M M), m ∈ (↑g : M ≃ₚ[L] M).dom ∧ Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) f f_FG ≤ g

Tactic:
⟨⟨⟨S, f'.toHom.range, f'.equivRange⟩, f_FG.sup (fg_closure_singleton _)⟩,
      subset_closure.trans (le_sup_right : _ ≤ S) (mem_singleton m), ⟨dom_le_S, ?_⟩⟩

Premises used: Set.mem_singleton, FirstOrder.Language.Substructure.fg_closure_singleton, HasSubset.Subset.trans, le_sup_right, Subtype.mk, FirstOrder.Language.Hom.range, FirstOrder.Language.Embedding.equivRange, FirstOrder.Language.PartialEquiv.mk, FirstOrder.Language.Substructure.subset_closure, FirstOrder.Language.Substructure.FG.sup, And.intro, Exists.intro, FirstOrder.Language.Embedding.toHom
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
f : M ≃ₚ[L] M
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
dom_le_S : f.dom ≤ S
f' : ↥S ↪[L] M
eq_f' : f.cod.subtype.comp f.toEquiv.toEmbedding = f'.comp (Substructure.inclusion dom_le_S)
mp :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                  { dom := S, cod := f'.toHom.range, toEquiv := f'.equivRange : M ≃ₚ[L] M } ⋯) :
              M ≃ₚ[L] M).cod.subtype.comp
      ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                    { dom := S, cod := f'.toHom.range, toEquiv := f'.equivRange : M ≃ₚ[L] M } ⋯) :
                M ≃ₚ[L] M).toEquiv.toEmbedding.comp
        (Substructure.inclusion dom_le_S)) =
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] M).cod.subtype.comp
      (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] M).toEquiv.toEmbedding
⊢ ∃ (g : L.FGEquiv M M), m ∈ (↑g : M ≃ₚ[L] M).dom ∧ Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) f f_FG ≤ g

Tactic:
refine ⟨⟨⟨S, f'.toHom.range, f'.equivRange⟩, f_FG.sup (fg_closure_singleton _)⟩,
      subset_closure.trans (le_sup_right : _ ≤ S) (mem_singleton m), ⟨dom_le_S, ?_⟩⟩
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
f : M ≃ₚ[L] M
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
dom_le_S : f.dom ≤ S
f' : ↥S ↪[L] M
eq_f' : f.cod.subtype.comp f.toEquiv.toEmbedding = f'.comp (Substructure.inclusion dom_le_S)
mp :
  ∀ (x : ↥(↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] M).dom),
    Eq (α := M)
      (((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                          { dom := S, cod := f'.toHom.range, toEquiv := f'.equivRange : M ≃ₚ[L] M } ⋯) :
                      M ≃ₚ[L] M).cod.subtype.comp
              ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                            { dom := S, cod := f'.toHom.range, toEquiv := f'.equivRange : M ≃ₚ[L] M } ⋯) :
                        M ≃ₚ[L] M).toEquiv.toEmbedding.comp
                (Substructure.inclusion dom_le_S)) :
            (a : ↥(↑⟨f, f_FG⟩ : M ≃ₚ[L] M).dom) → M)
          x :
        M)
      (((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] M).cod.subtype.comp
              (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] M).toEquiv.toEmbedding :
            (a : ↥(↑⟨f, f_FG⟩ : M ≃ₚ[L] M).dom) → M)
          x :
        M)
⊢ (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                  { dom := S, cod := f'.toHom.range, toEquiv := f'.equivRange : M ≃ₚ[L] M } ⋯) :
              M ≃ₚ[L] M).cod.subtype.comp
      ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                    { dom := S, cod := f'.toHom.range, toEquiv := f'.equivRange : M ≃ₚ[L] M } ⋯) :
                M ≃ₚ[L] M).toEquiv.toEmbedding.comp
        (Substructure.inclusion dom_le_S)) =
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] M).cod.subtype.comp
      (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] M).toEquiv.toEmbedding

Tactic:
ext
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
f : M ≃ₚ[L] M
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
dom_le_S : f.dom ≤ S
f' : ↥S ↪[L] M
eq_f' : f.cod.subtype.comp f.toEquiv.toEmbedding = f'.comp (Substructure.inclusion dom_le_S)
x : ↥(↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] M).dom
⊢ Eq (α := M)
    (((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                        { dom := S, cod := f'.toHom.range, toEquiv := f'.equivRange : M ≃ₚ[L] M } ⋯) :
                    M ≃ₚ[L] M).cod.subtype.comp
            ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                          { dom := S, cod := f'.toHom.range, toEquiv := f'.equivRange : M ≃ₚ[L] M } ⋯) :
                      M ≃ₚ[L] M).toEquiv.toEmbedding.comp
              (Substructure.inclusion dom_le_S)) :
          (a : ↥(↑⟨f, f_FG⟩ : M ≃ₚ[L] M).dom) → M)
        x :
      M)
    (((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] M).cod.subtype.comp
            (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] M).toEquiv.toEmbedding :
          (a : ↥(↑⟨f, f_FG⟩ : M ≃ₚ[L] M).dom) → M)
        x :
      M)

Tactic:
simp only [Embedding.comp_apply, Equiv.coe_toEmbedding, coe_subtype, eq_f',
      Embedding.equivRange_apply, Substructure.coe_inclusion]

Premises used: FirstOrder.Language.Substructure.coe_inclusion, FirstOrder.Language.Substructure.coe_subtype, FirstOrder.Language.Embedding.comp_apply, FirstOrder.Language.Equiv.coe_toEmbedding, FirstOrder.Language.Embedding.equivRange_apply
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
M_CG : Structure.CG L M
h : L.IsExtensionPair M M
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] M
mpr :
  ∀ (g : M ≃[L] M)
    (dom_le_dom :
      (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] M } S_FG) :
            M ≃ₚ[L] M).dom ≤
        g.toEmbedding.toPartialEquiv.dom)
    (eq :
      g.toEmbedding.toPartialEquiv.cod.subtype.comp
          (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
        (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                      { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] M } S_FG) :
                  M ≃ₚ[L] M).cod.subtype.comp
          (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                    { dom := S, cod := f.toHom.range, toEquiv := f.equivRange } S_FG) :
                M ≃ₚ[L] M).toEquiv.toEmbedding),
    ∃ (g : M ≃[L] M), f = g.toEmbedding.comp S.subtype
⊢ ∃ (g : M ≃[L] M), f = g.toEmbedding.comp S.subtype

Tactic:
let ⟨g, ⟨dom_le_dom, eq⟩⟩ :=
      equiv_between_cg M_CG M_CG ⟨⟨S, f.toHom.range, f.equivRange⟩, S_FG⟩ h h
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
M_CG : Structure.CG L M
h : L.IsExtensionPair M M
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] M
g : M ≃[L] M
dom_le_dom :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
            { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] M } S_FG) :
        M ≃ₚ[L] M).dom ≤
    g.toEmbedding.toPartialEquiv.dom
eq :
  g.toEmbedding.toPartialEquiv.cod.subtype.comp
      (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                  { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] M } S_FG) :
              M ≃ₚ[L] M).cod.subtype.comp
      (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) { dom := S, cod := f.toHom.range, toEquiv := f.equivRange }
                S_FG) :
            M ≃ₚ[L] M).toEquiv.toEmbedding
h₁ : f = g.toEmbedding.comp S.subtype
⊢ ∃ (g : M ≃[L] M), f = g.toEmbedding.comp S.subtype

Tactic:
use g
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
M_CG : Structure.CG L M
h : L.IsExtensionPair M M
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] M
g : M ≃[L] M
dom_le_dom :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
            { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] M } S_FG) :
        M ≃ₚ[L] M).dom ≤
    g.toEmbedding.toPartialEquiv.dom
eq :
  g.toEmbedding.toPartialEquiv.cod.subtype.comp
      (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                  { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] M } S_FG) :
              M ≃ₚ[L] M).cod.subtype.comp
      (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG) { dom := S, cod := f.toHom.range, toEquiv := f.equivRange }
                S_FG) :
            M ≃ₚ[L] M).toEquiv.toEmbedding
⊢ g.toEmbedding.toPartialEquiv.cod.subtype.comp
      (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
    f

Tactic:
simp only [Embedding.subtype_equivRange] at eq

Premises used: FirstOrder.Language.Embedding.subtype_equivRange
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
M_CG : Structure.CG L M
h : L.IsExtensionPair M M
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] M
g : M ≃[L] M
dom_le_dom :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
            { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] M } S_FG) :
        M ≃ₚ[L] M).dom ≤
    g.toEmbedding.toPartialEquiv.dom
eq :
  g.toEmbedding.toPartialEquiv.cod.subtype.comp
      (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
    f
h₁ :
  g.toEmbedding.toPartialEquiv.cod.subtype.comp
      (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
    g.toEmbedding.comp S.subtype
⊢ f = g.toEmbedding.comp S.subtype

Tactic:
rw [← eq]
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
M_CG : Structure.CG L M
h : L.IsExtensionPair M M
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] M
g : M ≃[L] M
dom_le_dom :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
            { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] M } S_FG) :
        M ≃ₚ[L] M).dom ≤
    g.toEmbedding.toPartialEquiv.dom
eq :
  g.toEmbedding.toPartialEquiv.cod.subtype.comp
      (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
    f
h₁ :
  ∀ (x : ↥S),
    Eq (α := M)
      ((g.toEmbedding.toPartialEquiv.cod.subtype.comp
              (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) :
            (a : ↥S) → M)
          x :
        M)
      ((g.toEmbedding.comp S.subtype : (a : ↥S) → M) x : M)
⊢ g.toEmbedding.toPartialEquiv.cod.subtype.comp
      (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
    g.toEmbedding.comp S.subtype

Tactic:
ext
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
M_CG : Structure.CG L M
h : L.IsExtensionPair M M
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] M
g : M ≃[L] M
dom_le_dom :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
            { dom := S, cod := f.toHom.range, toEquiv := f.equivRange : M ≃ₚ[L] M } S_FG) :
        M ≃ₚ[L] M).dom ≤
    g.toEmbedding.toPartialEquiv.dom
eq :
  g.toEmbedding.toPartialEquiv.cod.subtype.comp
      (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
    f
x : ↥S
⊢ Eq (α := M)
    ((g.toEmbedding.toPartialEquiv.cod.subtype.comp
            (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) :
          (a : ↥S) → M)
        x :
      M)
    ((g.toEmbedding.comp S.subtype : (a : ↥S) → M) x : M)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : (↑N : Type w) ↪[L] (↑P : Type w)
NQ : (↑N : Type w) ↪[L] (↑Q : Type w)
Nfg : Structure.FG.{w, u, v} L (↑N : Type w)
Pfg : Structure.FG.{w, u, v} L (↑P : Type w)
PM : (↑P : Type w) ↪[L] M
Qfg : Structure.FG.{w, u, v} L (↑Q : Type w)
QM : (↑Q : Type w) ↪[L] M
obtain :
  ∀ (g : M ≃[L] M)
    (hg :
      (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype),
    ∃ (Q_1 : Bundled L.Structure) (NQ_1 : (↑P : Type w) ↪[L] (↑Q_1 : Type w)) (PQ : (↑Q : Type w) ↪[L] (↑Q_1 : Type w)),
      Q_1 ∈ L.age M ∧ NQ_1.comp NP = PQ.comp NQ
⊢ ∃ (Q_1 : Bundled L.Structure) (NQ_1 : (↑P : Type w) ↪[L] (↑Q_1 : Type w)) (PQ : (↑Q : Type w) ↪[L] (↑Q_1 : Type w)),
    Q_1 ∈ L.age M ∧ NQ_1.comp NP = PQ.comp NQ

Tactic:
obtain ⟨g, hg⟩ := h (PM.comp NP).toHom.range (Nfg.range _)
    ((QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding)

Premises used: FirstOrder.Language.Embedding.comp, FirstOrder.Language.Hom.range, FirstOrder.Language.Embedding.equivRange, FirstOrder.Language.Equiv.toEmbedding, FirstOrder.Language.Structure.FG.range, FirstOrder.Language.Embedding.toHom, FirstOrder.Language.Equiv.symm
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : (↑N : Type w) ↪[L] (↑P : Type w)
NQ : (↑N : Type w) ↪[L] (↑Q : Type w)
Nfg : Structure.FG.{w, u, v} L (↑N : Type w)
Pfg : Structure.FG.{w, u, v} L (↑P : Type w)
PM : (↑P : Type w) ↪[L] M
Qfg : Structure.FG.{w, u, v} L (↑Q : Type w)
QM : (↑Q : Type w) ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
⊢ ∃ (Q_1 : Bundled L.Structure) (NQ_1 : (↑P : Type w) ↪[L] (↑Q_1 : Type w)) (PQ : (↑Q : Type w) ↪[L] (↑Q_1 : Type w)),
    Q_1 ∈ L.age M ∧ NQ_1.comp NP = PQ.comp NQ

Tactic:
⟨Bundled.of s,
    Embedding.comp (Substructure.inclusion le_sup_left)
      (g.toEmbedding.comp PM).equivRange.toEmbedding,
    Embedding.comp (Substructure.inclusion le_sup_right) QM.equivRange.toEmbedding,
    ⟨(fg_iff_structure_fg _).1 (FG.sup (Pfg.range _) (Qfg.range _)), ⟨Substructure.subtype _⟩⟩, ?_⟩

Premises used: FirstOrder.Language.Embedding.comp, le_sup_left, FirstOrder.Language.Substructure.fg_iff_structure_fg, Membership.mem, Subtype, le_sup_right, Nonempty.intro, CategoryTheory.Bundled.of, FirstOrder.Language.Embedding.equivRange, FirstOrder.Language.Substructure.FG.sup, FirstOrder.Language.Equiv.toEmbedding, FirstOrder.Language.Substructure.inclusion, And.intro, Exists.intro, Iff.mp, FirstOrder.Language.Substructure.subtype, FirstOrder.Language.Structure.FG.range
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : (↑N : Type w) ↪[L] (↑P : Type w)
NQ : (↑N : Type w) ↪[L] (↑Q : Type w)
Nfg : Structure.FG.{w, u, v} L (↑N : Type w)
Pfg : Structure.FG.{w, u, v} L (↑P : Type w)
PM : (↑P : Type w) ↪[L] M
Qfg : Structure.FG.{w, u, v} L (↑Q : Type w)
QM : (↑Q : Type w) ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
refine :
  Embedding.comp (Embedding.comp (Substructure.inclusion ⋯) (g.toEmbedding.comp PM).equivRange.toEmbedding) NP =
    Embedding.comp (Embedding.comp (Substructure.inclusion ⋯) QM.equivRange.toEmbedding) NQ
⊢ ∃ (Q_1 : Bundled L.Structure) (NQ_1 : (↑P : Type w) ↪[L] (↑Q_1 : Type w)) (PQ : (↑Q : Type w) ↪[L] (↑Q_1 : Type w)),
    Q_1 ∈ L.age M ∧ NQ_1.comp NP = PQ.comp NQ

Tactic:
refine ⟨Bundled.of s,
    Embedding.comp (Substructure.inclusion le_sup_left)
      (g.toEmbedding.comp PM).equivRange.toEmbedding,
    Embedding.comp (Substructure.inclusion le_sup_right) QM.equivRange.toEmbedding,
    ⟨(fg_iff_structure_fg _).1 (FG.sup (Pfg.range _) (Qfg.range _)), ⟨Substructure.subtype _⟩⟩, ?_⟩
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : (↑N : Type w) ↪[L] (↑P : Type w)
NQ : (↑N : Type w) ↪[L] (↑Q : Type w)
Nfg : Structure.FG.{w, u, v} L (↑N : Type w)
Pfg : Structure.FG.{w, u, v} L (↑P : Type w)
PM : (↑P : Type w) ↪[L] M
Qfg : Structure.FG.{w, u, v} L (↑Q : Type w)
QM : (↑Q : Type w) ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
h₁ :
  ∀ (n : (↑N : Type w)),
    Eq (α := (↑(Bundled.of ↥s) : Type w))
      ((Embedding.comp (Embedding.comp (Substructure.inclusion ⋯) (g.toEmbedding.comp PM).equivRange.toEmbedding) NP :
            (a : (↑N : Type w)) → (↑(Bundled.of ↥s) : Type w))
          n :
        (↑(Bundled.of ↥s) : Type w))
      ((Embedding.comp (Embedding.comp (Substructure.inclusion ⋯) QM.equivRange.toEmbedding) NQ :
            (a : (↑N : Type w)) → (↑(Bundled.of ↥s) : Type w))
          n :
        (↑(Bundled.of ↥s) : Type w))
⊢ Embedding.comp (Embedding.comp (Substructure.inclusion ⋯) (g.toEmbedding.comp PM).equivRange.toEmbedding) NP =
    Embedding.comp (Embedding.comp (Substructure.inclusion ⋯) QM.equivRange.toEmbedding) NQ

Tactic:
ext n
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : (↑N : Type w) ↪[L] (↑P : Type w)
NQ : (↑N : Type w) ↪[L] (↑Q : Type w)
Nfg : Structure.FG.{w, u, v} L (↑N : Type w)
Pfg : Structure.FG.{w, u, v} L (↑P : Type w)
PM : (↑P : Type w) ↪[L] M
Qfg : Structure.FG.{w, u, v} L (↑Q : Type w)
QM : (↑Q : Type w) ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
n : (↑N : Type w)
h₁ :
  Eq.{w + 1} (α := M)
    (↑((Embedding.comp (Embedding.comp (Substructure.inclusion ⋯) (g.toEmbedding.comp PM).equivRange.toEmbedding) NP :
            (a : (↑N : Type w)) → (↑(Bundled.of ↥s) : Type w))
          n) :
      M)
    (↑((Embedding.comp (Embedding.comp (Substructure.inclusion ⋯) QM.equivRange.toEmbedding) NQ :
            (a : (↑N : Type w)) → (↑(Bundled.of ↥s) : Type w))
          n) :
      M)
⊢ Eq (α := (↑(Bundled.of ↥s) : Type w))
    ((Embedding.comp (Embedding.comp (Substructure.inclusion ⋯) (g.toEmbedding.comp PM).equivRange.toEmbedding) NP :
          (a : (↑N : Type w)) → (↑(Bundled.of ↥s) : Type w))
        n :
      (↑(Bundled.of ↥s) : Type w))
    ((Embedding.comp (Embedding.comp (Substructure.inclusion ⋯) QM.equivRange.toEmbedding) NQ :
          (a : (↑N : Type w)) → (↑(Bundled.of ↥s) : Type w))
        n :
      (↑(Bundled.of ↥s) : Type w))

Tactic:
apply Subtype.ext

Premises used: Subtype.ext