internlm/Lean-Github huggingface dataset:
Theorem: CategoryTheory.List.joinF.assoc
Proof state before:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List (List (List α))), List.join (List.join a) = List.join (List.map List.join a)

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List (List (List α))) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.join f)) (DVect2.join (DVect2.map List.join List.join (fun {a b} ↦ DVect2.join) f))
Tactic:
. intros; exact List.join_join _
Proof state after:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List (List (List α))) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.join f)) (DVect2.join (DVect2.map List.join List.join (fun {a b} ↦ DVect2.join) f))
Theorem: CategoryTheory.List.joinF.assoc
Proof state before:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List (List (List α))) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.join f)) (DVect2.join (DVect2.map List.join List.join (fun {a b} ↦ DVect2.join) f))
Tactic:
. intros; exact DVect2.join_join _
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unitorLeft_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
as : List α
⊢ joinF.unitorLeftLax as ≫ joinF.unitorLeftOplax as = 𝟙 as
Tactic:
induction as
Proof state after:
case nil
α : Type u
inst✝ : Category α
⊢ joinF.unitorLeftLax [] ≫ joinF.unitorLeftOplax [] = 𝟙 []

case cons
α : Type u
inst✝ : Category α
head✝ : α
tail✝ : List α
tail_ih✝ : joinF.unitorLeftLax tail✝ ≫ joinF.unitorLeftOplax tail✝ = 𝟙 tail✝
⊢ joinF.unitorLeftLax (head✝ :: tail✝) ≫ joinF.unitorLeftOplax (head✝ :: tail✝) = 𝟙 (head✝ :: tail✝)
Theorem: CategoryTheory.List.joinF.unitorLeft_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
⊢ joinF.unitorLeftLax [] ≫ joinF.unitorLeftOplax [] = 𝟙 []
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unitorLeft_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorLeftLax as ≫ joinF.unitorLeftOplax as = 𝟙 as
⊢ joinF.unitorLeftLax (a :: as) ≫ joinF.unitorLeftOplax (a :: as) = 𝟙 (a :: as)
Tactic:
case cons a as h_ind =>
  dsimp [joinF.unitorLeftLax, joinF.unitorLeftOplax]
  rw [h_ind, Category.id_comp]
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unitorLeft_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
⊢ joinF.unitorLeftLax [] ≫ joinF.unitorLeftOplax [] = 𝟙 []
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unitorLeft_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorLeftLax as ≫ joinF.unitorLeftOplax as = 𝟙 as
⊢ joinF.unitorLeftLax (a :: as) ≫ joinF.unitorLeftOplax (a :: as) = 𝟙 (a :: as)
Tactic:
dsimp [joinF.unitorLeftLax, joinF.unitorLeftOplax]
Proof state after:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorLeftLax as ≫ joinF.unitorLeftOplax as = 𝟙 as
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (joinF.unitorLeftLax as ≫ joinF.unitorLeftOplax as) = DVect2.cons (𝟙 a) (𝟙 as)
Theorem: CategoryTheory.List.joinF.unitorLeft_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorLeftLax as ≫ joinF.unitorLeftOplax as = 𝟙 as
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (joinF.unitorLeftLax as ≫ joinF.unitorLeftOplax as) = DVect2.cons (𝟙 a) (𝟙 as)
Tactic:
rw [h_ind, Category.id_comp]
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unitorLeft_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
as : List α
⊢ joinF.unitorLeftOplax as ≫ joinF.unitorLeftLax as = 𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor as)
Tactic:
induction as
Proof state after:
case nil
α : Type u
inst✝ : Category α
⊢ joinF.unitorLeftOplax [] ≫ joinF.unitorLeftLax [] = 𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor [])

case cons
α : Type u
inst✝ : Category α
head✝ : α
tail✝ : List α
tail_ih✝ :
  joinF.unitorLeftOplax tail✝ ≫ joinF.unitorLeftLax tail✝ = 𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor tail✝)
⊢ joinF.unitorLeftOplax (head✝ :: tail✝) ≫ joinF.unitorLeftLax (head✝ :: tail✝) =
    𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor (head✝ :: tail✝))
