awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid
hF :
  ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Quotient.out (s := equivSetoid) (Quotient.mk' x) ≈ a) ↔ ∃ (y : ℕ), (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : (N : (↑K : Type (max (max u v) (w + 1)))) → (n : ℕ) → Bundled L.Structure
hPK : ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ), P N n ∈ K
hP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (↑N : Bundled L.Structure)
      (P N n)
hFP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (F (n + 1)).out (P N n)
G : ℕ → (↑K : Type (max (max u v) (w + 1))) :=
  Nat.rec (motive := fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1))))
    (Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (F 0).out ⋯)
    fun (n : ℕ) (N : (fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1)))) n) ↦
    Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (P N n) ⋯
f : (i j : ℕ) → i ≤ j → (↑(↑(G i) : Bundled L.Structure) : Type w) ↪[L] (↑(↑(G j) : Bundled L.Structure) : Type w) :=
  DirectedSystem.natLERec (G' := fun (i : ℕ) ↦ (↑(↑(G i) : Bundled L.Structure) : Type w)) fun (n : ℕ) ↦ Nonempty.some ⋯
N : Bundled L.Structure
KN : N ∈ K
this : Quotient.out (s := equivSetoid) (Quotient.mk' N) ≈ N
n : ℕ
e : (↑(F (n + 1)).out : Type w) ≃[L] (↑N : Type w)
⊢ (↑(F (n + 1)).out : Type w) ↪[L] (↑(↑(G (n + 1)) : Bundled L.Structure) : Type w)
have refine_2 : (↑(F (n + 1)).out : Type w) ↪[L]
  (↑(P
        (Nat.rec (motive := fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1))))
          (Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (F 0).out sorry)
          (fun (n : ℕ) (N : (↑K : Type (max (max u v) (w + 1)))) ↦
            Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (P N n) sorry)
          n)
        n) :
    Type w)
Tactic: dsimp [G]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
K : Set (Bundled L.Structure)
inst : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
⊢ (∃ (M : Bundled L.Structure), Countable.{w + 1} (↑M : Type w) ∧ L.age (↑M : Type w) = K) ↔
    K.Nonempty ∧
      (∀ (M N : Bundled L.Structure), Nonempty.{w + 1} ((↑M : Type w) ≃[L] (↑N : Type w)) → (M ∈ K ↔ N ∈ K)) ∧
        Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K) ∧
          (∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)) ∧ Hereditary K ∧ JointEmbedding K
have mp : (∃ (M : Bundled L.Structure), Countable.{w + 1} (↑M : Type w) ∧ L.age (↑M : Type w) = K) →
  K.Nonempty ∧
    (∀ (M N : Bundled L.Structure), Nonempty.{w + 1} ((↑M : Type w) ≃[L] (↑N : Type w)) → (M ∈ K ↔ N ∈ K)) ∧
      Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K) ∧
        (∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)) ∧ Hereditary K ∧ JointEmbedding K
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
K : Set (Bundled L.Structure)
inst : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
mp :
  (∃ (M : Bundled L.Structure), Countable.{w + 1} (↑M : Type w) ∧ L.age (↑M : Type w) = K) →
    K.Nonempty ∧
      (∀ (M N : Bundled L.Structure), Nonempty.{w + 1} ((↑M : Type w) ≃[L] (↑N : Type w)) → (M ∈ K ↔ N ∈ K)) ∧
        Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K) ∧
          (∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)) ∧ Hereditary K ∧ JointEmbedding K
⊢ (∃ (M : Bundled L.Structure), Countable.{w + 1} (↑M : Type w) ∧ L.age (↑M : Type w) = K) ↔
    K.Nonempty ∧
      (∀ (M N : Bundled L.Structure), Nonempty.{w + 1} ((↑M : Type w) ≃[L] (↑N : Type w)) → (M ∈ K ↔ N ∈ K)) ∧
        Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K) ∧
          (∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)) ∧ Hereditary K ∧ JointEmbedding K
