awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
rw : S.FG ↔ FG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
⊢ S.FG ↔ Structure.FG.{u_1, u_2, u_3} L ↥S

Tactic:
rw [Structure.fg_def]

Premises used: FirstOrder.Language.Structure.fg_def
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
⊢ S.FG ↔ FG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤

Tactic:
⟨fun h => FG.of_map_embedding S.subtype ?_, fun h => ?_⟩

Premises used: Iff.intro, FirstOrder.Language.Substructure.subtype, FirstOrder.Language.Substructure.FG.of_map_embedding
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
refine_1 : ∀ (h : S.FG), (map S.subtype.toHom ⊤).FG
refine_2 : ∀ (h : FG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤), S.FG
⊢ S.FG ↔ FG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤

Tactic:
refine ⟨fun h => FG.of_map_embedding S.subtype ?_, fun h => ?_⟩
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
h refine_1 : S.FG
⊢ (map S.subtype.toHom ⊤).FG

Tactic:
rw [← Hom.range_eq_map, range_subtype]

Premises used: FirstOrder.Language.Substructure.range_subtype, FirstOrder.Language.Hom.range_eq_map
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
h : S.FG
⊢ S.FG

Tactic:
h
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
h : S.FG
⊢ S.FG

Tactic:
exact h
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
h : FG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
⊢ (map S.subtype.toHom ⊤).FG

Tactic:
have h := h.map S.subtype.toHom
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
h_1 : FG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
h : (map S.subtype.toHom ⊤).FG
⊢ S.FG

Tactic:
rw [← Hom.range_eq_map, range_subtype] at h

Premises used: FirstOrder.Language.Substructure.range_subtype, FirstOrder.Language.Hom.range_eq_map
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
h_1 : FG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
h : S.FG
⊢ S.FG

Tactic:
h
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
h_1 : FG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
h : S.FG
⊢ S.FG

Tactic:
exact h
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
f : M ≃[L] N
⊢ Structure.CG L M ↔ Structure.CG L N

Tactic:
⟨fun h => h.map_of_surjective f.toHom f.toEquiv.surjective, fun h =>
    h.map_of_surjective f.symm.toHom f.toEquiv.symm.surjective⟩

Premises used: FirstOrder.Language.Structure.CG.map_of_surjective, FirstOrder.Language.Equiv.toHom, FirstOrder.Language.Equiv.toEquiv, Iff.intro, Equiv.surjective, Equiv.symm, FirstOrder.Language.Equiv.symm
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
rw : S.CG ↔ CG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
⊢ S.CG ↔ Structure.CG.{u_1, u_2, u_3} L ↥S

Tactic:
rw [Structure.cg_def]

Premises used: FirstOrder.Language.Structure.cg_def
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
⊢ S.CG ↔ CG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤

Tactic:
⟨fun h => CG.of_map_embedding S.subtype ?_, fun h => ?_⟩

Premises used: FirstOrder.Language.Substructure.CG.of_map_embedding, Iff.intro, FirstOrder.Language.Substructure.subtype
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
refine_1 : ∀ (h : S.CG), (map S.subtype.toHom ⊤).CG
refine_2 : ∀ (h : CG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤), S.CG
⊢ S.CG ↔ CG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤

Tactic:
refine ⟨fun h => CG.of_map_embedding S.subtype ?_, fun h => ?_⟩
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
h refine_1 : S.CG
⊢ (map S.subtype.toHom ⊤).CG

Tactic:
rw [← Hom.range_eq_map, range_subtype]

Premises used: FirstOrder.Language.Substructure.range_subtype, FirstOrder.Language.Hom.range_eq_map
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
h : S.CG
⊢ S.CG

Tactic:
h
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
h : S.CG
⊢ S.CG

Tactic:
exact h
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
h : CG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
⊢ (map S.subtype.toHom ⊤).CG

Tactic:
have h := h.map S.subtype.toHom
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
h_1 : CG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
h : (map S.subtype.toHom ⊤).CG
⊢ S.CG

Tactic:
rw [← Hom.range_eq_map, range_subtype] at h

Premises used: FirstOrder.Language.Substructure.range_subtype, FirstOrder.Language.Hom.range_eq_map
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
h_1 : CG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
h : S.CG
⊢ S.CG

Tactic:
h
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.Substructure M
h_1 : CG.{u_1, u_2, u_3} (L := L) (M := ↥S) ⊤
h : S.CG
⊢ S.CG

