[GOAL]
α : Type u
f g : MonoOver α
t : f ⟶ g
⊢ (fun f => Set.range f.obj.hom) f ≤ (fun f => Set.range f.obj.hom) g
[PROOFSTEP]
rintro a ⟨x, rfl⟩
[GOAL]
case intro
α : Type u
f g : MonoOver α
t : f ⟶ g
x : (𝟭 (Type u)).obj f.obj.left
⊢ Comma.hom f.obj x ∈ (fun f => Set.range f.obj.hom) g
[PROOFSTEP]
exact ⟨t.1 x, congr_fun t.w x⟩
