internlm/Lean-Github huggingface dataset:
Theorem: CategoryTheory.List.mapF.compositor_lax_oplax
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ mapF.compositorLax F G [] ≫ mapF.compositorOplax F G [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor [])
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.compositor_lax_oplax
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
a : α
as : List α
h_ind :
  mapF.compositorLax F G as ≫ mapF.compositorOplax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor as)
⊢ mapF.compositorLax F G (a :: as) ≫ mapF.compositorOplax F G (a :: as) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor (a :: as))
Tactic:
case cons a as h_ind =>
  dsimp [mapF.compositorLax, mapF.compositorOplax]
  rw [h_ind, Category.id_comp]
  rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.compositor_lax_oplax
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ mapF.compositorLax F G [] ≫ mapF.compositorOplax F G [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor [])
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.compositor_lax_oplax
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
a : α
as : List α
h_ind :
  mapF.compositorLax F G as ≫ mapF.compositorOplax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor as)
⊢ mapF.compositorLax F G (a :: as) ≫ mapF.compositorOplax F G (a :: as) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor (a :: as))
Tactic:
dsimp [mapF.compositorLax, mapF.compositorOplax]
Proof state after:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
a : α
as : List α
h_ind :
  mapF.compositorLax F G as ≫ mapF.compositorOplax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor as)
⊢ DVect2.cons
      (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)) ≫
        𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (mapF.compositorLax F G as ≫ mapF.compositorOplax F G as) =
    DVect2.cons (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (𝟙
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor G).toPrefunctor
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as)))
Theorem: CategoryTheory.List.mapF.compositor_lax_oplax
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
a : α
as : List α
h_ind :
  mapF.compositorLax F G as ≫ mapF.compositorOplax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor as)
⊢ DVect2.cons
      (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)) ≫
        𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (mapF.compositorLax F G as ≫ mapF.compositorOplax F G as) =
    DVect2.cons (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (𝟙
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor G).toPrefunctor
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as)))
Tactic:
rw [h_ind, Category.id_comp]
Proof state after:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
a : α
as : List α
h_ind :
  mapF.compositorLax F G as ≫ mapF.compositorOplax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor as)
⊢ DVect2.cons (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor as)) =
    DVect2.cons (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (𝟙
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor G).toPrefunctor
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as)))
Theorem: CategoryTheory.List.mapF.compositor_lax_oplax
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
a : α
as : List α
h_ind :
  mapF.compositorLax F G as ≫ mapF.compositorOplax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor as)
⊢ DVect2.cons (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F ⋙ Prefunctor.obj mapF.toPrefunctor G).toPrefunctor as)) =
    DVect2.cons (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (𝟙
        (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor G).toPrefunctor
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor as)))
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.compositor_oplax_lax
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
as : List α
⊢ mapF.compositorOplax F G as ≫ mapF.compositorLax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor as)
Tactic:
induction as
Proof state after:
case nil
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ mapF.compositorOplax F G [] ≫ mapF.compositorLax F G [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor [])

case cons
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
head✝ : α
tail✝ : List α
tail_ih✝ :
  mapF.compositorOplax F G tail✝ ≫ mapF.compositorLax F G tail✝ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor tail✝)
⊢ mapF.compositorOplax F G (head✝ :: tail✝) ≫ mapF.compositorLax F G (head✝ :: tail✝) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor (head✝ :: tail✝))
Theorem: CategoryTheory.List.mapF.compositor_oplax_lax
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ mapF.compositorOplax F G [] ≫ mapF.compositorLax F G [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor [])
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.compositor_oplax_lax
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
a : α
as : List α
h_ind :
  mapF.compositorOplax F G as ≫ mapF.compositorLax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor as)
⊢ mapF.compositorOplax F G (a :: as) ≫ mapF.compositorLax F G (a :: as) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor (a :: as))
Tactic:
case cons a as h_ind =>
dsimp [mapF.compositorLax, mapF.compositorOplax]
rw [h_ind, Category.id_comp]
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.compositor_oplax_lax
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ mapF.compositorOplax F G [] ≫ mapF.compositorLax F G [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor [])
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.compositor_oplax_lax
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
a : α
as : List α
h_ind :
  mapF.compositorOplax F G as ≫ mapF.compositorLax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor as)
