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
n : ℕ
P : Bundled L.Structure
hP1 : P ∈ K
hP2 : P ≈ (F n).out
⊢ (F n).out ∈ K

Tactic:
exact (hp.is_equiv_invariant_of_fg fg _ _ hP2).1 hP1

Premises used: FirstOrder.Language.Hereditary.is_equiv_invariant_of_fg, Iff.mp
-- 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
⊢ ∀ (n : ℕ), (F n).out ∈ K

Tactic:
have hF' : ∀ n : ℕ, (F n).out ∈ K := by
    intro n
    obtain ⟨P, hP1, hP2⟩ := (hF (F n).out).2 ⟨n, Setoid.refl _⟩
    -- Porting note: fix hP2 because `Quotient.out (Quotient.mk' x) ≈ a` was not simplified
    -- to `x ≈ a` in hF
    replace hP2 := Setoid.trans (Setoid.symm (Quotient.mk_out P)) hP2
    exact (hp.is_equiv_invariant_of_fg fg _ _ hP2).1 hP1
-- 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
choose :
  ∀ (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)),
    ∃ (M : Bundled L.Structure), Structure.CG.{w, u, v} L (↑M : Type w) ∧ L.age (↑M : Type w) = K
⊢ ∃ (M : Bundled L.Structure), Structure.CG.{w, u, v} L (↑M : Type w) ∧ L.age (↑M : Type w) = K

Tactic:
choose P hPK hP hFP using fun (N : K) (n : ℕ) => jep N N.2 (F (n + 1)).out (hF' _)

Premises used: Quotient.out, HAdd.hAdd, OfNat.ofNat, Subtype.val, Subtype.property
-- 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 ⋯
⊢ ∃ (M : Bundled L.Structure), Structure.CG.{w, u, v} L (↑M : Type w) ∧ L.age (↑M : Type w) = K

Tactic:
⟨Bundled.of (@DirectLimit L _ _ (fun n ↦ (G n).val) _ f _ _), ?_, ?_⟩

Premises used: CategoryTheory.Bundled.of, CategoryTheory.Bundled.α, And.intro, Exists.intro, FirstOrder.Language.DirectLimit, Subtype.val
-- 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 ⋯
refine_1 :
  Structure.CG.{w, u, v} L
    (↑(Bundled.of (DirectLimit (fun (n : ℕ) ↦ (↑(↑(G n) : Bundled L.Structure) : Type w)) f)) : Type w)
refine_2 : L.age (↑(Bundled.of (DirectLimit (fun (n : ℕ) ↦ (↑(↑(G n) : Bundled L.Structure) : Type w)) f)) : Type w) = K
⊢ ∃ (M : Bundled L.Structure), Structure.CG.{w, u, v} L (↑M : Type w) ∧ L.age (↑M : Type w) = K

Tactic:
refine ⟨Bundled.of (@DirectLimit L _ _ (fun n ↦ (G n).val) _ f _ _), ?_, ?_⟩
-- 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 ⋯
⊢ Structure.CG.{w, u, v} L
    (↑(Bundled.of (DirectLimit (fun (n : ℕ) ↦ (↑(↑(G n) : Bundled L.Structure) : Type w)) f)) : Type w)

Tactic:
DirectLimit.cg _ (fun n => (fg _ (G n).2).cg)

Premises used: FirstOrder.Language.Structure.FG.cg, FirstOrder.Language.DirectLimit.cg, Quotient, FirstOrder.Language.DirectLimit, Subtype.val, Subtype.property
-- 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 ⋯
⊢ Structure.CG.{w, u, v} L
    (↑(Bundled.of (DirectLimit (fun (n : ℕ) ↦ (↑(↑(G n) : Bundled L.Structure) : Type w)) f)) : Type w)

Tactic:
exact DirectLimit.cg _ (fun n => (fg _ (G n).2).cg)

Premises used: FirstOrder.Language.Structure.FG.cg, FirstOrder.Language.DirectLimit.cg, Subtype.val, Subtype.property
-- 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 ⋯
⊢ L.age (↑(Bundled.of (DirectLimit (fun (n : ℕ) ↦ (↑(↑(G n) : Bundled L.Structure) : Type w)) f)) : Type w) = K

Tactic:
(age_directLimit (fun n ↦ (G n).val) f).trans
      (subset_antisymm (iUnion_subset fun n N hN => hp (G n).val (G n).2 hN) fun N KN => ?_)

Premises used: Set.iUnion_subset, subset_antisymm, CategoryTheory.Bundled.α, Quotient, FirstOrder.Language.age_directLimit, FirstOrder.Language.DirectLimit, Subtype.val, Eq.trans, Subtype.property
-- 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 ⋯
refine_2 :
  ∀ (N : Bundled L.Structure) (KN : N ∈ K),
    Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ℕ), L.age (↑(↑(G i) : Bundled L.Structure) : Type w)) N
⊢ L.age (↑(Bundled.of (DirectLimit (fun (n : ℕ) ↦ (↑(↑(G n) : Bundled L.Structure) : Type w)) f)) : Type w) = K

Tactic:
refine (age_directLimit (fun n ↦ (G n).val) f).trans
      (subset_antisymm (iUnion_subset fun n N hN => hp (G n).val (G n).2 hN) fun N KN => ?_)

Premises used: Set.iUnion_subset, subset_antisymm, CategoryTheory.Bundled.α, FirstOrder.Language.age_directLimit, Subtype.val, Eq.trans, Subtype.property
-- 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
⊢ Quotient.out (s := equivSetoid) (Quotient.mk' N) ≈ N

Tactic:
have : Quotient.out (Quotient.mk' N) ≈ N := Quotient.eq_mk_iff_out.mp rfl
-- 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
refine_2 :
  ∀ (n : ℕ) (e : (↑(F n).out : Type w) ≃[L] (↑N : Type w)),
    Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ℕ), L.age (↑(↑(G i) : Bundled L.Structure) : Type w)) N
⊢ Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ℕ), L.age (↑(↑(G i) : Bundled L.Structure) : Type w)) N

Tactic:
obtain ⟨n, ⟨e⟩⟩ := (hF N).1 ⟨N, KN, this⟩

Premises used: And.intro, Exists.intro, Iff.mp
-- 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)
⊢ Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ℕ), L.age (↑(↑(G i) : Bundled L.Structure) : Type w)) N

Tactic:
mem_iUnion_of_mem n ⟨fg _ KN, ⟨Embedding.comp ?_ e.symm.toEmbedding⟩⟩

Premises used: FirstOrder.Language.Embedding.comp, Nonempty.intro, FirstOrder.Language.Equiv.toEmbedding, And.intro, Set.mem_iUnion_of_mem, FirstOrder.Language.Equiv.symm
-- 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 : (↑(F n).out : Type w) ↪[L] (↑(↑(G n) : Bundled L.Structure) : Type w)
⊢ Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ℕ), L.age (↑(↑(G i) : Bundled L.Structure) : Type w)) N

Tactic:
refine mem_iUnion_of_mem n ⟨fg _ KN, ⟨Embedding.comp ?_ e.symm.toEmbedding⟩⟩