internlm/Lean-Github huggingface dataset:
Theorem: DVect2.join_join
Proof state before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List (List α)
tail✝¹ : List (List (List α))
head✝ : List (List β)
tail✝ : List (List (List β))
fs : DVect2 (DVect2 γ) head✝¹ head✝
fsss : DVect2 (DVect2 (DVect2 γ)) tail✝¹ tail✝
⊢ join (join (cons fs fsss)) ≡ join (map List.join List.join (fun {a} {b} ↦ join) (cons fs fsss))
Tactic:
dsimp [DVect2.join, DVect2.map]
Proof state after:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List (List α)
tail✝¹ : List (List (List α))
head✝ : List (List β)
tail✝ : List (List (List β))
fs : DVect2 (DVect2 γ) head✝¹ head✝
fsss : DVect2 (DVect2 (DVect2 γ)) tail✝¹ tail✝
⊢ join (fs ++ join fsss) ≡ join fs ++ join (map List.join List.join (fun {a} {b} ↦ join) fsss)
Theorem: DVect2.join_join
Proof state before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List (List α)
tail✝¹ : List (List (List α))
head✝ : List (List β)
tail✝ : List (List (List β))
fs : DVect2 (DVect2 γ) head✝¹ head✝
fsss : DVect2 (DVect2 (DVect2 γ)) tail✝¹ tail✝
⊢ join (fs ++ join fsss) ≡ join fs ++ join (map List.join List.join (fun {a} {b} ↦ join) fsss)
Tactic:
apply DVect2.Eq.trans (DVect2.join_append fs _) _
Proof state after:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List (List α)
tail✝¹ : List (List (List α))
head✝ : List (List β)
tail✝ : List (List (List β))
fs : DVect2 (DVect2 γ) head✝¹ head✝
fsss : DVect2 (DVect2 (DVect2 γ)) tail✝¹ tail✝
⊢ join fs ++ join (join fsss) ≡ join fs ++ join (map List.join List.join (fun {a} {b} ↦ join) fsss)
Theorem: DVect2.join_join
Proof state before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List (List α)
tail✝¹ : List (List (List α))
head✝ : List (List β)
tail✝ : List (List (List β))
fs : DVect2 (DVect2 γ) head✝¹ head✝
fsss : DVect2 (DVect2 (DVect2 γ)) tail✝¹ tail✝
⊢ join fs ++ join (join fsss) ≡ join fs ++ join (map List.join List.join (fun {a} {b} ↦ join) fsss)
Tactic:
apply eq_of_eq_append_eq (DVect2.Eq.of rfl)
Proof state after:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List (List α)
tail✝¹ : List (List (List α))
head✝ : List (List β)
tail✝ : List (List (List β))
fs : DVect2 (DVect2 γ) head✝¹ head✝
fsss : DVect2 (DVect2 (DVect2 γ)) tail✝¹ tail✝
⊢ join (join fsss) ≡ join (map List.join List.join (fun {a} {b} ↦ join) fsss)
Theorem: DVect2.join_join
Proof state before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : List (List α)
tail✝¹ : List (List (List α))
head✝ : List (List β)
tail✝ : List (List (List β))
fs : DVect2 (DVect2 γ) head✝¹ head✝
fsss : DVect2 (DVect2 (DVect2 γ)) tail✝¹ tail✝
⊢ join (join fsss) ≡ join (map List.join List.join (fun {a} {b} ↦ join) fsss)
Tactic:
exact join_join fsss
Proof state after:
no goals
Theorem: DVect2.fromList_append
Proof state before:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
γ : α → α → Type v
f : (a : α) → γ a a
head✝ : α
as bs : List α
⊢ fromList γ f (head✝ :: as ++ bs) = fromList γ f (head✝ :: as) ++ fromList γ f bs
Tactic:
dsimp [fromList]
Proof state after:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
γ : α → α → Type v
f : (a : α) → γ a a
head✝ : α
as bs : List α
⊢ cons (f head✝) (fromList γ f (as ++ bs)) = cons (f head✝) (fromList γ f as) ++ fromList γ f bs
Theorem: DVect2.fromList_append
Proof state before:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
γ : α → α → Type v
f : (a : α) → γ a a
head✝ : α
as bs : List α
⊢ cons (f head✝) (fromList γ f (as ++ bs)) = cons (f head✝) (fromList γ f as) ++ fromList γ f bs
Tactic:
rw [cons_append]
Proof state after:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
γ : α → α → Type v
f : (a : α) → γ a a
head✝ : α
as bs : List α
⊢ cons (f head✝) (fromList γ f (as ++ bs)) = cons (f head✝) (fromList γ f as ++ fromList γ f bs)
Theorem: DVect2.fromList_append
Proof state before:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
γ : α → α → Type v
f : (a : α) → γ a a
head✝ : α
as bs : List α
⊢ cons (f head✝) (fromList γ f (as ++ bs)) = cons (f head✝) (fromList γ f as ++ fromList γ f bs)
Tactic:
rw [fromList_append γ f (as:=as) (bs:=bs)]
Proof state after:
no goals
Theorem: DVect2.dfromList_append
Proof state before:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
β₁ : Type u₁
β₂ : Type u₂
γ : β₁ → β₂ → Type v
f₁ : α → β₁
f₂ : α → β₂
g : (a : α) → γ (f₁ a) (f₂ a)
a : α
as bs : List α
⊢ dfromList f₁ f₂ g (a :: as ++ bs) ≡ dfromList f₁ f₂ g (a :: as) ++ dfromList f₁ f₂ g bs
Tactic:
dsimp [dfromList]
Proof state after:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
β₁ : Type u₁
β₂ : Type u₂
γ : β₁ → β₂ → Type v
f₁ : α → β₁
f₂ : α → β₂
g : (a : α) → γ (f₁ a) (f₂ a)
a : α
as bs : List α
⊢ cons (g a) (dfromList f₁ f₂ g (as ++ bs)) ≡ cons (g a) (dfromList f₁ f₂ g as) ++ dfromList f₁ f₂ g bs
Theorem: DVect2.dfromList_append
Proof state before:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
β₁ : Type u₁
β₂ : Type u₂
γ : β₁ → β₂ → Type v
f₁ : α → β₁
f₂ : α → β₂
g : (a : α) → γ (f₁ a) (f₂ a)
a : α
as bs : List α
⊢ cons (g a) (dfromList f₁ f₂ g (as ++ bs)) ≡ cons (g a) (dfromList f₁ f₂ g as) ++ dfromList f₁ f₂ g bs
Tactic:
rw [cons_append]
Proof state after:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
β₁ : Type u₁
β₂ : Type u₂
γ : β₁ → β₂ → Type v
f₁ : α → β₁
f₂ : α → β₂
g : (a : α) → γ (f₁ a) (f₂ a)
a : α
as bs : List α
⊢ cons (g a) (dfromList f₁ f₂ g (as ++ bs)) ≡ cons (g a) (dfromList f₁ f₂ g as ++ dfromList f₁ f₂ g bs)
Theorem: DVect2.dfromList_append
Proof state before:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
β₁ : Type u₁
β₂ : Type u₂
γ : β₁ → β₂ → Type v
f₁ : α → β₁
f₂ : α → β₂
g : (a : α) → γ (f₁ a) (f₂ a)
a : α
as bs : List α
⊢ cons (g a) (dfromList f₁ f₂ g (as ++ bs)) ≡ cons (g a) (dfromList f₁ f₂ g as ++ dfromList f₁ f₂ g bs)
Tactic:
apply DVect2.Eq.descend rfl
Proof state after:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
β₁ : Type u₁
β₂ : Type u₂
γ : β₁ → β₂ → Type v
f₁ : α → β₁
f₂ : α → β₂
g : (a : α) → γ (f₁ a) (f₂ a)
a : α
as bs : List α
⊢ dfromList f₁ f₂ g (as ++ bs) ≡ dfromList f₁ f₂ g as ++ dfromList f₁ f₂ g bs
Theorem: DVect2.dfromList_append
Proof state before:
α✝ : Type u₁
β : Type u₂
γ✝ : α✝ → β → Type v
α : Type u
β₁ : Type u₁
β₂ : Type u₂
γ : β₁ → β₂ → Type v
f₁ : α → β₁
f₂ : α → β₂
g : (a : α) → γ (f₁ a) (f₂ a)
a : α
as bs : List α
⊢ dfromList f₁ f₂ g (as ++ bs) ≡ dfromList f₁ f₂ g as ++ dfromList f₁ f₂ g bs
Tactic:
exact dfromList_append f₁ f₂ g (as:=as) (bs:=bs)
Proof state after:
no goals
Theorem: List.map_comp
Proof state before:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
⊢ ∀ {as : List α}, map (g ∘ f) as = map g (map f as)
Tactic:
intro as
Proof state after:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
as : List α
⊢ map (g ∘ f) as = map g (map f as)
Theorem: List.map_comp
Proof state before:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
as : List α
⊢ map (g ∘ f) as = map g (map f as)
Tactic:
induction as
Proof state after:
case nil
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
⊢ map (g ∘ f) [] = map g (map f [])

