awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
N : Bundled L.Structure
mpr :
  Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid)) (Quotient.mk' '' L.age M) ⟦N⟧ →
    ∃ (y : Finset M),
      (equivSetoid : Bundled L.Structure → Bundled L.Structure → Prop)
        { α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑y : Set M)), str := inferInstance } N
⊢ Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid)) (Quotient.mk' '' L.age M) ⟦N⟧ →
    Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid))
      (range fun (s : Finset M) ↦
        ⟦{ α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)), str := inferInstance }⟧)
      ⟦N⟧

Tactic:
simp only [mem_range, Quotient.eq]

Premises used: Set.mem_range, Quotient.eq
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Eq (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' P) ⟦N⟧
s : Finset (↑P : Type w)
hs :
  Eq (α := L.Substructure (↑P : Type w)) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (↑P : Type w))) ⊤
PM : (↑P : Type w) ↪[L] M
⊢ ∃ (y : Finset M),
    (equivSetoid : Bundled L.Structure → Bundled L.Structure → Prop)
      { α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑y : Set M)), str := inferInstance } N

Tactic:
⟨s.image PM, Setoid.trans (b := P) ?_ <| Quotient.exact hP2⟩

Premises used: Quotient.exact, Exists.intro, Setoid.trans, DFunLike.coe, Finset.image
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Eq (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' P) ⟦N⟧
s : Finset (↑P : Type w)
hs :
  Eq (α := L.Substructure (↑P : Type w)) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (↑P : Type w))) ⊤
PM : (↑P : Type w) ↪[L] M
mpr :
  {
      α :=
        ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L)
            (↑(Finset.image (⇑PM : (a : (↑P : Type w)) → M) s) : Set M)),
      str := inferInstance } ≈
    P
⊢ ∃ (y : Finset M),
    (equivSetoid : Bundled L.Structure → Bundled L.Structure → Prop)
      { α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑y : Set M)), str := inferInstance } N

Tactic:
refine ⟨s.image PM, Setoid.trans (b := P) ?_ <| Quotient.exact hP2⟩
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Eq (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' P) ⟦N⟧
s : Finset (↑P : Type w)
hs :
  Eq (α := L.Substructure (↑P : Type w)) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (↑P : Type w))) ⊤
PM : (↑P : Type w) ↪[L] M
mpr : { α := ↥PM.toHom.range, str := inferInstance } ≈ P
⊢ {
      α :=
        ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L)
            (↑(Finset.image (⇑PM : (a : (↑P : Type w)) → M) s) : Set M)),
      str := inferInstance } ≈
    P

Tactic:
rw [← Embedding.coe_toHom, Finset.coe_image, closure_image PM.toHom, hs, ← Hom.range_eq_map]

Premises used: Finset.coe_image, FirstOrder.Language.Hom.range_eq_map, FirstOrder.Language.Embedding.coe_toHom, FirstOrder.Language.Embedding.toHom, FirstOrder.Language.Substructure.closure_image
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Eq (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' P) ⟦N⟧
s : Finset (↑P : Type w)
hs :
  Eq (α := L.Substructure (↑P : Type w)) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (↑P : Type w))) ⊤
PM : (↑P : Type w) ↪[L] M
⊢ { α := ↥PM.toHom.range, str := inferInstance } ≈ P

Tactic:
⟨PM.equivRange.symm⟩

Premises used: Nonempty.intro, FirstOrder.Language.Embedding.equivRange, FirstOrder.Language.Equiv.symm
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Eq (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' P) ⟦N⟧
s : Finset (↑P : Type w)
hs :
  Eq (α := L.Substructure (↑P : Type w)) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (↑P : Type w))) ⊤
PM : (↑P : Type w) ↪[L] M
⊢ { α := ↥PM.toHom.range, str := inferInstance } ≈ P