Theorem: CategoryTheory.List.joinF.unitorLeft_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
⊢ joinF.unitorLeftOplax [] ≫ joinF.unitorLeftLax [] = 𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor [])
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unitorLeft_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorLeftOplax as ≫ joinF.unitorLeftLax as = 𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor as)
⊢ joinF.unitorLeftOplax (a :: as) ≫ joinF.unitorLeftLax (a :: as) =
    𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor (a :: as))
Tactic:
case cons a as h_ind =>
  dsimp [joinF.unitorLeftLax, joinF.unitorLeftOplax]
  rw [h_ind, Category.id_comp]
  rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unitorLeft_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
⊢ joinF.unitorLeftOplax [] ≫ joinF.unitorLeftLax [] = 𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor [])
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unitorLeft_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorLeftOplax as ≫ joinF.unitorLeftLax as = 𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor as)
⊢ joinF.unitorLeftOplax (a :: as) ≫ joinF.unitorLeftLax (a :: as) =
    𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor (a :: as))
Tactic:
dsimp [joinF.unitorLeftLax, joinF.unitorLeftOplax]
Proof state after:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorLeftOplax as ≫ joinF.unitorLeftLax as = 𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor as)
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (joinF.unitorLeftOplax as ≫ joinF.unitorLeftLax as) =
    𝟙 (Prefunctor.obj joinF.toPrefunctor (Prefunctor.obj singletonF.toPrefunctor (a :: as)))
Theorem: CategoryTheory.List.joinF.unitorLeft_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorLeftOplax as ≫ joinF.unitorLeftLax as = 𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor as)
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (joinF.unitorLeftOplax as ≫ joinF.unitorLeftLax as) =
    𝟙 (Prefunctor.obj joinF.toPrefunctor (Prefunctor.obj singletonF.toPrefunctor (a :: as)))
Tactic:
rw [h_ind, Category.id_comp]
Proof state after:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorLeftOplax as ≫ joinF.unitorLeftLax as = 𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor as)
⊢ DVect2.cons (𝟙 a) (𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor as)) =
    𝟙 (Prefunctor.obj joinF.toPrefunctor (Prefunctor.obj singletonF.toPrefunctor (a :: as)))
Theorem: CategoryTheory.List.joinF.unitorLeft_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorLeftOplax as ≫ joinF.unitorLeftLax as = 𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor as)
⊢ DVect2.cons (𝟙 a) (𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor as)) =
    𝟙 (Prefunctor.obj joinF.toPrefunctor (Prefunctor.obj singletonF.toPrefunctor (a :: as)))
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unitorRight_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
as : List α
⊢ joinF.unitorRightLax as ≫ joinF.unitorRightOplax as = 𝟙 as
Tactic:
induction as
Proof state after:
case nil
α : Type u
inst✝ : Category α
⊢ joinF.unitorRightLax [] ≫ joinF.unitorRightOplax [] = 𝟙 []

case cons
α : Type u
inst✝ : Category α
head✝ : α
tail✝ : List α
tail_ih✝ : joinF.unitorRightLax tail✝ ≫ joinF.unitorRightOplax tail✝ = 𝟙 tail✝
⊢ joinF.unitorRightLax (head✝ :: tail✝) ≫ joinF.unitorRightOplax (head✝ :: tail✝) = 𝟙 (head✝ :: tail✝)
Theorem: CategoryTheory.List.joinF.unitorRight_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
⊢ joinF.unitorRightLax [] ≫ joinF.unitorRightOplax [] = 𝟙 []
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unitorRight_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorRightLax as ≫ joinF.unitorRightOplax as = 𝟙 as
⊢ joinF.unitorRightLax (a :: as) ≫ joinF.unitorRightOplax (a :: as) = 𝟙 (a :: as)
Tactic:
case cons a as h_ind =>
  dsimp [joinF.unitorRightLax, joinF.unitorRightOplax]
  rw [Category.id_comp, h_ind]
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unitorRight_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
⊢ joinF.unitorRightLax [] ≫ joinF.unitorRightOplax [] = 𝟙 []
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unitorRight_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorRightLax as ≫ joinF.unitorRightOplax as = 𝟙 as
⊢ joinF.unitorRightLax (a :: as) ≫ joinF.unitorRightOplax (a :: as) = 𝟙 (a :: as)
Tactic:
dsimp [joinF.unitorRightLax, joinF.unitorRightOplax]
Proof state after:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorRightLax as ≫ joinF.unitorRightOplax as = 𝟙 as
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (joinF.unitorRightLax as ≫ joinF.unitorRightOplax as) = DVect2.cons (𝟙 a) (𝟙 as)
Theorem: CategoryTheory.List.joinF.unitorRight_lax_oplax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : joinF.unitorRightLax as ≫ joinF.unitorRightOplax as = 𝟙 as
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (joinF.unitorRightLax as ≫ joinF.unitorRightOplax as) = DVect2.cons (𝟙 a) (𝟙 as)
Tactic:
rw [Category.id_comp, h_ind]
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unitorRight_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
as : List α
⊢ joinF.unitorRightOplax as ≫ joinF.unitorRightLax as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor as)
Tactic:
induction as
Proof state after:
case nil
α : Type u
inst✝ : Category α
⊢ joinF.unitorRightOplax [] ≫ joinF.unitorRightLax [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor [])

