-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem FG.countable_hom (N : Type*) [L.Structure N] [Countable N] (h : FG L M) :
    Countable (M →[L] N)

Proof state:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h✝ : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f => ⇑f ∘ Subtype.val
f f' : M →[L] N
h : g f = g f'
x : M
x_in_S : x ∈ S
⊢ f x = f' x

Tactic:
exact congr_fun h ⟨x, x_in_S⟩

Result:
no goals

Proof state:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h : FG L M
⊢ Countable (M →[L] N)

Tactic:
let ⟨S, finite_S, closure_S⟩ := fg_iff.1 h

Result:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
⊢ Countable (M →[L] N)

Proof state:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
⊢ Countable (M →[L] N)

Tactic:
let g : (M →[L] N) → (S → N) :=
  fun f ↦ f ∘ (↑)

Result:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f => ⇑f ∘ Subtype.val
⊢ Countable (M →[L] N)

Proof state:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f => ⇑f ∘ Subtype.val
g_inj : Function.Injective g
this : Finite ↑S
⊢ Countable (M →[L] N)

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

Result:
no goals

Proof state:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h✝ : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f => ⇑f ∘ Subtype.val
f f' : M →[L] N
h : g f = g f'
⊢ f = f'

Tactic:
apply Hom.eq_of_eqOn_dense closure_S

Result:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h✝ : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f => ⇑f ∘ Subtype.val
f f' : M →[L] N
h : g f = g f'
⊢ EqOn (⇑f) (⇑f') S

Proof state:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f => ⇑f ∘ Subtype.val
⊢ Countable (M →[L] N)

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⟩

Result:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f => ⇑f ∘ Subtype.val
g_inj : Function.Injective g
⊢ Countable (M →[L] N)

Proof state:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h✝ : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f => ⇑f ∘ Subtype.val
f f' : M →[L] N
h : g f = g f'
⊢ EqOn (⇑f) (⇑f') S

Tactic:
intro x x_in_S

Result:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h✝ : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f => ⇑f ∘ Subtype.val
f f' : M →[L] N
h : g f = g f'
x : M
x_in_S : x ∈ S
⊢ f x = f' x

Proof state:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f => ⇑f ∘ Subtype.val
g_inj : Function.Injective g
⊢ Countable (M →[L] N)

Tactic:
have : Finite ↑S := (S.finite_coe_iff).2 finite_S

Result:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f => ⇑f ∘ Subtype.val
g_inj : Function.Injective g
this : Finite ↑S
⊢ Countable (M →[L] N)

Proof state:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f => ⇑f ∘ Subtype.val
⊢ Function.Injective g

Tactic:
intro f f' h

Result:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h✝ : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f => ⇑f ∘ Subtype.val
f f' : M →[L] N
h : g f = g f'
⊢ f = f'