Tactic:
exact ⟨PM.equivRange.symm⟩
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
refine :
  ∀ (N : Bundled L.Structure),
    Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid))
        (range fun (s : Finset M) ↦
          ⟦{ α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)), str := inferInstance }⟧)
        ⟦N⟧ ↔
      Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid)) (Quotient.mk' '' L.age M) ⟦N⟧
mp :
  ∀ (N : Bundled L.Structure),
    Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid))
        (range fun (s : Finset M) ↦
          ⟦{ α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)), str := inferInstance }⟧)
        ⟦N⟧ →
      Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid)) (Quotient.mk' '' L.age M) ⟦N⟧
mpr mpr₁ :
  ∀ (N : Bundled L.Structure),
    Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid)) (Quotient.mk' '' L.age M) ⟦N⟧ →
      Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid))
        (range fun (s : Finset M) ↦
          ⟦{ α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)), str := inferInstance }⟧)
        ⟦N⟧
⊢ Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' L.age M)

Tactic:
classical
  refine (congr_arg _ (Set.ext <| Quotient.forall.2 fun N => ?_)).mp
    (countable_range fun s : Finset M => ⟦⟨closure L (s : Set M), inferInstance⟩⟧)
  constructor
  · rintro ⟨s, hs⟩
    use Bundled.of (closure L (s : Set M))
    exact ⟨⟨(fg_iff_structure_fg _).1 (fg_closure s.finite_toSet), ⟨Substructure.subtype _⟩⟩, hs⟩
  · simp only [mem_range, Quotient.eq]
    rintro ⟨P, ⟨⟨s, hs⟩, ⟨PM⟩⟩, hP2⟩
    refine ⟨s.image PM, Setoid.trans (b := P) ?_ <| Quotient.exact hP2⟩
    rw [← Embedding.coe_toHom, Finset.coe_image, closure_image PM.toHom, hs, ← Hom.range_eq_map]
    exact ⟨PM.equivRange.symm⟩

Premises used: Iff.mpr, Set.ext, Set.mem_range, Quotient.forall, Finset.coe_image, Eq.mp, FirstOrder.Language.Hom.range_eq_map, Quotient.mk, Set.countable_range, congr_arg, FirstOrder.Language.Embedding.coe_toHom, Quotient.eq
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
h :
  ∀ (M : Bundled L.Structure),
    M ∈ L.age (DirectLimit G f) ↔ Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ι), L.age (G i)) M
⊢ L.age (DirectLimit G f) = ⋃ (i : ι), L.age (G i)

Tactic:
ext M
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
h : M ∈ L.age (DirectLimit G f) ↔ ∃ (i : ι), M ∈ L.age (G i)
⊢ M ∈ L.age (DirectLimit G f) ↔ Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ι), L.age (G i)) M

Tactic:
simp only [mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
h : M ∈ L.age (DirectLimit G f) → ∃ (i : ι), M ∈ L.age (G i)
h₁ : (∃ (i : ι), M ∈ L.age (G i)) → M ∈ L.age (DirectLimit G f)
⊢ M ∈ L.age (DirectLimit G f) ↔ ∃ (i : ι), M ∈ L.age (G i)

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
h :
  ∀ (s : Finset (DirectLimit G f))
    (hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range),
    ∃ (i : ι), M ∈ L.age (G i)
⊢ ∃ (i : ι), M ∈ L.age (G i)

Tactic:
obtain ⟨s, hs⟩ := Mfg.range e.toHom

Premises used: FirstOrder.Language.Structure.FG.range, FirstOrder.Language.Embedding.toHom
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma (G := G) f := Quotient.out
h :
  ∀ (i : ι) (hi : ∀ i_1 ∈ Finset.image (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ out) s, i_1 ≤ i),
    ∃ (i : ι), M ∈ L.age (G i)
⊢ ∃ (i : ι), M ∈ L.age (G i)

Tactic:
obtain ⟨i, hi⟩ := Finset.exists_le (s.image (Sigma.fst ∘ out))

Premises used: Function.comp, Sigma.fst, Finset.exists_le, Finset.image
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma (G := G) f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ out) s, i_1 ≤ i
h : ∀ (e' : ↥(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) ↪[L] G i), ∃ (i : ι), M ∈ L.age (G i)
⊢ ∃ (i : ι), M ∈ L.age (G i)

Tactic:
have e' := (DirectLimit.of L ι G f i).equivRange.symm.toEmbedding
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma (G := G) f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ out) s, i_1 ≤ i
e' : ↥(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) ↪[L] G i
⊢ ∃ (i : ι), M ∈ L.age (G i)

