Theorem: CategoryTheory.List.joinF.associator_right_left (Moncalc/CategoryTheory/List/Monad.lean)

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
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✝))

State before:
α : Type u
inst✝ : Category α
⊢ joinF.associatorRight [] ≫ joinF.associatorLeft [] = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor [])
Tactic:
case nil => rfl
State after:
no goals

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
State after:
no goals

State before:
α : Type u
inst✝ : Category α
⊢ joinF.associatorRight [] ≫ joinF.associatorLeft [] = 𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor [])
Tactic:
rfl
State after:
no goals

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
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))

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
State after:
no goals

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
State after:
no goals

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
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))

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
State after:
no goals

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
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))

State before:
α : 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))
Tactic:
case nil => simp; exact h_indss
State after:
no goals

State before:
α : 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))
a : α
as : List α
h_inds :
  joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))
⊢ joinF.associatorRight (((a :: as) :: ass) :: asss) ≫ joinF.associatorLeft (((a :: as) :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (((a :: as) :: ass) :: asss))
Tactic:
case cons a as h_inds => simp; rw [h_inds]; rfl
State after:
no goals

State before:
α : 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))
Tactic:
simp
State after:
α : 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.toPrefunctor (ass ++ Prefunctor.obj joinF.toPrefunctor asss))

State before:
α : 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.toPrefunctor (ass ++ Prefunctor.obj joinF.toPrefunctor asss))
Tactic:
exact h_indss
State after:
no goals

State before:
α : 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))
a : α
as : List α
h_inds :
  joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))
⊢ joinF.associatorRight (((a :: as) :: ass) :: asss) ≫ joinF.associatorLeft (((a :: as) :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor (((a :: as) :: ass) :: asss))
Tactic:
simp
State after:
α : 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))
a : α
as : List α
h_inds :
  joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))
⊢ DVect2.cons (𝟙 a) (joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss)) =
    DVect2.cons (𝟙 a) (𝟙 (as ++ Prefunctor.obj joinF.toPrefunctor (ass ++ Prefunctor.obj joinF.toPrefunctor asss)))

State before:
α : 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))
a : α
as : List α
h_inds :
  joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))
⊢ DVect2.cons (𝟙 a) (joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss)) =
    DVect2.cons (𝟙 a) (𝟙 (as ++ Prefunctor.obj joinF.toPrefunctor (ass ++ Prefunctor.obj joinF.toPrefunctor asss)))
Tactic:
rw [h_inds]
State after:
α : 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))
a : α
as : List α
h_inds :
  joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))
⊢ DVect2.cons (𝟙 a) (𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))) =
    DVect2.cons (𝟙 a) (𝟙 (as ++ Prefunctor.obj joinF.toPrefunctor (ass ++ Prefunctor.obj joinF.toPrefunctor asss)))

State before:
α : 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))
a : α
as : List α
h_inds :
  joinF.associatorRight ((as :: ass) :: asss) ≫ joinF.associatorLeft ((as :: ass) :: asss) =
    𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))
⊢ DVect2.cons (𝟙 a) (𝟙 (Prefunctor.obj (joinF ⋙ joinF).toPrefunctor ((as :: ass) :: asss))) =
    DVect2.cons (𝟙 a) (𝟙 (as ++ Prefunctor.obj joinF.toPrefunctor (ass ++ Prefunctor.obj joinF.toPrefunctor asss)))
Tactic:
rfl
State after:
no goals