internlm/Lean-Github huggingface dataset:
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:
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:
induction ass
Proof state after:
case nil
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss :
  joinF.associatorLeft asss ≫ joinF.associatorRight asss =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor asss)
⊢ joinF.associatorLeft ([] :: asss) ≫ joinF.associatorRight ([] :: asss) =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF).toPrefunctor ([] :: asss))

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

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

case cons
α : Type u
inst✝ : Category α
head✝ : List (List α)
tail✝ : List (List (List α))
tail_ih✝ :
  joinF.associatorRight tail✝ ≫ joinF.associatorLeft tail✝ = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor tail✝)
⊢ joinF.associatorRight (head✝ :: tail✝) ≫ joinF.associatorLeft (head✝ :: tail✝) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (head✝ :: tail✝))
Theorem: CategoryTheory.List.joinF.associator_right_left
Proof state before:
α : Type u
inst✝ : Category α
⊢ joinF.associatorRight [] ≫ joinF.associatorLeft [] = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor [])
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associator_right_left
Proof state before:
α : Type u
inst✝ : Category α
ass : List (List α)
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
⊢ joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (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
Theorem: CategoryTheory.List.joinF.associator_right_left
Proof state before:
α : Type u
inst✝ : Category α
⊢ joinF.associatorRight [] ≫ joinF.associatorLeft [] = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor [])
Tactic:
rfl
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associator_right_left
Proof state before:
α : Type u
inst✝ : Category α
ass : List (List α)
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
⊢ joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
Tactic:
induction ass
Proof state after:
case nil
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
⊢ joinF.associatorRight ([] :: asss) ≫ joinF.associatorLeft ([] :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ([] :: asss))

case cons
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
head✝ : List α
tail✝ : List (List α)
tail_ih✝ :
  joinF.associatorRight (tail✝ :: asss) ≫ joinF.associatorLeft (tail✝ :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (tail✝ :: asss))
⊢ joinF.associatorRight ((head✝ :: tail✝) :: asss) ≫ joinF.associatorLeft ((head✝ :: tail✝) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((head✝ :: tail✝) :: asss))
Theorem: CategoryTheory.List.joinF.associator_right_left
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
⊢ joinF.associatorRight ([] :: asss) ≫ joinF.associatorLeft ([] :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ([] :: asss))
Tactic:
case nil => simp; exact h_indsss
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associator_right_left
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
as : List α
ass : List (List α)
h_indss :
  joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
⊢ joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))
Tactic:
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
Theorem: CategoryTheory.List.joinF.associator_right_left
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
⊢ joinF.associatorRight ([] :: asss) ≫ joinF.associatorLeft ([] :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ([] :: asss))
Tactic:
simp
Proof state after:
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
⊢ joinF.associatorRight asss ≫ joinF.associatorLeft asss =
    𝟙 (Prefunctor.obj joinF.toPrefunctor (Prefunctor.obj joinF.toPrefunctor asss))
Theorem: CategoryTheory.List.joinF.associator_right_left
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
⊢ joinF.associatorRight asss ≫ joinF.associatorLeft asss =
    𝟙 (Prefunctor.obj joinF.toPrefunctor (Prefunctor.obj joinF.toPrefunctor asss))
Tactic:
exact h_indsss
Proof state after:
no goals
Theorem: CategoryTheory.List.joinF.associator_right_left
Proof state before:
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
as : List α
ass : List (List α)
h_indss :
  joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
⊢ joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))
Tactic:
induction as
Proof state after:
case nil
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
⊢ joinF.associatorRight (([] :: ass) :: asss) ≫ joinF.associatorLeft (([] :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (([] :: ass) :: asss))

case cons
α : Type u
inst✝ : Category α
asss : List (List (List α))
h_indsss : joinF.associatorRight asss ≫ joinF.associatorLeft asss = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor asss)
ass : List (List α)
h_indss :
  joinF.associatorRight (ass :: asss) ≫ joinF.associatorLeft (ass :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (ass :: asss))
head✝ : α
tail✝ : List α
tail_ih✝ :
  joinF.associatorRight ((tail✝ :: ass) :: asss) ≫ joinF.associatorLeft ((tail✝ :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((tail✝ :: ass) :: asss))
⊢ joinF.associatorRight (((head✝ :: tail✝) :: ass) :: asss) ≫ joinF.associatorLeft (((head✝ :: tail✝) :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (((head✝ :: tail✝) :: ass) :: asss))