awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ Eq (α := M)
    (((QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding : (a : ↥(PM.comp NP).toHom.range) → M)
        (((PM.comp NP).equivRange : (a : (↑N : Type w)) → ↥(PM.comp NP).toHom.range) n : ↥(PM.comp NP).toHom.range) :
      M)
    ((g.toEmbedding.comp (PM.comp NP).toHom.range.subtype : (a : ↥(PM.comp NP).toHom.range) → M)
        (((PM.comp NP).equivRange : (a : (↑N : Type w)) → ↥(PM.comp NP).toHom.range) n : ↥(PM.comp NP).toHom.range) :
      M)

Tactic:
have hgn := (Embedding.ext_iff.1 hg) ((PM.comp NP).equivRange 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)
hgn :
  Eq (α := M)
    (((QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding : (a : ↥(PM.comp NP).toHom.range) → M)
        (((PM.comp NP).equivRange : (a : (↑N : Type w)) → ↥(PM.comp NP).toHom.range) n : ↥(PM.comp NP).toHom.range) :
      M)
    ((g.toEmbedding.comp (PM.comp NP).toHom.range.subtype : (a : ↥(PM.comp NP).toHom.range) → M)
        (((PM.comp NP).equivRange : (a : (↑N : Type w)) → ↥(PM.comp NP).toHom.range) n : ↥(PM.comp NP).toHom.range) :
      M)
⊢ Eq (α := M) ((QM : (a : (↑Q : Type w)) → M) ((NQ : (a : (↑N : Type w)) → (↑Q : Type w)) n : (↑Q : Type w)) : M)
    ((g : (a : M) → M)
        ((PM : (a : (↑P : Type w)) → M) ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n : (↑P : Type w)) : M) :
      M)

Tactic:
simp only [Embedding.comp_apply, Equiv.coe_toEmbedding, Equiv.symm_apply_apply,
    Substructure.coe_subtype, Embedding.equivRange_apply] at hgn

Premises used: FirstOrder.Language.Equiv.symm_apply_apply, 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
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)
hgn :
  Eq (α := M) ((QM : (a : (↑Q : Type w)) → M) ((NQ : (a : (↑N : Type w)) → (↑Q : Type w)) n : (↑Q : Type w)) : M)
    ((g : (a : M) → M)
        ((PM : (a : (↑P : Type w)) → M) ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n : (↑P : Type w)) : M) :
      M)
h₁ :
  Eq.{w + 1} (α := M)
    (↑((Substructure.inclusion ⋯ : (a : ↥(g.toHom.comp PM.toHom).range) → (↑(Bundled.of ↥s) : Type w))
          (((g.toEmbedding.comp PM).equivRange.toEmbedding : (a : (↑P : Type w)) → ↥(g.toHom.comp PM.toHom).range)
            ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n))) :
      M)
    (↑((Substructure.inclusion ⋯ : (a : ↥QM.toHom.range) → (↑(Bundled.of ↥s) : Type w))
          ((QM.equivRange : (a : (↑Q : Type w)) → ↥QM.toHom.range) ((NQ : (a : (↑N : Type w)) → (↑Q : Type w)) n))) :
      M)
⊢ 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)

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

Premises used: FirstOrder.Language.Embedding.comp_apply, FirstOrder.Language.Equiv.coe_toEmbedding
-- 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)
hgn :
  Eq (α := M) ((QM : (a : (↑Q : Type w)) → M) ((NQ : (a : (↑N : Type w)) → (↑Q : Type w)) n : (↑Q : Type w)) : M)
    ((g : (a : M) → M)
        ((PM : (a : (↑P : Type w)) → M) ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n : (↑P : Type w)) : M) :
      M)
h₁ :
  Eq.{w + 1} (α := M)
    (↑(Set.inclusion (s := (↑(g.toHom.comp PM.toHom).range : Set M)) (t := (↑s : Set M)) ⋯
            (((g.toEmbedding.comp PM).equivRange.toEmbedding : (a : (↑P : Type w)) → ↥(g.toHom.comp PM.toHom).range)
              ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n)) :
          (↑(↑s : Set M) : Type w)) :
      M)
    (↑(Set.inclusion (s := (↑QM.toHom.range : Set M)) (t := (↑s : Set M)) ⋯
            ((QM.equivRange : (a : (↑Q : Type w)) → ↥QM.toHom.range) ((NQ : (a : (↑N : Type w)) → (↑Q : Type w)) n)) :
          (↑(↑s : Set M) : Type w)) :
      M)
