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

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

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

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

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

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

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

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