⊢ mapF.compositorOplax F G (a :: as) ≫ mapF.compositorLax F G (a :: as) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor (a :: as))
Tactic:
dsimp [mapF.compositorLax, mapF.compositorOplax]
Proof state after:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
a : α
as : List α
h_ind :
  mapF.compositorOplax F G as ≫ mapF.compositorLax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor as)
⊢ DVect2.cons
      (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)) ≫
        𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (mapF.compositorOplax F G as ≫ mapF.compositorLax F G as) =
    DVect2.cons (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor as))
Theorem: CategoryTheory.List.mapF.compositor_oplax_lax
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
a : α
as : List α
h_ind :
  mapF.compositorOplax F G as ≫ mapF.compositorLax F G as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor as)
⊢ DVect2.cons
      (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)) ≫
        𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (mapF.compositorOplax F G as ≫ mapF.compositorLax F G as) =
    DVect2.cons (𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor a)))
      (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (F ⋙ G)).toPrefunctor as))
Tactic:
rw [h_ind, Category.id_comp]
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.naturality₂
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
⊢ (Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom =
    (mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)
Tactic:
ext as
Proof state after:
case w.h
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
as : List α
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      as =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as
Theorem: CategoryTheory.List.mapF.naturality₂
Proof state before:
case w.h
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
as : List α
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      as =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as
Tactic:
induction as
Proof state after:
case w.h.nil
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      [] =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) []

case w.h.cons
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
head✝ : α
tail✝ : List α
tail_ih✝ :
  NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      tail✝ =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) tail✝
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      (head✝ :: tail✝) =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) (head✝ :: tail✝)
Theorem: CategoryTheory.List.mapF.naturality₂
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      [] =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) []
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.naturality₂
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
a : α
as : List α
h_ind :
  NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      as =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      (a :: as) =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) (a :: as)
Tactic:
case cons a as h_ind =>
  dsimp [mapF.compositor, mapF.compositorLax] at *
  rw [h_ind, Category.id_comp, Category.comp_id]
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.naturality₂
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      [] =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) []
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.mapF.naturality₂
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
a : α
as : List α
h_ind :
  NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      as =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as
⊢ NatTrans.app ((Prefunctor.map mapF.toPrefunctor φ ◫ Prefunctor.map mapF.toPrefunctor ψ) ≫ (mapF.compositor F₂ G₂).hom)
      (a :: as) =
    NatTrans.app ((mapF.compositor F₁ G₁).hom ≫ Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) (a :: as)
Tactic:
dsimp [mapF.compositor, mapF.compositorLax] at *
Proof state after:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
a : α
as : List α
h_ind :
  (NatTrans.app (Prefunctor.map mapF.toPrefunctor ψ)
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F₁).toPrefunctor as) ≫
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor G₂).toPrefunctor
          (NatTrans.app (Prefunctor.map mapF.toPrefunctor φ) as)) ≫
      mapF.compositorLax F₂ G₂ as =
    mapF.compositorLax F₁ G₁ as ≫ NatTrans.app (Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as
⊢ DVect2.cons
      ((NatTrans.app ψ (Prefunctor.obj F₁.toPrefunctor a) ≫ Prefunctor.map G₂.toPrefunctor (NatTrans.app φ a)) ≫
        𝟙 (Prefunctor.obj G₂.toPrefunctor (Prefunctor.obj F₂.toPrefunctor a)))
      ((NatTrans.app (Prefunctor.map mapF.toPrefunctor ψ)
            (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F₁).toPrefunctor as) ≫
          Prefunctor.map (Prefunctor.obj mapF.toPrefunctor G₂).toPrefunctor
            (NatTrans.app (Prefunctor.map mapF.toPrefunctor φ) as)) ≫
        mapF.compositorLax F₂ G₂ as) =
    DVect2.cons
      (𝟙 (Prefunctor.obj G₁.toPrefunctor (Prefunctor.obj F₁.toPrefunctor a)) ≫
        NatTrans.app ψ (Prefunctor.obj F₁.toPrefunctor a) ≫ Prefunctor.map G₂.toPrefunctor (NatTrans.app φ a))
      (mapF.compositorLax F₁ G₁ as ≫ NatTrans.app (Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as)
Theorem: CategoryTheory.List.mapF.naturality₂
Proof state before:
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F₁ F₂ : α ⥤ β
G₁ G₂ : β ⥤ γ
φ : F₁ ⟶ F₂
ψ : G₁ ⟶ G₂
a : α
as : List α
h_ind :
  (NatTrans.app (Prefunctor.map mapF.toPrefunctor ψ)
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F₁).toPrefunctor as) ≫
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor G₂).toPrefunctor
          (NatTrans.app (Prefunctor.map mapF.toPrefunctor φ) as)) ≫
      mapF.compositorLax F₂ G₂ as =
    mapF.compositorLax F₁ G₁ as ≫ NatTrans.app (Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as
⊢ DVect2.cons
      ((NatTrans.app ψ (Prefunctor.obj F₁.toPrefunctor a) ≫ Prefunctor.map G₂.toPrefunctor (NatTrans.app φ a)) ≫
        𝟙 (Prefunctor.obj G₂.toPrefunctor (Prefunctor.obj F₂.toPrefunctor a)))
      ((NatTrans.app (Prefunctor.map mapF.toPrefunctor ψ)
            (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor F₁).toPrefunctor as) ≫
          Prefunctor.map (Prefunctor.obj mapF.toPrefunctor G₂).toPrefunctor
            (NatTrans.app (Prefunctor.map mapF.toPrefunctor φ) as)) ≫
        mapF.compositorLax F₂ G₂ as) =
    DVect2.cons
      (𝟙 (Prefunctor.obj G₁.toPrefunctor (Prefunctor.obj F₁.toPrefunctor a)) ≫
        NatTrans.app ψ (Prefunctor.obj F₁.toPrefunctor a) ≫ Prefunctor.map G₂.toPrefunctor (NatTrans.app φ a))
      (mapF.compositorLax F₁ G₁ as ≫ NatTrans.app (Prefunctor.map mapF.toPrefunctor (φ ◫ ψ)) as)
