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

case refine'_2
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
h : CG ⊤
⊢ CG S
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
⊢ CG S ↔ CG ⊤
refine' ⟨fun h => CG.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 : CG S
⊢ CG S
case refine'_1
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
h : CG S
⊢ CG (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 : CG S
⊢ CG S
exact h
case refine'_2
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
h✝ : CG ⊤
h : CG (map (Embedding.toHom (subtype S)) ⊤)
⊢ CG S
case refine'_2
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
h : CG ⊤
⊢ CG 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✝ : CG ⊤
h : CG S
⊢ CG S
case refine'_2
L : Language
M : Type u_3
inst✝ : Structure L M
S : Substructure L M
h✝ : CG ⊤
h : CG (map (Embedding.toHom (subtype S)) ⊤)
⊢ CG 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✝ : CG ⊤
h : CG S
⊢ CG S
exact h