case cons
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : map (g ∘ f) tail✝ = map g (map f tail✝)
⊢ map (g ∘ f) (head✝ :: tail✝) = map g (map f (head✝ :: tail✝))
Theorem: List.map_comp
Proof state before:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
⊢ map (g ∘ f) [] = map g (map f [])
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: List.map_comp
Proof state before:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
a : α
as : List α
h_ind : map (g ∘ f) as = map g (map f as)
⊢ map (g ∘ f) (a :: as) = map g (map f (a :: as))
Tactic:
case cons a as h_ind =>
  dsimp [map]
  rw [h_ind]
Proof state after:
no goals
Theorem: List.map_comp
Proof state before:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
⊢ map (g ∘ f) [] = map g (map f [])
Tactic:
rfl
Proof state after:
no goals
Theorem: List.map_comp
Proof state before:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
a : α
as : List α
h_ind : map (g ∘ f) as = map g (map f as)
⊢ map (g ∘ f) (a :: as) = map g (map f (a :: as))
Tactic:
dsimp [map]
Proof state after:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
a : α
as : List α
h_ind : map (g ∘ f) as = map g (map f as)
⊢ g (f a) :: map (g ∘ f) as = g (f a) :: map g (map f as)
Theorem: List.map_comp
Proof state before:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
a : α
as : List α
h_ind : map (g ∘ f) as = map g (map f as)
⊢ g (f a) :: map (g ∘ f) as = g (f a) :: map g (map f as)
Tactic:
rw [h_ind]
Proof state after:
no goals
Theorem: List.join_append
Proof state before:
α : Type u
as : List α
ass bss : List (List α)
⊢ join (as :: ass ++ bss) = join (as :: ass) ++ join bss
Tactic:
dsimp [join]
Proof state after:
α : Type u
as : List α
ass bss : List (List α)
⊢ as ++ join (ass ++ bss) = as ++ join ass ++ join bss
Theorem: List.join_append
Proof state before:
α : Type u
as : List α
ass bss : List (List α)
⊢ as ++ join (ass ++ bss) = as ++ join ass ++ join bss
Tactic:
rw [List.append_assoc, join_append ass bss]
Proof state after:
no goals
Theorem: List.join_join
Proof state before:
α : Type u
as : List (List α)
asss : List (List (List α))
⊢ join (join (as :: asss)) = join (map join (as :: asss))
Tactic:
dsimp [join]
Proof state after:
α : Type u
as : List (List α)
asss : List (List (List α))
⊢ join (as ++ join asss) = join as ++ join (map join asss)
Theorem: List.join_join
Proof state before:
α : Type u
as : List (List α)
asss : List (List (List α))
⊢ join (as ++ join asss) = join as ++ join (map join asss)
Tactic:
rw [join_append, join_join asss]
Proof state after:
no goals
Theorem: List.map_join
Proof state before:
α : Type u
β : Type v
f : α → β
as : List α
ass : List (List α)
⊢ map f (join (as :: ass)) = join (map (map f) (as :: ass))
Tactic:
dsimp [join]
Proof state after:
α : Type u
β : Type v
f : α → β
as : List α
ass : List (List α)
⊢ map f (as ++ join ass) = map f as ++ join (map (map f) ass)
Theorem: List.map_join
Proof state before:
α : Type u
β : Type v
f : α → β
as : List α
ass : List (List α)
⊢ map f (as ++ join ass) = map f as ++ join (map (map f) ass)
Tactic:
rw [map_append, map_join f (ass:=ass)]
Proof state after:
no goals
Theorem: CategoryTheory.List.comp_cons'
Proof state before:
α : Type u
inst✝ : Category α
⊢ ∀ {a b c : α} {as bs cs : List α} {f : a ⟶ b} {fs : Hom as bs} {g : b ⟶ c} {gs : Hom bs cs},
    List.comp (DVect2.cons f fs) (DVect2.cons g gs) = DVect2.cons (f ≫ g) (List.comp fs gs)