Tactic:
exact h
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable M
g : { S : L.Substructure M // S.FG } → Finset M :=
  fun (S : { S : L.Substructure M // S.FG }) ↦
    Exists.choose (p := fun (a : Finset M) ↦
      LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S : L.Substructure M)) ⋯
S S' : { S : L.Substructure M // S.FG }
h : g S = g S'
a : (↑S : L.Substructure M) = (↑S' : L.Substructure M)
⊢ S = S'

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable M
g : { S : L.Substructure M // S.FG } → Finset M :=
  fun (S : { S : L.Substructure M // S.FG }) ↦
    Exists.choose (p := fun (a : Finset M) ↦
      LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S : L.Substructure M)) ⋯
S S' : { S : L.Substructure M // S.FG }
h : g S = g S'
a :
  Eq (α := L.Substructure M)
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L)
      (↑(Exists.choose (p := fun (a : Finset M) ↦
            LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S : L.Substructure M)) ⋯) :
        Set M))
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L)
      (↑(Exists.choose (p := fun (a : Finset M) ↦
            LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S' : L.Substructure M)) ⋯) :
        Set M))
⊢ (↑S : L.Substructure M) = (↑S' : L.Substructure M)

Tactic:
rw [(Exists.choose_spec S.prop).symm, (Exists.choose_spec S'.prop).symm]

Premises used: Exists.choose_spec, Subtype.prop, Eq.symm
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable M
g : { S : L.Substructure M // S.FG } → Finset M :=
  fun (S : { S : L.Substructure M // S.FG }) ↦
    Exists.choose (p := fun (a : Finset M) ↦
      LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S : L.Substructure M)) ⋯
S S' : { S : L.Substructure M // S.FG }
h : g S = g S'
⊢ Eq (α := L.Substructure M)
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L)
      (↑(Exists.choose (p := fun (a : Finset M) ↦
            LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S : L.Substructure M)) ⋯) :
        Set M))
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L)
      (↑(Exists.choose (p := fun (a : Finset M) ↦
            LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S' : L.Substructure M)) ⋯) :
        Set M))

Tactic:
congr_arg (closure L ∘ SetLike.coe) h

Premises used: Function.comp, congr_arg, SetLike.coe, LowerAdjoint.toFun, FirstOrder.Language.Substructure.closure
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable M
g : { S : L.Substructure M // S.FG } → Finset M :=
  fun (S : { S : L.Substructure M // S.FG }) ↦
    Exists.choose (p := fun (a : Finset M) ↦
      LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S : L.Substructure M)) ⋯
S S' : { S : L.Substructure M // S.FG }
h : g S = g S'
⊢ Eq (α := L.Substructure M)
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L)
      (↑(Exists.choose (p := fun (a : Finset M) ↦
            LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S : L.Substructure M)) ⋯) :
        Set M))
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L)
      (↑(Exists.choose (p := fun (a : Finset M) ↦
            LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S' : L.Substructure M)) ⋯) :
        Set M))

Tactic:
exact congr_arg (closure L ∘ SetLike.coe) h

Premises used: Function.comp, congr_arg, SetLike.coe, LowerAdjoint.toFun, FirstOrder.Language.Substructure.closure
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable M
g : { S : L.Substructure M // S.FG } → Finset M :=
  fun (S : { S : L.Substructure M // S.FG }) ↦
    Exists.choose (p := fun (a : Finset M) ↦
      LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S : L.Substructure M)) ⋯
⊢ Function.Injective g

Tactic:
have g_inj : Function.Injective g := by
    intro S S' h
    apply Subtype.ext
    rw [(Exists.choose_spec S.prop).symm, (Exists.choose_spec S'.prop).symm]
    exact congr_arg (closure L ∘ SetLike.coe) h
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable M
g : { S : L.Substructure M // S.FG } → Finset M :=
  fun (S : { S : L.Substructure M // S.FG }) ↦
    Exists.choose (p := fun (a : Finset M) ↦
      LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S : L.Substructure M)) ⋯
g_inj : Function.Injective g
⊢ Countable.{max 1 (u_1 + 1)} { S : L.Substructure M // S.FG }

Tactic:
Function.Embedding.countable ⟨g, g_inj⟩

Premises used: Function.Embedding.mk, Function.Embedding.countable
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable M
g : { S : L.Substructure M // S.FG } → Finset M :=
  fun (S : { S : L.Substructure M // S.FG }) ↦
    Exists.choose (p := fun (a : Finset M) ↦
      LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑a : Set M) = (↑S : L.Substructure M)) ⋯
g_inj : Function.Injective g
⊢ Countable.{max 1 (u_1 + 1)} { S : L.Substructure M // S.FG }

Tactic:
exact Function.Embedding.countable ⟨g, g_inj⟩

Premises used: Function.Embedding.mk, Function.Embedding.countable
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable M
⊢ Countable.{max 1 (u_1 + 1)} { S : L.Substructure M // S.FG }

Tactic:
countable_fg_substructures_of_countable

Premises used: FirstOrder.Language.Substructure.countable_fg_substructures_of_countable
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
N P : Bundled L.Structure
h : Nonempty.{w + 1} ((↑N : Type w) ≃[L] (↑P : Type w))
⊢ N ∈ L.age M ↔ P ∈ L.age M

Tactic:
and_congr h.some.fg_iff
    ⟨Nonempty.map fun x => Embedding.comp x h.some.symm.toEmbedding,
      Nonempty.map fun x => Embedding.comp x h.some.toEmbedding⟩

Premises used: FirstOrder.Language.Equiv.fg_iff, FirstOrder.Language.Embedding.comp, Set.Mem, FirstOrder.Language.age, setOf, Nonempty.some, FirstOrder.Language.Equiv.toEmbedding, Iff.intro, Nonempty.map, FirstOrder.Language.Equiv.symm, and_congr
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
MN : M ↪[L] N
⊢ L.age M ⊆ L.age N

Tactic:
fun _ =>
  And.imp_right (Nonempty.map MN.comp)

Premises used: FirstOrder.Language.Embedding.comp, Set.Mem, FirstOrder.Language.age, setOf, Set.Subset, And.imp_right, Nonempty.map
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
MN : M ≃[L] N
⊢ L.age M = L.age N

Tactic:
le_antisymm MN.toEmbedding.age_subset_age MN.symm.toEmbedding.age_subset_age

Premises used: FirstOrder.Language.Embedding.age_subset_age, le_antisymm, FirstOrder.Language.Equiv.toEmbedding, FirstOrder.Language.Equiv.symm
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M N : Bundled L.Structure
h : FG.{u_1, u, v} L (↑M : Type u_1)
MN : Nonempty.{u_1 + 1} ((↑M : Type u_1) ≃[L] (↑N : Type u_1))
⊢ N ∈ L.age (↑M : Type u_1)

Tactic:
⟨MN.some.fg_iff.1 h, ⟨MN.some.symm.toEmbedding⟩⟩

Premises used: FirstOrder.Language.Equiv.fg_iff, Set.Mem, FirstOrder.Language.age, setOf, Nonempty.some, Nonempty.intro, FirstOrder.Language.Equiv.toEmbedding, And.intro, Iff.mp, FirstOrder.Language.Equiv.symm
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
h : Hereditary K
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
M N : Bundled L.Structure
hn : Nonempty.{w + 1} ((↑M : Type w) ≃[L] (↑N : Type w))
⊢ M ∈ K ↔ N ∈ K

Tactic:
⟨fun MK => h M MK ((fg M MK).mem_age_of_equiv hn),
   fun NK => h N NK ((fg N NK).mem_age_of_equiv ⟨hn.some.symm⟩)⟩

Premises used: Nonempty.some, Nonempty.intro, Iff.intro, FirstOrder.Language.Structure.FG.mem_age_of_equiv, FirstOrder.Language.Equiv.symm
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
h : IsFraisse K
M N : Bundled L.Structure
hn : Nonempty.{w + 1} ((↑M : Type w) ≃[L] (↑N : Type w))
⊢ M ∈ K ↔ N ∈ K

Tactic:
h.hereditary.is_equiv_invariant_of_fg h.FG M N hn

Premises used: FirstOrder.Language.Hereditary.is_equiv_invariant_of_fg, FirstOrder.Language.IsFraisse.FG, FirstOrder.Language.IsFraisse.hereditary
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
⊢ (L.age M).Nonempty

Tactic:
⟨Bundled.of (Substructure.closure L (∅ : Set M)),
    (fg_iff_structure_fg _).1 (fg_closure Set.finite_empty), ⟨Substructure.subtype _⟩⟩

Premises used: Set.finite_empty, FirstOrder.Language.Substructure.fg_closure, FirstOrder.Language.Substructure.fg_iff_structure_fg, Membership.mem, Subtype, Nonempty.intro, CategoryTheory.Bundled.of, Set.Nonempty, And.intro, Exists.intro, Iff.mp, LowerAdjoint.toFun, FirstOrder.Language.Substructure.closure, FirstOrder.Language.Substructure.subtype, EmptyCollection.emptyCollection
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
⊢ Hereditary (L.age M)

Tactic:
fun _ hN _ hP => hN.2.some.age_subset_age hP

Premises used: FirstOrder.Language.Embedding.age_subset_age, Nonempty.some, Set.Subset, And.right, FirstOrder.Language.Hereditary
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
⊢ JointEmbedding (L.age M)

Tactic:
fun _ hN _ hP =>
  ⟨Bundled.of (↥(hN.2.some.toHom.range ⊔ hP.2.some.toHom.range)),
    ⟨(fg_iff_structure_fg _).1 ((hN.1.range hN.2.some.toHom).sup (hP.1.range hP.2.some.toHom)),
      ⟨Substructure.subtype _⟩⟩,
    ⟨Embedding.comp (inclusion le_sup_left) hN.2.some.equivRange.toEmbedding⟩,
    ⟨Embedding.comp (inclusion le_sup_right) hP.2.some.equivRange.toEmbedding⟩⟩

Premises used: FirstOrder.Language.Embedding.comp, le_sup_left, FirstOrder.Language.Substructure.fg_iff_structure_fg, DirectedOn, Membership.mem, Subtype, Nonempty.some, le_sup_right, Nonempty.intro, CategoryTheory.Bundled.of, FirstOrder.Language.Hom.range, FirstOrder.Language.Embedding.equivRange, And.right, And.left, Max.max, FirstOrder.Language.Substructure.FG.sup, FirstOrder.Language.Equiv.toEmbedding, FirstOrder.Language.Substructure.inclusion, And.intro, Exists.intro, Iff.mp, FirstOrder.Language.JointEmbedding, FirstOrder.Language.Substructure.subtype, FirstOrder.Language.Structure.FG.range, FirstOrder.Language.Embedding.toHom
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
fg : S.FG
⊢ { α := ↥S, str := inferInstance } ∈ L.age M

Tactic:
⟨(Substructure.fg_iff_structure_fg _).1 fg, ⟨subtype _⟩⟩

Premises used: Set.Mem, FirstOrder.Language.age, FirstOrder.Language.Substructure.fg_iff_structure_fg, setOf, Nonempty.intro, And.intro, Iff.mp, FirstOrder.Language.Substructure.subtype
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
fg : S.FG
⊢ { α := ↥S, str := inferInstance } ∈ L.age M

Tactic:
exact ⟨(Substructure.fg_iff_structure_fg _).1 fg, ⟨subtype _⟩⟩
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
C : Quotient (α := Bundled L.Structure) equivSetoid
N : Bundled L.Structure
N_eq : Quotient.mk' N = C
N_fg : Structure.FG.{w, u, v} L (↑N : Type w)
N_incl : (↑N : Type w) ↪[L] M
⊢ ∃ (V : { V : L.Substructure M // V.FG }), ⟦{ α := ↥(↑V : L.Substructure M), str := inferInstance }⟧ = C

Tactic:
N_eq.symm ▸ ⟨⟨N_incl.toHom.range, ?_⟩, Quotient.sound ⟨N_incl.equivRange.symm⟩⟩

Premises used: Eq.rec, Nonempty.intro, Subtype.mk, FirstOrder.Language.Hom.range, FirstOrder.Language.Embedding.equivRange, Exists.intro, Quotient.sound, Eq.symm, FirstOrder.Language.Embedding.toHom, FirstOrder.Language.Equiv.symm
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
C : Quotient (α := Bundled L.Structure) equivSetoid
N : Bundled L.Structure
N_eq : Quotient.mk' N = C
N_fg : Structure.FG.{w, u, v} L (↑N : Type w)
N_incl : (↑N : Type w) ↪[L] M
refine : N_incl.toHom.range.FG
⊢ ∃ (V : { V : L.Substructure M // V.FG }), ⟦{ α := ↥(↑V : L.Substructure M), str := inferInstance }⟧ = C

Tactic:
refine N_eq.symm ▸ ⟨⟨N_incl.toHom.range, ?_⟩, Quotient.sound ⟨N_incl.equivRange.symm⟩⟩
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
C : Quotient (α := Bundled L.Structure) equivSetoid
N : Bundled L.Structure
N_eq : Quotient.mk' N = C
N_fg : Structure.FG.{w, u, v} L (↑N : Type w)
N_incl : (↑N : Type w) ↪[L] M
⊢ N_incl.toHom.range.FG

Tactic:
FG.range N_fg (Embedding.toHom N_incl)

Premises used: FirstOrder.Language.Structure.FG.range, FirstOrder.Language.Embedding.toHom
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
C : Quotient (α := Bundled L.Structure) equivSetoid
N : Bundled L.Structure
N_eq : Quotient.mk' N = C
N_fg : Structure.FG.{w, u, v} L (↑N : Type w)
N_incl : (↑N : Type w) ↪[L] M
⊢ N_incl.toHom.range.FG

Tactic:
exact FG.range N_fg (Embedding.toHom N_incl)

Premises used: FirstOrder.Language.Structure.FG.range, FirstOrder.Language.Embedding.toHom
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
⊢ Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' L.age M)

Tactic:
(congr_arg _ (Set.ext <| Quotient.forall.2 fun N => ?_)).mp
    (countable_range fun s : Finset M => ⟦⟨closure L (s : Set M), inferInstance⟩⟧)

Premises used: Iff.mpr, Set.ext, Quotient.forall, Eq.mp, Quotient.mk, Set.countable_range, congr_arg
-- 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⟧
⊢ Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' L.age M)

Tactic:
refine (congr_arg _ (Set.ext <| Quotient.forall.2 fun N => ?_)).mp
    (countable_range fun s : Finset M => ⟦⟨closure L (s : Set M), inferInstance⟩⟧)

Premises used: Iff.mpr, Set.ext, Quotient.forall, Eq.mp, Quotient.mk, Set.countable_range, congr_arg
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
N : Bundled L.Structure
mp :
  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 :
  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⟧
⊢ 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⟧

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
N : Bundled L.Structure
s : Finset M
hs :
  Eq (α := Quotient (α := Bundled L.Structure) equivSetoid)
    ((fun (s : Finset M) ↦
        (⟦{ α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)), str := inferInstance }⟧ :
          Quotient (α := Bundled L.Structure) equivSetoid))
      s)
    ⟦N⟧
h₁ :
  Bundled.of ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)) ∈ L.age M ∧
    Eq (α := Quotient (α := Bundled L.Structure) equivSetoid)
      (Quotient.mk' (Bundled.of ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)))) ⟦N⟧
⊢ Membership.mem (γ := Set (Quotient (α := Bundled L.Structure) equivSetoid)) (Quotient.mk' '' L.age M) ⟦N⟧

Tactic:
use Bundled.of (closure L (s : Set M))
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
N : Bundled L.Structure
s : Finset M
hs :
  Eq (α := Quotient (α := Bundled L.Structure) equivSetoid)
    ((fun (s : Finset M) ↦
        (⟦{ α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)), str := inferInstance }⟧ :
          Quotient (α := Bundled L.Structure) equivSetoid))
      s)
    ⟦N⟧
⊢ Bundled.of ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)) ∈ L.age M ∧
    Eq (α := Quotient (α := Bundled L.Structure) equivSetoid)
      (Quotient.mk' (Bundled.of ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)))) ⟦N⟧

Tactic:
⟨⟨(fg_iff_structure_fg _).1 (fg_closure s.finite_toSet), ⟨Substructure.subtype _⟩⟩, hs⟩

Premises used: FirstOrder.Language.Substructure.fg_closure, FirstOrder.Language.Substructure.fg_iff_structure_fg, Nonempty.intro, And.intro, Iff.mp, FirstOrder.Language.Substructure.subtype, Finset.finite_toSet
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Countable M
N : Bundled L.Structure
s : Finset M
hs :
  Eq (α := Quotient (α := Bundled L.Structure) equivSetoid)
    ((fun (s : Finset M) ↦
        (⟦{ α := ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)), str := inferInstance }⟧ :
          Quotient (α := Bundled L.Structure) equivSetoid))
      s)
    ⟦N⟧
⊢ Bundled.of ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)) ∈ L.age M ∧
    Eq (α := Quotient (α := Bundled L.Structure) equivSetoid)
      (Quotient.mk' (Bundled.of ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑s : Set M)))) ⟦N⟧

Tactic:
exact ⟨⟨(fg_iff_structure_fg _).1 (fg_closure s.finite_toSet), ⟨Substructure.subtype _⟩⟩, hs⟩