Tactic:
rw [h_ind, Category.id_comp, Category.comp_id]
Proof state after:
no goals
Theorem: boxes_last
Proof state before:
a : Program
as : List Program
c : Program
P : Formula
⊢ (~⌈a⌉⌈⌈as ++ [c]⌉⌉P) = (~⌈a⌉⌈⌈as⌉⌉⌈c⌉P)
Tactic:
induction as
Proof state after:
case nil
a c : Program
P : Formula
⊢ (~⌈a⌉⌈⌈[] ++ [c]⌉⌉P) = (~⌈a⌉⌈⌈[]⌉⌉⌈c⌉P)

case cons
a c : Program
P : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (~⌈a⌉⌈⌈tail✝ ++ [c]⌉⌉P) = (~⌈a⌉⌈⌈tail✝⌉⌉⌈c⌉P)
⊢ (~⌈a⌉⌈⌈head✝ :: tail✝ ++ [c]⌉⌉P) = (~⌈a⌉⌈⌈head✝ :: tail✝⌉⌉⌈c⌉P)
Theorem: boxes_last
Proof state before:
case nil
a c : Program
P : Formula
⊢ (~⌈a⌉⌈⌈[] ++ [c]⌉⌉P) = (~⌈a⌉⌈⌈[]⌉⌉⌈c⌉P)
Tactic:
simp
Proof state after:
no goals
Theorem: boxes_last
Proof state before:
case cons
a c : Program
P : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (~⌈a⌉⌈⌈tail✝ ++ [c]⌉⌉P) = (~⌈a⌉⌈⌈tail✝⌉⌉⌈c⌉P)
⊢ (~⌈a⌉⌈⌈head✝ :: tail✝ ++ [c]⌉⌉P) = (~⌈a⌉⌈⌈head✝ :: tail✝⌉⌉⌈c⌉P)
Tactic:
simp at *
Proof state after:
case cons
a c : Program
P : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (⌈⌈tail✝ ++ [c]⌉⌉P) = ⌈⌈tail✝⌉⌉⌈c⌉P
⊢ (⌈⌈tail✝ ++ [c]⌉⌉P) = ⌈⌈tail✝⌉⌉⌈c⌉P
Theorem: boxes_last
Proof state before:
case cons
a c : Program
P : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (⌈⌈tail✝ ++ [c]⌉⌉P) = ⌈⌈tail✝⌉⌉⌈c⌉P
⊢ (⌈⌈tail✝ ++ [c]⌉⌉P) = ⌈⌈tail✝⌉⌉⌈c⌉P
Tactic:
assumption
Proof state after:
no goals
Theorem: boxes_append
Proof state before:
as bs : List Program
P : Formula
⊢ (⌈⌈as ++ bs⌉⌉P) = ⌈⌈as⌉⌉⌈⌈bs⌉⌉P
Tactic:
induction as
Proof state after:
case nil
bs : List Program
P : Formula
⊢ (⌈⌈[] ++ bs⌉⌉P) = ⌈⌈[]⌉⌉⌈⌈bs⌉⌉P

