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

State before:
α : Type u
inst✝ : Category α
as : List α
⊢ joinF.unitorLeftLax as ≫ joinF.unitorLeftOplax as = 𝟙 as
Tactic:
induction as
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✝)

State before:
α : Type u
inst✝ : Category α
⊢ joinF.unitorLeftLax [] ≫ joinF.unitorLeftOplax [] = 𝟙 []
Tactic:
case nil => rfl
State after:
no goals

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

State before:
α : Type u
inst✝ : Category α
⊢ joinF.unitorLeftLax [] ≫ joinF.unitorLeftOplax [] = 𝟙 []
Tactic:
rfl
State after:
no goals

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

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