have mpr : K.Nonempty ∧
    (∀ (M N : Bundled L.Structure), Nonempty.{w + 1} ((↑M : Type w) ≃[L] (↑N : Type w)) → (M ∈ K ↔ N ∈ K)) ∧
      Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K) ∧
        (∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)) ∧ Hereditary K ∧ JointEmbedding K →
  ∃ (M : Bundled L.Structure), Countable.{w + 1} (↑M : Type w) ∧ L.age (↑M : Type w) = K
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
K : Set (Bundled L.Structure)
inst : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
Kn : K.Nonempty
left : ∀ (M N : Bundled L.Structure), Nonempty.{w + 1} ((↑M : Type w) ≃[L] (↑N : Type w)) → (M ∈ K ↔ N ∈ K)
cq : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
hfg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
⊢ ∃ (M : Bundled L.Structure), Countable.{w + 1} (↑M : Type w) ∧ L.age (↑M : Type w) = K
have mpr : ∀ (M : Bundled L.Structure) (hM : Structure.CG.{w, u, v} L (↑M : Type w)) (Kn : (L.age (↑M : Type w)).Nonempty),
  (∀ (M_1 N : Bundled L.Structure),
      Nonempty.{w + 1} ((↑M_1 : Type w) ≃[L] (↑N : Type w)) → (M_1 ∈ L.age (↑M : Type w) ↔ N ∈ L.age (↑M : Type w))) →
    ∀ (cq : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' L.age (↑M : Type w)))
      (hfg : ∀ M_1 ∈ L.age (↑M : Type w), Structure.FG.{w, u, v} L (↑M_1 : Type w))
      (hp : Hereditary (L.age (↑M : Type w))) (jep : JointEmbedding (L.age (↑M : Type w))),
      ∃ (M_1 : Bundled L.Structure), Countable.{w + 1} (↑M_1 : Type w) ∧ L.age (↑M_1 : Type w) = L.age (↑M : Type w)
Tactic: obtain ⟨M, hM, rfl⟩ := exists_cg_is_age_of Kn cq hfg hp jep
Cleared hypotheses: K, Kn, left, cq, hfg, hp, jep
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
⊢ ∃ (f' : T ↪[L] M), f = f'.comp g
have let : ∀ (r : T ↪[L] M), ∃ (f' : T ↪[L] M), f = f'.comp g
Tactic: let ⟨r⟩ := h
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
⊢ ∃ (f' : T ↪[L] M), f = f'.comp g
have let : ∀ (t : M ≃[L] M) (eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype),
  ∃ (f' : T ↪[L] M), f = f'.comp g
Tactic: let ⟨t, eq⟩ := M_homog s.toHom.range (S_FG.range s.toHom) (f.comp s.equivRange.symm.toEmbedding)
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
⊢ ∃ (f' : T ↪[L] M), f = f'.comp g
have h₁ : f = (t.toEmbedding.comp r).comp g
Tactic: use t.toEmbedding.comp r
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
⊢ f = (t.toEmbedding.comp r).comp g
have h₁ : f = t.toEmbedding.comp s
Tactic: change _ = t.toEmbedding.comp s
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
⊢ f = t.toEmbedding.comp s
have h₁ : ∀ (x : S), Eq.{w + 1} (α := M) ((f : (a : S) → M) x : M) ((t.toEmbedding.comp s : (a : S) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
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.{w + 1} (α := M) ((f : (a : S) → M) x : M) ((t.toEmbedding.comp s : (a : S) → M) x : M)
have eq' : Eq (α := M)
  ((f.comp s.equivRange.symm.toEmbedding : (a : ↥s.toHom.range) → M)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ s.toHom.range) ((s : (a : S) → M) x) sorry : ↥s.toHom.range) :
    M)
  ((t.toEmbedding.comp s.toHom.range.subtype : (a : ↥s.toHom.range) → M)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ s.toHom.range) ((s : (a : S) → M) x) sorry : ↥s.toHom.range) :
    M)
Tactic: have eq' := congr_fun (congr_arg DFunLike.coe eq) ⟨s x, Hom.mem_range.2 ⟨x, rfl⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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) ((f : (a : S) → M) x : M) ((t.toEmbedding.comp s : (a : S) → M) x : M)
have h₁ : x =
  (s.equivRange.symm : (a : ↥s.toHom.range) → S)
    (Subtype.mk (p := fun (x : M) ↦ x ∈ s.toHom.range) ((s : (a : S) → M) x) sorry : ↥s.toHom.range)
Tactic: simp only [Embedding.comp_apply, ← eq', Equiv.coe_toEmbedding, EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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)
⊢ x =
    (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)
have h₁ : 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) sorry : ↥s.toHom.range)) :
    ↥(r.comp g).toHom.range)
Tactic: apply (Embedding.equivRange (Embedding.comp r g)).injective
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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} (α := ↥(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)
have 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) sorry : ↥s.toHom.range))) :
    M)
Tactic: ext
-- 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
⊢ L.IsUltrahomogeneous M ↔ L.IsExtensionPair M M
have mp : L.IsUltrahomogeneous M → L.IsExtensionPair M M
Tactic: constructor
-- 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
mp : L.IsUltrahomogeneous M → L.IsExtensionPair M M
⊢ L.IsUltrahomogeneous M ↔ L.IsExtensionPair M M
have mpr : L.IsExtensionPair M M → L.IsUltrahomogeneous M
Tactic: constructor
-- 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
M_homog : L.IsUltrahomogeneous M
⊢ L.IsExtensionPair M M
have 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
Tactic: ⟨f, f_FG⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
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}
⊢ ∃ (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
have dom_le_S : f.dom ≤ S
Tactic: have dom_le_S : f.dom ≤ S := le_sup_left
-- 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
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
⊢ ∃ (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
have 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
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 _⟩)
-- 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
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
have mp : (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] M) ↦ f.dom.FG)
                { dom := S, cod := f'.toHom.range, toEquiv := f'.equivRange : M ≃ₚ[L] M } sorry) :
            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 } sorry) :
              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: 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, ?_⟩⟩
-- 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
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)
⊢ (↑(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
have 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 } sorry) :
                    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 } sorry) :
                      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: ext
-- 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), f = g.toEmbedding.comp S.subtype
have 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
Tactic: let ⟨g, ⟨dom_le_dom, eq⟩⟩ :=
      equiv_between_cg M_CG M_CG ⟨⟨S, f.toHom.range, f.equivRange⟩, S_FG⟩ h h
-- 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)) =
    (↑(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
have h₁ : f = g.toEmbedding.comp S.subtype
Tactic: use g
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
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
⊢ f = g.toEmbedding.comp S.subtype
have eq₁ : 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
Cleared hypotheses: eq
-- 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
⊢ f = g.toEmbedding.comp S.subtype
have h₁ : g.toEmbedding.toPartialEquiv.cod.subtype.comp
    (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
  g.toEmbedding.comp S.subtype
Tactic: rw [← eq]