awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N₁ N₂ : L.Substructure M
hN₁ : N₁.CG
hN₂ : N₂.CG
t₁ : Set M
ht₁ : t₁.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₁ = N₁
t₂ : Set M
ht₂ : t₂.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₂ = N₂
rw :
  LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₁ ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₂ = N₁ ⊔ N₂
rw₁ : N₁ ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t₂ = N₁ ⊔ N₂
rw₂ rw₃ : N₁ ⊔ N₂ = N₁ ⊔ N₂
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) (t₁ ∪ t₂) = N₁ ⊔ N₂

Tactic:
rw [closure_union, ht₁.2, ht₂.2]

Premises used: And.right, FirstOrder.Language.Substructure.closure_union
-- 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
s : L.Substructure M
hs : s.CG
t : Set M
ht : t.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = s
rw : Substructure.map f (LowerAdjoint.toFun (u := SetLike.coe) (closure L) t) = Substructure.map f s
rw₁ rw₂ : Substructure.map f s = Substructure.map f s
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) '' t) = Substructure.map f s

Tactic:
rw [closure_image, ht.2]

Premises used: And.right, FirstOrder.Language.Substructure.closure_image
-- 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
s : L.Substructure M
hs : (Substructure.map f.toHom s).CG
rcases :
  ∀ (t : Set N) (h1 : t.Countable)
    (h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = Substructure.map f.toHom s), s.CG
⊢ s.CG

Tactic:
rcases hs with ⟨t, h1, h2⟩
-- 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
s : L.Substructure M
t : Set N
h1 : t.Countable
h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = Substructure.map f.toHom s
⊢ ∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = s

Tactic:
⟨f ⁻¹' t, h1.preimage f.injective, ?_⟩

Premises used: Set.preimage, And.intro, Exists.intro, FirstOrder.Language.Embedding.injective, Set.Countable.preimage, DFunLike.coe
-- 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
s : L.Substructure M
t : Set N
h1 : t.Countable
h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = Substructure.map f.toHom s
refine : LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' t) = s
⊢ ∃ (S : Set M), S.Countable ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = s

Tactic:
refine ⟨f ⁻¹' t, h1.preimage f.injective, ?_⟩
-- 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
s : L.Substructure M
t : Set N
h1 : t.Countable
h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = Substructure.map f.toHom s
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)

Tactic:
have hf : Function.Injective f.toHom := f.injective
-- 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
s : L.Substructure M
t : Set N
h1 : t.Countable
h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = Substructure.map f.toHom s
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' t) = s

Tactic:
map_injective_of_injective hf ?_

Premises used: FirstOrder.Language.Substructure.map_injective_of_injective
-- 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
s : L.Substructure M
t : Set N
h1 : t.Countable
h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = Substructure.map f.toHom s
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)
refine :
  Substructure.map f.toHom (LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' t)) =
    Substructure.map f.toHom s
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' t) = s

Tactic:
refine map_injective_of_injective hf ?_

Premises used: FirstOrder.Language.Substructure.map_injective_of_injective
-- 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
s : L.Substructure M
t : Set N
h1 : t.Countable
h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = Substructure.map f.toHom s
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)
rw : t ⊆ range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)
⊢ Substructure.map f.toHom (LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) ⁻¹' t)) =
    Substructure.map f.toHom s

Tactic:
rw [← h2, map_closure, Embedding.coe_toHom, image_preimage_eq_of_subset]

Premises used: Set.image_preimage_eq_of_subset, FirstOrder.Language.Embedding.coe_toHom, FirstOrder.Language.Substructure.map_closure
-- 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
s : L.Substructure M
t : Set N
h1 : t.Countable
h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = Substructure.map f.toHom s
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)
x : N
hx : x ∈ t
⊢ x ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) t) : Set N)

Tactic:
have h' := subset_closure (L := L) hx
-- 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
s : L.Substructure M
t : Set N
h1 : t.Countable
h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = Substructure.map f.toHom s
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)
x : N
hx : x ∈ t
h' : x ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) t) : Set N)
⊢ x ∈ (↑(Substructure.map f.toHom s) : Set N)

Tactic:
rw [h2] at 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
s : L.Substructure M
t : Set N
h1 : t.Countable
h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = Substructure.map f.toHom s
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)
x : N
hx : x ∈ t
h' : x ∈ (↑(Substructure.map f.toHom s) : Set N)
⊢ Membership.mem (γ := Set N) (range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) x

Tactic:
Hom.map_le_range h'

