cases G with | mk G_obj G_map =>
intro hobj
have : F_obj = G_obj := funext hobj
cases this
dsimp
intro hmap
have : @F_map = @G_map := by
  apply funext; intro a; apply funext; intro b
  apply funext
  intro f
  exact (hmap a b f).eq_of
cases this
rfl
case mk
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
G : α ⥤q List β
map_id✝¹ : ∀ (X : α), Prefunctor.map G (𝟙 X) = 𝟙 (Prefunctor.obj G X)
map_comp✝¹ : ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z), Prefunctor.map G (f ≫ g) = Prefunctor.map G f ≫ Prefunctor.map G g
F_obj : α → List β
F_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := F_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := F_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := F_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := F_map } f ≫ Prefunctor.map { obj := F_obj, map := F_map } g
⊢ (∀ (a : α),
      Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
        Prefunctor.obj (Functor.mk G).toPrefunctor a) →
    (∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂),
        DVect2.Eq (Prefunctor.map (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor f)
          (Prefunctor.map (Functor.mk G).toPrefunctor f)) →
      Functor.mk { obj := F_obj, map := F_map } = Functor.mk G
no goals