⊢ Eq.{w + 1} (α := M)
    (↑((Substructure.inclusion ⋯ : (a : ↥(g.toHom.comp PM.toHom).range) → (↑(Bundled.of ↥s) : Type w))
          (((g.toEmbedding.comp PM).equivRange.toEmbedding : (a : (↑P : Type w)) → ↥(g.toHom.comp PM.toHom).range)
            ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n))) :
      M)
    (↑((Substructure.inclusion ⋯ : (a : ↥QM.toHom.range) → (↑(Bundled.of ↥s) : Type w))
          ((QM.equivRange : (a : (↑Q : Type w)) → ↥QM.toHom.range) ((NQ : (a : (↑N : Type w)) → (↑Q : Type w)) n))) :
      M)

Tactic:
erw [Substructure.coe_inclusion, Substructure.coe_inclusion]

Premises used: FirstOrder.Language.Substructure.coe_inclusion
-- 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)
hgn :
  Eq (α := M) ((QM : (a : (↑Q : Type w)) → M) ((NQ : (a : (↑N : Type w)) → (↑Q : Type w)) n : (↑Q : Type w)) : M)
    ((g : (a : M) → M)
        ((PM : (a : (↑P : Type w)) → M) ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n : (↑P : Type w)) : M) :
      M)
h₁ :
  Eq (α := M)
    ((↑(((g.toEmbedding.comp PM).equivRange.toEmbedding : (a : (↑P : Type w)) → ↥(g.toHom.comp PM.toHom).range)
            ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n)) :
        M) :
      M)
    ((g : (a : M) → M)
        ((PM : (a : (↑P : Type w)) → M) ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n : (↑P : Type w)) : M) :
      M)
⊢ Eq.{w + 1} (α := M)
    (↑(Set.inclusion (s := (↑(g.toHom.comp PM.toHom).range : Set M)) (t := (↑s : Set M)) ⋯
            (((g.toEmbedding.comp PM).equivRange.toEmbedding : (a : (↑P : Type w)) → ↥(g.toHom.comp PM.toHom).range)
              ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n)) :
          (↑(↑s : Set M) : Type w)) :
      M)
    (↑(Set.inclusion (s := (↑QM.toHom.range : Set M)) (t := (↑s : Set M)) ⋯
            ((QM.equivRange : (a : (↑Q : Type w)) → ↥QM.toHom.range) ((NQ : (a : (↑N : Type w)) → (↑Q : Type w)) n)) :
          (↑(↑s : Set M) : Type w)) :
      M)

Tactic:
simp only [Embedding.equivRange_apply, hgn]

Premises used: FirstOrder.Language.Embedding.equivRange_apply
-- 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)
hgn :
  Eq (α := M) ((QM : (a : (↑Q : Type w)) → M) ((NQ : (a : (↑N : Type w)) → (↑Q : Type w)) n : (↑Q : Type w)) : M)
    ((g : (a : M) → M)
        ((PM : (a : (↑P : Type w)) → M) ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n : (↑P : Type w)) : M) :
      M)
h₁ :
  Eq (α := M)
    ((g.toEmbedding.comp PM : (a : (↑P : Type w)) → M) ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n : (↑P : Type w)) :
      M)
    ((g : (a : M) → M)
        ((PM : (a : (↑P : Type w)) → M) ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n : (↑P : Type w)) : M) :
      M)
⊢ Eq (α := M)
    ((↑(((g.toEmbedding.comp PM).equivRange.toEmbedding : (a : (↑P : Type w)) → ↥(g.toHom.comp PM.toHom).range)
            ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n)) :
        M) :
      M)
    ((g : (a : M) → M)
        ((PM : (a : (↑P : Type w)) → M) ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n : (↑P : Type w)) : M) :
      M)

Tactic:
erw [Embedding.comp_apply, Equiv.coe_toEmbedding,
    Embedding.equivRange_apply]