Premises used: Set.Mem, setOf, FirstOrder.Language.Hom.map_le_range, Set.range
-- 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
s : L.Substructure M
t : Set N
h1 : t.Countable
h2 : LowerAdjoint.toFun (u := SetLike.coe) (closure L) t = Substructure.map f.toHom s
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f.toHom : (a : M) → N)
x : N
hx : x ∈ t
h' : x ∈ (↑(Substructure.map f.toHom s) : Set N)
⊢ Membership.mem (γ := Set N) (range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) x

Tactic:
exact Hom.map_le_range h'

Premises used: FirstOrder.Language.Hom.map_le_range
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable.{u_2 + 1} ((l : ℕ) × L.Functions l)
s : L.Substructure M
⊢ s.CG ↔ Countable.{u_1 + 1} ↥s

Tactic:
⟨?_, fun h => ⟨s, h.to_set, s.closure_eq⟩⟩

Premises used: Countable.to_set, SetLike.coe, And.intro, Iff.intro, Exists.intro, FirstOrder.Language.Substructure.closure_eq
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable.{u_2 + 1} ((l : ℕ) × L.Functions l)
s : L.Substructure M
refine : s.CG → Countable.{u_1 + 1} ↥s
⊢ s.CG ↔ Countable.{u_1 + 1} ↥s

Tactic:
refine ⟨?_, fun h => ⟨s, h.to_set, s.closure_eq⟩⟩
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable.{u_2 + 1} ((l : ℕ) × L.Functions l)
s : Set M
h : s.Countable
⊢ Countable.{u_1 + 1} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)

Tactic:
h.substructure_closure L

Premises used: Set.Countable.substructure_closure
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable.{u_2 + 1} ((l : ℕ) × L.Functions l)
s : Set M
h : s.Countable
⊢ Countable.{u_1 + 1} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)

Tactic:
exact h.substructure_closure L

Premises used: Set.Countable.substructure_closure
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
s : L.Substructure M
h : Countable.{u_1 + 1} ↥s
⊢ s.CG

Tactic:
⟨s, h.to_set, s.closure_eq⟩

Premises used: Countable.to_set, SetLike.coe, And.intro, FirstOrder.Language.Substructure.CG, Exists.intro, FirstOrder.Language.Substructure.closure_eq
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
⊢ FG L M ↔ Substructure.FG.{u_1, u_2, u_3} (L := L) (M := M) ⊤

Tactic:
⟨fun h => h.1, fun h => ⟨h⟩⟩

Premises used: Iff.intro, FirstOrder.Language.Structure.FG.out, FirstOrder.Language.Structure.FG.mk
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
rw :
  Substructure.FG.{u_1, u_2, u_3} (L := L) (M := M) ⊤ ↔
    ∃ (S : Set M), S.Finite ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
rw₁ rw₂ :
  (∃ (S : Set M), S.Finite ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤) ↔
    ∃ (S : Set M), S.Finite ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
⊢ FG L M ↔ ∃ (S : Set M), S.Finite ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤

Tactic:
rw [fg_def, Substructure.fg_def]

Premises used: FirstOrder.Language.Structure.fg_def, FirstOrder.Language.Substructure.fg_def
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
h : FG L M
f : M →[L] N
rw : (map f ⊤).FG
⊢ f.range.FG

Tactic:
rw [Hom.range_eq_map]

Premises used: FirstOrder.Language.Hom.range_eq_map
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
h : FG L M
f : M →[L] N
⊢ (map f ⊤).FG

Tactic:
(fg_def.1 h).map f

Premises used: FirstOrder.Language.Structure.fg_def, Iff.mp, FirstOrder.Language.Substructure.FG.map
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
h : FG L M
f : M →[L] N
⊢ (map f ⊤).FG

Tactic:
exact (fg_def.1 h).map f

Premises used: FirstOrder.Language.Structure.fg_def, Iff.mp, FirstOrder.Language.Substructure.FG.map
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
h : FG L M
f : M →[L] N
hs : Function.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ f.range = ⊤

Tactic:
rw [← Hom.range_eq_top] at hs

Premises used: FirstOrder.Language.Hom.range_eq_top
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
h : FG L M
f : M →[L] N
hs : f.range = ⊤
rw : f.range.FG
⊢ FG L N

Tactic:
rw [fg_def, ← hs]

Premises used: FirstOrder.Language.Structure.fg_def
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
h : FG L M
f : M →[L] N
hs : f.range = ⊤
⊢ f.range.FG

Tactic:
h.range f

Premises used: FirstOrder.Language.Structure.FG.range
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
h : FG L M
f : M →[L] N
hs : f.range = ⊤
⊢ f.range.FG

Tactic:
exact h.range f