case cons
α : Type u
inst✝ : Category α
head✝ : α
tail✝ : List α
tail_ih✝ :
  joinF.unitorRightOplax tail✝ ≫ joinF.unitorRightLax tail✝ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor tail✝)
⊢ joinF.unitorRightOplax (head✝ :: tail✝) ≫ joinF.unitorRightLax (head✝ :: tail✝) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor (head✝ :: tail✝))
Theorem: CategoryTheory.List.joinF.unitorRight_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
⊢ joinF.unitorRightOplax [] ≫ joinF.unitorRightLax [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor [])
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unitorRight_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind :
  joinF.unitorRightOplax as ≫ joinF.unitorRightLax as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor as)
⊢ joinF.unitorRightOplax (a :: as) ≫ joinF.unitorRightLax (a :: as) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor (a :: as))
Tactic:
case cons a as h_ind =>
  dsimp [joinF.unitorRightLax, joinF.unitorRightOplax]
  rw [Category.id_comp, h_ind]
  rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unitorRight_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
⊢ joinF.unitorRightOplax [] ≫ joinF.unitorRightLax [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor [])
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.unitorRight_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind :
  joinF.unitorRightOplax as ≫ joinF.unitorRightLax as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor as)
⊢ joinF.unitorRightOplax (a :: as) ≫ joinF.unitorRightLax (a :: as) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor (a :: as))
Tactic:
dsimp [joinF.unitorRightLax, joinF.unitorRightOplax]
Proof state after:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind :
  joinF.unitorRightOplax as ≫ joinF.unitorRightLax as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor as)
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (joinF.unitorRightOplax as ≫ joinF.unitorRightLax as) =
    𝟙
      (Prefunctor.obj singletonF.toPrefunctor a ++
        Prefunctor.obj joinF.toPrefunctor
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF).toPrefunctor as))
Theorem: CategoryTheory.List.joinF.unitorRight_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind :
  joinF.unitorRightOplax as ≫ joinF.unitorRightLax as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor as)
⊢ DVect2.cons (𝟙 a ≫ 𝟙 a) (joinF.unitorRightOplax as ≫ joinF.unitorRightLax as) =
    𝟙
      (Prefunctor.obj singletonF.toPrefunctor a ++
        Prefunctor.obj joinF.toPrefunctor
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF).toPrefunctor as))
Tactic:
rw [Category.id_comp, h_ind]
Proof state after:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind :
  joinF.unitorRightOplax as ≫ joinF.unitorRightLax as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor as)
⊢ DVect2.cons (𝟙 a) (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor as)) =
    𝟙
      (Prefunctor.obj singletonF.toPrefunctor a ++
        Prefunctor.obj joinF.toPrefunctor
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF).toPrefunctor as))
Theorem: CategoryTheory.List.joinF.unitorRight_oplax_lax
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind :
  joinF.unitorRightOplax as ≫ joinF.unitorRightLax as =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor as)
