L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
⊢ FG S ↔ FG ⊤
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
⊢ FG S ↔ Structure.FG L { x // x ∈ S }
rw [Structure.fg_def]
case refine'_1
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
h : FG S
⊢ FG (map (Embedding.toHom (subtype S)) ⊤)

case refine'_2
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
h : FG ⊤
⊢ FG S
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
⊢ FG S ↔ FG ⊤
refine' ⟨fun h => FG.of_map_embedding S.subtype _, fun h => _⟩
case refine'_1
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
h : FG S
⊢ FG S
case refine'_1
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
h : FG S
⊢ FG (map (Embedding.toHom (subtype S)) ⊤)
rw [← Hom.range_eq_map, range_subtype]
no goals
case refine'_1
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
h : FG S
⊢ FG S
exact h
case refine'_2
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
h✝ : FG ⊤
h : FG (map (Embedding.toHom (subtype S)) ⊤)
⊢ FG S
case refine'_2
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
h : FG ⊤
⊢ FG S
have h := h.map S.subtype.toHom
case refine'_2
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
h✝ : FG ⊤
h : FG S
⊢ FG S
case refine'_2
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
h✝ : FG ⊤
h : FG (map (Embedding.toHom (subtype S)) ⊤)
⊢ FG S
rw [← Hom.range_eq_map, range_subtype] at h
no goals
case refine'_2
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
h✝ : FG ⊤
h : FG S
⊢ FG S
exact h