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

State before:
α : Type u
inst✝ : Category α
⊢ singletonF ⋙ joinF = 𝟭 (List α)
Tactic:
dsimp [Functor.comp, Functor.id]
State after:
α : Type u
inst✝ : Category α
⊢ Functor.mk
      { obj := fun X ↦ Prefunctor.obj joinF.toPrefunctor (Prefunctor.obj singletonF.toPrefunctor X),
        map := fun {X Y} f ↦ Prefunctor.map joinF.toPrefunctor (Prefunctor.map singletonF.toPrefunctor f) } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }

State before:
α : Type u
inst✝ : Category α
⊢ Functor.mk
      { obj := fun X ↦ Prefunctor.obj joinF.toPrefunctor (Prefunctor.obj singletonF.toPrefunctor X),
        map := fun {X Y} f ↦ Prefunctor.map joinF.toPrefunctor (Prefunctor.map singletonF.toPrefunctor f) } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }
Tactic:
dsimp [singletonF, joinF, DVect2.join]
State after:
α : Type u
inst✝ : Category α
⊢ Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }

State before:
α : Type u
inst✝ : Category α
⊢ Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }
Tactic:
apply eqF_List
State after:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List α),
    Prefunctor.obj (Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }).toPrefunctor a

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil }).toPrefunctor f)
      (Prefunctor.map (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }).toPrefunctor f)

State before:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List α),
    Prefunctor.obj (Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }).toPrefunctor a

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil }).toPrefunctor f)
      (Prefunctor.map (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }).toPrefunctor f)
Tactic:
. intro as
  dsimp
  exact List.append_nil as
State after:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil }).toPrefunctor f)
      (Prefunctor.map (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }).toPrefunctor f)

State before:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil }).toPrefunctor f)
      (Prefunctor.map (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }).toPrefunctor f)
Tactic:
. intro as bs fs
  dsimp
  exact DVect2.append_nil _
State after:
no goals