Premises used: 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
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)
hgn :
  Eq (α := M) ((QM : (a : (↑Q : Type w)) → M) ((NQ : (a : (↑N : Type w)) → (↑Q : Type w)) n : (↑Q : Type w)) : M)
    ((g : (a : M) → M)
        ((PM : (a : (↑P : Type w)) → M) ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n : (↑P : Type w)) : M) :
      M)
⊢ Eq (α := M)
    ((g.toEmbedding.comp PM : (a : (↑P : Type w)) → M) ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n : (↑P : Type w)) :
      M)
    ((g : (a : M) → M)
        ((PM : (a : (↑P : Type w)) → M) ((NP : (a : (↑N : Type w)) → (↑P : Type w)) n : (↑P : Type w)) : M) :
      M)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
inst_1 : Countable M
h : L.IsUltrahomogeneous M
⊢ IsFraisse (L.age M)

Tactic:
⟨age.nonempty M, fun _ hN => hN.1, age.countable_quotient M,
    age.hereditary M, age.jointEmbedding M, h.amalgamation_age⟩

Premises used: FirstOrder.Language.age.nonempty, FirstOrder.Language.age.countable_quotient, And.left, FirstOrder.Language.IsFraisse.mk, FirstOrder.Language.age.jointEmbedding, FirstOrder.Language.IsUltrahomogeneous.amalgamation_age, FirstOrder.Language.age.hereditary
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
inst_1 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_2 : Countable M
h : IsFraisseLimit K M
⊢ IsFraisse K

Tactic:
(congr rfl h.age).mp h.ultrahomogeneous.age_isFraisse

Premises used: Eq.mp, FirstOrder.Language.IsFraisseLimit.age, FirstOrder.Language.IsFraisseLimit.ultrahomogeneous, congr, FirstOrder.Language.IsUltrahomogeneous.age_isFraisse, rfl
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
⊢ S.FG

Tactic:
have S_FG : S.FG := f_FG.sup (Substructure.fg_closure_singleton _)
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
S_FG : S.FG
rw : { α := ↥S, str := inferInstance } ∈ L.age M
⊢ { α := ↥S, str := inferInstance } ∈ L.age N

Tactic:
rw [hN.age, ← hM.age]

Premises used: FirstOrder.Language.IsFraisseLimit.age
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
S_FG : S.FG
⊢ { α := ↥S, str := inferInstance } ∈ L.age M

Tactic:
⟨(fg_iff_structure_fg S).1 S_FG, ⟨subtype _⟩⟩

Premises used: Set.Mem, FirstOrder.Language.age, FirstOrder.Language.Substructure.fg_iff_structure_fg, setOf, Nonempty.intro, And.intro, Iff.mp, FirstOrder.Language.Substructure.subtype
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
S_FG : S.FG
⊢ { α := ↥S, str := inferInstance } ∈ L.age M

Tactic:
exact ⟨(fg_iff_structure_fg S).1 S_FG, ⟨subtype _⟩⟩
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
S_FG : S.FG
⊢ { α := ↥S, str := inferInstance } ∈ L.age N

Tactic:
have S_in_age_N : ⟨S, inferInstance⟩ ∈ L.age N := by
    rw [hN.age, ← hM.age]
    exact ⟨(fg_iff_structure_fg S).1 S_FG, ⟨subtype _⟩⟩
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
S_FG : S.FG
S_in_age_N : { α := ↥S, str := inferInstance } ∈ L.age N
⊢ Nonempty.{w + 1} (↥S ↪[L] N)

Tactic:
haveI nonempty_S_N : Nonempty (S ↪[L] N) := S_in_age_N.2
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
S_FG : S.FG
S_in_age_N : { α := ↥S, str := inferInstance } ∈ L.age N
nonempty_S_N : Nonempty.{w + 1} (↥S ↪[L] N)
let :
  ∀ (g : ↥(f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}) ↪[L] N)
    (g_eq : f.cod.subtype.comp f.toEquiv.toEmbedding = g.comp (Substructure.inclusion ⋯)),
    ∃ (g : L.FGEquiv M N), m ∈ (↑g : M ≃ₚ[L] N).dom ∧ Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG ≤ g
⊢ ∃ (g : L.FGEquiv M N), m ∈ (↑g : M ≃ₚ[L] N).dom ∧ Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG ≤ g

