-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem FG.of_map_embedding {N : Type*} [L.Structure N] (f : M ↪[L] N) {s : L.Substructure M}
    (hs : (s.map f.toHom).FG) : s.FG

Proof state:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
⊢ ∃ S, S.Finite ∧ (closure L).toFun S = s

Tactic:
refine ⟨f ⁻¹' t, t.finite_toSet.preimage f.injective.injOn, ?_⟩

Result:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
⊢ (closure L).toFun (⇑f ⁻¹' ↑t) = s

Proof state:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
x : N
hx : x ∈ ↑t
h' : x ∈ ↑((closure L).toFun ↑t)
⊢ x ∈ range ⇑f

Tactic:
rw [h] at h'

Result:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
x : N
hx : x ∈ ↑t
h' : x ∈ ↑(Substructure.map f.toHom s)
⊢ x ∈ range ⇑f

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
hs : (Substructure.map f.toHom s).FG
⊢ s.FG

Tactic:
rcases hs with ⟨t, h⟩

Result:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
⊢ s.FG

Proof state:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
x : N
hx : x ∈ ↑t
h' : x ∈ ↑(Substructure.map f.toHom s)
⊢ x ∈ range ⇑f

Tactic:
exact Hom.map_le_range h'

Result:
no goals

Proof state:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
x : N
hx : x ∈ ↑t
⊢ x ∈ range ⇑f

Tactic:
have h' := subset_closure (L := L) hx

Result:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
x : N
hx : x ∈ ↑t
h' : x ∈ ↑((closure L).toFun ↑t)
⊢ x ∈ range ⇑f

Proof state:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
⊢ ↑t ⊆ range ⇑f

Tactic:
intro x hx

Result:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
x : N
hx : x ∈ ↑t
⊢ x ∈ range ⇑f

Proof state:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
⊢ (closure L).toFun (⇑f ⁻¹' ↑t) = s

Tactic:
refine map_injective_of_injective hf ?_

Result:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
⊢ Substructure.map f.toHom ((closure L).toFun (⇑f ⁻¹' ↑t)) = Substructure.map f.toHom s

Proof state:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
⊢ (closure L).toFun (⇑f ⁻¹' ↑t) = s

Tactic:
have hf : Function.Injective f.toHom := f.injective

Result:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
⊢ (closure L).toFun (⇑f ⁻¹' ↑t) = s

Proof state:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
⊢ s.FG

Tactic:
rw [fg_def]

Result:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
⊢ ∃ S, S.Finite ∧ (closure L).toFun S = s

Proof state:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
⊢ Substructure.map f.toHom ((closure L).toFun (⇑f ⁻¹' ↑t)) = Substructure.map f.toHom s

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

Result:
case intro
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
⊢ ↑t ⊆ range ⇑f