Tactic:
⟨i, Mfg, ⟨e'.comp ((Substructure.inclusion ?_).comp e.equivRange.toEmbedding)⟩⟩

Premises used: FirstOrder.Language.Embedding.comp, Nonempty.intro, FirstOrder.Language.Embedding.equivRange, FirstOrder.Language.Equiv.toEmbedding, FirstOrder.Language.Substructure.inclusion, And.intro, Exists.intro
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma (G := G) f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ out) s, i_1 ≤ i
e' : ↥(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) ↪[L] G i
h : e.toHom.range ≤ Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))
⊢ ∃ (i : ι), M ∈ L.age (G i)

Tactic:
refine ⟨i, Mfg, ⟨e'.comp ((Substructure.inclusion ?_).comp e.equivRange.toEmbedding)⟩⟩
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma (G := G) f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ out) s, i_1 ≤ i
e' : ↥(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) ↪[L] G i
h : (↑s : Set (DirectLimit G f)) ⊆ (↑(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) : Set (DirectLimit G f))
⊢ e.toHom.range ≤ Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))

Tactic:
rw [← hs, closure_le]

Premises used: FirstOrder.Language.Substructure.closure_le
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma (G := G) f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ out) s, i_1 ≤ i
e' : ↥(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) ↪[L] G i
x : DirectLimit G f
hx : x ∈ (↑s : Set (DirectLimit G f))
⊢ x ∈ (↑(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) : Set (DirectLimit G f))

Tactic:
⟨f (out x).1 i (hi (out x).1 (Finset.mem_image_of_mem _ hx)) (out x).2, ?_⟩

Premises used: Set.Mem, setOf, Sigma.fst, Exists.intro, Set.range, Finset.mem_image_of_mem, Sigma.snd, DFunLike.coe
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set (DirectLimit G f)) = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma (G := G) f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ out) s, i_1 ≤ i
e' : ↥(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) ↪[L] G i
x : DirectLimit G f
hx : x ∈ (↑s : Set (DirectLimit G f))
h :
  (Embedding.toHom (DirectLimit.of L ι G f i) : (a : G i) → DirectLimit G f)
      ((f ((out x).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (out x).fst) → G i)
        ((out x).snd (β := fun (i : ι) ↦ G i))) =
    x
⊢ x ∈ (↑(Hom.range (Embedding.toHom (DirectLimit.of L ι G f i))) : Set (DirectLimit G f))

Tactic:
refine ⟨f (out x).1 i (hi (out x).1 (Finset.mem_image_of_mem _ hx)) (out x).2, ?_⟩
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
i : ι
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] G i
⊢ M ∈ L.age (DirectLimit G f)

Tactic:
⟨Mfg, ⟨Embedding.comp (DirectLimit.of L ι G f i) e⟩⟩

