awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
⊢ g.toEmbedding.toPartialEquiv.cod.subtype.comp
      (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
    g.toEmbedding.comp S.subtype
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨g, hg⟩ := h (PM.comp NP).toHom.range (Nfg.range _)
    ((QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding)
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
have refine : Embedding.comp (Embedding.comp (Substructure.inclusion sorry) (g.toEmbedding.comp PM).equivRange.toEmbedding) NP =
  Embedding.comp (Embedding.comp (Substructure.inclusion sorry) QM.equivRange.toEmbedding) 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 _⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
⊢ Embedding.comp (Embedding.comp (Substructure.inclusion ⋯) (g.toEmbedding.comp PM).equivRange.toEmbedding) NP =
    Embedding.comp (Embedding.comp (Substructure.inclusion ⋯) QM.equivRange.toEmbedding) NQ
have h₁ : ∀ (n : (↑N : Type w)),
  Eq (α := (↑(Bundled.of ↥s) : Type w))
    ((Embedding.comp (Embedding.comp (Substructure.inclusion sorry) (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 sorry) QM.equivRange.toEmbedding) NQ :
          (a : (↑N : Type w)) → (↑(Bundled.of ↥s) : Type w))
        n :
      (↑(Bundled.of ↥s) : Type w))
Tactic: ext n
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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 (α := (↑(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))
have h₁ : Eq.{w + 1} (α := M)
  (↑((Embedding.comp (Embedding.comp (Substructure.inclusion sorry) (g.toEmbedding.comp PM).equivRange.toEmbedding) NP :
          (a : (↑N : Type w)) → (↑(Bundled.of ↥s) : Type w))
        n) :
    M)
  (↑((Embedding.comp (Embedding.comp (Substructure.inclusion sorry) QM.equivRange.toEmbedding) NQ :
          (a : (↑N : Type w)) → (↑(Bundled.of ↥s) : Type w))
        n) :
    M)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
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.{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)
have 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)
Tactic: have hgn := (Embedding.ext_iff.1 hg) ((PM.comp NP).equivRange n)
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
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.{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)
have 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)
Tactic: simp only [Embedding.comp_apply, Equiv.coe_toEmbedding, Equiv.symm_apply_apply,
    Substructure.coe_subtype, Embedding.equivRange_apply] at hgn
Cleared hypotheses: hgn
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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.{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)
have h₁ : Eq.{w + 1} (α := M)
  (↑((Substructure.inclusion sorry : (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 sorry : (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: simp only [Embedding.comp_apply, Equiv.coe_toEmbedding]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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.{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)
have h₁ : Eq.{w + 1} (α := M)
  (↑(Set.inclusion (s := (↑(g.toHom.comp PM.toHom).range : Set M)) (t := (↑s : Set M)) sorry
          (((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)) sorry
          ((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: erw [Substructure.coe_inclusion, Substructure.coe_inclusion]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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.{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)
have 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)
Tactic: simp only [Embedding.equivRange_apply, hgn]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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).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)
have 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)
Tactic: erw [Embedding.comp_apply, Equiv.coe_toEmbedding,
    Embedding.equivRange_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
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}
⊢ ∃ (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
have S_FG : S.FG
Tactic: have S_FG : S.FG := f_FG.sup (Substructure.fg_closure_singleton _)
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
have rw : { α := ↥S, str := inferInstance } ∈ L.age M
Tactic: rw [hN.age, ← hM.age]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
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
⊢ ∃ (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
have S_in_age_N : { α := ↥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 _⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
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
⊢ ∃ (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
have nonempty_S_N : Nonempty.{w + 1} (↥S ↪[L] N)
Tactic: haveI nonempty_S_N : Nonempty (S ↪[L] N) := S_in_age_N.2
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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 : 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
have 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 sorry)),
  ∃ (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))
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
have 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 sorry)) =
  (↑(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: refine ⟨⟨⟨S, g.toHom.range, g.equivRange⟩, S_FG⟩,
    subset_closure.trans (le_sup_right : _ ≤ S) (mem_singleton m), ⟨le_sup_left, ?_⟩⟩