internlm/Lean-Github huggingface dataset:
Theorem: CategoryTheory.List.eqF_List
Proof 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
Proof 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 }
Theorem: CategoryTheory.List.eqF_List
Proof 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
Proof 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 }
Theorem: CategoryTheory.List.eqF_List
Proof 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
Proof 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 }
Theorem: CategoryTheory.List.eqF_List
Proof 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
Proof 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 }
Theorem: CategoryTheory.List.eqF_List
Proof 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
Proof 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 }
Theorem: CategoryTheory.List.eqF_List
Proof 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
Proof state after:
no goals
Theorem: CategoryTheory.List.eqF_List
Proof 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
Proof 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
Theorem: CategoryTheory.List.eqF_List
Proof 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
Proof 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
Theorem: CategoryTheory.List.eqF_List
Proof 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
Proof 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
Theorem: CategoryTheory.List.eqF_List
Proof 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
Proof 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