Tactic:
intros
Proof state after:
α : Type u
inst✝ : Category α
a✝ b✝ c✝ : α
as✝ bs✝ cs✝ : List α
f✝ : a✝ ⟶ b✝
fs✝ : Hom as✝ bs✝
g✝ : b✝ ⟶ c✝
gs✝ : Hom bs✝ cs✝
⊢ List.comp (DVect2.cons f✝ fs✝) (DVect2.cons g✝ gs✝) = DVect2.cons (f✝ ≫ g✝) (List.comp fs✝ gs✝)
Theorem: CategoryTheory.List.comp_cons'
Proof state before:
α : Type u
inst✝ : Category α
a✝ b✝ c✝ : α
as✝ bs✝ cs✝ : List α
f✝ : a✝ ⟶ b✝
fs✝ : Hom as✝ bs✝
g✝ : b✝ ⟶ c✝
gs✝ : Hom bs✝ cs✝
⊢ List.comp (DVect2.cons f✝ fs✝) (DVect2.cons g✝ gs✝) = DVect2.cons (f✝ ≫ g✝) (List.comp fs✝ gs✝)
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.id_comp
Proof state before:
α : Type u
inst✝ : Category α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
f : head✝¹ ⟶ head✝
fs : DVect2 Quiver.Hom tail✝¹ tail✝
⊢ List.comp (List.id (head✝¹ :: tail✝¹)) (DVect2.cons f fs) = DVect2.cons f fs
Tactic:
dsimp
Proof state after:
α : Type u
inst✝ : Category α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
f : head✝¹ ⟶ head✝
fs : DVect2 Quiver.Hom tail✝¹ tail✝
⊢ DVect2.cons (𝟙 head✝¹ ≫ f) (List.comp (List.id tail✝¹) fs) = DVect2.cons f fs
Theorem: CategoryTheory.List.id_comp
Proof state before:
α : Type u
inst✝ : Category α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
f : head✝¹ ⟶ head✝
fs : DVect2 Quiver.Hom tail✝¹ tail✝
⊢ DVect2.cons (𝟙 head✝¹ ≫ f) (List.comp (List.id tail✝¹) fs) = DVect2.cons f fs
Tactic:
rw [Category.id_comp, List.id_comp fs]
Proof state after:
no goals
Theorem: CategoryTheory.List.comp_id
Proof state before:
α : Type u
inst✝ : Category α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
f : head✝¹ ⟶ head✝
fs : DVect2 Quiver.Hom tail✝¹ tail✝
⊢ List.comp (DVect2.cons f fs) (List.id (head✝ :: tail✝)) = DVect2.cons f fs
Tactic:
dsimp
Proof state after:
α : Type u
inst✝ : Category α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
f : head✝¹ ⟶ head✝
fs : DVect2 Quiver.Hom tail✝¹ tail✝
⊢ DVect2.cons (f ≫ 𝟙 head✝) (List.comp fs (List.id tail✝)) = DVect2.cons f fs
Theorem: CategoryTheory.List.comp_id
Proof state before:
α : Type u
inst✝ : Category α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
f : head✝¹ ⟶ head✝
fs : DVect2 Quiver.Hom tail✝¹ tail✝
⊢ DVect2.cons (f ≫ 𝟙 head✝) (List.comp fs (List.id tail✝)) = DVect2.cons f fs
Tactic:
rw [Category.comp_id, List.comp_id fs]
Proof state after:
no goals
Theorem: CategoryTheory.List.assoc
Proof state before:
α : Type u
inst✝ : Category α
head✝³ : α
tail✝³ : List α
head✝² : α
tail✝² : List α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
f : head✝³ ⟶ head✝²
fs : DVect2 Quiver.Hom tail✝³ tail✝²
g : head✝² ⟶ head✝¹
gs : DVect2 Quiver.Hom tail✝² tail✝¹
h : head✝¹ ⟶ head✝
hs : DVect2 Quiver.Hom tail✝¹ tail✝
⊢ List.comp (List.comp (DVect2.cons f fs) (DVect2.cons g gs)) (DVect2.cons h hs) =
    List.comp (DVect2.cons f fs) (List.comp (DVect2.cons g gs) (DVect2.cons h hs))
