∀ (G : Type u_2) [inst : Group G] {X Y : Action FintypeCat G} (f : X ⟶ Y) (g : G)
  (y : (CategoryTheory.FintypeCat.imageComplement f.hom).carrier),
  (Y.ρ g).hom ↑y ∈ (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.hom))ᶜ