awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Fraisse
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).out : Type w) ≃[L] (↑N : Type w)
refine_2 :
  (e : (↑(F 0).out : Type w) ≃[L] (↑N : Type w)) → (↑(F 0).out : Type w) ↪[L] (↑(↑(G 0) : Bundled L.Structure) : Type w)
refine_2₁ :
  (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)
⊢ (↑(F n).out : Type w) ↪[L] (↑(↑(G n) : Bundled L.Structure) : Type w)

Tactic:
rcases n with - | n
-- Module: Mathlib.ModelTheory.Fraisse
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
e : (↑(F 0).out : Type w) ≃[L] (↑N : Type w)
refine_2 : (↑(F 0).out : Type w) ↪[L] (↑(F 0).out : Type w)
⊢ (↑(F 0).out : Type w) ↪[L] (↑(↑(G 0) : Bundled L.Structure) : Type w)

Tactic:
dsimp [G]
-- Module: Mathlib.ModelTheory.Fraisse
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
e : (↑(F 0).out : Type w) ≃[L] (↑N : Type w)
⊢ (↑(F 0).out : Type w) ↪[L] (↑(F 0).out : Type w)

Tactic:
exact Embedding.refl _ _

Premises used: FirstOrder.Language.Embedding.refl
-- Module: Mathlib.ModelTheory.Fraisse
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)
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 ⋯)
            (fun (n : ℕ) (N : (↑K : Type (max (max u v) (w + 1)))) ↦
              Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (P N n) ⋯)
            n)
          n) :
      Type w)
⊢ (↑(F (n + 1)).out : Type w) ↪[L] (↑(↑(G (n + 1)) : Bundled L.Structure) : Type w)

Tactic:
dsimp [G]
-- Module: Mathlib.ModelTheory.Fraisse
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]
    (↑(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 ⋯)
            (fun (n : ℕ) (N : (↑K : Type (max (max u v) (w + 1)))) ↦
              Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (P N n) ⋯)
            n)
          n) :
      Type w)

Tactic:
exact (hFP _ n).some

Premises used: Nonempty.some
-- Module: Mathlib.ModelTheory.Fraisse
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
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
⊢ (∃ (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
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
inst : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
M : Bundled L.Structure
h1 : Countable.{w + 1} (↑M : Type w)
⊢ (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))) ∧
      Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' L.age (↑M : Type w)) ∧
        (∀ M_1 ∈ L.age (↑M : Type w), Structure.FG.{w, u, v} L (↑M_1 : Type w)) ∧
          Hereditary (L.age (↑M : Type w)) ∧ JointEmbedding (L.age (↑M : Type w))

Tactic:
⟨age.nonempty M, age.is_equiv_invariant L M, age.countable_quotient M, fun N hN => hN.1,
      age.hereditary M, age.jointEmbedding M⟩

Premises used: FirstOrder.Language.age.nonempty, FirstOrder.Language.age.countable_quotient, FirstOrder.Language.age.is_equiv_invariant, CategoryTheory.Bundled.α, And.left, And.intro, FirstOrder.Language.age.jointEmbedding, FirstOrder.Language.age.hereditary
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
inst : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
M : Bundled L.Structure
h1 : Countable.{w + 1} (↑M : Type w)
⊢ (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))) ∧
      Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' L.age (↑M : Type w)) ∧
        (∀ M_1 ∈ L.age (↑M : Type w), Structure.FG.{w, u, v} L (↑M_1 : Type w)) ∧
          Hereditary (L.age (↑M : Type w)) ∧ JointEmbedding (L.age (↑M : Type w))

Tactic:
refine ⟨age.nonempty M, age.is_equiv_invariant L M, age.countable_quotient M, fun N hN => hN.1,
      age.hereditary M, age.jointEmbedding M⟩
-- Module: Mathlib.ModelTheory.Fraisse
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
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)
⊢ ∃ (M : Bundled L.Structure), Countable.{w + 1} (↑M : Type w) ∧ L.age (↑M : Type w) = K

Tactic:
obtain ⟨M, hM, rfl⟩ := exists_cg_is_age_of Kn cq hfg hp jep

Premises used: FirstOrder.Language.exists_cg_is_age_of, rfl
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
inst : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
M : Bundled L.Structure
hM : Structure.CG.{w, u, v} L (↑M : Type w)
Kn : (L.age (↑M : Type w)).Nonempty
left :
  ∀ (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:
⟨M, Structure.cg_iff_countable.1 hM, rfl⟩

Premises used: And.intro, Exists.intro, Iff.mp, FirstOrder.Language.Structure.cg_iff_countable, rfl
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
inst : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
M : Bundled L.Structure
hM : Structure.CG.{w, u, v} L (↑M : Type w)
Kn : (L.age (↑M : Type w)).Nonempty
left :
  ∀ (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:
exact ⟨M, Structure.cg_iff_countable.1 hM, rfl⟩
-- 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
let : ∀ (r : T ↪[L] M), ∃ (f' : T ↪[L] M), f = f'.comp g
⊢ ∃ (f' : T ↪[L] M), f = f'.comp g

Tactic:
let ⟨r⟩ := h
-- 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
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
⊢ ∃ (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)
-- 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
h₁ : f = (t.toEmbedding.comp r).comp g
⊢ ∃ (f' : T ↪[L] M), f = f'.comp g

Tactic:
use t.toEmbedding.comp r

Premises used: FirstOrder.Language.Embedding.comp, FirstOrder.Language.Equiv.toEmbedding
-- 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
h₁ : f = t.toEmbedding.comp s
⊢ f = (t.toEmbedding.comp r).comp g

Tactic:
change _ = t.toEmbedding.comp s

Premises used: FirstOrder.Language.Embedding.comp, FirstOrder.Language.Equiv.toEmbedding
-- 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
h₁ : ∀ (x : S), Eq.{w + 1} (α := M) ((f : (a : S) → M) x : M) ((t.toEmbedding.comp s : (a : S) → M) x : M)
⊢ f = t.toEmbedding.comp s

Tactic:
ext x
-- 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 (α := 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) ⋯ : ↥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) ⋯ : ↥s.toHom.range) :
      M)

Tactic:
have eq' := congr_fun (congr_arg DFunLike.coe eq) ⟨s x, Hom.mem_range.2 ⟨x, rfl⟩⟩
-- 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₁ :
  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)
⊢ Eq.{w + 1} (α := M) ((f : (a : S) → M) x : M) ((t.toEmbedding.comp s : (a : S) → M) x : M)

Tactic:
simp only [Embedding.comp_apply, ← eq', Equiv.coe_toEmbedding, EmbeddingLike.apply_eq_iff_eq]

Premises used: EmbeddingLike.apply_eq_iff_eq, FirstOrder.Language.Embedding.comp_apply, FirstOrder.Language.Equiv.coe_toEmbedding
-- 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} (α := ↥(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)
⊢ 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)

Tactic:
apply (Embedding.equivRange (Embedding.comp r g)).injective

Premises used: FirstOrder.Language.Embedding.comp, FirstOrder.Language.Equiv.injective, FirstOrder.Language.Embedding.equivRange