⊢ DVect2.cons (𝟙 a) (𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor as)) =
    𝟙
      (Prefunctor.obj singletonF.toPrefunctor a ++
        Prefunctor.obj joinF.toPrefunctor
          (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF).toPrefunctor as))
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associatorLeft_nil
Proof state before:
α : Type u
inst✝ : Category α
⊢ joinF.associatorLeft [] = 𝟙 []
Tactic:
unfold joinF.associatorLeft
Proof state after:
α : Type u
inst✝ : Category α
⊢ associatorLeft.aux [] [] [] = 𝟙 []
Theorem: CategoryTheory.List.joinF.associatorLeft_nil
Proof state before:
α : Type u
inst✝ : Category α
⊢ associatorLeft.aux [] [] [] = 𝟙 []
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associatorLeft_cons_nil
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
⊢ joinF.associatorLeft ([] :: asss) = joinF.associatorLeft asss
Tactic:
unfold joinF.associatorLeft
Proof state after:
α : Type u
inst✝ : Category α
asss : List (List (List α))
⊢ associatorLeft.aux [] [] ([] :: asss) = associatorLeft.aux [] [] asss
Theorem: CategoryTheory.List.joinF.associatorLeft_cons_nil
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
⊢ associatorLeft.aux [] [] ([] :: asss) = associatorLeft.aux [] [] asss
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associatorLeft_cons_cons_nil
Proof state before:
α : Type u
inst✝ : Category α
ass : List (List α)
asss : List (List (List α))
⊢ joinF.associatorLeft (([] :: ass) :: asss) = joinF.associatorLeft (ass :: asss)
Tactic:
unfold joinF.associatorLeft
Proof state after:
α : Type u
inst✝ : Category α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux [] [] (([] :: ass) :: asss) = associatorLeft.aux [] [] (ass :: asss)
Theorem: CategoryTheory.List.joinF.associatorLeft_cons_cons_nil
Proof state before:
α : Type u
inst✝ : Category α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux [] [] (([] :: ass) :: asss) = associatorLeft.aux [] [] (ass :: asss)
Tactic:
conv => lhs; unfold associatorLeft.aux; unfold associatorLeft.aux
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associatorLeft_cons_cons_cons
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ joinF.associatorLeft (((a :: as) :: ass) :: asss) = DVect2.cons (𝟙 a) (joinF.associatorLeft ((as :: ass) :: asss))
Tactic:
unfold joinF.associatorLeft
Proof state after:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux [] [] (((a :: as) :: ass) :: asss) =
    DVect2.cons (𝟙 a) (associatorLeft.aux [] [] ((as :: ass) :: asss))
Theorem: CategoryTheory.List.joinF.associatorLeft_cons_cons_cons
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux [] [] (((a :: as) :: ass) :: asss) =
    DVect2.cons (𝟙 a) (associatorLeft.aux [] [] ((as :: ass) :: asss))
Tactic:
unfold joinF.associatorLeft.aux
Proof state after:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux [] ((a :: as) :: ass) asss = DVect2.cons (𝟙 a) (associatorLeft.aux [] (as :: ass) asss)
Theorem: CategoryTheory.List.joinF.associatorLeft_cons_cons_cons
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux [] ((a :: as) :: ass) asss = DVect2.cons (𝟙 a) (associatorLeft.aux [] (as :: ass) asss)
Tactic:
unfold joinF.associatorLeft.aux
Proof state after:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux (a :: as) ass asss = DVect2.cons (𝟙 a) (associatorLeft.aux as ass asss)
Theorem: CategoryTheory.List.joinF.associatorLeft_cons_cons_cons
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux (a :: as) ass asss = DVect2.cons (𝟙 a) (associatorLeft.aux as ass asss)
Tactic:
conv => lhs; unfold joinF.associatorLeft.aux
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associatorRight_nil
Proof state before:
α : Type u
inst✝ : Category α
⊢ joinF.associatorRight [] = 𝟙 []
Tactic:
unfold joinF.associatorRight
Proof state after:
α : Type u
inst✝ : Category α
⊢ associatorRight.aux [] [] [] = 𝟙 []
Theorem: CategoryTheory.List.joinF.associatorRight_nil
Proof state before:
α : Type u
inst✝ : Category α
⊢ associatorRight.aux [] [] [] = 𝟙 []
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associatorRight_cons_nil
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
⊢ joinF.associatorRight ([] :: asss) = joinF.associatorRight asss
Tactic:
unfold joinF.associatorRight
Proof state after:
α : Type u
inst✝ : Category α
asss : List (List (List α))
⊢ associatorRight.aux [] [] ([] :: asss) = associatorRight.aux [] [] asss
Theorem: CategoryTheory.List.joinF.associatorRight_cons_nil
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
⊢ associatorRight.aux [] [] ([] :: asss) = associatorRight.aux [] [] asss
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associatorRight_cons_cons_nil
Proof state before:
α : Type u
inst✝ : Category α
ass : List (List α)
asss : List (List (List α))
⊢ joinF.associatorRight (([] :: ass) :: asss) = joinF.associatorRight (ass :: asss)
Tactic:
unfold joinF.associatorRight
Proof state after:
α : Type u
inst✝ : Category α
ass : List (List α)
asss : List (List (List α))
⊢ associatorRight.aux [] [] (([] :: ass) :: asss) = associatorRight.aux [] [] (ass :: asss)
Theorem: CategoryTheory.List.joinF.associatorRight_cons_cons_nil
Proof state before:
α : Type u
inst✝ : Category α
ass : List (List α)
asss : List (List (List α))
⊢ associatorRight.aux [] [] (([] :: ass) :: asss) = associatorRight.aux [] [] (ass :: asss)
Tactic:
conv => lhs; unfold associatorRight.aux; unfold associatorRight.aux
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associatorRight_cons_cons_cons
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ joinF.associatorRight (((a :: as) :: ass) :: asss) = DVect2.cons (𝟙 a) (joinF.associatorRight ((as :: ass) :: asss))
Tactic:
unfold joinF.associatorRight
Proof state after:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorRight.aux [] [] (((a :: as) :: ass) :: asss) =
    DVect2.cons (𝟙 a) (associatorRight.aux [] [] ((as :: ass) :: asss))