Tactic:
let ⟨g, g_eq⟩ := hN.ultrahomogeneous.extend_embedding (f.dom.fg_iff_structure_fg.1 f_FG)
    ((subtype f.cod).comp f.toEquiv.toEmbedding) (inclusion (le_sup_left : _ ≤ S))
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
S_FG : S.FG
S_in_age_N : { α := ↥S, str := inferInstance } ∈ L.age N
nonempty_S_N : Nonempty.{w + 1} (↥S ↪[L] N)
g : ↥(f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}) ↪[L] N
g_eq : f.cod.subtype.comp f.toEquiv.toEmbedding = g.comp (Substructure.inclusion ⋯)
⊢ ∃ (g : L.FGEquiv M N), m ∈ (↑g : M ≃ₚ[L] N).dom ∧ Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG ≤ g

Tactic:
⟨⟨⟨S, g.toHom.range, g.equivRange⟩, S_FG⟩,
    subset_closure.trans (le_sup_right : _ ≤ S) (mem_singleton m), ⟨le_sup_left, ?_⟩⟩

Premises used: Set.mem_singleton, le_sup_left, 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, And.intro, Exists.intro, FirstOrder.Language.Embedding.toHom
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
S_FG : S.FG
S_in_age_N : { α := ↥S, str := inferInstance } ∈ L.age N
nonempty_S_N : Nonempty.{w + 1} (↥S ↪[L] N)
g : ↥(f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}) ↪[L] N
g_eq : f.cod.subtype.comp f.toEquiv.toEmbedding = g.comp (Substructure.inclusion ⋯)
refine :
  (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                  { dom := S, cod := g.toHom.range, toEquiv := g.equivRange : M ≃ₚ[L] N } S_FG) :
              M ≃ₚ[L] N).cod.subtype.comp
      ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                    { dom := S, cod := g.toHom.range, toEquiv := g.equivRange : M ≃ₚ[L] N } S_FG) :
                M ≃ₚ[L] N).toEquiv.toEmbedding.comp
        (Substructure.inclusion ⋯)) =
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).cod.subtype.comp
      (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).toEquiv.toEmbedding
⊢ ∃ (g : L.FGEquiv M N), m ∈ (↑g : M ≃ₚ[L] N).dom ∧ Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG ≤ g

Tactic:
refine ⟨⟨⟨S, g.toHom.range, g.equivRange⟩, S_FG⟩,
    subset_closure.trans (le_sup_right : _ ≤ S) (mem_singleton m), ⟨le_sup_left, ?_⟩⟩
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
S_FG : S.FG
S_in_age_N : { α := ↥S, str := inferInstance } ∈ L.age N
nonempty_S_N : Nonempty.{w + 1} (↥S ↪[L] N)
g : ↥(f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}) ↪[L] N
g_eq : f.cod.subtype.comp f.toEquiv.toEmbedding = g.comp (Substructure.inclusion ⋯)
h :
  ∀ (x : ↥(↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).dom),
    Eq (α := N)
      (((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                          { dom := S, cod := g.toHom.range, toEquiv := g.equivRange : M ≃ₚ[L] N } S_FG) :
                      M ≃ₚ[L] N).cod.subtype.comp
              ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                            { dom := S, cod := g.toHom.range, toEquiv := g.equivRange : M ≃ₚ[L] N } S_FG) :
                        M ≃ₚ[L] N).toEquiv.toEmbedding.comp
                (Substructure.inclusion ⋯)) :
            (a : ↥(↑⟨f, f_FG⟩ : M ≃ₚ[L] N).dom) → N)
          x :
        N)
      (((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).cod.subtype.comp
              (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).toEquiv.toEmbedding :
            (a : ↥(↑⟨f, f_FG⟩ : M ≃ₚ[L] N).dom) → N)
          x :
        N)
⊢ (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                  { dom := S, cod := g.toHom.range, toEquiv := g.equivRange : M ≃ₚ[L] N } S_FG) :
              M ≃ₚ[L] N).cod.subtype.comp
      ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                    { dom := S, cod := g.toHom.range, toEquiv := g.equivRange : M ≃ₚ[L] N } S_FG) :
                M ≃ₚ[L] N).toEquiv.toEmbedding.comp
        (Substructure.inclusion ⋯)) =
    (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).cod.subtype.comp
      (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).toEquiv.toEmbedding

Tactic:
ext