no goals
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j✝ k✝ : J
s : Set (F.obj i)
h : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
j k : J
g : k ⟶ j
⊢ range (F.map (𝟙 j)) ⊆ range (F.map g)
rw [map_id, types_id, range_id, (h g).range_eq]