Premises used: FirstOrder.Language.Structure.FG.range
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
inst_2 : Countable N
h : FG L M
let :
  ∀ (S : Set M) (finite_S : S.Finite)
    (closure_S : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤),
    Countable (M →[L] N)
⊢ Countable (M →[L] N)

Tactic:
let ⟨S, finite_S, closure_S⟩ := fg_iff.1 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
inst_2 : Countable N
h_1 : FG L M
S : Set M
finite_S : S.Finite
closure_S : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
g : (M →[L] N) → (↑S : Type u_1) → N := fun (f : M →[L] N) ↦ (⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ S)
f f' : M →[L] N
h : g f = g f'
apply : EqOn.{u_1, u_2} (β := N) (⇑f : (a : M) → N) (⇑f' : (a : M) → N) S
⊢ f = f'

Tactic:
apply Hom.eq_of_eqOn_dense closure_S

Premises used: FirstOrder.Language.Hom.eq_of_eqOn_dense
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
inst_2 : Countable N
h_1 : FG L M
S : Set M
finite_S : S.Finite
closure_S : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
g : (M →[L] N) → (↑S : Type u_1) → N := fun (f : M →[L] N) ↦ (⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ S)
f f' : M →[L] N
h : g f = g f'
x : M
x_in_S : x ∈ S
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f' : (a : M) → N) x : N)

Tactic:
congr_fun h ⟨x, x_in_S⟩

Premises used: Subtype.mk, congr_fun
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
inst_2 : Countable N
h_1 : FG L M
S : Set M
finite_S : S.Finite
closure_S : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
g : (M →[L] N) → (↑S : Type u_1) → N := fun (f : M →[L] N) ↦ (⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ S)
f f' : M →[L] N
h : g f = g f'
x : M
x_in_S : x ∈ S
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f' : (a : M) → N) x : N)

Tactic:
exact congr_fun h ⟨x, x_in_S⟩

Premises used: Subtype.mk, congr_fun
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
inst_2 : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
g : (M →[L] N) → (↑S : Type u_1) → N := fun (f : M →[L] N) ↦ (⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ S)
⊢ Function.Injective g

Tactic:
have g_inj : Function.Injective g := by
    intro f f' h
    apply Hom.eq_of_eqOn_dense closure_S
    intro x x_in_S
    exact congr_fun h ⟨x, x_in_S⟩
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
inst_2 : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
g : (M →[L] N) → (↑S : Type u_1) → N := fun (f : M →[L] N) ↦ (⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ S)
g_inj : Function.Injective g
⊢ Finite.{u_1 + 1} (↑S : Type u_1)

Tactic:
have : Finite ↑S := (S.finite_coe_iff).2 finite_S
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
inst_2 : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
g : (M →[L] N) → (↑S : Type u_1) → N := fun (f : M →[L] N) ↦ (⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ S)
g_inj : Function.Injective g
this : Finite.{u_1 + 1} (↑S : Type u_1)
⊢ Countable (M →[L] N)

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
N : Type u_2
inst_1 : L.Structure N
inst_2 : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
g : (M →[L] N) → (↑S : Type u_1) → N := fun (f : M →[L] N) ↦ (⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ S)
g_inj : Function.Injective g
this : Finite.{u_1 + 1} (↑S : Type u_1)
⊢ Countable (M →[L] N)

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
N : Type u_2
inst_1 : L.Structure N
inst_2 : Countable N
h : FG L M
⊢ Countable (M →[L] N)

Tactic:
FG.countable_hom N h

Premises used: FirstOrder.Language.Structure.FG.countable_hom
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
inst_2 : Countable N
h : FG L M
⊢ Countable (M ↪[L] N)

Tactic:
Function.Embedding.countable ⟨Embedding.toHom, Embedding.toHom_injective⟩

Premises used: Function.Embedding.mk, Function.Embedding.countable, FirstOrder.Language.Embedding.toHom_injective, FirstOrder.Language.Embedding.toHom
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
inst_2 : Countable N
h : FG L M
⊢ Countable (M ↪[L] N)

Tactic:
FG.countable_embedding N h

Premises used: FirstOrder.Language.Structure.FG.countable_embedding
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Finite M
⊢ FG L M

Tactic:
simp only [fg_def, Substructure.FG.of_finite]

Premises used: FirstOrder.Language.Structure.fg_def, FirstOrder.Language.Substructure.FG.of_finite
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : L.IsRelational
h : FG L M
⊢ Finite M

Tactic:
Finite.of_finite_univ (Substructure.FG.finite (fg_def.1 h))

Premises used: FirstOrder.Language.Structure.fg_def, FirstOrder.Language.Substructure.FG.finite, Iff.mp, Finite.of_finite_univ
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : L.IsRelational
⊢ FG L M ↔ Finite M

Tactic:
⟨FG.finite, fun _ => FG.of_finite⟩

Premises used: FirstOrder.Language.Structure.FG.finite, Iff.intro, FirstOrder.Language.Structure.FG.of_finite
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
⊢ CG L M ↔ Substructure.CG.{u_1, u_2, u_3} (L := L) (M := M) ⊤

Tactic:
⟨fun h => h.1, fun h => ⟨h⟩⟩

Premises used: FirstOrder.Language.Structure.CG.mk, Iff.intro, FirstOrder.Language.Structure.CG.out
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
rw :
  Substructure.CG.{u_1, u_2, u_3} (L := L) (M := M) ⊤ ↔
    ∃ (S : Set M), S.Countable ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
rw₁ rw₂ :
  (∃ (S : Set M), S.Countable ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤) ↔
    ∃ (S : Set M), S.Countable ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤
⊢ CG L M ↔
    ∃ (S : Set M), S.Countable ∧ Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) S) ⊤