Theorem: CategoryTheory.List.joinF.associatorRight_cons_cons_cons
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorRight.aux [] [] (((a :: as) :: ass) :: asss) =
    DVect2.cons (𝟙 a) (associatorRight.aux [] [] ((as :: ass) :: asss))
Tactic:
unfold joinF.associatorRight.aux
Proof state after:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorRight.aux [] ((a :: as) :: ass) asss = DVect2.cons (𝟙 a) (associatorRight.aux [] (as :: ass) asss)
Theorem: CategoryTheory.List.joinF.associatorRight_cons_cons_cons
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorRight.aux [] ((a :: as) :: ass) asss = DVect2.cons (𝟙 a) (associatorRight.aux [] (as :: ass) asss)
Tactic:
unfold joinF.associatorRight.aux
Proof state after:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorRight.aux (a :: as) ass asss = DVect2.cons (𝟙 a) (associatorRight.aux as ass asss)
Theorem: CategoryTheory.List.joinF.associatorRight_cons_cons_cons
Proof state before:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorRight.aux (a :: as) ass asss = DVect2.cons (𝟙 a) (associatorRight.aux as ass asss)
Tactic:
conv => lhs; unfold joinF.associatorRight.aux
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associator_left_right
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
⊢ joinF.associatorLeft asss ≫ joinF.associatorRight asss =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor asss)
Tactic:
induction asss
Proof state after:
case nil
α : Type u
inst✝ : Category α
⊢ joinF.associatorLeft [] ≫ joinF.associatorRight [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor [])

case cons
α : Type u
inst✝ : Category α
head✝ : List (List α)
tail✝ : List (List (List α))
tail_ih✝ :
  joinF.associatorLeft tail✝ ≫ joinF.associatorRight tail✝ =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor tail✝)
⊢ joinF.associatorLeft (head✝ :: tail✝) ≫ joinF.associatorRight (head✝ :: tail✝) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor (head✝ :: tail✝))
Theorem: CategoryTheory.List.joinF.associator_left_right
Proof state before:
α : Type u
inst✝ : Category α
⊢ joinF.associatorLeft [] ≫ joinF.associatorRight [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor [])
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associator_left_right
Proof state before:
α : Type u
inst✝ : Category α
ass : List (List α)
asss : List (List (List α))
h_indsss :
  joinF.associatorLeft asss ≫ joinF.associatorRight asss =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor asss)
⊢ joinF.associatorLeft (ass :: asss) ≫ joinF.associatorRight (ass :: asss) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor (ass :: asss))
Tactic:
case cons ass asss h_indsss =>
  induction ass 
  case nil => simp; exact h_indsss
  case cons as ass h_indss =>
    induction as
    case nil => simp; exact h_indss
    case cons a as h_inds => simp; rw [h_inds]; rfl
Proof state after:
no goals