Theorem: CategoryTheory.List.eqF_List (Moncalc/CategoryTheory/List/Basic.lean)

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤q List β
map_id✝¹ : ∀ (X : α), Prefunctor.map F (𝟙 X) = 𝟙 (Prefunctor.obj F X)
map_comp✝¹ : ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z), Prefunctor.map F (f ≫ g) = Prefunctor.map F f ≫ Prefunctor.map F g
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
⊢ (∀ (a : α), Prefunctor.obj (Functor.mk F).toPrefunctor a = Prefunctor.obj (Functor.mk G).toPrefunctor a) →
    (∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂),
        DVect2.Eq (Prefunctor.map (Functor.mk F).toPrefunctor f) (Prefunctor.map (Functor.mk G).toPrefunctor f)) →
      Functor.mk F = Functor.mk G
Tactic:
cases F with | mk F_obj F_map =>
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
State after:
no goals

State before:
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
Tactic:
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
State after:
no goals

State before:
case mk.mk
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_obj : α → List β
G_map : {X Y : α} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := G_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := G_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := G_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := G_obj, map := G_map } f ≫ Prefunctor.map { obj := G_obj, map := G_map } g
⊢ (∀ (a : α),
      Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
        Prefunctor.obj (Functor.mk { obj := G_obj, map := G_map }).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 { obj := G_obj, map := G_map }).toPrefunctor f)) →
      Functor.mk { obj := F_obj, map := F_map } = Functor.mk { obj := G_obj, map := G_map }
Tactic:
intro hobj
State after:
case mk.mk
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_obj : α → List β
G_map : {X Y : α} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := G_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := G_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := G_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := G_obj, map := G_map } f ≫ Prefunctor.map { obj := G_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := G_obj, map := G_map }).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 { obj := G_obj, map := G_map }).toPrefunctor f)) →
    Functor.mk { obj := F_obj, map := F_map } = Functor.mk { obj := G_obj, map := G_map }

State before:
case mk.mk
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_obj : α → List β
G_map : {X Y : α} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := G_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := G_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := G_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := G_obj, map := G_map } f ≫ Prefunctor.map { obj := G_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := G_obj, map := G_map }).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 { obj := G_obj, map := G_map }).toPrefunctor f)) →
    Functor.mk { obj := F_obj, map := F_map } = Functor.mk { obj := G_obj, map := G_map }
Tactic:
have : F_obj = G_obj := funext hobj
State after:
case mk.mk
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_obj : α → List β
G_map : {X Y : α} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := G_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := G_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := G_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := G_obj, map := G_map } f ≫ Prefunctor.map { obj := G_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := G_obj, map := G_map }).toPrefunctor a
this : F_obj = G_obj
⊢ (∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂),
      DVect2.Eq (Prefunctor.map (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor f)
        (Prefunctor.map (Functor.mk { obj := G_obj, map := G_map }).toPrefunctor f)) →
    Functor.mk { obj := F_obj, map := F_map } = Functor.mk { obj := G_obj, map := G_map }

State before:
case mk.mk
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_obj : α → List β
G_map : {X Y : α} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := G_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := G_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := G_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := G_obj, map := G_map } f ≫ Prefunctor.map { obj := G_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := G_obj, map := G_map }).toPrefunctor a
this : F_obj = G_obj
⊢ (∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂),
      DVect2.Eq (Prefunctor.map (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor f)
        (Prefunctor.map (Functor.mk { obj := G_obj, map := G_map }).toPrefunctor f)) →
    Functor.mk { obj := F_obj, map := F_map } = Functor.mk { obj := G_obj, map := G_map }
Tactic:
cases this
State after:
case mk.mk.refl
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).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 { obj := F_obj, map := G_map }).toPrefunctor f)) →
    Functor.mk { obj := F_obj, map := F_map } = Functor.mk { obj := F_obj, map := G_map }

State before:
case mk.mk.refl
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).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 { obj := F_obj, map := G_map }).toPrefunctor f)) →
    Functor.mk { obj := F_obj, map := F_map } = Functor.mk { obj := F_obj, map := G_map }
Tactic:
dsimp
State after:
case mk.mk.refl
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
⊢ (∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)) →
    Functor.mk { obj := F_obj, map := F_map } = Functor.mk { obj := F_obj, map := G_map }

State before:
case mk.mk.refl
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
⊢ (∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)) →
    Functor.mk { obj := F_obj, map := F_map } = Functor.mk { obj := F_obj, map := G_map }
Tactic:
intro hmap
State after:
case mk.mk.refl
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
⊢ Functor.mk { obj := F_obj, map := F_map } = Functor.mk { obj := F_obj, map := G_map }

State before:
case mk.mk.refl
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
⊢ Functor.mk { obj := F_obj, map := F_map } = Functor.mk { obj := F_obj, map := G_map }
Tactic:
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
State after:
case mk.mk.refl
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
this : F_map = G_map
⊢ Functor.mk { obj := F_obj, map := F_map } = Functor.mk { obj := F_obj, map := G_map }

State before:
case mk.mk.refl
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
this : F_map = G_map
⊢ Functor.mk { obj := F_obj, map := F_map } = Functor.mk { obj := F_obj, map := G_map }
Tactic:
cases this
State after:
case mk.mk.refl.refl
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
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
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (F_map f)
⊢ Functor.mk { obj := F_obj, map := F_map } = Functor.mk { obj := F_obj, map := F_map }

State before:
case mk.mk.refl.refl
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
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
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (F_map f)
⊢ Functor.mk { obj := F_obj, map := F_map } = Functor.mk { obj := F_obj, map := F_map }
Tactic:
rfl
State after:
no goals

State before:
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
⊢ F_map = G_map
Tactic:
apply funext
State after:
case h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
⊢ ∀ (x : α), @F_map x = @G_map x

State before:
case h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
⊢ ∀ (x : α), @F_map x = @G_map x
Tactic:
intro a
State after:
case h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a : α
⊢ @F_map a = @G_map a

State before:
case h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a : α
⊢ @F_map a = @G_map a
Tactic:
apply funext
State after:
case h.h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a : α
⊢ ∀ (x : α), F_map = G_map

State before:
case h.h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a : α
⊢ ∀ (x : α), F_map = G_map
Tactic:
intro b
State after:
case h.h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a b : α
⊢ F_map = G_map

State before:
case h.h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a b : α
⊢ F_map = G_map
Tactic:
apply funext
State after:
case h.h.h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a b : α
⊢ ∀ (x : a ⟶ b), F_map x = G_map x

State before:
case h.h.h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a b : α
⊢ ∀ (x : a ⟶ b), F_map x = G_map x
Tactic:
intro f
State after:
case h.h.h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a b : α
f : a ⟶ b
⊢ F_map f = G_map f

State before:
case h.h.h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
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
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a b : α
f : a ⟶ b
⊢ F_map f = G_map f
Tactic:
exact (hmap a b f).eq_of
State after:
no goals