Tactic:
rw [cg_def, Substructure.cg_def]

Premises used: FirstOrder.Language.Substructure.cg_def, FirstOrder.Language.Structure.cg_def
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
h : CG L M
f : M →[L] N
rw : (map f ⊤).CG
⊢ f.range.CG

Tactic:
rw [Hom.range_eq_map]

Premises used: FirstOrder.Language.Hom.range_eq_map
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
h : CG L M
f : M →[L] N
⊢ (map f ⊤).CG

Tactic:
(cg_def.1 h).map f

Premises used: FirstOrder.Language.Substructure.CG.map, FirstOrder.Language.Structure.cg_def, Iff.mp
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
h : CG L M
f : M →[L] N
⊢ (map f ⊤).CG

Tactic:
exact (cg_def.1 h).map f

Premises used: FirstOrder.Language.Substructure.CG.map, FirstOrder.Language.Structure.cg_def, Iff.mp
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
h : CG L M
f : M →[L] N
hs : Function.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ f.range = ⊤

Tactic:
rw [← Hom.range_eq_top] at hs

Premises used: FirstOrder.Language.Hom.range_eq_top
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
h : CG L M
f : M →[L] N
hs : f.range = ⊤
rw : f.range.CG
⊢ CG L N

Tactic:
rw [cg_def, ← hs]

Premises used: FirstOrder.Language.Structure.cg_def
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
h : CG L M
f : M →[L] N
hs : f.range = ⊤
⊢ f.range.CG

Tactic:
h.range f

Premises used: FirstOrder.Language.Structure.CG.range
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
h : CG L M
f : M →[L] N
hs : f.range = ⊤
⊢ f.range.CG

Tactic:
exact h.range f

Premises used: FirstOrder.Language.Structure.CG.range
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable.{u_2 + 1} ((l : ℕ) × L.Functions l)
rw : Substructure.CG.{u_1, u_2, u_3} (L := L) (M := M) ⊤ ↔ Countable M
rw₁ : Countable.{u_1 + 1} ↥⊤ ↔ Countable M
rw₂ rw₃ : Countable M ↔ Countable M
⊢ CG L M ↔ Countable M

Tactic:
rw [cg_def, Substructure.cg_iff_countable, topEquiv.toEquiv.countable_iff]

Premises used: FirstOrder.Language.Equiv.toEquiv, FirstOrder.Language.Structure.cg_def, Equiv.countable_iff, FirstOrder.Language.Substructure.cg_iff_countable, FirstOrder.Language.Substructure.topEquiv
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
inst_1 : Countable M
⊢ CG L M

Tactic:
simp only [cg_def, Substructure.cg_of_countable]

Premises used: FirstOrder.Language.Substructure.cg_of_countable, FirstOrder.Language.Structure.cg_def
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
h : FG L M
⊢ CG L M

Tactic:
cg_def.2 (fg_def.1 h).cg

Premises used: Iff.mpr, FirstOrder.Language.Structure.fg_def, FirstOrder.Language.Structure.cg_def, Iff.mp, FirstOrder.Language.Substructure.FG.cg
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
h : FG L M
⊢ CG L M

Tactic:
h.cg

Premises used: FirstOrder.Language.Structure.FG.cg
-- 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.FG L M ↔ Structure.FG 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.Equiv.toHom, FirstOrder.Language.Structure.FG.map_of_surjective, FirstOrder.Language.Equiv.toEquiv, Iff.intro, Equiv.surjective, Equiv.symm, FirstOrder.Language.Equiv.symm