case a
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
f : i ⟶ j
g : j ⟶ k
h : eventualRange F k = range (F.map g)
⊢ eventualRange F k ⊆ range (F.map (f ≫ g))

case a
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
f : i ⟶ j
g : j ⟶ k
h : eventualRange F k = range (F.map g)
⊢ range (F.map (f ≫ g)) ⊆ eventualRange F k
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
f : i ⟶ j
g : j ⟶ k
h : eventualRange F k = range (F.map g)
⊢ eventualRange F k = range (F.map (f ≫ g))
apply subset_antisymm
no goals
case a
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
f : i ⟶ j
g : j ⟶ k
h : eventualRange F k = range (F.map g)
⊢ eventualRange F k ⊆ range (F.map (f ≫ g))
apply iInter₂_subset
case a
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
f : i ⟶ j
g : j ⟶ k
h : eventualRange F k = range (F.map g)
⊢ range (F.map f ≫ F.map g) ⊆ range (F.map g)
case a
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
f : i ⟶ j
g : j ⟶ k
h : eventualRange F k = range (F.map g)
⊢ range (F.map (f ≫ g)) ⊆ eventualRange F k
rw [h, F.map_comp]
no goals
case a
J : Type u
inst✝ : Category J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
f : i ⟶ j
g : j ⟶ k
h : eventualRange F k = range (F.map g)
⊢ range (F.map f ≫ F.map g) ⊆ range (F.map g)
apply range_comp_subset_range