Tactic:
dsimp
Proof state after:
α : Type u
inst✝ : Category α
head✝³ : α
tail✝³ : List α
head✝² : α
tail✝² : List α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
f : head✝³ ⟶ head✝²
fs : DVect2 Quiver.Hom tail✝³ tail✝²
g : head✝² ⟶ head✝¹
gs : DVect2 Quiver.Hom tail✝² tail✝¹
h : head✝¹ ⟶ head✝
hs : DVect2 Quiver.Hom tail✝¹ tail✝
⊢ DVect2.cons ((f ≫ g) ≫ h) (List.comp (List.comp fs gs) hs) = DVect2.cons (f ≫ g ≫ h) (List.comp fs (List.comp gs hs))
Theorem: CategoryTheory.List.assoc
Proof state before:
α : Type u
inst✝ : Category α
head✝³ : α
tail✝³ : List α
head✝² : α
tail✝² : List α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
f : head✝³ ⟶ head✝²
fs : DVect2 Quiver.Hom tail✝³ tail✝²
g : head✝² ⟶ head✝¹
gs : DVect2 Quiver.Hom tail✝² tail✝¹
h : head✝¹ ⟶ head✝
hs : DVect2 Quiver.Hom tail✝¹ tail✝
⊢ DVect2.cons ((f ≫ g) ≫ h) (List.comp (List.comp fs gs) hs) = DVect2.cons (f ≫ g ≫ h) (List.comp fs (List.comp gs hs))
Tactic:
rw [Category.assoc, List.assoc fs gs hs]
Proof state after:
no goals
Theorem: CategoryTheory.List.eqF_List
Proof 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
Proof state after:
no goals
Theorem: CategoryTheory.List.eqF_List
Proof 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
Proof state after:
no goals
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
⊢ (∀ (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
Proof 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 }
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
⊢ (∀ (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
Proof 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 }