L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
h : CG L M
f : M →[L] N
hs : Hom.range f = ⊤
⊢ CG L N
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
h : CG L M
f : M →[L] N
hs : Function.Surjective ↑f
⊢ CG L N
rw [← Hom.range_eq_top] at hs
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
h : CG L M
f : M →[L] N
hs : Hom.range f = ⊤
⊢ Substructure.CG (Hom.range f)
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
h : CG L M
f : M →[L] N
hs : Hom.range f = ⊤
⊢ CG L N
rw [cg_def, ← hs]
no goals
L : Language
M : Type u_4
inst✝¹ : Structure L M
N : Type u_1
inst✝ : Structure L N
h : CG L M
f : M →[L] N
hs : Hom.range f = ⊤
⊢ Substructure.CG (Hom.range f)
exact h.range f