Premises used: FirstOrder.Language.DirectLimit.of, FirstOrder.Language.Embedding.comp, Set.Mem, FirstOrder.Language.age, setOf, Nonempty.intro, And.intro
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
M : Bundled L.Structure
i : ι
Mfg : Structure.FG L (↑M : Type (max w w'))
e : (↑M : Type (max w w')) ↪[L] G i
⊢ M ∈ L.age (DirectLimit G f)

Tactic:
exact ⟨Mfg, ⟨Embedding.comp (DirectLimit.of L ι G f i) e⟩⟩
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
ι : Type w
inst : Preorder ι
inst_1 : IsDirectedOrder ι
inst_2 : Nonempty ι
G : ι → Type (max w w')
inst_3 : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
h :
  ∀ (M : Bundled L.Structure),
    M ∈ L.age (DirectLimit G f) ↔ Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ι), L.age (G i)) M
h₁ : ∀ (M : Bundled L.Structure), M ∈ L.age (DirectLimit G f) ↔ ∃ (i : ι), M ∈ L.age (G i)
h₂ : ∀ M ∈ L.age (DirectLimit G f), ∃ (i : ι), M ∈ L.age (G i)
h₃ h₄ : ∀ (M : Bundled L.Structure), (∃ (i : ι), M ∈ L.age (G i)) → M ∈ L.age (DirectLimit G f)
⊢ L.age (DirectLimit G f) = ⋃ (i : ι), L.age (G i)

Tactic:
classical
  ext M
  simp only [mem_iUnion]
  constructor
  · rintro ⟨Mfg, ⟨e⟩⟩
    obtain ⟨s, hs⟩ := Mfg.range e.toHom
    let out := @Quotient.out _ (DirectLimit.setoid G f)
    obtain ⟨i, hi⟩ := Finset.exists_le (s.image (Sigma.fst ∘ out))
    have e' := (DirectLimit.of L ι G f i).equivRange.symm.toEmbedding
    refine ⟨i, Mfg, ⟨e'.comp ((Substructure.inclusion ?_).comp e.equivRange.toEmbedding)⟩⟩
    rw [← hs, closure_le]
    intro x hx
    refine ⟨f (out x).1 i (hi (out x).1 (Finset.mem_image_of_mem _ hx)) (out x).2, ?_⟩
    rw [Embedding.coe_toHom, DirectLimit.of_apply, @Quotient.mk_eq_iff_out _ (_),
      DirectLimit.equiv_iff G f (le_refl _) (hi (out x).1 (Finset.mem_image_of_mem _ hx)),
      DirectedSystem.map_self]
  · rintro ⟨i, Mfg, ⟨e⟩⟩
    exact ⟨Mfg, ⟨Embedding.comp (DirectLimit.of L ι G f i) e⟩⟩

Premises used: Quotient.mk_eq_iff_out, FirstOrder.Language.DirectedSystem.map_self, Set.mem_iUnion, FirstOrder.Language.Embedding.coe_toHom, FirstOrder.Language.DirectLimit.of_apply, FirstOrder.Language.Substructure.closure_le
-- 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
obtain :
  ∀ (F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid) (hF : Quotient.mk' '' K = range F),
    ∃ (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:
obtain ⟨F, hF⟩ := hc.exists_eq_range (hn.image _)

Premises used: Set.Nonempty.image, Set.Countable.exists_eq_range
-- 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 : Quotient.mk' '' K = range F
⊢ ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Eq (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' x) ⟦a⟧) ↔ ∃ (y : ℕ), F y = ⟦a⟧

Tactic:
simp only [Set.ext_iff, Quotient.forall, mem_image, mem_range] at hF

Premises used: Set.mem_range, Quotient.forall, Set.mem_image, Set.ext_iff
-- 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, Eq (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' x) ⟦a⟧) ↔ ∃ (y : ℕ), F y = ⟦a⟧
⊢ ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Quotient.out (s := equivSetoid) (Quotient.mk' x) ≈ a) ↔ ∃ (y : ℕ), (F y).out ≈ a

Tactic:
simp_rw [Quotient.eq_mk_iff_out] at hF

Premises used: Quotient.eq_mk_iff_out
-- 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 : ℕ
obtain :
  ∀ (P : Bundled L.Structure) (hP1 : P ∈ K) (hP2 : Quotient.out (s := equivSetoid) (Quotient.mk' P) ≈ (F n).out),
    (F n).out ∈ K
⊢ (F n).out ∈ K

Tactic:
obtain ⟨P, hP1, hP2⟩ := (hF (F n).out).2 ⟨n, Setoid.refl _⟩

Premises used: Iff.mpr, Quotient.out, Exists.intro, Setoid.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
n : ℕ
P : Bundled L.Structure
hP1 : P ∈ K
hP2 : Quotient.out (s := equivSetoid) (Quotient.mk' P) ≈ (F n).out
⊢ P ≈ (F n).out

Tactic:
replace hP2 := Setoid.trans (Setoid.symm (Quotient.mk_out P)) hP2
-- 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:
(hp.is_equiv_invariant_of_fg fg _ _ hP2).1 hP1

Premises used: FirstOrder.Language.Hereditary.is_equiv_invariant_of_fg, Iff.mp