case cons
bs : List Program
P : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (⌈⌈tail✝ ++ bs⌉⌉P) = ⌈⌈tail✝⌉⌉⌈⌈bs⌉⌉P
⊢ (⌈⌈head✝ :: tail✝ ++ bs⌉⌉P) = ⌈⌈head✝ :: tail✝⌉⌉⌈⌈bs⌉⌉P
Theorem: boxes_append
Proof state before:
case nil
bs : List Program
P : Formula
⊢ (⌈⌈[] ++ bs⌉⌉P) = ⌈⌈[]⌉⌉⌈⌈bs⌉⌉P
Tactic:
simp
Proof state after:
no goals
Theorem: boxes_append
Proof state before:
case cons
bs : List Program
P : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (⌈⌈tail✝ ++ bs⌉⌉P) = ⌈⌈tail✝⌉⌉⌈⌈bs⌉⌉P
⊢ (⌈⌈head✝ :: tail✝ ++ bs⌉⌉P) = ⌈⌈head✝ :: tail✝⌉⌉⌈⌈bs⌉⌉P
Tactic:
simp at *
Proof state after:
case cons
bs : List Program
P : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (⌈⌈tail✝ ++ bs⌉⌉P) = ⌈⌈tail✝⌉⌉⌈⌈bs⌉⌉P
⊢ (⌈⌈tail✝ ++ bs⌉⌉P) = ⌈⌈tail✝⌉⌉⌈⌈bs⌉⌉P
Theorem: boxes_append
Proof state before:
case cons
bs : List Program
P : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (⌈⌈tail✝ ++ bs⌉⌉P) = ⌈⌈tail✝⌉⌉⌈⌈bs⌉⌉P
⊢ (⌈⌈tail✝ ++ bs⌉⌉P) = ⌈⌈tail✝⌉⌉⌈⌈bs⌉⌉P
Tactic:
assumption
Proof state after:
no goals
Theorem: loadBoxes_last
Proof state before:
a : Program
as : List Program
c : Program
P : LoadFormula
⊢ (~'⌊a⌋⌊⌊as ++ [c]⌋⌋P) = ~'⌊a⌋⌊⌊as⌋⌋⌊c⌋P
Tactic:
induction as
Proof state after:
case nil
a c : Program
P : LoadFormula
⊢ (~'⌊a⌋⌊⌊[] ++ [c]⌋⌋P) = ~'⌊a⌋⌊⌊[]⌋⌋⌊c⌋P

case cons
a c : Program
P : LoadFormula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (~'⌊a⌋⌊⌊tail✝ ++ [c]⌋⌋P) = ~'⌊a⌋⌊⌊tail✝⌋⌋⌊c⌋P
⊢ (~'⌊a⌋⌊⌊head✝ :: tail✝ ++ [c]⌋⌋P) = ~'⌊a⌋⌊⌊head✝ :: tail✝⌋⌋⌊c⌋P
Theorem: loadBoxes_last
Proof state before:
case nil
a c : Program
P : LoadFormula
⊢ (~'⌊a⌋⌊⌊[] ++ [c]⌋⌋P) = ~'⌊a⌋⌊⌊[]⌋⌋⌊c⌋P
Tactic:
simp
Proof state after:
no goals
Theorem: loadBoxes_last
Proof state before:
case cons
a c : Program
P : LoadFormula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (~'⌊a⌋⌊⌊tail✝ ++ [c]⌋⌋P) = ~'⌊a⌋⌊⌊tail✝⌋⌋⌊c⌋P
⊢ (~'⌊a⌋⌊⌊head✝ :: tail✝ ++ [c]⌋⌋P) = ~'⌊a⌋⌊⌊head✝ :: tail✝⌋⌋⌊c⌋P
Tactic:
simp at *
Proof state after:
case cons
a c : Program
P : LoadFormula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (⌊⌊tail✝ ++ [c]⌋⌋P) = ⌊⌊tail✝⌋⌋⌊c⌋P
⊢ (⌊⌊tail✝ ++ [c]⌋⌋P) = ⌊⌊tail✝⌋⌋⌊c⌋P
Theorem: loadBoxes_last
Proof state before:
case cons
a c : Program
P : LoadFormula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (⌊⌊tail✝ ++ [c]⌋⌋P) = ⌊⌊tail✝⌋⌋⌊c⌋P
⊢ (⌊⌊tail✝ ++ [c]⌋⌋P) = ⌊⌊tail✝⌋⌋⌊c⌋P
Tactic:
assumption
Proof state after:
no goals
Theorem: loadBoxes_append
Proof state before:
as bs : List Program
P : LoadFormula
⊢ (⌊⌊as ++ bs⌋⌋P) = ⌊⌊as⌋⌋⌊⌊bs⌋⌋P
Tactic:
induction as
Proof state after:
case nil
bs : List Program
P : LoadFormula
⊢ (⌊⌊[] ++ bs⌋⌋P) = ⌊⌊[]⌋⌋⌊⌊bs⌋⌋P

case cons
bs : List Program
P : LoadFormula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (⌊⌊tail✝ ++ bs⌋⌋P) = ⌊⌊tail✝⌋⌋⌊⌊bs⌋⌋P
⊢ (⌊⌊head✝ :: tail✝ ++ bs⌋⌋P) = ⌊⌊head✝ :: tail✝⌋⌋⌊⌊bs⌋⌋P
Theorem: loadBoxes_append
Proof state before:
case nil
bs : List Program
P : LoadFormula
⊢ (⌊⌊[] ++ bs⌋⌋P) = ⌊⌊[]⌋⌋⌊⌊bs⌋⌋P
Tactic:
simp
Proof state after:
no goals
Theorem: loadBoxes_append
Proof state before:
case cons
bs : List Program
P : LoadFormula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (⌊⌊tail✝ ++ bs⌋⌋P) = ⌊⌊tail✝⌋⌋⌊⌊bs⌋⌋P
⊢ (⌊⌊head✝ :: tail✝ ++ bs⌋⌋P) = ⌊⌊head✝ :: tail✝⌋⌋⌊⌊bs⌋⌋P
Tactic:
simp at *
Proof state after:
case cons
bs : List Program
P : LoadFormula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (⌊⌊tail✝ ++ bs⌋⌋P) = ⌊⌊tail✝⌋⌋⌊⌊bs⌋⌋P
⊢ (⌊⌊tail✝ ++ bs⌋⌋P) = ⌊⌊tail✝⌋⌋⌊⌊bs⌋⌋P
Theorem: loadBoxes_append
Proof state before:
case cons
bs : List Program
P : LoadFormula
head✝ : Program
tail✝ : List Program
tail_ih✝ : (⌊⌊tail✝ ++ bs⌋⌋P) = ⌊⌊tail✝⌋⌋⌊⌊bs⌋⌋P
⊢ (⌊⌊tail✝ ++ bs⌋⌋P) = ⌊⌊tail✝⌋⌋⌊⌊bs⌋⌋P
Tactic:
assumption
Proof state after:
no goals
Theorem: inVocList
Proof state before:
ℓ : ℕ
L : List Formula
⊢ ℓ ∈ vocabOfListFormula L ↔ ∃ φ ∈ L, ℓ ∈ vocabOfFormula φ
Tactic:
simp only [vocabOfListFormula, Finset.mem_biUnion, List.mem_toFinset]
Proof state after:
no goals
Theorem: modelExistence
Proof state before:
X : TNode
⊢ consistent X → ∃ WS x W, X.toFinset ⊆ ↑W
Tactic:
sorry
Proof state after:
no goals
Theorem: completeness
Proof state before:
⊢ ∀ (X : TNode), consistent X ↔ satisfiable X
Tactic:
intro X
Proof state after:
X : TNode
⊢ consistent X ↔ satisfiable X
Theorem: completeness
Proof state before:
X : TNode
⊢ consistent X ↔ satisfiable X
Tactic:
constructor
Proof state after:
case mp
X : TNode
⊢ consistent X → satisfiable X

case mpr
X : TNode
⊢ satisfiable X → consistent X
Theorem: completeness
Proof state before:
case mp
X : TNode
⊢ consistent X → satisfiable X
Tactic:
intro X_is_consistent
Proof state after:
case mp
X : TNode
X_is_consistent : consistent X
⊢ satisfiable X